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

A trap property is the negation of the original (desired) property for systems. It plays important notion in a techniques of test-cases generation using model checking. The techniques of test-cases generation using model checking consists …