397.7 선형 시제 논리(LTL) 기반 임무 명세

1. 개요

선형 시제 논리(Linear Temporal Logic, LTL)는 시간의 선형적 흐름 위에서 시스템의 행동을 형식적으로 기술하는 논리 체계이다. LTL은 Pnueli (1977)에 의하여 프로그램 검증(Program Verification)을 위하여 최초로 제안되었으며, 이후 로봇 공학에서 임무 명세의 표준적 도구로 자리매김하였다 (Kress-Gazit et al., 2009). LTL 기반 임무 명세의 핵심 장점은 임무의 시간적 요구사항을 수학적으로 엄밀하게 기술할 수 있으며, 이를 오토마타로 변환하여 자동화된 제어기 합성(Controller Synthesis)과 모델 검사(Model Checking)를 수행할 수 있다는 점이다.

2. LTL의 구문론 (Syntax)

LTL 공식(Formula)은 원자 명제(Atomic Propositions) \mathcal{AP}의 집합 위에서 다음의 귀납적 규칙(Inductive Rules)에 의하여 정의된다.

\varphi ::= p \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \bigcirc \varphi \mid \varphi_1 \mathcal{U} \varphi_2

여기서 p \in \mathcal{AP}는 원자 명제이고, \neg는 부정(Negation), \wedge는 논리곱(Conjunction), \bigcirc는 다음(Next) 연산자, \mathcal{U}는 때까지(Until) 연산자이다.

추가적인 연산자는 기본 연산자로부터 다음과 같이 유도된다.

3. LTL의 의미론 (Semantics)

LTL 공식의 의미는 무한 단어(Infinite Word) \sigma = \sigma_0 \sigma_1 \sigma_2 \cdots \in (2^{\mathcal{AP}})^\omega 위에서 정의된다. 여기서 \sigma_i \subseteq \mathcal{AP}는 시각 i에서 참인 원자 명제의 집합이다.

만족 관계(Satisfaction Relation) \sigma, i \models \varphi는 다음과 같이 귀납적으로 정의된다.

\sigma, i \models p \iff p \in \sigma_i

\sigma, i \models \neg \varphi \iff \sigma, i \not\models \varphi

\sigma, i \models \varphi_1 \wedge \varphi_2 \iff \sigma, i \models \varphi_1 \text{ and } \sigma, i \models \varphi_2

\sigma, i \models \bigcirc \varphi \iff \sigma, i+1 \models \varphi

\sigma, i \models \varphi_1 \mathcal{U} \varphi_2 \iff \exists j \geq i: \sigma, j \models \varphi_2 \text{ and } \forall k \in [i, j): \sigma, k \models \varphi_1

단어 \sigma가 공식 \varphi를 만족한다는 것은 \sigma, 0 \models \varphi가 성립하는 것으로 정의하며, 이를 간략하게 \sigma \models \varphi로 표기한다.

4. LTL의 로봇 임무 명세에의 적용

LTL은 로봇 공학에서 다양한 유형의 임무 사양을 형식적으로 표현하는 데 활용된다. 대표적인 임무 패턴(Mission Pattern)과 이에 대응하는 LTL 공식은 다음과 같다.

4.1 도달성 (Reachability)

“결국 목표 영역 R_{\text{goal}}에 도달하라“는 임무는 다음과 같이 표현된다.

\varphi_{\text{reach}} = \lozenge R_{\text{goal}}

4.2 안전성 (Safety)

“항상 위험 영역 R_{\text{danger}}를 회피하라“는 임무는 다음과 같이 표현된다.

\varphi_{\text{safe}} = \square \neg R_{\text{danger}}

4.3 순서 방문 (Sequencing)

“먼저 영역 R_A를 방문한 후 영역 R_B를 방문하라“는 임무는 다음과 같이 표현된다.

\varphi_{\text{seq}} = \neg R_B \mathcal{U} R_A \wedge \lozenge R_B

4.4 반복 방문 (Recurrence/Liveness)

“영역 R_{\text{patrol}}을 무한히 반복 방문하라“는 임무는 다음과 같이 표현된다.

\varphi_{\text{patrol}} = \square \lozenge R_{\text{patrol}}

4.5 반응성 (Reactivity)

“비상 신호 \text{alarm}이 발생하면 결국 대피 지점 R_{\text{evac}}으로 이동하라“는 임무는 다음과 같이 표현된다.

\varphi_{\text{react}} = \square (\text{alarm} \rightarrow \lozenge R_{\text{evac}})

4.6 조건부 방문 (Conditional Visit)

“센서 데이터 수집이 완료되면 데이터 전송 지점을 방문하라“는 임무는 다음과 같이 표현된다.

\varphi_{\text{cond}} = \square (\text{data\_collected} \rightarrow \lozenge R_{\text{upload}})

5. LTL 기반 임무 계획의 절차

LTL 기반 임무 계획은 다음과 같은 체계적인 절차로 수행된다 (Belta et al., 2017).

단계 1: 환경의 전이 시스템 구성

로봇의 작업 공간을 이산적 전이 시스템 \mathcal{TS} = (Q, q_0, \delta, \mathcal{AP}, L)으로 모델링한다. 각 상태 q \in Q는 작업 공간의 추상화된 영역에 대응하며, 전이 관계 \delta는 영역 간의 이동 가능성을 나타낸다. 라벨링 함수 L: Q \rightarrow 2^{\mathcal{AP}}는 각 상태에서 성립하는 원자 명제를 부여한다.

단계 2: LTL 사양의 뷔히 오토마톤 변환

