397.11 CTL과 LTL의 표현력 비교

1. 표현력 비교의 이론적 배경

계산 트리 논리(CTL)와 선형 시제 논리(LTL)는 시간적 성질을 명세하기 위한 대표적인 형식 논리 체계이나, 양자는 서로 다른 시간 모델에 기반하므로 표현 가능한 성질의 범위가 상이하다. LTL은 선형 시간(linear time) 모델에 기초하여 단일 실행 경로(single execution path) 위에서 시간적 성질을 기술하며, CTL은 분기형 시간(branching time) 모델에 기초하여 계산 트리(computation tree) 위에서 경로 한정자와 시간 연산자의 쌍(pair)을 통하여 성질을 기술한다. Emerson과 Halpern은 이 두 논리의 표현력이 비교 불가능(incomparable)함을 엄밀하게 증명하였다 (Emerson & Halpern, 1986).

2. 표현력 비교의 형식적 정의

두 논리 체계 $\mathcal{L}_1$ 과 $\mathcal{L}_2$ 의 표현력(expressiveness)을 비교하기 위하여, 다음과 같은 기준을 도입한다. 논리 $\mathcal{L}$ 의 공식 $\Phi$ 가 나타내는 모델 집합을 $\text{Mod}(\Phi)$ 라 하자. 논리 $\mathcal{L}_1$ 이 $\mathcal{L}_2$ 보다 표현력이 동등하거나 강하다 함은, $\mathcal{L}_2$ 의 임의 공식 $\Phi_2$ 에 대하여 $\text{Mod}(\Phi_1) = \text{Mod}(\Phi_2)$ 를 만족하는 $\mathcal{L}_1$ 의 공식 $\Phi_1$ 이 존재함을 의미한다.

그러나 CTL과 LTL은 서로 다른 의미론적 기반을 가지므로, 비교를 위하여 공통의 의미론적 토대가 필요하다. 이를 위하여 크립키 구조(Kripke structure) $\mathcal{M} = (S, S_0, R, L)$ 위에서 양 논리의 만족 관계를 통일적으로 정의한다. CTL 공식은 상태(state)에 대한 만족 관계로, LTL 공식은 경로(path)에 대한 만족 관계로 해석되므로, LTL 공식 $\phi$ 가 크립키 구조 $\mathcal{M}$ 을 만족한다 함은 $\mathcal{M}$ 의 모든 초기 상태에서 출발하는 모든 경로가 $\phi$ 를 만족함을 의미하며, 이는 CTL 공식 $\mathbf{A}\phi$ 와 대응한다.

3. CTL로 표현 가능하나 LTL로 표현 불가능한 성질

CTL은 존재적 경로 한정자(existential path quantifier) $\mathbf{E}$ 를 통하여, 특정 경로의 존재성에 관한 성질을 직접 명세할 수 있다. 이는 LTL의 표현 범위에 속하지 않는 고유한 능력이다.

3.1 도달 가능성의 존재적 명세

대표적 예는 다음의 CTL 공식이다:

$\mathbf{AG}(\mathbf{EF}\, \textit{restart})$

이 공식은 “모든 도달 가능한 상태에서, $\textit{restart}$ 상태로 되돌아갈 수 있는 경로가 존재한다“는 성질을 명세한다. 이러한 성질은 리셋 가능성(resetability)이라 불리며, 자율 로봇 시스템에서 오류 복구(fault recovery) 능력을 보장하는 데 중요하다. Emerson과 Halpern(1986)은 이 성질이 어떠한 LTL 공식으로도 표현될 수 없음을 증명하였다.

LTL은 개별 경로 위에서의 성질만을 기술할 수 있으므로, “어떤 경로가 존재한다“는 존재적 양화를 직접 표현하는 것이 구조적으로 불가능하다. LTL 공식은 암묵적으로 보편적 경로 한정자 $\mathbf{A}$ 아래에서 해석되기 때문이다.

3.2 비결정론적 선택의 명세

또 다른 예로, 다음의 CTL 공식을 고려하라:

$\mathbf{EX}\, p \wedge \mathbf{EX}\, \neg p$

이 공식은 현재 상태에서 $p$ 가 성립하는 후속 상태와 $p$ 가 성립하지 않는 후속 상태가 모두 존재함을 명세한다. 이는 비결정론적 분기(nondeterministic branching)의 존재를 직접 기술하는 것으로, 선형 시간 논리의 범주에서는 표현이 불가능하다.

4. LTL로 표현 가능하나 CTL로 표현 불가능한 성질

LTL 또한 CTL의 표현 범위에 속하지 않는 고유한 표현 능력을 보유한다. 이는 CTL에서 경로 한정자와 시간 연산자가 반드시 쌍으로 결합되어야 하는 구문적 제약에 기인한다.

