397.12 신호 시제 논리(STL) 기반 연속 시간 임무 정의

1. 신호 시제 논리의 개요

신호 시제 논리(Signal Temporal Logic, STL)는 연속 시간(continuous time) 및 실수값 신호(real-valued signal) 위에서 시간적 성질을 명세하기 위하여 개발된 형식 논리 체계이다. Maler와 Nickovic이 2004년에 제안한 STL은 선형 시제 논리(LTL)의 이산 시간 기반 구조를 연속 시간 영역으로 확장하고, 원자 명제를 실수값 술어(real-valued predicate)로 대체함으로써, 물리적 시스템의 동적 행동을 직접 명세할 수 있는 표현력을 제공한다 (Maler & Nickovic, 2004).

자율 로봇 시스템의 임무는 위치, 속도, 가속도, 센서 판독값 등 연속적인 물리량에 의하여 특성화되는 경우가 대부분이다. LTL이나 CTL과 같은 이산 시간 논리에서는 이러한 연속적 물리량을 직접 다루기 어려우며, 유한 상태 추상화(finite-state abstraction)를 통한 이산화 과정이 필요하다. STL은 이러한 추상화 과정 없이 연속 신호에 대한 시간적 성질을 직접 명세할 수 있어, 사이버-물리 시스템(Cyber-Physical System, CPS)의 설계와 검증에 핵심적 도구로 활용되고 있다.

2. STL의 구문론

STL의 구문(syntax)은 연속 시간 신호 \mathbf{x} : \mathbb{R}_{\geq 0} \rightarrow \mathbb{R}^n 위에서 정의되며, 원자 술어(atomic predicate)로서 실수값 함수에 대한 부등식을 사용한다.

2.1 원자 술어

STL의 원자 술어 \mu는 다음과 같이 정의된다:

\mu ::= f(\mathbf{x}) > 0

여기서 f : \mathbb{R}^n \rightarrow \mathbb{R}는 신호 \mathbf{x}의 값에 대한 실수값 함수이다. 예를 들어, 로봇의 위치 \mathbf{x}(t) = (x_1(t), x_2(t))가 특정 영역 내에 있는 조건은 다음의 원자 술어로 표현된다:

\mu_{\text{region}} := r^2 - (x_1 - c_1)^2 - (x_2 - c_2)^2 > 0

이 술어는 시각 t에서 로봇의 위치가 중심 (c_1, c_2), 반지름 r인 원형 영역 내에 있을 때 참이 된다.

2.2 공식의 귀납적 정의

STL 공식 \varphi는 다음의 귀납적 규칙에 의하여 정의된다:

\varphi ::= \mu \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \varphi_1 \vee \varphi_2 \mid \mathbf{F}_{[a,b]}\, \varphi \mid \mathbf{G}_{[a,b]}\, \varphi \mid \varphi_1 \, \mathbf{U}_{[a,b]}\, \varphi_2

여기서 [a, b]는 시간 구간(time interval)으로 a, b \in \mathbb{R}_{\geq 0}이고 a \leq b이다. 각 시간 연산자의 의미는 다음과 같다:

시간 구간을 명시하지 않은 경우, [0, \infty)로 해석된다.

3. STL의 의미론

STL 공식의 부울론적 의미론(Boolean semantics)은 연속 시간 신호 \mathbf{x}와 시각 t에 대하여 만족 관계 (\mathbf{x}, t) \models \varphi를 다음과 같이 귀납적으로 정의한다:

