到達可能性と安全性を検証する－NuSMVとLTSAによる時相論理式の実験

摘要

前回（2007年4月号，pp.160-165）では時相論理式の二つのタイプ，CTL（計算木論理）とLTL（線形時相論理）の比較を行った．そして，モデル検査ツールNuSMVを使ってLTLの実験場を構築した．構築したといっても，必要な論理変数をIVARで定義して，後は実験対象の論理式を書くだけである．CTLでは実験場としてステート・マシンも作らなければならないので面倒であると言った．