397.14 메트릭 시제 논리(MTL) 기반 시간 제약 임무 명세

1. 메트릭 시제 논리의 개요

메트릭 시제 논리(Metric Temporal Logic, MTL)는 Koymans(1990)가 제안한 형식 논리 체계로서, 선형 시제 논리(LTL)의 시간 연산자에 정량적 시간 제약(quantitative time constraint)을 부가하여 실시간 시간 성질을 명세할 수 있도록 확장한 것이다. LTL의 시간 연산자는 “언젠가(eventually)” 또는 “항상(always)“과 같이 정성적 시간 관계만을 표현하지만, MTL은 “5초 이내에” 또는 “10초에서 20초 사이에“와 같은 정밀한 시간 경계(time bound)를 공식에 직접 포함할 수 있다 (Koymans, 1990).

자율 로봇 시스템의 임무는 실시간 시간 제약과 불가분의 관계에 있다. 물류 로봇의 배송 시한, 드론의 귀환 제한 시간, 수색 및 구조 로봇의 탐색 시간 제한 등은 모두 정량적 시간 경계를 수반하는 임무 요구사항이다. MTL은 이러한 시간 제약을 형식적으로 표현하고 검증할 수 있는 논리적 기반을 제공한다.

2. MTL의 구문론

MTL의 구문(syntax)은 원자 명제 집합 AP 위에서 다음의 귀납적 규칙에 의하여 정의된다:

\varphi ::= p \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \varphi_1 \vee \varphi_2 \mid \mathbf{X}\, \varphi \mid \varphi_1 \, \mathbf{U}_I \, \varphi_2

여기서 p \in AP는 원자 명제이고, I는 시간 구간(time interval)이다. 시간 구간 I는 다음의 형태 중 하나를 취한다:

I \in \{[a, b], \; (a, b], \; [a, b), \; (a, b), \; [a, \infty), \; (a, \infty)\}

여기서 a, b \in \mathbb{Q}_{\geq 0} (비음의 유리수)이고, a \leq b이다.

파생 연산자(derived operator)는 Until 연산자로부터 다음과 같이 정의된다:

\begin{aligned} \mathbf{F}_I\, \varphi &\equiv \top \, \mathbf{U}_I \, \varphi \quad (\text{Eventually within } I) \\ \mathbf{G}_I\, \varphi &\equiv \neg \mathbf{F}_I\, \neg \varphi \quad (\text{Globally within } I) \end{aligned}

시간 구간 I가 지정되지 않은 경우, I = [0, \infty)로 해석되며, 이는 표준 LTL 연산자와 동일한 의미를 가진다.

3. MTL의 의미론

MTL의 의미론은 연속 시간 모델과 이산 시간 모델의 두 가지 해석 체계에 따라 구분된다.

3.1 연속 시간 모델(Pointwise Semantics)

연속 시간 신호(continuous-time signal) \sigma : \mathbb{R}_{\geq 0} \rightarrow 2^{AP}에 대한 점별 의미론(pointwise semantics)에서, 시각 t \geq 0에서의 만족 관계 (\sigma, t) \models \varphi는 다음과 같이 귀납적으로 정의된다:

