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