계산 트리 논리

위키백과, 우리 모두의 백과사전.
이동: 둘러보기, 검색

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

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

문법[편집]

\phi::=F|T|p|(\neg\phi)|(\phi\and\phi)|(\phi\or\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)이다.

EF EG p \rightarrow AF r

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

EF (r U q)

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 을 만족할 가능성이 없다.

  1. 소프트웨어과학기초, TopSE 기초강좌1, 磯部祥尚 외, 近代科学社, ISBN 978-4-7659-0355-5