397.6 임무 명세(Mission Specification)의 형식화 기법

1. 개요

임무 명세(Mission Specification)란 자율 로봇 시스템이 달성해야 할 목표와 준수해야 할 제약 조건을 형식적(Formal)으로 기술하는 과정이다. 형식적 임무 명세는 자연어의 모호성을 제거하고, 수학적으로 엄밀한(Rigorous) 표현을 통하여 자동화된 계획 수립, 검증(Verification), 합성(Synthesis) 과정을 가능하게 한다 (Kress-Gazit et al., 2009). 임무 명세의 형식화 수준과 방법론의 선택은 임무 계획 시스템의 표현력(Expressiveness), 계산 복잡도(Computational Complexity), 그리고 실제 운용에서의 사용성(Usability)을 결정짓는 핵심 요소이다.

2. 임무 명세의 필요성

자연어 기반 임무 기술의 한계를 이해함으로써 형식적 임무 명세의 필요성을 파악할 수 있다. 자연어 임무 기술은 다음과 같은 문제를 유발한다.

모호성(Ambiguity): “영역 A를 탐색한 후 기지로 돌아가라“라는 지시는 영역 A의 범위, 탐색의 완료 기준, 복귀 경로의 조건 등에 대한 모호성을 내포한다.

불완전성(Incompleteness): 자연어 기술은 모든 예외 상황과 경계 조건을 명시하지 못하는 경우가 많다.

비검증성(Non-Verifiability): 자연어로 기술된 임무는 자동화된 도구를 사용하여 계획의 정확성을 검증하기 어렵다.

형식적 임무 명세는 이러한 한계를 극복하기 위하여 수학적으로 정의된 언어와 구조를 사용하여 임무를 표현한다.

3. 형식화 기법의 분류

임무 명세의 형식화 기법은 크게 다음과 같은 범주로 분류할 수 있다.

3.1 시제 논리 기반 형식화 (Temporal Logic-Based Formalization)

시제 논리(Temporal Logic)는 시간의 흐름에 따른 시스템의 행동을 형식적으로 기술하는 논리 체계이다. 임무 명세에서 시제 논리는 “항상 안전한 상태를 유지하라”, “결국 목표 지점에 도달하라”, “특정 영역을 방문하기 전에 다른 영역을 먼저 방문하라“와 같은 시간적 속성(Temporal Property)을 표현하는 데 사용된다.

시제 논리의 기본 틀은 명제 논리(Propositional Logic)에 시간 연산자(Temporal Operators)를 추가한 것이다. 명제 논리의 기본 연산자는 다음과 같다.

• 부정(Negation): \neg \varphi
• 논리곱(Conjunction): \varphi_1 \wedge \varphi_2
• 논리합(Disjunction): \varphi_1 \vee \varphi_2
• 함의(Implication): \varphi_1 \rightarrow \varphi_2

시간 연산자를 추가한 시제 논리는 선형 시제 논리(LTL), 계산 트리 논리(CTL), 신호 시제 논리(STL), 메트릭 시제 논리(MTL) 등 다양한 변형을 포함한다. 각각의 시제 논리는 표현력과 계산 복잡도에서 서로 다른 특성을 보인다.

시제 논리 간의 표현력 관계는 다음과 같이 정리된다.

\text{LTL} \subset \text{MTL} \subset \text{STL (연속 시간)}

\text{LTL} \not\subset \text{CTL}, \quad \text{CTL} \not\subset \text{LTL}

\text{LTL} \cup \text{CTL} \subset \text{CTL}^*

즉, LTL과 CTL은 표현력에서 서로 비교 불가능(Incomparable)한 관계에 있으며, CTL*이 이 둘을 모두 포함한다 (Baier & Katoen, 2008).

3.2 계획 언어 기반 형식화 (Planning Language-Based Formalization)

PDDL(Planning Domain Definition Language)은 자동화된 계획(Automated Planning) 분야에서 가장 널리 사용되는 임무 명세 언어이다 (McDermott et al., 1998). PDDL은 도메인(Domain)과 문제(Problem)를 분리하여 기술하는 구조를 가지며, 행동의 전제 조건(Preconditions)과 효과(Effects)를 선언적(Declarative)으로 정의한다.

PDDL의 기본 구조는 다음과 같은 형식을 따른다.

도메인 정의:

\mathcal{D} = \langle \text{Types}, \text{Predicates}, \text{Functions}, \text{Actions} \rangle

각 행동(Action)은 다음과 같이 정의된다.

\text{Action}(a) = \langle \text{Parameters}(a), \text{Precondition}(a), \text{Effect}(a) \rangle

문제 정의:

\mathcal{P} = \langle \text{Objects}, \text{Init}, \text{Goal} \rangle

여기서 \text{Init}은 초기 상태, \text{Goal}은 목표 조건이다.

PDDL은 여러 버전을 거치며 확장되어 왔으며, 주요 확장 요소는 다음과 같다.

3.3 오토마타 기반 형식화 (Automata-Based Formalization)

