計算ツリーロジック

論理演算子は、一般的な¬、∨、∧ 、⇒、⇔です。これらの演算子に加えて、CTL式ではブール定数trueとfalseも使用できます。

時間演算子は以下のとおりです。

• パス上の量化子
  • A Φ – All : Φ は現在の状態から始まるすべてのパスで成り立つ必要があります。 
  • E Φ – Eが存在する: 現在の状態から出発してΦが成り立つ経路が少なくとも 1 つ存在する。 
• パス固有の量指定子
  • X φ – Ne x t: φ は次の状態でも成立しなければならない (この演算子はXの代わりにN と表記されることもある)。 
  • G φ – Gグローバル: φ は後続のパス全体で維持されなければならない。 
  • F φ – F最終的に、φ は最終的に (後続の経路のどこかで) 成立しなければならない。 
  • φ U ψ – Until : φ は、少なくともある位置でψ が成り立つまで成り立たなければならない。これは、将来的にψ が検証されることを意味する。 
  • φ W ψ –弱条件: ψ が成り立つまでφ が成り立つ必要があります。Uとの違いは、 ψが必ず検証されるという保証がないことです。W演算子は「unless」と呼ばれることもあります。 

CTL*では、時間演算子を自由に組み合わせることができます。CTL では、演算子は常にペアでグループ化する必要があります。つまり、パス演算子の後に状態演算子が続きます。以下の例を参照してください。CTL *は、CTL よりも表現力に優れています。

CTLには最小限の演算子セットが存在します。すべてのCTL式は、これらの演算子のみを使用するように変換できます。これはモデル検査で役立ちます。最小限の演算子セットの1つは、{true, ∨ , ¬, EG , EU , EX }です。

時間演算子に使用される変換には、次のようなものがあります。

• EF φ == E [true U ( φ )] ( F φ == [true U ( φ )] であるため)
• AX φ == ¬ EX (¬ φ )
• AG φ == ¬ EF (¬ φ ) == ¬ E [true U (¬ φ )]
• AF φ == A [真のU φ ] == ε EG (ε φ )
• A [ φ U ψ ] == з( E [( ψ ) U з( φ ∨ ψ )] ∨ EG ( ψ ) )

CTL式は遷移システム上で解釈される。遷移システムは三つ組である。${\displaystyle {\mathcal {M}}=(S,{\rightarrow },L)}$、 どこ${\displaystyle S}$は状態の集合であり、${\displaystyle {\rightarrow }\subseteq S\times S}$は遷移関係であり、直列であると仮定される。つまり、すべての状態には少なくとも 1 つの後継状態があり、${\displaystyle L}$は、命題文字を状態に割り当てるラベル付け関数です。${\displaystyle {\mathcal {M}}=(S,\rightarrow ,L)}$このような移行モデルであり、${\displaystyle s\in S}$、 そして${\displaystyle \phi \in F}$、 どこ${\displaystyle F}$は、言語上の整形式式の集合である。${\displaystyle {\mathcal {M}}}$。

次に意味的含意の関係${\displaystyle ({\mathcal {M}},s\models \phi )}$は再帰的に定義される${\displaystyle \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 AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
9. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
10. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AG\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
11. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
12. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
13. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
14. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models A[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$
15. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$

上記のルール10 ～ 15は、モデルにおける計算パスに関するものであり、最終的に「計算ツリー」を特徴づけるものです。これらは、与えられた状態を根とする無限に深い計算ツリーの性質に関する主張です。${\displaystyle s}$。

数式${\displaystyle \phi }$そして${\displaystyle \psi }$は、あるモデルにおいて一方を満たす状態が他方も満たす場合、意味的に同等であると言われます。これは次のように表されます。${\displaystyle \phi \equiv \psi }$

分かるように${\displaystyle \mathrm {A} }$そして${\displaystyle \mathrm {E} }$これらは双対関係にあり、それぞれ普遍的計算経路量化子と存在量化子である。 ${\displaystyle \neg \mathrm {A} \Phi \equiv \mathrm {E} \neg \Phi }$。

さらに、${\displaystyle \mathrm {G} }$そして${\displaystyle \mathrm {F} }$。

したがって、CTLではド・モルガンの法則の一例を次のように定式化できる。

${\displaystyle \neg AF\phi \equiv EG\neg \phi }$

${\displaystyle \neg EF\phi \equiv AG\neg \phi }$

${\displaystyle \neg AX\phi \equiv EX\neg \phi }$

このような恒等式を用いると、CTL時間的接続詞のサブセットが、以下を含む場合に十分であることが示される。${\displaystyle EU}$少なくとも1つ${\displaystyle \{AX,EX\}}$そして少なくとも1つは${\displaystyle \{EG,AF,AU\}}$そしてブール論理結合子。

以下の重要な同値関係は展開法則と呼ばれ、CTL結合子の検証を時間的に後継の結合子へと展開することを可能にする。

${\displaystyle AG\phi \equiv \phi \land AXAG\phi }$

${\displaystyle EG\phi \equiv \phi \land EXEG\phi }$

${\displaystyle AF\phi \equiv \phi \lor AXAF\phi }$

${\displaystyle EF\phi \equiv \phi \lor EXEF\phi }$

${\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}$

${\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}$