4.1 공정성 성질

대표적 예는 다음의 LTL 공식이다:

$\mathbf{FG}\, p$

이 공식은 “결국 어느 시점부터 $p$ 가 영원히 성립한다“는 성질을 명세하며, 궁극적 안정성(eventual stability)이라 불린다. 이를 CTL로 변환하려면 $\mathbf{AF}(\mathbf{AG}\, p)$ 를 고려할 수 있으나, 이 두 공식은 의미론적으로 동치가 아니다.

$\mathbf{AF}(\mathbf{AG}\, p)$ 는 “모든 경로에서, 결국 그 이후의 모든 경로에서 $p$ 가 항상 성립하는 상태에 도달한다“는 의미인 반면, $\mathbf{FG}\, p$ 는 “개별 경로 위에서, 결국 어느 시점부터 $p$ 가 영원히 성립한다“는 의미이다. 전자는 분기 지점(branching point)에서의 모든 미래를 고려하는 반면, 후자는 단일 경로 내에서의 궁극적 행동만을 기술한다.

Lamport(1980)에 의한 엄밀한 반례 구성을 통하여, 특정 크립키 구조에서 $\mathbf{FG}\, p$ 는 참이나 $\mathbf{AF}(\mathbf{AG}\, p)$ 는 거짓이 되는 경우가 존재함이 증명되었다. 이는 LTL의 $\mathbf{FG}$ 패턴이 CTL의 어떠한 공식으로도 정확하게 포착될 수 없음을 입증한다.

4.2 경로 내 시간 연산자의 자유 결합

LTL에서는 시간 연산자를 경로 내에서 자유롭게 결합할 수 있다. 예를 들어:

$\mathbf{G}(\textit{request} \rightarrow \mathbf{F}\, \textit{response})$

이 공식은 “모든 시점에서, 요청이 발생하면 언젠가 응답이 따른다“는 성질을 명세한다. 이를 CTL로 번역하면 $\mathbf{AG}(\textit{request} \rightarrow \mathbf{AF}\, \textit{response})$ 가 되며, 이 특정 경우에는 양자가 동치이다. 그러나 보다 복잡한 결합의 경우, 예를 들어:

$\mathbf{G}(\mathbf{F}\, p \rightarrow \mathbf{F}\, q)$

이 공식은 “모든 시점에서, $p$ 가 미래에 성립할 것이라면 $q$ 도 미래에 성립한다“는 성질을 명세하며, 이는 CTL의 어떠한 공식으로도 동치적으로 표현될 수 없다.

5. 표현력 관계의 계층 구조

CTL과 LTL의 표현력 관계는 다음과 같은 계층 구조로 정리된다:

        CTL*
       /    \
     CTL    LTL
       \    /
      CTL ∩ LTL

여기서 CTL은 CTL과 LTL을 모두 진부분 논리(proper sublogic)로 포함하는 상위 논리 체계이다 (Emerson & Halpern, 1986). CTL에서는 경로 한정자와 시간 연산자의 자유로운 조합이 허용되므로, CTL과 LTL에서 각각 표현 가능한 모든 성질을 표현할 수 있다.

CTL과 LTL의 교집합(CTL $\cap$ LTL)에 해당하는 성질들은 양쪽 논리 모두에서 표현 가능한 성질들로서, 다음과 같은 기본적 안전성 및 활성 성질들이 이에 해당한다:

성질	LTL 표현	CTL 표현	분류
불변성	$\mathbf{G}\, p$	$\mathbf{AG}\, p$	CTL $\cap$ LTL
단순 도달 가능성	$\mathbf{F}\, p$	$\mathbf{AF}\, p$	CTL $\cap$ LTL
응답성	$\mathbf{G}(p \rightarrow \mathbf{F}\, q)$	$\mathbf{AG}(p \rightarrow \mathbf{AF}\, q)$	CTL $\cap$ LTL
궁극적 안정성	$\mathbf{FG}\, p$	동치 표현 없음	LTL $\setminus$ CTL
리셋 가능성	동치 표현 없음	$\mathbf{AG}(\mathbf{EF}\, \textit{restart})$	CTL $\setminus$ LTL

6. 모델 검사 복잡도의 비교

CTL과 LTL의 표현력 차이는 모델 검사의 계산 복잡도에도 영향을 미친다.

6.1 CTL 모델 검사의 복잡도

CTL 모델 검사의 시간 복잡도는 $O(\lvert \Phi \rvert \cdot (\lvert S \rvert + \lvert R \rvert))$ 이다 (Clarke, Emerson, & Sistla, 1986). 이는 공식 크기와 상태 전이 시스템 크기의 곱에 선형적으로 비례하므로, 다항 시간(polynomial time) 알고리즘에 해당한다. 이러한 효율적 검증은 CTL의 구문적 제약, 즉 경로 한정자와 시간 연산자의 쌍 결합 구조가 고정점 계산(fixpoint computation)을 통한 체계적 라벨링 알고리즘을 가능하게 하기 때문이다.

