396.23 형식 언어 기반 임무 명세

1. 형식 언어의 정의와 역할

형식 언어(Formal Language)란 수학적으로 엄밀하게 정의된 구문론(Syntax)과 의미론(Semantics)을 갖춘 언어이다. 로봇 임무 명세에 형식 언어를 적용하면, 임무 기술의 모호성을 완전히 배제하고, 자동화된 검증(Verification)과 합성(Synthesis)을 가능하게 한다.

형식 언어 $\mathcal{L}_F$ 는 알파벳 $\Sigma$ 위의 문자열 집합으로 정의된다.

$\mathcal{L}_F \subseteq \Sigma^*$

여기서 $\Sigma^*$ 는 알파벳 $\Sigma$ 로 구성 가능한 모든 유한 문자열의 집합(클리니 폐포, Kleene Closure)이다. 형식 언어에 속하는 문자열만이 합법적인(Well-Formed) 임무 명세로 인정된다.

2. 명제 논리 기반 임무 명세

2.1 명제 논리(Propositional Logic)

가장 기본적인 형식 체계로서, 명제(Proposition)와 논리 연결사(Logical Connective)를 사용하여 임무 조건을 기술한다. 명제 논리의 구문은 다음과 같이 귀납적으로 정의된다.

$\varphi ::= p \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \varphi_1 \vee \varphi_2 \mid \varphi_1 \rightarrow \varphi_2$

여기서 $p$ 는 원자 명제(Atomic Proposition), $\neg$ 는 부정, $\wedge$ 는 논리곱, $\vee$ 는 논리합, $\rightarrow$ 는 함의이다.

명제 논리는 상태 기반 조건(예: “배터리가 충분하다”, “목표 지점에 도달하였다”)을 기술하는 데 적합하나, 시간적 순서나 동적 변화를 표현하는 데는 한계가 있다.

2.2 임무 명세에의 적용

명제 논리를 활용한 임무 조건의 예시는 다음과 같다.

임무 시작 조건:
$\varphi_{\text{start}} = \text{battery\_ok} \wedge \text{gps\_fix} \wedge \text{comm\_link} \wedge \neg \text{obstacle\_detected}$

임무 성공 조건:
$\varphi_{\text{success}} = \text{all\_waypoints\_visited} \wedge \text{data\_transmitted}$

3. 시간 논리 기반 임무 명세

3.1 선형 시간 논리(LTL)

선형 시간 논리(Linear Temporal Logic, LTL)는 무한 실행 경로(Infinite Execution Path) 위에서의 시간적 속성을 표현하는 형식 체계이다. LTL의 구문은 명제 논리에 시간 연산자를 추가하여 확장된다.

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

여기서 $\bigcirc$ (Next)은 다음 시점 연산자, $\mathcal{U}$ (Until)은 ~할 때까지 연산자이다. 이로부터 파생 연산자가 정의된다.

$\Diamond \varphi \equiv \text{true} \, \mathcal{U} \, \varphi \quad (\text{Eventually}: \text{결국 } \varphi)$

$\Box \varphi \equiv \neg \Diamond \neg \varphi \quad (\text{Always}: \text{항상 } \varphi)$

LTL은 다음과 같은 로봇 임무 패턴을 표현할 수 있다.

안전성(Safety): “위험 구역에 결코 진입하지 않는다.”
$\Box \neg \text{in\_danger\_zone}$

활동성(Liveness): “결국 목표에 도달한다.”
$\Diamond \text{at\_goal}$

반응성(Reactivity): “장애물을 감지하면 반드시 회피한다.”
$\Box (\text{obstacle\_detected} \rightarrow \Diamond \text{obstacle\_avoided})$

순환성(Recurrence): “기지를 반복적으로 방문한다.”
$\Box \Diamond \text{at\_base}$

지속성(Persistence): “결국 정상 통신 상태가 영구적으로 유지된다.”
$\Diamond \Box \text{comm\_ok}$

3.2 LTL 명세의 모델 검사(Model Checking)

LTL 명세의 만족 여부를 검증하기 위하여 모델 검사 기법이 활용된다. 로봇 시스템을 크립키 구조(Kripke Structure) $\mathcal{K} = (S, S_0, R, L)$ 로 모델링한다.

$\mathcal{K} \models \varphi \iff \forall \pi \in \text{Paths}(\mathcal{K}), \quad \pi \models \varphi$

