397.13 STL의 강건성 의미론(Robustness Semantics)

1. 강건성 의미론의 동기와 개요

신호 시제 논리(STL)의 부울론적 의미론(Boolean semantics)은 주어진 신호가 STL 공식을 만족하는지 여부를 이진적(참/거짓)으로 판정한다. 그러나 이러한 이진적 판정만으로는 신호가 공식을 “얼마나 강하게” 만족하는지, 혹은 “얼마나 아슬아슬하게” 위반하는지에 관한 정량적 정보를 제공할 수 없다. Fainekos와 Pappas(2009)는 이러한 한계를 극복하기 위하여 강건성 의미론(robustness semantics)을 도입하였으며, 이는 STL 공식의 만족도를 실수값으로 정량화하는 체계이다.

강건성 의미론은 자율 로봇 시스템의 임무 명세에서 다음과 같은 핵심적 기여를 제공한다:

1. 정량적 만족도 평가: 임무 명세의 만족 정도를 연속적인 실수값으로 평가하여, 임무 수행의 품질을 정밀하게 분석할 수 있다.
2. 최적화 기반 제어 합성: 강건성 값을 목적 함수로 활용하여, STL 명세를 최대한 강건하게 만족하는 제어 입력을 최적화 기법으로 합성할 수 있다.
3. 위반 근접도 경고: 강건성 값이 0에 가까워지면 명세 위반의 위험이 임박함을 조기에 감지할 수 있다.

2. 강건성 의미론의 수학적 정의

2.1 원자 술어의 강건성

STL의 원자 술어 \mu := f(\mathbf{x}) > 0에 대하여, 신호 \mathbf{x}와 시각 t에서의 강건성(robustness degree)은 다음과 같이 정의된다:

\rho(\mu, \mathbf{x}, t) = f(\mathbf{x}(t))

이 정의에 의하면, \rho > 0일 때 원자 술어가 만족되며, \rho < 0일 때 위반된다. \rho의 절대값은 만족 혹은 위반의 정도(margin)를 나타낸다. 예를 들어, 로봇의 장애물까지의 거리에 대한 원자 술어 f(\mathbf{x}) = d(\mathbf{x}, \mathbf{x}_{\text{obs}}) - d_{\text{safe}}에서, 강건성 값 \rho = 2.5는 로봇이 안전 거리보다 2.5 단위만큼 여유 있게 떨어져 있음을 의미한다.

2.2 논리 연산자의 강건성

부정(negation), 논리곱(conjunction), 논리합(disjunction)에 대한 강건성은 다음과 같이 정의된다:

\begin{aligned} \rho(\neg \varphi, \mathbf{x}, t) &= -\rho(\varphi, \mathbf{x}, t) \\ \rho(\varphi_1 \wedge \varphi_2, \mathbf{x}, t) &= \min\left(\rho(\varphi_1, \mathbf{x}, t),\; \rho(\varphi_2, \mathbf{x}, t)\right) \\ \rho(\varphi_1 \vee \varphi_2, \mathbf{x}, t) &= \max\left(\rho(\varphi_1, \mathbf{x}, t),\; \rho(\varphi_2, \mathbf{x}, t)\right) \end{aligned}

논리곱의 강건성이 \min 연산으로 정의되는 이유는, 결합된 공식의 만족 여유가 가장 약한 부분 공식에 의하여 결정되기 때문이다. 이는 직관적으로 “사슬의 강도는 가장 약한 고리에 의하여 결정된다“는 원리에 대응한다.

2.3 시간 연산자의 강건성

시간 연산자 \mathbf{F}_{[a,b]}(Eventually), \mathbf{G}_{[a,b]}(Globally), \mathbf{U}_{[a,b]}(Until)에 대한 강건성은 다음과 같이 정의된다:

