397.9 LTL 기반 임무 명세 사례 분석
1. 개요
이 절에서는 선형 시제 논리(LTL)를 활용한 로봇 임무 명세의 구체적 사례를 분석한다. 각 사례는 실제 로봇 공학 응용 분야에서 발생하는 전형적 임무 시나리오를 대상으로 하며, 자연어 임무 기술로부터 형식적 LTL 사양으로의 변환 과정, 전이 시스템의 구성, 곱 오토마톤 기반 경로 탐색까지의 전 과정을 상세히 기술한다.
2. 사례 1: UAV 순찰 및 정찰 임무
2.1 시나리오 설명
무인 항공기(UAV)가 네 개의 관심 영역 R_1, R_2, R_3, R_4를 순찰하는 임무를 수행한다. 구체적인 요구 사항은 다음과 같다.
- 금지 구역 R_{\text{no}}에 진입하지 않을 것
- 네 개의 관심 영역을 모두 방문할 것
- 영역 R_1과 R_3을 무한히 반복 방문하여 지속적 감시를 수행할 것
- 영역 R_2를 방문하기 전에 반드시 R_1을 먼저 방문할 것
2.2 원자 명제 정의
\mathcal{AP} = \{r_1, r_2, r_3, r_4, r_{\text{no}}\}
각 원자 명제 r_i는 UAV가 영역 R_i에 위치함을 나타낸다.
2.3 LTL 사양 구성
각 요구 사항에 대응하는 LTL 공식은 다음과 같다.
안전 제약 (금지 구역 회피):
\varphi_1 = \square \neg r_{\text{no}}
모든 영역 방문 (도달성):
\varphi_2 = \lozenge r_1 \wedge \lozenge r_2 \wedge \lozenge r_3 \wedge \lozenge r_4
지속적 감시 (반복 방문):
\varphi_3 = \square \lozenge r_1 \wedge \square \lozenge r_3
순서 제약 (방문 순서):
\varphi_4 = \neg r_2 \mathcal{U} r_1
전체 임무 사양:
\varphi = \varphi_1 \wedge \varphi_2 \wedge \varphi_3 \wedge \varphi_4
2.4 전이 시스템 구성
UAV의 작업 공간을 6개 영역으로 분할한 전이 시스템 \mathcal{TS}를 구성한다.
Q = \{q_1, q_2, q_3, q_4, q_5, q_{\text{no}}\}
각 상태의 라벨링:
| 상태 | 라벨링 L(q) | 의미 |
|---|---|---|
| q_1 | \{r_1\} | 영역 R_1에 위치 |
| q_2 | \{r_2\} | 영역 R_2에 위치 |
| q_3 | \{r_3\} | 영역 R_3에 위치 |
| q_4 | \{r_4\} | 영역 R_4에 위치 |
| q_5 | \emptyset | 중간 이동 영역 |
| q_{\text{no}} | \{r_{\text{no}}\} | 금지 구역 |
전이 관계 \delta는 인접 영역 간의 이동 가능성에 따라 정의된다.
2.5 풀이 과정
- LTL 공식 \varphi를 뷔히 오토마톤 \mathcal{A}_\varphi로 변환한다.
- 전이 시스템 \mathcal{TS}와 \mathcal{A}_\varphi의 곱 오토마톤 \mathcal{P} = \mathcal{TS} \otimes \mathcal{A}_\varphi를 구성한다.
- 곱 오토마톤에서 수용 조건을 만족하는 경로를 탐색한다.
- 경로를 접두사-접미사(Prefix-Suffix) 형태로 분해한다.
결과적으로 도출되는 경로의 예시:
\rho = \underbrace{q_5, q_1, q_5, q_4, q_5, q_2}_{\text{접두사}} \cdot \underbrace{(q_5, q_1, q_5, q_3)^\omega}_{\text{접미사}}
이 경로는 먼저 R_1을 방문하고(\varphi_4 만족), 모든 영역을 방문하며(\varphi_2 만족), 이후 R_1과 R_3를 무한히 반복 방문하고(\varphi_3 만족), 금지 구역을 결코 통과하지 않는다(\varphi_1 만족).
3. 사례 2: 물류 로봇의 다중 화물 배송 임무
3.1 시나리오 설명
물류 로봇이 창고 환경에서 다중 화물 배송 임무를 수행한다. 환경은 적재 구역(Loading Zone, L), 배송 구역 A/B (D_A, D_B), 충전 구역(Charging Zone, C)으로 구성된다.
- 충전 구역을 제외한 모든 영역에서는 배터리 잔량이 임계값 이상이어야 한다
- 적재 구역에서 화물을 적재한 후 배송 구역으로 이동하여야 한다
- 배송 구역 A를 배송 구역 B보다 먼저 방문하여야 한다
- 모든 배송이 완료되면 기지(Home, H)로 복귀하여야 한다
3.2 원자 명제 정의
\mathcal{AP} = \{l, d_a, d_b, c, h, \text{loaded}, \text{battery\_ok}\}
3.3 LTL 사양
배터리 안전 제약:
\varphi_1 = \square (\neg c \rightarrow \text{battery\_ok})
적재 후 배송 순서:
\varphi_2 = \neg d_a \mathcal{U} (l \wedge \text{loaded})
배송 순서 제약:
\varphi_3 = \neg d_b \mathcal{U} d_a
최종 기지 복귀:
\varphi_4 = \lozenge (d_a \wedge \lozenge (d_b \wedge \lozenge h))
전체 임무 사양:
\varphi = \varphi_1 \wedge \varphi_2 \wedge \varphi_3 \wedge \varphi_4
4. 사례 3: 수색 구조 로봇의 탐색 임무
4.1 시나리오 설명
재난 현장에서 수색 구조(Search and Rescue, SAR) 로봇이 생존자 탐색 임무를 수행한다 (Murphy, 2014). 환경은 탐색 영역 S_1, S_2, S_3, 위험 영역 D, 보고 지점 R_P로 구성된다.
- 위험 영역에 진입하지 않을 것
- 세 개의 탐색 영역을 모두 탐색할 것
- 각 탐색 영역을 방문한 후 보고 지점에서 탐색 결과를 보고할 것
- 탐색 영역 방문 순서는 S_1 \rightarrow S_2 \rightarrow S_3를 따를 것
4.2 LTL 사양
안전 제약:
\varphi_1 = \square \neg d
순차 탐색 및 보고:
\varphi_2 = \lozenge \left( s_1 \wedge \lozenge \left( r_p \wedge \lozenge \left( s_2 \wedge \lozenge \left( r_p \wedge \lozenge \left( s_3 \wedge \lozenge r_p \right) \right) \right) \right) \right)
이 공식은 S_1 \rightarrow R_P \rightarrow S_2 \rightarrow R_P \rightarrow S_3 \rightarrow R_P의 순차적 방문을 강제한다.
전체 임무 사양:
\varphi = \varphi_1 \wedge \varphi_2
5. 사례 4: 자율 주행 차량의 교차로 통과 임무
5.1 시나리오 설명
자율 주행 차량이 도심 환경에서 교차로를 통과하는 시나리오를 고려한다. 차선 L_1 (현재 차선), L_2 (좌회전 차선), L_3 (우회전 차선), 교차로 영역 I, 목적지 G가 정의된다.
- 교차로 진입 시 신호 \text{green}이 활성화되어야 한다
- 교차로에서 항상 보행자 확인 \text{ped\_clear}가 선행되어야 한다
- 결국 목적지 G에 도달하여야 한다
- 충돌 영역 C_Z에 진입하지 않을 것
5.2 LTL 사양
\varphi_1 = \square (i \rightarrow \text{green})
\varphi_2 = \square (i \rightarrow \text{ped\_clear})
\varphi_3 = \lozenge g
\varphi_4 = \square \neg c_z
\varphi = \varphi_1 \wedge \varphi_2 \wedge \varphi_3 \wedge \varphi_4
6. 사례 5: 다중 로봇 협력 탐사 임무
6.1 시나리오 설명
두 대의 로봇 \text{Robot}_1과 \text{Robot}_2가 협력하여 네 개의 탐사 지점 P_1, P_2, P_3, P_4를 분담 탐사하는 임무를 수행한다 (Kloetzer & Belta, 2010).
- 모든 탐사 지점이 적어도 한 대의 로봇에 의하여 방문되어야 한다
- 두 로봇이 동시에 같은 지점에 위치하면 안 된다 (충돌 회피)
- 각 로봇은 임무 완료 후 기지로 복귀하여야 한다
6.2 LTL 사양
로봇 i가 지점 P_j에 위치함을 나타내는 원자 명제를 p_j^i로 표기한다. 로봇 i의 기지 위치를 h^i로 표기한다.
완전 커버리지:
\varphi_1 = \bigwedge_{j=1}^{4} \lozenge \left( p_j^1 \vee p_j^2 \right)
충돌 회피:
\varphi_2 = \square \bigwedge_{j=1}^{4} \neg \left( p_j^1 \wedge p_j^2 \right)
기지 복귀:
\varphi_3 = \lozenge h^1 \wedge \lozenge h^2
전체 임무 사양:
\varphi = \varphi_1 \wedge \varphi_2 \wedge \varphi_3
다중 로봇 시스템에서의 LTL 기반 계획은 각 로봇의 전이 시스템을 곱(Product)으로 구성한 합성 시스템(Composite System) 위에서 수행되며, 이에 따라 상태 공간의 크기가 로봇 수에 지수적으로 증가하는 문제가 발생한다. 이를 완화하기 위하여 분산 합성(Distributed Synthesis)이나 점진적 합성(Incremental Synthesis) 기법이 연구되고 있다.
7. 사례 분석의 종합
위의 사례들을 통하여 LTL 기반 임무 명세의 주요 패턴을 다음과 같이 분류할 수 있다.
| 패턴 유형 | LTL 형식 | 사용 사례 |
|---|---|---|
| 안전 (Safety) | \square \neg \varphi_{\text{bad}} | 금지 구역 회피, 충돌 방지 |
| 도달 (Reachability) | \lozenge \varphi_{\text{goal}} | 목표 도달, 기지 복귀 |
| 생존 (Liveness) | \square \lozenge \varphi | 순찰, 반복 감시 |
| 순서 (Sequencing) | \neg \varphi_2 \mathcal{U} \varphi_1 | 방문 순서 제약, 전제 조건 |
| 반응 (Response) | \square (\varphi_1 \rightarrow \lozenge \varphi_2) | 이벤트 대응, 조건부 행동 |
| 공정 (Fairness) | \square \lozenge \varphi_1 \wedge \square \lozenge \varphi_2 | 균등 분배, 공정한 자원 사용 |
이러한 기본 패턴을 조합함으로써 복잡한 실세계 임무를 체계적으로 명세할 수 있으며, 자동화된 도구를 통하여 정확성이 보장된 제어 전략을 합성할 수 있다.
8. 참고 문헌
- 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.
- Murphy, R. R. (2014). Disaster Robotics. MIT Press.
- Kloetzer, M., & Belta, C. (2010). Automatic deployment of distributed teams of robots from temporal logic motion specifications. IEEE Transactions on Robotics, 26(1), 48-63.
- Belta, C., Yordanov, B., & Gol, E. A. (2017). Formal Methods for Discrete-Time Dynamical Systems. Springer.
버전: 2026-03-24 v1.0