계산 트리 논리

계산 트리 논리 또는 계산 나무 논리(Computational Tree Logic, CTL)은 분기시간논리의 한 종류로, 어떤 상태에서 실행이 가능한 상태로의 경로를 트리 구조로 전개한 결과인 계산 트리와 의미론이 정의된 논리 체계이다.

CTL에서는 PLTL에서 사용되는 시간 연산자인 F, G, X, U, R 외에 '모든 실행 가능한 경로에 대해'를 의미하는 A, '어떤 실행가능한 경로에 대해'를 의미하는 E가 포함되어 사용된다.

문법

$\phi ::=F|T|p|(\neg \phi )|(\phi \land \phi )|(\phi \lor \phi )|(\phi \rightarrow \phi )|AX\phi |EX\phi |AF\phi |EF\phi |AG\phi |EG\phi |A[\phi U\phi ]|E[\phi U\phi ]$
p는 기본항이다. A는 '모든 실행 가능한 경로에 대해 필연적으로'의 의미를 나타내며, E는 '적어도 한개의 어떤 실행 가능한 경로가 어느 때에 존재하여'의 의미를 나타낸다. 다음 식은 CTL의 정형식(well-formed formula)이다.

$EFEGp\rightarrow AFr$

그러나 다음 CTL 식은 정형식이 아니다.

$EF(rUq)$

CTL에서는 U 등의 연산자 앞에 반드시 A 또는 E가 나와야 한다는 규칙을 지켜야 한다. CTL은 1차 술어논리에서 사용되는 어휘를 기본 요소로 사용하며, 여기에 시간 개념을 위한 연산자가 부가되어 논리식을 형성한다.

연산자

어떤 논리식 φ, ψ에 대하여, 각 연산자가 붙은 다음 CTL 식들의 의미는 다음과 같다.

• AXφ : 현재 상태에서 모든 실행가능한 경로에 대하여, 그 다음 상태에서 φ가 성립한다.
• EXφ : 현재 상태에서 연결되는 경로 중 어떤 경로에 대하여, 그 다음 상태에서 φ가 성립한다.
• AGφ : 현재 상태에서 모든 실행가능한 경로에 대하여, 언제나 φ가 성립한다.
• EGφ : 현재 상태에서 연결되는 경로 중 어떤 경로에 대하여, 언제나 φ가 성립한다.
• AFφ : 현재 상태에서 모든 실행가능한 경로에 대하여, 언젠가는 φ가 성립한다.
• EFφ : 현재 상태에서 연결되는 경로 중 어떤 경로에 대하여, 언젠가는 φ가 성립한다.
• A[φ U ψ ] : 현재 상태에서 모든 실행가능한 경로에 대하여, 언젠가는 ψ가 성립하며, 동시에 최초에 ψ가 성립되기까지는 φ가 성립한다.

• E[φ U ψ ] : 현재 상태에서 연결되는 경로 중 어떤 경로에 대하여, 언젠가는 ψ가 성립하며, 동시에 최초에 ψ가 성립되기까지는 φ가 성립한다.

CTL의 예

• EF(x < n)

어떤 실행가능한 경로가 있어, 이에 대해 언젠가는 x < n이 성립한다. 즉 x < n을 만족할 가능성이 존재한다.

• ￢ EF (x < n)

위의 식의 부정의 의미, 즉 x < n 을 만족할 가능성이 없다.