여기서 $S$ 는 상태 집합, $S_0$ 는 초기 상태 집합, $R \subseteq S \times S$ 는 전이 관계, $L: S \rightarrow 2^{AP}$ 는 라벨링 함수, $\pi$ 는 실행 경로이다.

모델 검사의 계산 복잡도는 LTL 수식의 크기 $|\varphi|$ 와 상태 공간의 크기 $|S|$ 에 대하여 다음과 같다.

$\mathcal{O}(|S| \times 2^{|\varphi|})$

3.3 계산 트리 논리(CTL)

계산 트리 논리(Computation Tree Logic, CTL)는 분기하는 시간 모델(Branching Time Model) 위에서의 속성을 표현한다. CTL은 경로 한정자 $\mathbf{A}$ (모든 경로)와 $\mathbf{E}$ (어떤 경로)를 시간 연산자 앞에 결합한다.

$\varphi ::= p \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \mathbf{AX}\varphi \mid \mathbf{EX}\varphi \mid \mathbf{AF}\varphi \mid \mathbf{EF}\varphi \mid \mathbf{AG}\varphi \mid \mathbf{EG}\varphi$

CTL 명세의 예시는 다음과 같다.

어떤 경로에서 목표 도달 가능: $\mathbf{EF} \, \text{at\_goal}$

모든 경로에서 안전 유지: $\mathbf{AG} \neg \text{collision}$

3.4 CTL*

CTL*은 LTL과 CTL을 모두 포괄하는 상위 논리 체계로서, 가장 풍부한 표현력을 제공한다. 그러나 모델 검사의 계산 복잡도가 높아 실용적 적용에는 제약이 존재한다.

논리 체계	표현력	모델 검사 복잡도	적용 용이성
명제 논리	낮음	$\mathcal{O}(n)$	높음
LTL	중간	$\mathcal{O}(\vert S \vert \times 2^{\vert\varphi\vert})$	중간
CTL	중간	$\mathcal{O}(\vert S \vert \times \vert\varphi\vert)$	중간
CTL*	높음	$\mathcal{O}(\vert S \vert \times 2^{\vert\varphi\vert})$	낮음

4. 차 논리 기반 임무 명세

4.1 차 논리(First-Order Logic, FOL)

1차 논리는 개체(Individual), 관계(Relation), 한정자(Quantifier)를 사용하여 보다 풍부한 표현을 가능하게 한다. 1차 논리의 구문은 다음과 같다.

$\varphi ::= P(t_1, \ldots, t_n) \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \forall x. \varphi \mid \exists x. \varphi$

여기서 $P$ 는 술어 기호, $t_i$ 는 항(Term), $\forall$ 는 전칭 한정자, $\exists$ 는 존재 한정자이다.

4.2 PDDL의 형식적 기반

PDDL(Planning Domain Definition Language)은 1차 논리를 기반으로 구축된 계획 수립 전용 형식 언어이다. PDDL에서 행동(Action) $a$ 의 형식적 정의는 다음과 같다.

$a = (\text{name}, \text{params}, \text{pre}(a), \text{eff}(a))$

여기서 $\text{pre}(a)$ 는 사전 조건(1차 논리 수식), $\text{eff}(a)$ 는 효과(상태 변화)이다. PDDL의 확장인 PDDL 2.1에서는 지속적 행동(Durative Action)과 수치적 유창성(Numeric Fluent)이 추가되어 시간과 자원을 형식적으로 표현할 수 있다.

지속적 행동의 정의는 다음과 같다.

$a_d = (\text{name}, \text{params}, \text{duration}, \text{condition}, \text{effect})$

여기서 $\text{duration}$ 은 행동의 지속 시간, $\text{condition}$ 은 행동 시작, 종료, 전체 기간에 걸친 조건을 각각 명시한다.

5. 시그널 시간 논리(STL) 기반 명세

5.1 시그널 시간 논리(Signal Temporal Logic, STL)

STL은 연속 시간 실수값 신호(Real-Valued Signal) 위에서의 시간적 속성을 표현하는 형식 체계이다(Maler & Nickovic, 2004). 로봇의 센서 데이터나 연속 상태 변수에 대한 제약을 직접적으로 표현할 수 있다.

STL의 구문은 다음과 같다.

