計算木論理

計算木論理（CTL）について

計算木論理、略してCTL（Computational Tree Logic）は、コンピュータサイエンスや論理学の分野で重要な役割を果たす、分岐時相論理の一種です。これは、未来の時間が不確定であることを前提としており、木状構造を用いて表現されます。CTLの基本的な考え方は、様々な未来の経路の中から実際に選択される経路が存在するという点です。

1. CTLの文法

CTLの論理式は以下の文法規則に従って構築されます。

```
ϕ ::= F | T | p | (¬ϕ) | (ϕ ∧ ϕ) | (ϕ ∨ ϕ) | (ϕ → ϕ) | AXϕ | EXϕ | AFϕ | EFϕ | AGϕ | EGϕ | A[ϕ U ϕ] | E[ϕ U ϕ]
```

ここで、`p`は原子論理式を表します。そして、`A`は「すべての経路について」といった意味で、`E`は「少なくとも一つの経路が存在」という意味になります。これにより、CTLは複雑な時間論理を簡潔に表現できるのです。

1.1 例

例えば、以下の論理式はCTLの形式に則っています：

```
EF EGp → AF r
```

一方で、次の例はCTのシンタックスルールに従っていないため無効です：

```
EF (r U q)
```

ここで、`U`の前には必ず`A`か`E`が必要であるため、CTLの基本的なルールを守っていません。

2. 作用素

CTLでは、論理作用素と時相作用素の2種類の作用素が使用されます。これにより、論理式を複雑にし、正確な動作を表現できます。

2.1 論理作用素

論理作用素には、否定（¬）、論理和（∨）、論理積（∧）、ならびに含意（→）などがあります。これらの基本的な作用素は、論理的な関係を構築するために使われます。

2.2 時相作用素

時相作用素は、経路作用素と状態作用素の2つのグループに分けられます。

• - 経路作用素:

- `A ϕ` : すべての経路で`ϕ`が真である。
- `E ϕ` : 少なくとも1つの経路で`ϕ`が真である。

• - 状態作用素:

- `X ϕ` : 次の状態で`ϕ`が真である。
- `G ϕ` : 未来のすべての状態で`ϕ`が真である。
- `F ϕ` : 未来のどこかの状態で`ϕ`が真である。
- `ϕ U ψ` : `ψ`が真になるまで`ϕ`が真である。

2.3 作用素の組み合わせ

CTL*では、時相作用素を自由に組み合わせ可能ですが、CTLでは上記のようにグループ分けされ、経路と状態の組み合わせのみが許容されます。

3. CTLの最小セット

すべてのCTL論理式は、限られた数の作用素によって表現できます。これを最小セットと呼び、モデル検査の場面で効率的です。例としては `{false, ∨, ¬, EG, EU, EX}` が挙げられます。例えば、`EF ϕ` は `E[true U ϕ]` に書き換え可能です。

4. 他の論理との関係

CTLは線形時相論理（LTL）のサブセットであり、共通部分を持つも、それぞれの特性には違いがあります。例として、LTLに存在する`GF.P`は、CTLにはありません。逆に、`AG(P → (EF.Q))`はCTL内にはあるがLTLには含まれません。

このように計算木論理は、プレkodや自動検証の分野で幅広く利用されています。解析を行うにあたり、設定された時間の枠組みや未来の不確定性を考慮する上で大変重要です。

もう一度検索