CTL*

Branching-time logic that is a superset of LTL and CTL

CTL*は、計算木論理（CTL）と線形時相論理（LTL）のスーパーセットです。パス量指定子と時相演算子を自由に組み合わせることができます。CTLと同様に、CTL*は分岐時間論理です。CTL*論理式の形式意味論は、与えられたクリプキ構造に基づいて定義されます。

歴史

LTLは、1977年にアミール・プヌエリによって初めてコンピュータプログラムの検証のために提案されました。4年後の1981年、EMクラークとEAエマーソンはCTLとCTLモデル検査を発明しました。CTL*は1983年にEAエマーソンとジョセフ・Y・ハルパーンによって定義されました。^[1]

CTLとLTLはCTL*より前に独立して開発されました。どちらのサブロジックもモデル検査コミュニティの標準となっていますが、CTL*はこれらのロジックや他のロジックを表現・比較するための表現力豊かなテストベッドを提供するため、実用上重要です。これは驚くべきことです^[要出典] 。なぜなら、 CTL*におけるモデル検査の計算量はLTLよりも悪くないからです。どちらもPSPACE内にあります。

構文

整形式の CTL* 式の言語は、次のような明確な（括弧に関して）文脈自由文法によって生成されます。

${\displaystyle \Phi ::=\bot \mid \top \mid p\mid (\neg \Phi )\mid (\Phi \land \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \Rightarrow \Phi )\mid (\Phi \Leftrightarrow \Phi )\mid A\phi \mid E\phi }$

${\displaystyle \phi ::=\Phi \mid (\neg \phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\mid X\phi \mid F\phi \mid G\phi \mid [\phi U\phi ]}$

ここで、 は一連の原子式の範囲を取ります。有効なCTL*式は非終端記号 を用いて構築されます。これらの式は状態式と呼ばれ、記号 によって作成される式はパス式と呼ばれます。(上記の文法には冗長性が含まれています。例えば、含意と同値性は、ブール代数（または命題論理）においてのみ、否定と連言から と定義でき、他の2つは時相演算子XとUで定義できます。) ${\displaystyle p}$ ${\displaystyle \Phi }$ ${\displaystyle \phi }$ ${\displaystyle \Phi \lor \Phi }$

演算子は基本的にCTLと同じです。ただし、CTLではすべての時間演算子（ ）の直前に量指定子を置く必要がありますが、CTL*ではこれは必須ではありません。普遍パス量指定子は、CTL*では古典的な述語論理と同様に定義できますが、CTLフラグメントでは定義できません。 ${\displaystyle X,F,G,U}$ ${\displaystyle A\phi =\neg E\neg \phi }$

数式の例

• LTL でも CTL でもない CTL* 式: ${\displaystyle EX(p)\land AFG(p)}$
• CTL にない LTL 式: ${\displaystyle \ AFG(p)}$
• LTL にない CTL 式: ${\displaystyle \ EX(p)}$
• CTL と LTL にある CTL* 式: ${\displaystyle \ AG(p)}$

注意: LTL を CTL* のサブセットとして扱う場合、すべての LTL 式には暗黙的にユニバーサル パス量指定子が接頭辞として付けられます。 ${\displaystyle A}$

セマンティクス

CTL* の意味論は、あるクリプキ構造に関して定義されます。その名前が示すように、状態式はこの構造の状態に関して解釈され、経路式はこの構造上の経路に関して解釈されます。

州の公式

クリプキ構造の状態が状態式を満たす場合、それは と表記されます。この関係は次のように帰納的に定義されます。 ${\displaystyle s}$ ${\displaystyle \Phi }$ ${\displaystyle s\models \Phi }$

1. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}}$
2. ${\displaystyle {\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}}$
3. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \neg \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \Phi {\Big )}}$
4. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \Phi _{1}\land \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}}$
5. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \Phi _{1}\lor \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}}$
6. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \Phi _{1}\Rightarrow \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\not \models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}}$
7. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models \Phi _{1}\Leftrightarrow \Phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}{\bigg )}}$
8. ${\displaystyle {\Big (}({\mathcal {M}},s)\models A\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi }$すべてのパスが ${\displaystyle \ \pi }$ ${\displaystyle s{\Big )}}$
9. ${\displaystyle {\Big (}({\mathcal {M}},s)\models E\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi }$から始まるいくつかのパス ${\displaystyle \ \pi }$ ${\displaystyle s{\Big )}}$

