397.10 계산 트리 논리(CTL) 기반 임무 명세

1. 계산 트리 논리의 개요

계산 트리 논리(Computation Tree Logic, CTL)는 시간 논리(temporal logic)의 한 분류로서, 분기형 시간 구조(branching-time structure)를 기반으로 시스템의 동적 행동 양식을 형식적으로 명세하는 논리 체계이다. Edmund M. Clarke와 E. Allen Emerson이 1981년에 제안한 CTL은 모델 검사(model checking) 분야에서 핵심적인 역할을 수행하며, 자율 로봇 시스템의 임무 명세에도 널리 적용된다 (Clarke & Emerson, 1981).

선형 시제 논리(LTL)가 단일 실행 경로(single execution path)를 기준으로 시간적 성질을 기술하는 것과 달리, CTL은 계산 트리(computation tree)라 불리는 트리 구조 위에서 분기하는 모든 가능한 미래 경로를 동시에 고려한다. 이러한 분기형 시간 모델은 비결정론적(nondeterministic) 환경에서 시스템의 행동을 보다 풍부하게 표현할 수 있는 장점을 제공한다.

2. CTL의 구문론

CTL의 구문(syntax)은 상태 공식(state formula)과 경로 공식(path formula)의 두 가지 범주로 구성된다. 임의의 원자 명제(atomic proposition) 집합 AP가 주어졌을 때, CTL 공식은 다음의 귀납적 규칙에 의하여 정의된다.

상태 공식(State Formula):

\Phi ::= p \mid \neg \Phi \mid \Phi_1 \wedge \Phi_2 \mid \mathbf{A}\varphi \mid \mathbf{E}\varphi

여기서 p \in AP는 원자 명제이고, \varphi는 경로 공식이다.

경로 공식(Path Formula):

\varphi ::= \mathbf{X}\Phi \mid \Phi_1 \mathbf{U} \Phi_2 \mid \mathbf{G}\Phi \mid \mathbf{F}\Phi

CTL의 핵심적 특징은 경로 한정자(path quantifier)와 시간 연산자(temporal operator)가 반드시 쌍(pair)으로 결합되어야 한다는 점이다. 경로 한정자 \mathbf{A}(for All paths)와 \mathbf{E}(there Exists a path)는 시간 연산자 \mathbf{X}(neXt), \mathbf{U}(Until), \mathbf{G}(Globally), \mathbf{F}(Future)와 결합하여 다음의 8가지 기본 연산자 조합을 형성한다:

3. CTL의 의미론

CTL 공식의 의미론(semantics)은 크립키 구조(Kripke structure) \mathcal{M} = (S, S_0, R, L) 위에서 정의된다. 여기서 S는 유한 상태 집합, S_0 \subseteq S는 초기 상태 집합, R \subseteq S \times S는 전이 관계(transition relation), L : S \rightarrow 2^{AP}는 라벨링 함수(labeling function)이다.

특정 상태 s \in S에서 CTL 공식 \Phi의 만족 관계 \mathcal{M}, s \models \Phi는 다음과 같이 귀납적으로 정의된다:

