**CTL (Computation Tree Logic)**은 **분기 시계열 논리(branching-time temporal logic)**의 한 종류로, 시스템의 모든 가능한 미래 경로에 대해 명제를 기술하는 데 사용되는 형식 논리입니다. 주로 Model Checking에서 사용됩니다.
---
핵심 개념:
CTL의 식은 항상 두 종류의 기호가 함께 쓰입니다:
경로 한정자 (path quantifier):
A: 모든 경로 (All paths)
E: 어떤 경로 (Exists a path)
시제 연산자 (temporal operator):
X: 다음 (neXt)
F: 미래에 언젠가 (Future)
G: 항상 (Globally)
U: ~까지 (Until)
CTL에서는 항상 이 두 종류가 쌍으로 사용됩니다.
예를 들어:
AX p: 모든 경로에서 다음 상태에 p가 참
EF q: 어떤 경로에서는 미래에 q가 언젠가 참
AG r: 모든 경로에서 항상 r이 참
E[p U q]: 어떤 경로에서 p가 계속 참이고, 언젠가 q가 참
---
사용 예시 (Model Checking):
"어떤 실행에서 eventually success 상태에 도달할 수 있는가?" → EF success
"항상 요청이 오면 언젠가 응답이 오는가?" → AG (request → AF response)
---
요약:
CTL은 시스템의 모든 가능 경로를 고려하며, 상태의 논리적 특성을 시간 축을 따라 기술하는 데 매우 적합한 논리입니다.
카테고리 없음