\begin{aligned} \rho(\mathbf{F}_{[a,b]}\, \varphi, \mathbf{x}, t) &= \sup_{t' \in [t+a,\, t+b]} \rho(\varphi, \mathbf{x}, t') \\ \rho(\mathbf{G}_{[a,b]}\, \varphi, \mathbf{x}, t) &= \inf_{t' \in [t+a,\, t+b]} \rho(\varphi, \mathbf{x}, t') \\ \rho(\varphi_1 \, \mathbf{U}_{[a,b]}\, \varphi_2, \mathbf{x}, t) &= \sup_{t' \in [t+a,\, t+b]} \min\left(\rho(\varphi_2, \mathbf{x}, t'),\; \inf_{t'' \in [t,\, t']} \rho(\varphi_1, \mathbf{x}, t'')\right) \end{aligned}

\mathbf{F}_{[a,b]}\, \varphi의 강건성이 \sup 연산으로 정의되는 이유는, “언젠가 만족한다“는 성질의 만족 정도가 시간 구간 내에서 가장 강하게 만족하는 시점에 의하여 결정되기 때문이다. 반대로, \mathbf{G}_{[a,b]}\, \varphi의 강건성이 \inf 연산으로 정의되는 이유는, “항상 만족한다“는 성질의 만족 정도가 가장 약하게 만족하는 시점에 의하여 결정되기 때문이다.

3. 강건성 의미론의 건전성

강건성 의미론의 핵심적 이론적 성질은 부울론적 의미론과의 일관성, 즉 건전성(soundness)이다. 다음의 정리가 성립한다 (Fainekos & Pappas, 2009):

정리 (건전성). 임의의 STL 공식 \varphi, 신호 \mathbf{x}, 시각 t에 대하여:

\rho(\varphi, \mathbf{x}, t) > 0 \implies (\mathbf{x}, t) \models \varphi

\rho(\varphi, \mathbf{x}, t) < 0 \implies (\mathbf{x}, t) \not\models \varphi

이 정리는 강건성 값의 부호가 부울론적 만족 여부와 일치함을 보장한다. 강건성 값이 정확히 0인 경우는 경계 사례(boundary case)로서, 만족과 위반의 경계에 위치한다.

4. 공간적 강건성과 시간적 강건성

강건성의 개념은 측정 기준에 따라 공간적 강건성(spatial robustness)과 시간적 강건성(temporal robustness)으로 세분화될 수 있다.

4.1 공간적 강건성

앞서 정의한 표준 강건성 \rho는 공간적 강건성에 해당한다. 이는 원자 술어의 함수값 f(\mathbf{x}(t))을 직접 사용하므로, 신호 값의 공간적 변동에 대한 여유도를 측정한다. 구체적으로, 공간적 강건성 \rho는 다음과 같은 교란 한계(perturbation bound)를 제공한다:

\rho(\varphi, \mathbf{x}, t) = \epsilon \implies \forall \mathbf{x}' \text{ s.t. } \lVert \mathbf{x} - \mathbf{x}' \rVert_\infty < \epsilon, \; (\mathbf{x}', t) \models \varphi

이는 신호 \mathbf{x}에 \epsilon 미만의 교란이 가해져도 공식의 만족이 유지됨을 보장한다.

4.2 시간적 강건성

Donzé와 Maler(2010)는 시간적 강건성(temporal robustness, \theta)의 개념을 도입하였다. 시간적 강건성은 신호의 시간 축 이동(time shift)에 대한 공식 만족의 여유도를 측정한다:

\theta(\varphi, \mathbf{x}, t) = \sup \{\delta \geq 0 \mid \forall \lvert \Delta t \rvert < \delta, \; (\mathbf{x}, t + \Delta t) \models \varphi\}

시간적 강건성은 센서 지연(sensor delay), 통신 지연(communication latency), 타이밍 불확실성 등이 존재하는 실제 로봇 시스템에서, 시간적 교란에 대한 임무 만족의 안정성을 평가하는 데 유용하다.

5. 강건성 값의 계산

5.1 이산 시간 근사

실제 응용에서 연속 시간 신호는 이산 시간 샘플(discrete-time sample)로 관측되므로, 강건성 값은 이산 시간 근사를 통하여 계산된다. 신호 \mathbf{x}가 시각 t_0, t_1, \ldots, t_N에서 샘플링된 경우, \sup 및 \inf 연산은 유한 집합에 대한 \max 및 \min 연산으로 대체된다:

\rho(\mathbf{G}_{[a,b]}\, \varphi, \mathbf{x}, t_k) \approx \min_{t_i \in [t_k + a, \, t_k + b]} \rho(\varphi, \mathbf{x}, t_i)

\rho(\mathbf{F}_{[a,b]}\, \varphi, \mathbf{x}, t_k) \approx \max_{t_i \in [t_k + a, \, t_k + b]} \rho(\varphi, \mathbf{x}, t_i)

이산 시간 근사의 정확도는 샘플링 주파수(sampling frequency)에 의존하며, 나이퀴스트 정리(Nyquist theorem)에 의한 충분한 샘플링이 보장될 경우 원래의 연속 시간 강건성에 수렴한다.

5.2 효율적 계산 알고리즘

Donzé(2013)는 O(\lvert \varphi \rvert \cdot N)의 시간 복잡도를 가지는 효율적인 강건성 계산 알고리즘을 제안하였으며, 여기서 \lvert \varphi \rvert는 공식의 크기, N은 샘플 수이다. 이 알고리즘은 슬라이딩 윈도우(sliding window) 기반의 최대/최소 연산을 활용하여, 시간 연산자가 중첩된 공식에 대해서도 선형 시간 내에 강건성 값을 계산한다.

Lemire(2006)의 스트리밍 최대/최소 알고리즘을 활용하면, 각 시간 연산자에 대한 슬라이딩 윈도우 최대/최소를 O(N)에 계산할 수 있으며, 이를 통하여 전체 알고리즘의 효율성이 보장된다.

6. 강건성 기반 최적화

6.1 목적 함수로서의 강건성

STL 강건성 값은 연속적이고 조각별 미분 가능(piecewise differentiable)하므로, 최적화 기법의 목적 함수로 직접 활용할 수 있다. 임무 명세 \varphi를 최대한 강건하게 만족하는 제어 입력 \mathbf{u}를 구하는 문제는 다음과 같이 정식화된다:

\max_{\mathbf{u}} \; \rho(\varphi, \mathbf{x}_{\mathbf{u}}, 0)

\text{subject to} \quad \mathbf{x}_{k+1} = f(\mathbf{x}_k, \mathbf{u}_k)

여기서 \mathbf{x}_{\mathbf{u}}는 제어 입력 \mathbf{u}에 의하여 생성된 시스템 궤적이다. 강건성을 최대화함으로써, 명세를 만족할 뿐만 아니라 교란에 대한 여유도를 최대한 확보하는 제어 정책을 산출할 수 있다.

6.2 매끄러운 강건성 근사

\min 및 \max 연산은 미분 불가능한 점(non-differentiable point)을 가지므로, 경사 기반 최적화를 직접 적용하기 어려운 경우가 있다. 이를 해결하기 위하여 매끄러운 근사(smooth approximation)가 도입된다 (Pant, Abbas, & Mangharam, 2017):

\widetilde{\max}(a_1, \ldots, a_n) = \frac{1}{\beta} \ln\left(\sum_{i=1}^{n} e^{\beta a_i}\right)

\widetilde{\min}(a_1, \ldots, a_n) = -\frac{1}{\beta} \ln\left(\sum_{i=1}^{n} e^{-\beta a_i}\right)

여기서 \beta > 0는 근사 정밀도 매개변수(approximation precision parameter)로서, \beta \rightarrow \infty일 때 정확한 \max/\min에 수렴한다. 이러한 매끄러운 근사를 통하여 강건성 값을 미분 가능한 함수로 변환하면, 경사 하강법(gradient descent)이나 역전파(backpropagation) 기반의 최적화를 효과적으로 적용할 수 있다.

6.3 혼합 정수 프로그래밍 인코딩

Raman 등(2014)은 STL 강건성을 혼합 정수 선형 프로그래밍(MILP)의 제약 조건으로 인코딩하는 기법을 제안하였다. 이 접근법에서는 시간 연산자의 \max/\min 구조를 이진 결정 변수(binary decision variable)와 빅-M 제약(big-M constraint)으로 변환한다. 예를 들어, z = \max(a, b)는 다음의 선형 제약으로 인코딩된다:

\begin{aligned} z &\geq a, \quad z \geq b \\ z &\leq a + M(1 - \delta) \\ z &\leq b + M\delta \\ \delta &\in \{0, 1\} \end{aligned}

이러한 MILP 인코딩은 전역 최적해(global optimum)를 보장하나, 이진 변수의 수가 공식의 크기와 시간 지평(time horizon)에 비례하여 증가하므로, 대규모 문제에 대한 확장성(scalability)이 제한될 수 있다.

7. 자율 로봇 임무에서의 강건성 활용 사례

7.1 궤적 최적화

자율 드론의 비행 궤적 최적화에서, 장애물 회피와 목표 도달을 동시에 만족하는 궤적을 생성하는 문제는 강건성 최대화로 정식화된다. 임무 명세:

\varphi = \mathbf{G}_{[0, T]}(\textit{avoid\_obstacle}) \wedge \mathbf{F}_{[0, T]}(\textit{reach\_goal})

에 대하여, \rho(\varphi, \mathbf{x}_{\mathbf{u}}, 0)을 최대화하는 제어 입력 \mathbf{u}를 구하면, 장애물로부터 최대한 떨어지면서 목표에 도달하는 궤적이 산출된다.

7.2 강건성 기반 임무 우선순위

복수의 임무 명세 \varphi_1, \varphi_2, \ldots, \varphi_m이 주어졌을 때, 각 명세의 강건성 값 \rho_1, \rho_2, \ldots, \rho_m을 비교함으로써 임무 간의 상대적 만족 여유를 평가할 수 있다. 강건성 값이 낮은 명세에 대하여 우선적으로 자원을 배분하는 전략은 전체 임무의 강건한 수행을 보장하는 데 유용하다.

7.3 반복 신뢰 영역 탐색

Gilpin 등(2021)은 강건성 기반 반복 신뢰 영역 탐색(counterexample-guided robustness analysis)을 통하여, 시스템이 STL 명세를 위반하는 최악의 교란(worst-case perturbation)을 체계적으로 탐색하는 기법을 제안하였다. 이는 자율 로봇 시스템의 안전성 검증에서, 명세 위반에 가장 가까운 시나리오를 식별하고 대비하는 데 활용된다.

8. 강건성 의미론의 확장

8.1 가중 강건성

표준 강건성 의미론은 모든 원자 술어와 시간 구간을 동등하게 취급한다. 그러나 실제 임무에서는 특정 요구사항이 다른 요구사항보다 중요할 수 있으므로, 가중 강건성(weighted robustness)이 도입된다 (Mehdipour et al., 2019):

\rho_w(\varphi_1 \wedge \varphi_2, \mathbf{x}, t) = \min\left(w_1 \cdot \rho(\varphi_1, \mathbf{x}, t),\; w_2 \cdot \rho(\varphi_2, \mathbf{x}, t)\right)

여기서 w_1, w_2 > 0는 가중치이다. 가중 강건성을 통하여 안전성 제약에 높은 가중치를 부여하고, 성능 관련 제약에 낮은 가중치를 부여하는 등의 우선순위 반영이 가능하다.

8.2 누적 강건성

Akazaki 등(2015)은 표준 강건성의 \inf/\sup 구조가 “가장 나쁜 시점“만을 반영하여, 전체 시간 구간에 걸친 만족도의 누적적 정보를 상실하는 문제를 지적하였다. 이를 보완하기 위하여 누적 강건성(cumulative robustness) 또는 평균 강건성(average robustness)이 제안되었다:

\rho_{\text{avg}}(\mathbf{G}_{[a,b]}\, \varphi, \mathbf{x}, t) = \frac{1}{b - a} \int_{t+a}^{t+b} \rho(\varphi, \mathbf{x}, t') \, dt'

누적 강건성은 전체 시간 구간에서의 평균적 만족 정도를 반영하므로, 임무 수행의 전반적 품질을 평가하는 데 유용하다.

9. 참고문헌

• Donzé, A. (2013). “On Signal Temporal Logic.” In Proceedings of the International Conference on Runtime Verification (RV), LNCS 7687, Springer, 382–383.
• Donzé, A., & Maler, O. (2010). “Robust Satisfaction of Temporal Logic over Real-Valued Signals.” In Formal Modeling and Analysis of Timed Systems (FORMATS), LNCS 6246, Springer, 92–106.
• Fainekos, G. E., & Pappas, G. J. (2009). “Robustness of Temporal Logic Specifications for Continuous-Time Signals.” Theoretical Computer Science, 410(42), 4262–4291.
• Gilpin, Y., Kurtz, V., & Lin, H. (2021). “A Smooth Robustness Measure of Signal Temporal Logic for Symbolic Control.” IEEE Control Systems Letters, 5(1), 241–246.
• Lemire, D. (2006). “Streaming Maximum-Minimum Filter Using No More Than Three Comparisons Per Element.” Nordic Journal of Computing, 13(4), 328–339.
• Mehdipour, N., Vasile, C. I., & Belta, C. (2019). “Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Specifications.” In Proceedings of the American Control Conference (ACC), 1690–1695.
• 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.