パス式

パス式とパスの満足関係も帰納的に定義されます。このために、部分パスを次のように表記します。 ${\displaystyle \pi \models \phi }$ ${\displaystyle \ \phi }$ ${\displaystyle \pi =s_{0}\to s_{1}\to \cdots }$ ${\displaystyle \ \pi [n]}$ ${\displaystyle s_{n}\to s_{n+1}\to \cdots }$

1. ${\displaystyle {\Big (}\pi \models \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s_{0})\models \Phi {\Big )}}$
2. ${\displaystyle {\Big (}\pi \models \neg \phi {\Big )}\Leftrightarrow {\Big (}\pi \not \models \phi {\Big )}}$
3. ${\displaystyle {\Big (}\pi \models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}}$
4. ${\displaystyle {\Big (}\pi \models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}}$
5. ${\displaystyle {\Big (}\pi \models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \not \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}}$
6. ${\displaystyle {\bigg (}\pi \models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}\pi \models \phi _{1}{\big )}\land \neg {\big (}\pi \models \phi _{2}{\big )}{\Big )}{\bigg )}}$
7. ${\displaystyle {\Big (}\pi \models X\phi {\Big )}\Leftrightarrow {\Big (}\pi [1]\models \phi {\Big )}}$
8. ${\displaystyle {\Big (}\pi \models F\phi {\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:\pi [n]\models \phi {\Big )}}$
9. ${\displaystyle {\Big (}\pi \models G\phi {\Big )}\Leftrightarrow {\Big (}\forall n\geqslant 0:\pi [n]\models \phi {\Big )}}$
10. ${\displaystyle {\Big (}\pi \models [\phi _{1}U\phi _{2}]{\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:{\big (}\pi [n]\models \phi _{2}\land \forall 0\leqslant k<n:~\pi [k]\models \phi _{1}{\big )}{\Big )}}$

意思決定の問題

CTL*モデル検査（固定モデル上の入力式）はPSPACE完全^[2]であり、充足可能性問題は2EXPTIME完全である。^{[2] [3]}

参照

• 時相論理
• クリプキ構造
• モデル検査
• レオ調整言語

参考文献

1. エマーソン、E. アレン;ハルパーン、ジョセフ Y. (1983)。 」「時々」と「決してない」の再考」。第10回ACM SIGPLAN-SIGACTプログラミング言語原理シンポジウム- POPL '83の議事録。pp.  127– 140。doi :10.1145/567067.567081。ISBN 0897910907. S2CID  15728260。
2. Baier, Christel ; Katoen, Joost-Pieter (2008-01-01). モデル検査の原理 (表現と心のシリーズ). MIT Press. ISBN 978-0262026499。
3. Orna Kupferman ; Moshe Y. Vardi (1999年6月). 「Churchの問題再考」. Bulletin of Symbolic Logic . 5 (2): 245– 263. doi :10.2307/421091. JSTOR  421091. S2CID  18833301.

• アミール・プヌエリ「プログラムの時相論理」第18回IEEEコンピュータサイエンス基礎シンポジウム（FOCS）論文集、1977年、46-57ページ。DOI= 10.1109/SFCS.1977.32
• E. アレン・エマーソン、ジョセフ・Y. ハルパーン：「時々」と「決してないわけではない」の再考：分岐型時相論理と線形時間時相論理について。Journal of the ACM 33, 1 (1986年1月), 151–178. DOI= http://doi.acm.org/10.1145/4904.4999
• Ph. Schnoebelen: 時相論理モデル検査の複雑性。様相論理の進歩 2002: 393–436

外部リンク

• ボルツァーノ自由大学のアレサンドロ・アルターレ教授のCTL授業スライド

Retrieved from "https://en.wikipedia.org/w/index.php?title=CTL*&oldid=1294122656"