TL;DR
時相論理のうち、分岐時相論理の一種。未来は 1 つに決まっておらず、木構造のように分岐していると考え、分岐する経路についての性質を表す。
仕組み
Wikipedia によると、計算木論理では、現在の状態から複数の未来の経路が伸びており、そのうち 1 つが実際の経路になると考える。経路についての量化子と、時間についての演算子を組み合わせて性質を書く。
経路の量化子は 2 つある。
- A: 現在の状態から分岐するすべての経路で成り立つ
- E: 分岐する経路のうち、少なくとも 1 つで成り立つ
時相演算子には次のものがある。
- X（Next）: 次の状態で成り立つ
- F（Finally）: 将来のどこかの時点で成り立つ
- G（Globally）: その後ずっと成り立つ
- U（Until）: ψ が真になるまで φ が真であり続ける（ψ が将来必ず真になることも求める）
計算木論理では、時相演算子は必ず A か E と組にして使う（EF、AG、A[φ U ψ] など）。これらの演算子は EG、EU、EX などの最小の組に書き換えられ、この性質はモデル検査に便利である。
注意点
線形時相論理（LTL）とは共通する部分があるが、表せる性質は同じではない。たとえば GF.P は LTL では表せるが計算木論理では表せず、AG(P → EF.Q) は計算木論理では表せるが LTL では表せない。