Local Model Checking for Propositional Model Mu-Calculus toward Model Construction

並列・分散オブジェクトシステムを構築する際には、そのシステムが公平で、デッドロック、飢餓状態などの可能性の有無を検証する必要がある。これらの性質はliveness、safetyと呼ばれる時間的性質に帰着できる。本論文では、これらを最小不動点を用いた命題μ計算により記述した。また、システムが大規模になった場合の証明手順の複雑化を回避するために、既存のローカルモデルチェック技法をパスプロパティという概念により拡張した、抽象化タブローを定義し、大規模なモデル構築へ応用するための方法を示した。

千葉短大紀要