計算ツリーロジック

計算木論理( CTL ) は分岐時間論理であり、時間モデルが未来が決定されていないツリーのような構造であることを意味します。未来にはさまざまなパスがあり、そのいずれもが実際に実現されるパスである可能性があります。これは、ソフトウェアまたはハードウェア成果物の形式検証で使用され、通常はモデルチェッカーと呼ばれるソフトウェアアプリケーションによって、特定の成果物が安全性プロパティまたは活性プロパティを備えているかどうかを判定します。たとえば、 CTL では、ある初期条件(すべてのプログラム変数が正である、または高速道路で 2 つの車線にまたがる車がないなど) が満たされた場合、プログラムのすべての実行で望ましくない状態 (数を 0 で割る、高速道路で 2 台の車が衝突するなど) が回避されるように指定できます。この例では、安全性プロパティは、初期条件を満たすプログラム状態からのすべての可能な遷移を調査し、そのようなすべての実行がプロパティを満たしていることを確認するモデルチェッカーによって検証できます。計算木論理は、線形時相論理 (LTL)を含む時相論理のクラスに属します。 CTL でのみ表現可能なプロパティと LTL でのみ表現可能なプロパティがありますが、どちらのロジックでも表現可能なすべてのプロパティは CTL*でも表現できます。

歴史

CTL は 1981 年にEdmund M. ClarkeとE. Allen Emersonによって初めて提案され、彼らはそれを、いわゆる同期スケルトン、つまり並行プログラムの抽象化を合成するために使用しました。

CTLの導入以来、CTLとLTLの相対的な利点について議論が続いてきました。CTLはモデル検査において計算効率が高いため、産業用途で広く利用されるようになり、多くの最も成功したモデル検査ツールはCTLを仕様言語として採用しています。^[1]

CTLの構文

CTL の整形式の数式の言語は、次の文法によって生成されます。

{\begin{aligned}\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 \quad {\mbox{AX }}\phi \mid {\mbox{EX }}\phi \mid {\mbox{AF }}\phi \mid {\mbox{EF }}\phi \mid {\mbox{AG }}\phi \mid {\mbox{EG }}\phi \mid {\mbox{A }}[\phi {\mbox{ U }}\phi ]\mid {\mbox{E }}[\phi {\mbox{ U }}\phi ]\end{aligned}}

ここで、は原子式の集合の範囲に及びます。すべての接続詞を使用する必要はありません。例えば、は接続詞の完全な集合を構成しており、他の接続詞もそれらを用いて定義できます。 $p$ $\{\neg ,\land ,{\mbox{AX}},{\mbox{AU}},{\mbox{EU}}\}$

${\mbox{A}}$ 「すべての道に沿って」（必然的に）という意味
${\mbox{E}}$ 「少なくとも（存在する）1つのパスに沿って」（おそらく）という意味です

たとえば、次は適切に形成された CTL 式です。

{\mbox{EF }}({\mbox{EG }}p\Rightarrow {\mbox{AF }}r)

以下は、適切に形成された CTL 式ではありません。

{\mbox{EF }}{\big (}r{\mbox{ U }}q{\big )}

この文字列の問題は、またはとペアになっている場合にのみ発生することです。 $\mathrm {U}$ $\mathrm {A}$ $\mathrm {E}$

CTLは、原子命題を構成要素として用いて、システムの状態に関する記述を行います。これらの命題は、論理演算子と時相演算子を用いて式にまとめられます。

オペレーター

論理演算子

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

時間演算子

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

パス上の量指定子
- A Φ – Aすべて: Φ は現在の状態から始まるすべてのパスで保持される必要があります。
- E Φ – Eが存在する: Φ が成り立つ現在の状態から始まるパスが少なくとも 1 つ存在します。
パス固有の量指定子
- X φ – Ne x t: φ は次の状態でも保持される必要があります (この演算子はXではなくNと表記されることもあります)。
- G φ – G全体的: φ は後続のパス全体で保持される必要があります。
- F φ –最終的に: φ は最終的に保持される必要があります (後続のパスのどこかで)。
- φ U ψ – U ntil: φ は、少なくともある位置でψが成立するまで成立する必要がある。これは、ψが将来検証されることを意味する。
- φ W ψ –成立するまではW eak until: φはψが成立するまで成立しなければならない。U演算子との違いは、 ψが成立するかどうかが保証されない点である。W演算子は「unless」と呼ばれることもある。

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

