계산 트리 논리 문서 원본 보기

{{위키데이터 속성 추적}}
[[파일:CTL model.png|thumb]]
'''계산 트리 논리''' 또는 '''계산 나무 논리'''(Computational Tree Logic, '''CTL''')은 [[분기시간논리]]의 한 종류로, 어떤 상태에서 실행이 가능한 상태로의 경로를 트리 구조로 전개한 결과인 계산 트리와 의미론이 정의된 논리 체계이다.<ref>소프트웨어과학기초, TopSE 기초강좌1, 磯部祥尚 외, 近代科学社, {{ISBN|978-4-7659-0355-5}}</ref>

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

== 문법 ==

<math>\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]</math><br />
p는 기본항이다. ''A''는 '모든 실행 가능한 경로에 대해 필연적으로'의 의미를 나타내며, ''E''는 '적어도 한개의 어떤 실행 가능한 경로가 어느 때에 존재하여'의 의미를 나타낸다. 다음 식은 CTL의 [[논리식]](well-formed formula)이다.

<math>EF EG p \rightarrow AF r </math><br /> 

그러나 다음 CTL 식은 논리식이 아니다. 

<math>EF (r U q) </math><br />

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

== 같이 보기 ==
* [[선형 시제 논리]]
== 각주 ==
{{각주}}

{{전거 통제}}

[[분류:컴퓨터 과학 내 논리]]
[[분류:시간 논리]]
[[분류:오토마타 이론]]