制御*

CTL* は、計算ツリー論理(CTL) と線形時相論理(LTL)のスーパーセットです。パス量指定子と時相演算子を自由に組み合わせます。CTL と同様に、CTL* は分岐時間論理です。CTL* 式の形式意味論は、特定のKripke 構造に関して定義されます。

LTLは、1977年にAmir Pnueliによって最初にコンピュータプログラムの検証のために提案されました。4年後の1981年にEM ClarkeとEA EmersonがCTLとCTLモデル検査を発明しました。CTL*は1983年にEA EmersonとJoseph Y. Halpernによって定義されました。 ^[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 ]\mid [\phi R\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]}

• 時間的論理
• クリプキ構造
• モデルチェック
• レオ調整言語

• アミール・プヌエリ：プログラムの時相論理。第 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授業スライド