$\varphi ::= \mu \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \Diamond_{[a,b]} \varphi \mid \Box_{[a,b]} \varphi \mid \varphi_1 \, \mathcal{U}_{[a,b]} \, \varphi_2$

여기서 $\mu$ 는 실수값 술어 $\mu \equiv f(\mathbf{x}) > 0$ 이며, $[a, b]$ 는 시간 구간이다.

STL 명세의 예시는 다음과 같다.

5초에서 10초 사이에 속도가 2 m/s 이하여야 한다:
$\Box_{[5, 10]} (v \leq 2.0)$

30초 이내에 목표까지의 거리가 0.5m 이내가 되어야 한다:
$\Diamond_{[0, 30]} (\|\mathbf{p} - \mathbf{p}_{\text{goal}}\| \leq 0.5)$

5.2 STL의 정량적 의미론(Quantitative Semantics)

STL의 강건도(Robustness) $\rho(\varphi, \mathbf{x}, t)$ 는 신호 $\mathbf{x}$ 가 시각 $t$ 에서 수식 $\varphi$ 를 만족하는 정도를 실수값으로 나타낸다.

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

$\rho(\varphi_1 \wedge \varphi_2, \mathbf{x}, t) = \min(\rho(\varphi_1, \mathbf{x}, t), \rho(\varphi_2, \mathbf{x}, t))$

$\rho(\Diamond_{[a,b]} \varphi, \mathbf{x}, t) = \sup_{t' \in [t+a, t+b]} \rho(\varphi, \mathbf{x}, t')$

$\rho > 0$ 이면 명세가 만족되며, $\rho < 0$ 이면 위반된다. 강건도 값의 절대값이 클수록 만족 또는 위반의 여유(Margin)가 크음을 의미한다. 이 정량적 의미론은 최적화 기반 임무 계획과 자연스럽게 결합된다.

6. 형식 언어 기반 임무 합성(Mission Synthesis)

형식 명세로부터 이를 만족하는 제어 전략을 자동으로 합성하는 반응적 합성(Reactive Synthesis) 기법이 연구되고 있다. GR(1)(Generalized Reactivity 1) 합성은 다음 형태의 명세에 대하여 다항 시간 합성 알고리즘을 제공한다(Piterman et al., 2006).

$\varphi = \varphi_{\text{env}} \rightarrow \varphi_{\text{sys}}$

여기서 $\varphi_{\text{env}}$ 는 환경에 대한 가정, $\varphi_{\text{sys}}$ 는 시스템이 만족해야 하는 보장이다. 환경 가정과 시스템 보장 모두 다음과 같은 GR(1) 형식을 따른다.

$\varphi_{\text{GR(1)}} = \underbrace{\Box \Diamond p_1 \wedge \Box \Diamond p_2 \wedge \cdots \wedge \Box \Diamond p_m}_{\text{안전성 + 활동성 조건}}$

7. 형식 언어 기반 명세의 도전 과제

형식 언어 기반 임무 명세는 높은 엄밀성을 제공하지만, 다음과 같은 실용적 도전 과제가 존재한다.

상태 폭발(State Explosion): 시스템 복잡도가 증가하면 모델 검사의 상태 공간이 지수적으로 증가한다.
명세 난이도(Specification Difficulty): 비전문가가 시간 논리 수식을 작성하는 것은 상당한 학습을 요구한다.
연속-이산 간극(Continuous-Discrete Gap): 로봇의 연속 역학을 이산적 형식 모델에 정확하게 반영하기 어렵다.
불확실성 처리: 표준 형식 논리는 확률적 불확실성을 직접 표현하지 못한다. 이를 해결하기 위해 확률적 모델 검사(Probabilistic Model Checking)가 연구되고 있다.

8. 참고 문헌

Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model Checking. MIT Press.
Baier, C., & Katoen, J. P. (2008). Principles of Model Checking. MIT Press.
Maler, O., & Nickovic, D. (2004). “Monitoring temporal properties of continuous signals.” In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (pp. 152–166). Springer.
Piterman, N., Pnueli, A., & Sa’ar, Y. (2006). “Synthesis of reactive(1) designs.” In VMCAI (pp. 364–380). Springer.
Fox, M., & Long, D. (2003). “PDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains.” JAIR, 20, 61–124.
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.

v0.1.0