最小限の演算子セット

CTLには最小限の演算子セットがあります。すべてのCTL式は、これらの演算子のみを使用するように変換できます。これはモデル検査に便利です。最小限の演算子セットの例としては、{true, ∨, ¬, EG , EU , EX }などがあります。

時間演算子に使用される変換の一部は次のとおりです。

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

CTLのセマンティクス

意味

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

すると、意味的含意の関係は上で再帰的に定義されます。 $({\mathcal {M}},s\models \phi )$ $\phi$

${\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}$
${\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}$
${\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$

CTLの特性

上記の規則 10 ～ 15 は、モデル内の計算パスを参照し、最終的に「計算ツリー」を特徴付けるものです。つまり、特定の状態をルートとする無限に深い計算ツリーの性質に関するアサーションです。 $s$

意味的同値性

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

とはそれぞれ普遍的計算パス量指定子と存在的計算パス量指定子である双対であることがわかります。 $\mathrm {A}$ $\mathrm {E}$ $\neg \mathrm {A} \Phi \equiv \mathrm {E} \neg \Phi$

さらに、およびも同様です。 $\mathrm {G}$ $\mathrm {F}$

したがって、ド・モルガンの法則の例をCTL で定式化することができます。

\neg AF\phi \equiv EG\neg \phi

\neg EF\phi \equiv AG\neg \phi

\neg AX\phi \equiv EX\neg \phi

このような恒等式を使用すると、CTL 時間的接続詞のサブセットは、、およびブール接続詞の少なくとも 1つを含む場合に適切であることが示されます。 $EU$ $\{AX,EX\}$ $\{EG,AF,AU\}$

以下の重要な同値性は展開法則と呼ばれ、CTL 接続子の検証を時間的に後続のものへと展開することを可能にします。

AG\phi \equiv \phi \land AXAG\phi

EG\phi \equiv \phi \land EXEG\phi

AF\phi \equiv \phi \lor AXAF\phi

EF\phi \equiv \phi \lor EXEF\phi

A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])

E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])

例

「P」は「私はチョコレートが好きだ」、Qは「外は暖かい」という意味になります。

AG .P

「これから先、何があってもチョコレートは好きになります。」

EF .P

「いつか、少なくとも一日だけでも、チョコレートが好きになるかもしれない。」

AF . EG . P

「突然、一生チョコレートが好きになる可能性は常にある（AF）」（注：私の人生は有限だが、Gは無限なので、残りの人生だけではない）。

例：AF、 P

将来（E）に何が起こるかにもよりますが、残りの人生（G）で少なくとも一日（AF）はチョコレートが好きな日が保証されるかもしれません。しかし、何か問題が起きれば、すべてが台無しになり、いつかチョコレートが好きになるかどうかは保証されません。

次の 2 つの例は、 until 演算子をパス演算子 ( AまたはE ) で修飾しないことを許可する CTL と CTL* の違いを示しています。

AG (P U Q)

「これから暖かくなるまでは、毎日チョコレートが食べたくなります。暖かくなったら、もうチョコレートが好きになるかどうかは分かりません。あ、そうそう、たとえ1日だけでも、いつかは必ず暖かくなるはずです。」

EF (( EX .P) U ( AG .Q))

「いつかはずっと暖かい日が来るかもしれないし（AG.Q）、その日が来る前に、次の日にチョコレートを好きになる方法が必ずあるかもしれない（ EX.P）」

他の論理との関係

計算木論理（CTL）は、CTL* および様相μ計算のサブセットです。また、CTLは、Alur、Henzinger、Kupfermanの交代時間時相論理（ATL）の一部でもあります。

計算木論理（CTL）と線形時相論理（LTL）はどちらもCTL*のサブセットです。CTLとLTLは同等ではなく、共通のサブセットを持ちます。このサブセットはCTLとLTLの両方の真サブセットです。

FG .P は LTL には存在しますが、CTL には存在しません。
AG (P⇒(( EX .Q)∧( EX ¬Q))) とAG.EF .P は CTL には存在しますが、LTL には存在しません。

拡張機能

CTLは二階量化と量化計算木論理（QCTL）に拡張されている。^[2] 2つの意味論がある。 $\exists p$ $\forall p$

木の意味論。計算木のノードにラベルを付ける。QCTL* = QCTL =木上のMSO。モデル検査と充足可能性は完全である。
構造意味論。状態にラベルを付ける。グラフ上のQCTL* = QCTL = MSO 。モデル検査はPSPACE完全だが、充足可能性は決定不能である。