6.2 LTL 모델 검사의 복잡도

LTL 모델 검사의 시간 복잡도는 $O(\lvert S \rvert \cdot 2^{O(\lvert \phi \rvert)})$ 이다 (Vardi & Wolper, 1986). LTL 공식을 뷔히 오토마타(Büchi automaton)로 변환하는 과정에서 공식 크기에 대한 지수적 확장(exponential blowup)이 발생하며, 이는 PSPACE-complete 문제에 해당한다. 따라서 LTL 모델 검사는 공식 크기가 커질수록 CTL 모델 검사에 비하여 계산 비용이 급격히 증가한다.

속성	CTL 모델 검사	LTL 모델 검사
시간 복잡도	$O(\lvert \Phi \rvert \cdot (\lvert S \rvert + \lvert R \rvert))$	$O(\lvert S \rvert \cdot 2^{O(\lvert \phi \rvert)})$
복잡도 분류	P (다항 시간)	PSPACE-complete
공식 크기 의존성	선형	지수적
상태 공간 의존성	선형	선형

7. 자율 로봇 임무 명세에서의 선택 기준

CTL과 LTL의 표현력 차이를 고려할 때, 자율 로봇 시스템의 임무 명세에 적합한 논리의 선택은 임무의 특성에 따라 결정되어야 한다.

7.1 CTL이 적합한 경우

비결정론적 환경에서의 존재적 성질: 로봇이 복수의 대안적 행동 중 적어도 하나를 수행할 수 있음을 보장해야 하는 경우, 존재적 경로 한정자 $\mathbf{E}$ 를 필요로 한다.
리셋 가능성 및 오류 복구: 시스템이 임의의 상태에서 안전 상태로 복귀할 수 있는 경로의 존재를 보장해야 하는 경우, $\mathbf{AG}(\mathbf{EF}\, \textit{safe})$ 형태의 명세가 필요하다.
효율적 자동 검증: 다항 시간 모델 검사의 장점을 최대한 활용하고자 하는 경우, CTL 기반 명세가 계산적으로 유리하다.

7.2 LTL이 적합한 경우

경로 단위의 시간적 패턴: 개별 실행 경로 위에서의 사건 순서(event ordering)나 궁극적 행동 패턴을 명세해야 하는 경우, LTL의 자유로운 시간 연산자 결합이 유리하다.
공정성 및 활성 명세: 기아 방지(starvation freedom)나 궁극적 안정성과 같은 공정성 제약을 기술해야 하는 경우, LTL의 $\mathbf{FG}$ 및 $\mathbf{GF}$ 패턴이 필수적이다.
제어 합성과의 통합: 오토마타 기반 제어 정책 합성에서는 LTL 공식의 뷔히 오토마타 변환이 표준적 절차로 확립되어 있어, LTL 기반 명세가 합성 파이프라인과의 통합에 유리하다.

7.3 실무적 고려사항

실제 자율 로봇 시스템에서는 단일 논리만을 고수하기보다, 임무의 상이한 요구사항에 따라 CTL과 LTL을 병용하거나, 양자를 모두 포함하는 CTL*을 활용하는 접근법이 권장된다 (Baier & Katoen, 2008). 특히, 안전성 요구사항은 CTL의 $\mathbf{AG}$ 패턴으로, 공정성 요구사항은 LTL의 $\mathbf{GF}$ 패턴으로, 비결정론적 환경에서의 대안적 행동 보장은 CTL의 $\mathbf{E}$ 한정자로 각각 명세하는 혼합 전략이 효과적이다.

8. 참고문헌

Baier, C., & Katoen, J. P. (2008). Principles of Model Checking. MIT Press.
Clarke, E. M., Emerson, E. A., & Sistla, A. P. (1986). “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications.” ACM Transactions on Programming Languages and Systems, 8(2), 244–263.
Emerson, E. A., & Halpern, J. Y. (1986). “‘Sometimes’ and ‘Not Never’ Revisited: On Branching Versus Linear Time Temporal Logic.” Journal of the ACM, 33(1), 151–178.
Lamport, L. (1980). “‘Sometime’ Is Sometimes ‘Not Never’: On the Temporal Logic of Programs.” In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 174–185.
Vardi, M. Y., & Wolper, P. (1986). “An Automata-Theoretic Approach to Automatic Program Verification.” In Proceedings of the 1st IEEE Symposium on Logic in Computer Science (LICS), 332–344.