>>37
元の系が有限状態でなくても、抽象解釈して有限状態として検査するのが
「今のモデルチェッキング」の流行りでは？といってみるテスト。