モデル検査おおよその限界値

model checking

記号的に扱ったり、抽象的に扱うのにも限界ってものがあります。 うまくやれば 10^20 とか 10^1300 くらいのオーダーの状態数でも扱えますが、 無制限に状態数が増えるとすぐに限界が来ます。
http://www.epics.jp/mc/modelchecking.html

10種類の値を取り得る変数が2つあったら、その状態の組み合わせは10*10=100パターンとなります。 この調子で、状態の組み合わせが指数的に増加していくことを状態爆発 (State Explosion) と呼びます。
http://www.epics.jp/mc/modelchecking.html

疑問：10種類の値を取り得る2つの変数では，単純計算では，そのその状態の組み合わせは10*10=100パターンとなるのはわかる．しかし，遷移情報も加えると状態を減らすことができるのでは？例えば，遷移が奇数をぐるぐる回す情報だとしたら，自然数[1...10]をとりうる変数でも5つのケースに減らすことができる

300 (of state variables) is generally regarded as thepoint where model checking can become difficult.

Generating Efficient Test Sets with a Model Checker Gregoire Hamon, Leonardo de Moura and John Rushby Computer Science Laboratory, SRI International

http://research.microsoft.com/en-us/um/people/leonardo/testgen.pdf