\begin{aligned} &(\sigma, t) \models p &&\iff p \in \sigma(t) \\ &(\sigma, t) \models \neg \varphi &&\iff (\sigma, t) \not\models \varphi \\ &(\sigma, t) \models \varphi_1 \wedge \varphi_2 &&\iff (\sigma, t) \models \varphi_1 \text{ 이고 } (\sigma, t) \models \varphi_2 \\ &(\sigma, t) \models \mathbf{X}\, \varphi &&\iff (\sigma, t') \models \varphi \text{, 여기서 } t' \text{은 } t \text{ 이후의 다음 이벤트 시각} \\ &(\sigma, t) \models \varphi_1 \, \mathbf{U}_I \, \varphi_2 &&\iff \exists t' \in (t + I), \; (\sigma, t') \models \varphi_2 \;\wedge \\ & && \quad\; \forall t'' \in [t, t'), \; (\sigma, t'') \models \varphi_1 \end{aligned}

여기서 t + I = \{t + \delta \mid \delta \in I\}이다.

3.2 연속 시간 모델(Continuous Semantics)

Alur와 Henzinger(1993)는 구간 의미론(interval-based semantics)을 제안하여, MTL 공식의 만족을 시간 구간의 집합에 대하여 정의하였다. 이 해석은 실시간 시스템의 검증에서 보다 풍부한 추론을 가능하게 한다.

4. MTL 기반 시간 제약 임무 명세의 사례

4.1 제한 시간 내 도달 임무

로봇이 T 시간 단위 이내에 목표 지점에 도달해야 하는 임무는 다음과 같이 명세된다:

\mathbf{F}_{[0, T]}\, \textit{target\_reached}

이 공식은 시각 0부터 T 사이의 어떤 시점에서 \textit{target\_reached}가 참이 되어야 함을 표현한다. LTL의 단순 \mathbf{F}\, \textit{target\_reached}는 시간 제한 없이 “언젠가” 도달하면 됨을 의미하므로, MTL은 보다 정밀한 시간 요구사항을 명세할 수 있다.

4.2 지연 응답 임무

특정 사건 발생 후 일정 시간 이내에 응답해야 하는 임무는 다음과 같이 명세된다:

\mathbf{G}\, (\textit{event\_detected} \rightarrow \mathbf{F}_{[0, \Delta t]}\, \textit{response\_initiated})

이 공식은 “항상, 사건이 탐지되면 \Delta t 시간 단위 이내에 응답이 개시되어야 한다“는 요구사항을 형식화한다. 이는 실시간 시스템에서의 응답 시간(response time) 보장에 핵심적인 명세 패턴이다.

4.3 최소 체류 시간 임무

로봇이 특정 구역에 최소 시간 동안 체류해야 하는 임무는 다음과 같이 명세된다:

\mathbf{G}\, (\textit{enter\_region} \rightarrow \mathbf{G}_{[0, T_{\min}]}\, \textit{in\_region})

이 공식은 “구역에 진입하면, 진입 시점부터 적어도 T_{\min} 시간 동안 해당 구역에 머물러야 한다“는 요구사항을 표현한다. 이는 감시, 정찰, 데이터 수집 등의 임무에서 센서 데이터의 충분한 확보를 위한 요구사항에 해당한다.

4.4 주기적 방문 임무

로봇이 특정 구역을 일정 주기 이내로 반복 방문해야 하는 임무는 다음과 같이 명세된다:

\mathbf{G}\, \mathbf{F}_{[0, P]}\, \textit{region\_visited}

이 공식은 “모든 시점에서, P 시간 단위 이내에 해당 구역을 방문한다“는 요구사항을 나타내며, 순찰(patrol) 임무의 주기적 방문 제약을 형식화한다.

4.5 순서 제약이 포함된 복합 임무

복수의 작업을 특정 시간 간격을 두고 순차적으로 수행해야 하는 임무는 다음과 같이 명세된다:

\mathbf{F}_{[0, T_1]}\, \left( \textit{task\_A\_done} \wedge \mathbf{F}_{[T_2, T_3]}\, \textit{task\_B\_done} \right)

이 공식은 “T_1 시간 이내에 작업 A를 완료하고, 작업 A 완료 후 T_2에서 T_3 시간 사이에 작업 B를 완료해야 한다“는 복합적 시간 제약을 포함한 임무를 명세한다.

5. MTL의 만족가능성과 모델 검사

5.1 결정가능성과 복잡도

MTL의 만족가능성(satisfiability) 문제와 모델 검사(model checking) 문제의 결정가능성 및 복잡도는 해석 의미론에 따라 상이하다.

Alur와 Henzinger(1993)는 연속 의미론 하에서의 MTL 만족가능성이 결정 불가능(undecidable)임을 증명하였다. 이는 MTL의 표현력이 매우 강력함을 의미하는 동시에, 자동 검증의 한계를 시사한다.

5.2 제한된 MTL 부분 논리

결정 불가능성 문제를 우회하기 위하여, MTL의 표현력을 제한한 부분 논리(fragment)들이 연구되었다.

MITL(Metric Interval Temporal Logic): Alur, Feder, 그리고 Henzinger(1996)가 제안한 MITL은 MTL에서 점 구간(punctual interval), 즉 [a, a] 형태의 구간을 금지한 부분 논리이다. MITL의 만족가능성은 EXPSPACE-complete이며, 모델 검사는 결정 가능하다. MITL은 “정확히 5초 후“와 같은 점 시간 제약은 표현할 수 없으나, “5초에서 10초 사이“와 같은 구간 제약은 표현 가능하다.

\varphi_{\text{MITL}} ::= p \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \varphi_1 \, \mathbf{U}_I \, \varphi_2 \quad (I \text{는 비축퇴 구간})

Safety-MTL: Ouaknine과 Worrell(2006)이 연구한 Safety-MTL은 MTL에서 안전성 성질만을 표현하는 부분 논리로서, 유한 시간 지평(bounded time horizon) 내에서의 모델 검사가 결정 가능하다.

6. 시간 자동자와 MTL의 연결

MTL 명세는 시간 자동자(timed automata)와 밀접한 관계를 가진다. Alur와 Dill(1994)이 제안한 시간 자동자는 유한 상태 자동자에 실수값 시계 변수(clock variable)를 추가한 모델로서, MTL 공식의 의미론적 기반을 제공한다.

6.1 시간 자동자의 구조

시간 자동자 \mathcal{A} = (L, L_0, C, \Sigma, E, F)는 다음의 구성 요소로 정의된다:

• L: 유한 위치(location) 집합
• L_0 \subseteq L: 초기 위치 집합
• C: 유한 시계 변수(clock variable) 집합
• \Sigma: 입력 알파벳
• E \subseteq L \times \Sigma \times \mathcal{G}(C) \times 2^C \times L: 에지(edge) 집합
• F \subseteq L: 수용 위치(accepting location) 집합

여기서 \mathcal{G}(C)는 시계 제약(clock constraint)의 집합이다. 시계 변수는 시간의 경과와 함께 동일한 속도로 증가하며, 전이(transition) 시에 선택적으로 0으로 리셋될 수 있다.

6.2 MTL에서 시간 자동자로의 변환

MTL 공식을 시간 자동자로 변환하는 절차는 다음의 단계를 따른다:

1. MTL 공식을 부정 정규형(Negation Normal Form, NNF)으로 변환한다.
2. 각 부분 공식에 대응하는 시계 변수를 도입한다.
3. 시간 연산자의 구간 제약을 시계 제약으로 인코딩한다.
4. 부분 공식 간의 논리적 관계를 위치 전이로 표현한다.

이 변환은 일반적으로 공식 크기에 대하여 지수적 확장을 수반하나, MITL의 경우 2중 지수(doubly exponential)보다 효율적인 변환이 가능하다 (Alur, Feder, & Henzinger, 1996).

7. MTL의 로봇 임무 계획에의 적용

7.1 시간 제약 경로 계획

MTL 명세를 만족하는 로봇 경로를 생성하는 문제는, MTL 공식에서 시간 자동자를 구성하고, 이를 로봇의 전이 시스템(transition system)과 동기적 곱(synchronous product)하여 제품 자동자(product automaton)를 생성한 후, 이 제품 자동자 위에서 수용 경로(accepting path)를 탐색하는 절차로 해결된다.

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

1. 환경을 전이 시스템 \mathcal{T} = (S, s_0, \delta, AP, L)으로 모델링한다.
2. MTL 명세 \varphi를 시간 자동자 \mathcal{A}_\varphi로 변환한다.
3. 제품 자동자 \mathcal{P} = \mathcal{T} \otimes \mathcal{A}_\varphi를 구성한다.
4. \mathcal{P} 위에서 수용 조건을 만족하는 경로를 탐색한다.

시간 자동자의 시계 변수로 인하여, 제품 자동자의 상태 공간은 연속적(continuous)이 되므로, 영역 그래프(region graph)나 구역 그래프(zone graph)를 통한 유한화(finiteization)가 필요하다.

7.2 실시간 임무 모니터링

MTL 공식에 대한 실시간 모니터링은 시간 이벤트의 발생과 시계 변수의 진행을 추적하면서 공식의 만족 여부를 점진적으로 판정하는 과정이다. Thati와 Rosu(2005)는 유한 추적(finite trace)에 대한 MTL 모니터링 알고리즘을 제안하였다.

8. MTL과 관련 시간 논리의 비교

MTL은 LTL의 자연스러운 정량적 확장으로서, 시간 경계를 명시적으로 포함한 임무 명세를 가능하게 한다. 그러나 완전한 MTL의 결정 불가능성으로 인하여, 실질적 응용에서는 MITL과 같은 결정 가능한 부분 논리가 선호되는 경우가 많다. STL과의 차이점은, STL이 실수값 신호에 대한 술어와 강건성 의미론을 지원하는 반면, MTL은 부울 원자 명제에 기반한다는 점이다.

9. 참고문헌

• Alur, R., & Dill, D. L. (1994). “A Theory of Timed Automata.” Theoretical Computer Science, 126(2), 183–235.
• Alur, R., Feder, T., & Henzinger, T. A. (1996). “The Benefits of Relaxing Punctuality.” Journal of the ACM, 43(1), 116–146.
• Alur, R., & Henzinger, T. A. (1993). “Real-Time Logics: Complexity and Expressiveness.” Information and Computation, 104(1), 35–77.
• Koymans, R. (1990). “Specifying Real-Time Properties with Metric Temporal Logic.” Real-Time Systems, 2(4), 255–299.
• Ouaknine, J., & Worrell, J. (2006). “On the Decidability of Metric Temporal Logic.” In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS), 188–197.
• Thati, P., & Rosu, G. (2005). “Monitoring Algorithms for Metric Temporal Logic Specifications.” Electronic Notes in Theoretical Computer Science, 113, 145–162.