오토마타(Automata) 이론은 임무 명세와 제어 정책 합성의 연결고리를 제공한다. 시제 논리로 표현된 임무 사양을 오토마타로 변환함으로써, 모델 검사(Model Checking)나 제어기 합성(Controller Synthesis) 등의 자동화된 기법을 적용할 수 있다 (Baier & Katoen, 2008).

LTL 사양 \varphi는 비결정적 뷔히 오토마톤(Nondeterministic Büchi Automaton, NBA) \mathcal{A}_\varphi로 변환할 수 있다.

\varphi \xrightarrow{\text{변환}} \mathcal{A}_\varphi = (Q, \Sigma, \delta, Q_0, F)

여기서 Q는 상태 집합, \Sigma = 2^{\mathcal{AP}}는 알파벳(입력 심볼의 집합), \delta: Q \times \Sigma \rightarrow 2^Q는 전이 함수, Q_0 \subseteq Q는 초기 상태 집합, F \subseteq Q는 수용 상태(Accepting States) 집합이다.

이 변환의 핵심적 성질은 오토마톤 \mathcal{A}_\varphi의 언어(Language)가 LTL 사양 \varphi를 만족하는 모든 무한 단어(Infinite Word)의 집합과 일치한다는 것이다.

\mathcal{L}(\mathcal{A}_\varphi) = \{\sigma \in \Sigma^\omega \mid \sigma \models \varphi\}

3.4 제약 만족 기반 형식화 (Constraint Satisfaction-Based Formalization)

제약 만족 문제(Constraint Satisfaction Problem, CSP) 또는 충족 가능성 모듈 이론(Satisfiability Modulo Theories, SMT) 기반 형식화는 변수, 정의역, 제약의 삼중쌍으로 임무를 기술한다 (Rossi et al., 2006).

\text{CSP} = \langle \mathcal{X}, \mathcal{D}, \mathcal{C} \rangle

여기서 \mathcal{X} = \{x_1, x_2, \ldots, x_n\}은 변수의 집합, \mathcal{D} = \{D_1, D_2, \ldots, D_n\}은 각 변수의 정의역(Domain), \mathcal{C} = \{c_1, c_2, \ldots, c_m\}은 제약 조건의 집합이다.

임무 계획에서 CSP 변수는 작업의 수행 순서, 자원 할당, 시간 배정 등을 나타내며, 제약 조건은 선후 관계, 자원 용량, 시간 윈도우 등을 표현한다.

4. 형식화 수준의 스펙트럼

임무 명세의 형식화 수준은 완전 비형식적(Fully Informal)에서 완전 형식적(Fully Formal)까지의 스펙트럼(Spectrum)으로 표현할 수 있다.

\text{자연어} \rightarrow \text{반형식적} \rightarrow \text{형식적}

완전 비형식적: 자연어로 기술된 임무 사양. 인간의 이해에는 적합하나 자동화에 부적합하다.

반형식적(Semi-Formal): 구조화된 템플릿(Template)이나 도메인 특화 언어(Domain-Specific Language, DSL)를 사용하여 일부 구조가 정의된 임무 사양. 인간의 가독성과 기계 처리 가능성의 절충이다.

완전 형식적: 시제 논리, PDDL, 오토마타 등의 수학적 프레임워크를 사용한 임무 사양. 자동화된 처리와 검증이 가능하나 전문 지식이 필요하다.

5. 형식적 임무 명세와 제어 합성의 연결

형식적 임무 명세의 핵심적 장점은 자동 합성(Automatic Synthesis)이 가능하다는 점이다. LTL 사양 \varphi로 표현된 임무와 로봇의 전이 시스템 \mathcal{TS}가 주어졌을 때, 두 모델의 곱(Product)을 구성하여 사양을 만족하는 제어 전략을 자동으로 도출할 수 있다.

\mathcal{P} = \mathcal{TS} \otimes \mathcal{A}_\varphi

여기서 \mathcal{P}는 곱 오토마톤(Product Automaton), \otimes는 동기적 곱(Synchronous Product) 연산이다. 곱 오토마톤에서 수용 조건을 만족하는 경로(Run)를 탐색함으로써, 임무 사양을 만족하는 로봇의 행동 순서를 체계적으로 도출할 수 있다.

이 과정의 정확성은 다음과 같이 보장된다.

\text{run} \in \mathcal{L}(\mathcal{P}) \iff \text{trace}(\text{run}) \models \varphi

즉, 곱 오토마톤의 수용 경로가 존재한다면, 이 경로에 대응하는 로봇의 행동은 LTL 사양 \varphi를 만족한다.

6. 임무 명세 도구와 프레임워크

형식적 임무 명세를 지원하는 대표적인 소프트웨어 도구와 프레임워크는 다음과 같다.

7. 참고 문헌

• 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.
• Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking. MIT Press.
• McDermott, D., et al. (1998). PDDL – The Planning Domain Definition Language. Technical Report, Yale Center for Computational Vision and Control.
• Rossi, F., van Beek, P., & Walsh, T. (2006). Handbook of Constraint Programming. Elsevier.

버전: 2026-03-24 v1.0