QBFソルバーの利点を活用するために、構造意味論を含むQCTLのモデル検査問題をTQBF（真量化ブール式）に縮減することが提案されている。^[3]

参照

参考文献

^ Vardi, Moshe Y. (2001). 分岐 vs. 線形時間：最終決戦(PDF) . システムの構築と分析のためのツールとアルゴリズム. コンピュータサイエンス講義ノート. 第2031巻. Springer, ベルリン. pp. 1– 22. doi :10.1007/3-540-45319-9_1. ISBN 978-3-540-41865-8。
^ デヴィッド、アメリ;ラルシニー、フランソワ。マーキー、ニコラス (2016)。デシャルネ、ジョゼ。ジャガディーサン、ラダ (編)。「QCTL の表現力について」。第 27 回並行性理論に関する国際会議 (CONCUR 2016)。ライプニッツ国際情報学会議 (LIPIcs)。59 .ダグシュトゥール、ドイツ: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 28:1–28:15。土井：10.4230/LIPIcs.CONCUR.2016.28。ISBN 978-3-95977-017-0。
^ Hossain, Akash; Laroussinie, François (2019). Gamper, Johann; Pinchinat, Sophie; Sciavicco, Guido (編). 「定量化CTLからQBFへ」.第26回国際時間表現・推論シンポジウム (TIME 2019) . ライプニッツ国際情報科学会報 (LIPIcs). 147.ダグストゥール、ドイツ: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 11:1–11:20. doi : 10.4230/LIPIcs.TIME.2019.11 . ISBN 978-3-95977-127-6. S2CID 195345645。

EM Clarke; EA Emerson (1981). 「分岐時間時相論理を用いた同期スケルトンの設計と合成」(PDF) . Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science . Vol. 131. Springer, Berlin. pp. 52– 71. doi :10.1007/BFb0025774. ISBN 3-540-11212-X。
マイケル・フース、マーク・ライアン（2004年）『コンピュータサイエンスにおける論理』（第2版）ケンブリッジ大学出版局、207頁。ISBN 978-0-521-54310-1。
エマーソン, EA;ハルパーン, JY (1985). 「分岐時間の時相論理における決定手続きと表現力」.コンピュータとシステム科学ジャーナル. 30 (1): 1– 24. CiteSeerX 10.1.1.221.6187 . doi :10.1016/0022-0000(85)90001-7.
Clarke, EM; Emerson, EA & Sistla, AP (1986). 「時相論理仕様を用いた有限状態並行システムの自動検証」. ACM Transactions on Programming Languages and Systems . 8 (2): 244– 263. doi : 10.1145/5397.5399 . S2CID 52853200.
エマーソン, EA (1990). 「時相論理と様相論理」.ヤン・ファン・レーウェン編.理論計算機科学ハンドブック, 第B巻. MIT出版. pp. 955– 1072. ISBN 978-0-262-22039-2。

外部リンク

CTLの指導スライド

[1] Vardi, Moshe Y. (2001). 分岐 vs. 線形時間：最終決戦(PDF) . システムの構築と分析のためのツールとアルゴリズム. コンピュータサイエンス講義ノート. 第2031巻. Springer, ベルリン. pp. 1– 22. doi :10.1007/3-540-45319-9_1. ISBN 978-3-540-41865-8。

[2] デヴィッド、アメリ;ラルシニー、フランソワ。マーキー、ニコラス (2016)。デシャルネ、ジョゼ。ジャガディーサン、ラダ (編)。「QCTL の表現力について」。第 27 回並行性理論に関する国際会議 (CONCUR 2016)。ライプニッツ国際情報学会議 (LIPIcs)。59 .ダグシュトゥール、ドイツ: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 28:1–28:15。土井：10.4230/LIPIcs.CONCUR.2016.28。ISBN 978-3-95977-017-0。

[3] Hossain, Akash; Laroussinie, François (2019). Gamper, Johann; Pinchinat, Sophie; Sciavicco, Guido (編). 「定量化CTLからQBFへ」.第26回国際時間表現・推論シンポジウム (TIME 2019) . ライプニッツ国際情報科学会報 (LIPIcs). 147.ダグストゥール、ドイツ: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 11:1–11:20. doi : 10.4230/LIPIcs.TIME.2019.11 . ISBN 978-3-95977-127-6. S2CID 195345645。