\begin{aligned} &\mathcal{M}, s \models p &&\iff p \in L(s) \\ &\mathcal{M}, s \models \neg \Phi &&\iff \mathcal{M}, s \not\models \Phi \\ &\mathcal{M}, s \models \Phi_1 \wedge \Phi_2 &&\iff \mathcal{M}, s \models \Phi_1 \text{ 이고 } \mathcal{M}, s \models \Phi_2 \\ &\mathcal{M}, s \models \mathbf{AX}\Phi &&\iff \text{모든 } (s, s') \in R \text{에 대하여 } \mathcal{M}, s' \models \Phi \\ &\mathcal{M}, s \models \mathbf{EX}\Phi &&\iff \text{어떤 } (s, s') \in R \text{에 대하여 } \mathcal{M}, s' \models \Phi \\ &\mathcal{M}, s \models \mathbf{AG}\Phi &&\iff \text{모든 경로 } \pi = s_0 s_1 s_2 \ldots \text{에서 모든 } i \geq 0, \; \mathcal{M}, s_i \models \Phi \\ &\mathcal{M}, s \models \mathbf{EG}\Phi &&\iff \text{어떤 경로 } \pi \text{에서 모든 } i \geq 0, \; \mathcal{M}, s_i \models \Phi \\ &\mathcal{M}, s \models \mathbf{AF}\Phi &&\iff \text{모든 경로에서 어떤 } i \geq 0, \; \mathcal{M}, s_i \models \Phi \\ &\mathcal{M}, s \models \mathbf{EF}\Phi &&\iff \text{어떤 경로에서 어떤 } i \geq 0, \; \mathcal{M}, s_i \models \Phi \end{aligned}

이러한 의미론적 정의는 계산 트리 상에서 분기하는 경로들에 대한 양화(quantification)를 명시적으로 표현하므로, 시스템의 비결정론적 행동에 대한 정밀한 추론을 가능하게 한다.

4. 자율 로봇 임무 명세에서의 CTL 적용

자율 로봇 시스템의 임무를 CTL로 명세할 때, 원자 명제는 로봇의 상태, 위치, 센서 판독값, 환경 조건 등을 추상화한 것으로 정의된다. 이를 통하여 다양한 임무 요구사항을 형식적 논리 공식으로 변환할 수 있다.

4.1 안전성(Safety) 명세

안전성은 시스템이 허용되지 않는 상태에 진입하지 않음을 보장하는 성질이다. CTL에서는 \mathbf{AG} 연산자를 활용하여 다음과 같이 표현한다:

\mathbf{AG}(\neg \textit{collision})

이 공식은 모든 가능한 실행 경로의 모든 상태에서 충돌(collision) 상태가 발생하지 않음을 명세한다. 로봇의 장애물 회피 임무에서 이러한 안전성 명세는 필수적 요구사항으로 작용한다.

4.2 도달 가능성(Reachability) 명세

도달 가능성은 시스템이 특정 목표 상태에 도달할 수 있는지를 기술하는 성질이다. 존재적 도달 가능성과 보편적 도달 가능성을 구분하여 명세할 수 있다:

\mathbf{EF}(\textit{target\_reached})

위 공식은 적어도 하나의 실행 경로에서 목표 지점에 도달하는 상태가 존재함을 의미한다. 반면,

\mathbf{AF}(\textit{target\_reached})

이 공식은 모든 가능한 실행 경로에서 로봇이 반드시 목표 지점에 도달해야 함을 명세하며, 비결정론적 환경에서도 임무 달성을 보장하는 강한 요구사항을 표현한다.

4.3 활성(Liveness) 명세

활성 성질은 시스템이 원하는 행동을 반복적으로 수행할 수 있음을 보장한다. 예를 들어 순찰(patrol) 임무에서 로봇이 특정 구역을 반복적으로 방문해야 하는 요구사항은 다음과 같이 명세된다:

\mathbf{AG}(\mathbf{AF}(\textit{region\_A\_visited}))

이 공식은 모든 실행 경로의 모든 상태에서, 이후 반드시 \textit{region\_A\_visited}가 성립하는 시점이 존재함을 보장한다. 이는 로봇이 어떤 상태에 있더라도 결국 구역 A를 방문하게 됨을 의미한다.

4.4 공정성(Fairness) 명세

공정성 제약은 특정 사건이 무한히 자주 발생하거나 특정 조건이 공정하게 충족되어야 함을 보장한다. 다중 임무 환경에서 로봇이 특정 작업을 무한히 지연시키지 않도록 보장하는 요구사항은 다음과 같이 표현된다:

\mathbf{AG}(\mathbf{AF}(\textit{task\_served}))

이 공식은 시스템의 어느 시점에서든, 해당 작업이 결국 서비스됨을 보장하여, 기아 상태(starvation) 방지를 형식적으로 명세한다.

5. CTL 모델 검사 알고리즘

CTL 기반 임무 명세의 핵심적 장점은 효율적인 모델 검사 알고리즘이 존재한다는 것이다. 주어진 크립키 구조 \mathcal{M}과 CTL 공식 \Phi에 대하여, \mathcal{M} \models \Phi 여부를 검증하는 문제는 다항 시간(polynomial time) 내에 해결 가능하다.

5.1 명시적 상태 모델 검사

Clarke, Emerson, 그리고 Sistla가 제안한 CTL 모델 검사 알고리즘은 공식의 부분 공식(subformula)에 대하여 바텀업(bottom-up) 방식으로 각 상태에 라벨을 부착하는 절차를 따른다 (Clarke, Emerson, & Sistla, 1986). 알고리즘의 시간 복잡도는 O(\lvert \Phi \rvert \cdot (\lvert S \rvert + \lvert R \rvert))이며, 여기서 \lvert \Phi \rvert는 공식의 크기, \lvert S \rvert는 상태 수, \lvert R \rvert는 전이 관계의 크기이다.

구체적 절차는 다음과 같다:

1. 공식 \Phi의 모든 부분 공식을 파싱 트리(parse tree)의 잎(leaf) 노드부터 루트(root)까지 순서대로 나열한다.
2. 각 부분 공식 \Phi_i에 대하여, \Phi_i를 만족하는 상태 집합 \text{Sat}(\Phi_i)를 계산한다.
3. 원자 명제 p에 대하여, \text{Sat}(p) = \{s \in S \mid p \in L(s)\}이다.
4. \mathbf{EX}\Phi_i에 대하여, \text{Sat}(\mathbf{EX}\Phi_i) = \{s \in S \mid \exists s'. \; (s, s') \in R \wedge s' \in \text{Sat}(\Phi_i)\}이다.
5. \mathbf{E}[\Phi_1 \mathbf{U} \Phi_2]에 대하여, 고정점 계산(fixpoint computation)을 수행한다:

\text{Sat}(\mathbf{E}[\Phi_1 \mathbf{U} \Phi_2]) = \mu Z. \; (\text{Sat}(\Phi_2) \cup (\text{Sat}(\Phi_1) \cap \{s \mid \exists s'. \; (s,s') \in R \wedge s' \in Z\}))

여기서 \mu Z는 최소 고정점(least fixpoint)을 나타낸다.

6. \mathbf{EG}\Phi_i에 대하여, 최대 고정점(greatest fixpoint) 계산을 수행한다:

\text{Sat}(\mathbf{EG}\Phi_i) = \nu Z. \; (\text{Sat}(\Phi_i) \cap \{s \mid \exists s'. \; (s,s') \in R \wedge s' \in Z\})

5.2 기호적 모델 검사

상태 공간의 폭발(state space explosion) 문제를 완화하기 위하여, McMillan은 이진 결정 다이어그램(Binary Decision Diagram, BDD)을 활용한 기호적 모델 검사(symbolic model checking) 기법을 도입하였다 (McMillan, 1993). 기호적 모델 검사에서는 상태 집합과 전이 관계를 부울 함수(Boolean function)로 표현하고, BDD 연산을 통하여 고정점 계산을 수행한다. 이 기법은 10^{20} 이상의 상태 공간을 가진 시스템에 대해서도 검증을 가능하게 하며, 복잡한 로봇 임무의 검증에 실질적 적용 가능성을 확보하였다.

6. CTL 기반 로봇 임무 명세의 사례

6.1 탐색 및 구조 임무

수색 및 구조(Search and Rescue, SAR) 시나리오에서 로봇에게 부여되는 임무는 CTL을 활용하여 다음과 같이 명세할 수 있다:

\mathbf{AG}(\textit{survivor\_detected} \rightarrow \mathbf{AF}(\textit{rescue\_initiated}))

이 명세는 모든 실행 경로에서, 생존자가 탐지되면 모든 가능한 미래 경로에서 반드시 구조 작업이 개시됨을 보장한다. 비결정론적 환경 변화에도 구조 작업의 개시가 보장되어야 하므로, 보편적 경로 한정자 \mathbf{A}의 사용이 적절하다.

6.2 자율 물류 임무

물류 로봇의 배송 임무에서, 로봇이 물품을 적재한 후 반드시 목적지에 도달해야 하는 요구사항은 다음과 같이 명세된다:

\mathbf{AG}(\textit{payload\_loaded} \rightarrow \mathbf{AF}(\textit{destination\_reached}))

동시에, 배터리 잔량(State of Charge, SoC)이 임계치 아래로 떨어지지 않아야 하는 안전성 제약은 다음과 같다:

\mathbf{AG}(\textit{SoC} > \textit{threshold})

6.3 다중 로봇 순찰 임무

다수의 로봇이 여러 구역을 순찰하는 임무에서, 각 구역이 무한히 자주 방문되어야 하는 요구사항은 다음과 같이 명세된다:

\bigwedge_{i=1}^{n} \mathbf{AG}(\mathbf{AF}(\textit{region}_i \textit{\_visited}))

이 공식은 n개의 순찰 구역 각각에 대하여, 모든 가능한 실행 경로에서 해당 구역이 반복적으로 방문됨을 보장한다.

7. CTL의 확장과 변형

7.1 CTL*

CTL은 CTL과 LTL을 모두 포함하는 상위 논리 체계로서, 경로 한정자와 시간 연산자의 자유로운 조합을 허용한다 (Emerson & Halpern, 1986). CTL에서는 경로 한정자와 시간 연산자가 반드시 쌍으로 결합될 필요가 없으므로, CTL이나 LTL 단독으로는 표현할 수 없는 성질도 명세할 수 있다. 그러나 CTL*의 모델 검사는 PSPACE-complete 문제로 알려져 있어, CTL에 비하여 계산 비용이 높다.

7.2 확률적 CTL(PCTL)

확률적 CTL(Probabilistic CTL, PCTL)은 경로 한정자에 확률적 한계(probability bound)를 부여함으로써 확률적 시스템의 성질을 명세한다 (Hansson & Jonsson, 1994). PCTL의 공식은 다음과 같은 형태를 취한다:

\mathbf{P}_{\bowtie p}[\varphi]

여기서 \bowtie \in \{<, \leq, \geq, >\}이고, p \in [0,1]은 확률 임계치이다. 예를 들어, 로봇이 90% 이상의 확률로 목표에 도달하는 요구사항은 다음과 같이 명세된다:

\mathbf{P}_{\geq 0.9}[\mathbf{F}(\textit{target\_reached})]

이러한 확장은 센서 불확실성과 환경의 확률적 변동이 존재하는 실제 로봇 시스템의 임무 명세에 특히 유용하다.

7.3 시간 제한 CTL(TCTL)

시간 제한 CTL(Timed CTL, TCTL)은 시간 제약을 명시적으로 포함할 수 있는 확장 형태로서, 시간 자동자(timed automata) 위에서 해석된다 (Alur, Courcoubetis, & Dill, 1993). TCTL에서는 시간 연산자에 시간 경계(time bound)를 부착할 수 있으며, 예를 들어:

\mathbf{AF}_{\leq T}(\textit{mission\_complete})

이 공식은 모든 실행 경로에서 T 시간 단위 이내에 임무가 완료됨을 명세한다. 실시간 자율 로봇 시스템에서 시간 제약이 중요한 임무의 명세에 필수적으로 활용된다.

8. 로봇 임무 명세에서 CTL의 장점과 한계

8.1 장점

CTL 기반 임무 명세는 다음과 같은 장점을 제공한다:

1. 다항 시간 모델 검사: CTL의 모델 검사는 O(\lvert \Phi \rvert \cdot (\lvert S \rvert + \lvert R \rvert))의 시간 복잡도를 가지며, 이는 LTL의 모델 검사(PSPACE-complete)에 비하여 계산적으로 효율적이다.
2. 분기적 추론: 경로 한정자 \mathbf{A}와 \mathbf{E}를 통하여, 모든 가능한 미래와 특정 가능한 미래를 구분하여 명세할 수 있으므로, 비결정론적 환경에서의 임무 요구사항을 보다 세밀하게 표현할 수 있다.
3. 고정점 이론 기반: CTL의 의미론은 고정점 이론(fixpoint theory)에 기반하므로, 구조적이고 체계적인 검증 알고리즘의 설계가 가능하다.
4. 반례 생성: 모델 검사 과정에서 명세를 위반하는 반례(counterexample)를 자동으로 생성할 수 있어, 임무 계획의 디버깅과 수정에 유용하다.

8.2 한계

1. 경로 독립적 성질의 제한: CTL에서는 경로 한정자와 시간 연산자가 반드시 쌍으로 결합되므로, \mathbf{A}(\mathbf{F}p \rightarrow \mathbf{F}q)와 같이 경로 내에서 여러 시간 연산자를 자유롭게 조합하는 표현이 불가능하다. 이를 위해서는 CTL*이 필요하다.
2. 상태 공간 폭발: 모델 검사의 효율성에도 불구하고, 대규모 로봇 시스템에서는 상태 공간의 지수적 증가로 인한 계산적 부담이 발생할 수 있다. 기호적 모델 검사, 추상화(abstraction), 부분 순서 감축(partial order reduction) 등의 기법이 이를 완화하는 데 활용된다.
3. 실수값 변수 처리의 어려움: CTL은 기본적으로 유한 상태 시스템 위에서 정의되므로, 연속적인 물리적 변수(위치, 속도, 가속도 등)를 직접 다루기 어렵다. 이를 해결하기 위하여 하이브리드 시스템 모델이나 추상화 기법과의 결합이 필요하다.

9. 참고문헌

• Alur, R., Courcoubetis, C., & Dill, D. (1993). “Model-Checking in Dense Real-Time.” Information and Computation, 104(1), 2–34.
• Clarke, E. M., & Emerson, E. A. (1981). “Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.” In Logic of Programs Workshop, LNCS 131, Springer.
• 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.
• Hansson, H., & Jonsson, B. (1994). “A Logic for Reasoning about Time and Reliability.” Formal Aspects of Computing, 6(5), 512–535.
• McMillan, K. L. (1993). Symbolic Model Checking. Kluwer Academic Publishers.