計算における時相論理と様相論理

時相論理と様相論理は、古典論理を時間と可能性の演算子で拡張し、プログラムやリアクティブシステムがその実行全体にわたってどのように振る舞うべきかを正確に指定するための言語を提供します。

Definition

時相論理は、命題論理または一階述語論理を、常に、最終的に、〜まで、といった計算に沿ってプロパティがいつ成立するかを記述する演算子で拡張します。様相論理は、状態と遷移の構造に対する必然性と可能性の演算子でこれを一般化します。

Scope

このトピックでは、LTLやCTLなどの線形時相論理と分岐時相論理、動的論理や様相μ計算を含む様相論理、安全性と活性プロパティの表現、そしてこれらの論理を自動検証の中心とするモデル検査と充足可能性のアルゴリズム的問題について扱います。

Core questions

• 何らかの良いことが最終的に起こる、あるいは悪いことが決して起こらない、ということを論理はどのように表現できるでしょうか？
• 単一の実行について推論することと、すべての可能な未来について推論することの違いは何でしょうか？
• システムが時相プロパティを満たすかどうかをチェックすることは、どのようにアルゴリズム化されるのでしょうか？
• 表現力と効率的な検証のバランスが取れている時相論理はどれでしょうか？

Key theories

プログラム仕様のための時相論理

Pnueliは、時相論理がリアクティブプログラムと並行プログラムの正しさを、その実行に関するプロパティを表現することで捉え、安全性と活性の要件に対する統一された言語を提供することを示しました。

分岐時相論理のモデル検査

ClarkeとEmersonは、計算木論理と、有限状態モデルに対してそれを自動的に検証するアルゴリズムを導入し、モデル検査の分野を確立しました。

Clinical relevance

時相論理は、ハードウェア設計、通信プロトコル、並行ソフトウェアの検証に日常的に使用されるモデルチェッカーの仕様言語であり、デプロイ前にデッドロックや安全性および活性の違反を検出します。この技術は、その考案者にチューリング賞をもたらし、チップ設計の標準となっています。

History

Pnueliは1977年にプログラムの推論のために時相論理を提案し、ClarkeとEmersonはQueilleとSifakisと独立して、1981年頃にモデル検査を開発しました。このアプローチは1990年代初頭の記号的手法によって産業システムにまで規模を拡大し、その考案者たちはこの技術でチューリング賞を受賞しました。

Key figures

• Amir Pnueli
• Edmund Clarke
• E. Allen Emerson
• Joseph Sifakis

Seminal works

• clarkeEmerson1981
• huthRyan2004

Frequently asked questions

線形時相論理と分岐時相論理の違いは何ですか？

LTLのような線形時相論理は、単一の、おそらく無限の実行パスのプロパティを記述します。CTLのような分岐時相論理は、各状態からのすべての可能な未来の木を定量化し、あるパスに沿って、またはすべてのパスに沿ってプロパティが成立すると言うことができます。これらは異なる表現力と検証アルゴリズムを持っています。

モデル検査はこれらの論理をどのように使用しますか？

システムは有限状態モデルとして表現され、望ましいプロパティは時相論理式として表現されます。モデルチェッカーは、式が成立するかどうかを判断するために状態を網羅的に探索し、失敗した場合は反例トレースを生成するため、検証は自動的かつ診断的になります。