\begin{aligned} &(\mathbf{x}, t) \models \mu &&\iff f(\mathbf{x}(t)) > 0 \\ &(\mathbf{x}, t) \models \neg \varphi &&\iff (\mathbf{x}, t) \not\models \varphi \\ &(\mathbf{x}, t) \models \varphi_1 \wedge \varphi_2 &&\iff (\mathbf{x}, t) \models \varphi_1 \text{ 이고 } (\mathbf{x}, t) \models \varphi_2 \\ &(\mathbf{x}, t) \models \mathbf{F}_{[a,b]}\, \varphi &&\iff \exists t' \in [t+a,\, t+b], \; (\mathbf{x}, t') \models \varphi \\ &(\mathbf{x}, t) \models \mathbf{G}_{[a,b]}\, \varphi &&\iff \forall t' \in [t+a,\, t+b], \; (\mathbf{x}, t') \models \varphi \\ &(\mathbf{x}, t) \models \varphi_1 \, \mathbf{U}_{[a,b]}\, \varphi_2 &&\iff \exists t' \in [t+a,\, t+b], \; (\mathbf{x}, t') \models \varphi_2 \;\wedge \\ & && \quad\; \forall t'' \in [t, t'], \; (\mathbf{x}, t'') \models \varphi_1 \end{aligned}

이러한 의미론은 LTL의 이산 시간 의미론을 연속 시간 영역으로 자연스럽게 확장한 것이며, 시간 구간의 명시적 지정을 통하여 정량적 시간 제약을 형식적으로 포착한다.

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

STL은 연속 시간 신호에 대한 시간적 성질을 직접 명세할 수 있으므로, 자율 로봇 시스템의 다양한 임무 요구사항을 풍부하게 표현할 수 있다.

4.1 영역 도달 임무

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

\varphi_{\text{reach}} = \mathbf{F}_{[0, T]}\, (\lVert \mathbf{x}(t) - \mathbf{x}_{\text{goal}} \rVert < \epsilon)

여기서 \mathbf{x}_{\text{goal}}은 목표 위치, \epsilon은 허용 오차(tolerance)이다. 원자 술어 형식으로 변환하면 f(\mathbf{x}) = \epsilon - \lVert \mathbf{x} - \mathbf{x}_{\text{goal}} \rVert > 0이 된다.

4.2 장애물 회피 임무

로봇이 임무 수행 중 장애물 영역을 회피해야 하는 안전성 제약은 다음과 같이 명세된다:

\varphi_{\text{avoid}} = \mathbf{G}_{[0, T]}\, (\lVert \mathbf{x}(t) - \mathbf{x}_{\text{obs}} \rVert > d_{\text{safe}})

여기서 \mathbf{x}_{\text{obs}}는 장애물의 위치, d_{\text{safe}}는 안전 거리이다. 이 공식은 시간 구간 [0, T] 동안 로봇이 장애물로부터 항상 안전 거리 이상을 유지해야 함을 보장한다.

4.3 순차적 방문 임무

로봇이 여러 영역을 순차적으로 방문해야 하는 임무는 Until 연산자를 활용하여 명세할 수 있다:

\varphi_{\text{seq}} = \mathbf{F}_{[0, T_1]}\, \left( \textit{region}_A \wedge \mathbf{F}_{[0, T_2]}\, \textit{region}_B \right)

이 공식은 T_1 시간 이내에 영역 A에 도달하고, 그 이후 T_2 시간 이내에 영역 B에 도달해야 함을 명세한다.

4.4 속도 제한 임무

로봇의 속도가 특정 범위 이내로 유지되어야 하는 제약은 다음과 같이 명세된다:

\varphi_{\text{speed}} = \mathbf{G}_{[0, T]}\, (\lVert \dot{\mathbf{x}}(t) \rVert \leq v_{\max})

이는 STL이 위치뿐만 아니라 속도, 가속도 등 임의의 연속 신호에 대한 제약을 직접 명세할 수 있음을 보여준다.

4.5 복합 임무 명세

실제 자율 로봇 임무는 복수의 요구사항을 동시에 충족해야 하므로, 개별 명세를 논리적 결합(conjunction)으로 합성한다:

\varphi_{\text{mission}} = \varphi_{\text{reach}} \wedge \varphi_{\text{avoid}} \wedge \varphi_{\text{speed}}

이러한 합성 구조는 STL의 구성적(compositional) 특성을 반영하며, 복잡한 임무를 모듈적으로 설계하고 검증하는 데 유리하다.

5. STL 기반 임무 모니터링

STL의 중요한 실무적 장점 중 하나는 실시간 모니터링(online monitoring)에 대한 적합성이다. 주어진 STL 공식 \varphi와 실시간으로 수집되는 신호 \mathbf{x}(t)에 대하여, 공식의 만족 여부를 실시간으로 판정할 수 있다.

5.1 오프라인 모니터링

오프라인 모니터링(offline monitoring)에서는 완전한 신호 궤적(signal trace)이 주어진 상태에서, STL 공식의 만족 여부를 사후적으로 검증한다. 이는 시뮬레이션 결과의 분석이나 비행 기록(flight log)의 사후 검증에 활용된다.

오프라인 모니터링 알고리즘의 시간 복잡도는 O(\lvert \varphi \rvert \cdot N)이며, 여기서 \lvert \varphi \rvert는 공식의 크기, N은 신호 샘플 수이다 (Donzé, 2010).

5.2 온라인 모니터링

온라인 모니터링(online monitoring)에서는 신호가 실시간으로 생성되는 과정 중에 STL 공식의 만족 여부를 점진적으로 판정한다. Deshmukh 등(2017)은 효율적인 온라인 모니터링 알고리즘을 제안하였으며, 이는 자율 로봇 시스템의 실시간 임무 감시에 직접 적용 가능하다.

온라인 모니터링의 핵심적 과제는 미래 신호 값이 아직 관측되지 않은 시점에서 공식의 만족 여부를 조기에 판정하는 것이다. 이를 위하여 삼치 논리(three-valued logic)가 도입되며, 각 시점에서 공식의 판정 결과를 다음 세 가지로 분류한다:

• 참(True): 미래 신호에 무관하게 공식이 만족됨
• 거짓(False): 미래 신호에 무관하게 공식이 위반됨
• 미결정(Inconclusive): 미래 신호에 따라 판정이 달라질 수 있음

6. STL과 제어 합성의 연결

STL 기반 임무 명세는 제어 합성(control synthesis)과 밀접하게 연결된다. STL 공식으로 명세된 임무를 만족하는 제어 입력(control input)을 자동으로 생성하는 문제는 활발히 연구되고 있는 분야이다.

6.1 혼합 정수 프로그래밍 기반 합성

Raman 등(2014)은 STL 공식의 만족 조건을 혼합 정수 선형 프로그래밍(Mixed Integer Linear Programming, MILP)의 제약 조건으로 인코딩하는 기법을 제안하였다. 이 접근법에서는 STL 공식의 부울 구조를 이진 변수(binary variable)로 변환하고, 시간적 성질을 시간 인덱스에 대한 선형 제약으로 인코딩한다.

\begin{aligned} &\min_{\mathbf{u}} \quad J(\mathbf{x}, \mathbf{u}) \\ &\text{subject to} \quad \mathbf{x}_{k+1} = A\mathbf{x}_k + B\mathbf{u}_k \\ &\phantom{\text{subject to} \quad} (\mathbf{x}, 0) \models \varphi \end{aligned}

이 최적화 문제에서 J는 비용 함수, \mathbf{u}는 제어 입력 시퀀스, \varphi는 STL 임무 명세이다. MILP 솔버를 통하여 이 문제를 풀면, 임무 명세를 만족하는 최적 제어 입력을 동시에 획득할 수 있다.

6.2 경사 기반 최적화

Pant 등(2017)은 STL의 강건성 의미론(robustness semantics)이 미분 가능하다는 성질을 활용하여, 경사 기반 최적화(gradient-based optimization)를 통한 제어 합성을 제안하였다. 이 접근법은 MILP에 비하여 계산 효율이 높으며, 고차원 시스템에 대한 확장이 용이한 장점을 가진다.

6.3 강화 학습과의 결합

최근에는 STL 공식을 보상 함수(reward function)로 변환하여 강화 학습(reinforcement learning)에 활용하는 연구가 진행되고 있다 (Aksaray et al., 2016). STL의 강건성 값(robustness value)을 보상 신호로 사용함으로써, 에이전트가 STL 명세를 만족하는 정책을 학습하도록 유도할 수 있다.

7. STL의 이산 시간 논리와의 비교

STL은 연속 시간 및 실수값 신호를 직접 다룰 수 있으므로, 자율 로봇 시스템의 물리적 역학을 포함한 임무 명세에 가장 적합한 형식 논리 체계 중 하나로 평가된다. 특히, 시간 구간의 명시적 지정과 강건성 의미론의 제공은 실제 로봇 시스템의 임무 설계, 검증, 및 최적화에 필수적인 기능을 제공한다.

8. 참고문헌

• Aksaray, D., Jones, A., Kong, Z., Schwager, M., & Belta, C. (2016). “Q-Learning for Robust Satisfaction of Signal Temporal Logic Specifications.” In Proceedings of the 55th IEEE Conference on Decision and Control (CDC), 6565–6570.
• Deshmukh, J. V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., & Seshia, S. A. (2017). “Robust Online Monitoring of Signal Temporal Logic.” Formal Methods in System Design, 51(1), 5–30.
• Donzé, A. (2010). “Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems.” In International Conference on Computer Aided Verification (CAV), LNCS 6174, Springer, 167–170.
• Maler, O., & Nickovic, D. (2004). “Monitoring Temporal Properties of Continuous Signals.” In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, LNCS 3253, Springer, 152–166.
• Pant, Y. V., Abbas, H., & Mangharam, R. (2017). “Smooth Operator: Control Using the Smooth Robustness of Temporal Logic.” In Proceedings of the IEEE Conference on Control Technology and Applications (CCTA), 1235–1240.
• Raman, V., Donzé, A., Maasoumy, M., Murray, R. M., Sangiovanni-Vincentelli, A., & Seshia, S. A. (2014). “Model Predictive Control with Signal Temporal Logic Specifications.” In Proceedings of the 53rd IEEE Conference on Decision and Control (CDC), 81–87.