임무 사양 LTL 공식 \varphi를 비결정적 뷔히 오토마톤(Nondeterministic Büchi Automaton, NBA) \mathcal{A}_\varphi = (Q_A, \Sigma, \delta_A, Q_{A,0}, F_A)로 변환한다. 이 변환은 다항 시간 내에 수행 가능한 알고리즘이 존재하나, 최악의 경우 오토마톤의 상태 수가 LTL 공식의 크기에 대하여 지수적으로 증가할 수 있다 (Baier & Katoen, 2008).

|\mathcal{A}_\varphi| = O(2^{|\varphi|})

단계 3: 곱 오토마톤 구성

전이 시스템 \mathcal{TS}와 뷔히 오토마톤 \mathcal{A}_\varphi의 곱(Product)을 구성하여 곱 오토마톤 \mathcal{P}를 생성한다.

\mathcal{P} = \mathcal{TS} \otimes \mathcal{A}_\varphi

곱 오토마톤의 상태는 (q, q_A) \in Q \times Q_A의 쌍으로 구성되며, 전이 규칙은 양 오토마톤의 전이가 동기적으로 일어나는 것으로 정의된다.

((q, q_A), (q', q_A')) \in \delta_\mathcal{P} \iff (q, q') \in \delta \text{ and } q_A' \in \delta_A(q_A, L(q'))

단계 4: 수용 경로 탐색

곱 오토마톤 \mathcal{P}에서 수용 조건(Acceptance Condition)을 만족하는 경로를 탐색한다. 뷔히 수용 조건의 경우, 수용 상태 집합 F_A에 속하는 상태를 무한히 자주 방문하는 경로를 찾아야 한다. 이는 중첩 깊이 우선 탐색(Nested Depth-First Search) 알고리즘을 통하여 효율적으로 수행할 수 있다.

수용 경로가 존재하면, 이 경로의 \mathcal{TS} 구성 요소 투영(Projection)이 임무 사양을 만족하는 로봇의 행동 순서가 된다.

단계 5: 경로의 접두사-접미사 분해

무한 길이의 수용 경로는 일반적으로 접두사(Prefix) \rho_{\text{pre}}와 주기적으로 반복되는 접미사(Suffix) \rho_{\text{suf}}로 분해된다.

\rho = \rho_{\text{pre}} \cdot (\rho_{\text{suf}})^\omega

접두사는 한 번만 실행되고, 접미사는 무한히 반복 실행되며, 이를 통하여 무한 지평 임무의 유한한 구현이 가능해진다.

6. LTL 기반 임무 명세의 장점과 한계

6.1 장점

• 형식적 정확성(Formal Correctness): 임무 사양의 모호성을 완전히 제거하고, 생성된 계획의 정확성을 수학적으로 보장할 수 있다.
• 자동화된 합성: LTL 사양으로부터 제어 전략을 자동으로 합성할 수 있어 수작업 설계의 오류를 방지한다.
• 모듈적 사양 구성: 복잡한 임무를 단순한 LTL 공식의 논리적 결합으로 구성할 수 있다.
• 검증 가능성: 모델 검사 도구를 활용하여 시스템이 사양을 만족하는지 자동으로 검증할 수 있다.

6.2 한계

• 상태 폭발 문제(State Explosion Problem): 곱 오토마톤의 크기가 전이 시스템과 오토마톤의 크기에 곱으로 비례하여 증가하므로, 대규모 환경에서 계산 가능성(Tractability)이 제한된다.
• 정량적 표현의 제약: 기본 LTL은 “10초 이내에 도달하라“와 같은 정량적 시간 제약을 직접 표현할 수 없다.
• 전문 지식 요구: LTL 사양의 작성에는 형식 논리에 대한 전문 지식이 필요하며, 비전문가의 접근성이 낮다.
• 결정론적 환경 가정: 기본적인 LTL 기반 계획은 결정론적 전이 시스템을 가정하며, 확률적 환경에의 적용에는 추가적인 확장이 필요하다.

7. LTL의 확장

기본 LTL의 한계를 극복하기 위한 다양한 확장이 연구되고 있다.

가중 LTL(Weighted LTL): 전이에 비용(Cost)을 부여하여 최소 비용 경로를 탐색한다.

확률적 LTL 계획: MDP 위에서 LTL 사양을 만족하는 최적 정책을 탐색한다.

\max_\pi \Pr_\pi(\sigma \models \varphi)

여기서 \Pr_\pi는 정책 \pi 하에서의 확률 측도(Probability Measure)이다 (Ding et al., 2014).

공동 LTL(co-safe LTL): 유한 접두사(Finite Prefix)에 의하여 만족이 결정되는 LTL의 부분 집합으로, 유한 지평 임무에 적합하다.

\text{co-safe LTL}: \quad \varphi \text{는 유한 단어에 의하여 만족 가능}

8. 참고 문헌

• Pnueli, A. (1977). The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 46-57.
• Kress-Gazit, H., Fainekos, G. E., & Pappas, G. J. (2009). Temporal-logic-based reactive mission and motion planning. IEEE Transactions on Robotics, 25(6), 1370-1381.
• Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking. MIT Press.
• Belta, C., Yordanov, B., & Gol, E. A. (2017). Formal Methods for Discrete-Time Dynamical Systems. Springer.
• Ding, X., Smith, S. L., Belta, C., & Rus, D. (2014). Optimal control of Markov decision processes with linear temporal logic constraints. IEEE Transactions on Automatic Control, 59(5), 1244-1257.

버전: 2026-03-24 v1.0