こんにちは、チェシャ猫です。
先日開催された YAPC::Hakodate 2024 で、様相論理について登壇してきました。公募 CFP 枠です。
しばらく後に録画アーカイブも公開される予定です。
質問への回答
当日は、ありがたいことに会場で何名かの方が質問を出してくれました。回答をまとめておきます。
EG φ の検査アルゴリズムにおいて、φ が真になるような強連結成分が複数見つかった場合はどうするのか？
EG φ が真になるのは「その状態から始まって φ を満たし続ける無限パスが存在するとき」なので、そのようなパスが複数見つかっても真偽に影響はありません。
もし実装するのであれば、強連結成分を順に試し、最初に条件に合致したものを見つけた時点で真を返すのが自然だと思います。
濾過法を適用する際の φ はどこから出てきたのか？
濾過法は大まかに言えば、「φ の（有限とは限らない）モデルが存在するとき、そこから有限モデルを作り出す手法」です。
つまり φ は最初から与えられていて、「その φ の有限モデルが存在するか？」という問題を考える上で使用されるのが濾過法です。より一般には、濾過法は「部分論理式について論理式の集合」に対して定式化されます。
システムを Kripke モデルに変換する際にギャップがあると思うが、実際にはどのように使用されるのか？
基本的に、モデル検査はアルゴリズムやプロトコルの設計時点で役に立つものだと考えておくのが良いと思います。
モデル検査では状態数の爆発が問題になることもあり、検査する対象は実際のソースコードというよりは抽象的な設計の方がメインになります。モデル検査を含む形式手法は品質保証の手法として語られることもありますが、品質保証として一般にイメージするような統合テストではなく、もっと手前の段階で設計検討時に仕様バグを探すという方が実態に近いです。
また、今回のスライドではあまり触れなかった部分ですが、人間が直接 Kripke モデルを書き下すのは困難なので、大抵のツールでは何らかの DSL でアルゴリズムを記述し、それを内部的に変換することになります。
