396.21 고수준(High-Level) 임무 명세 기술

1. 고수준 임무 명세의 개념

고수준 임무 명세(High-Level Mission Specification)란 임무의 목표와 제약 조건을 로봇의 구체적인 동작이나 제어 명령이 아닌, 추상적이고 선언적인(Declarative) 수준에서 기술하는 것을 의미한다. 고수준 명세는 “무엇(What)을 달성해야 하는가“를 기술하되, “어떻게(How) 달성하는가“에 대한 세부 사항은 로봇 시스템의 계획기(Planner)와 실행기(Executor)에 위임한다.

고수준 명세와 저수준 명세의 관계는 다음과 같은 추상화 계층(Abstraction Hierarchy)으로 표현된다.

\mathcal{M}_{\text{high}} \xrightarrow{\text{refinement}} \mathcal{M}_{\text{mid}} \xrightarrow{\text{grounding}} \mathcal{M}_{\text{low}}

여기서 \mathcal{M}_{\text{high}}는 고수준 명세(선언적 목표), \mathcal{M}_{\text{mid}}는 중간 수준 명세(과업 시퀀스), \mathcal{M}_{\text{low}}는 저수준 명세(제어 명령)이다. 정제(Refinement) 과정은 고수준 목표를 중간 수준의 과업으로 분해하며, 접지(Grounding) 과정은 과업을 구체적인 로봇 행동으로 변환한다.

2. 고수준 명세의 표현 패러다임

2.1 목표 기반 명세(Goal-Based Specification)

목표 기반 명세는 임무의 최종 상태(Goal State)를 정의하는 방식이다. 로봇 시스템은 현재 상태에서 목표 상태에 도달하기 위한 행동 시퀀스를 자율적으로 계획한다.

목표 상태 \mathbf{s}_{\text{goal}}은 상태 공간 \mathcal{S} 위의 술어(Predicate) 집합으로 정의된다.

\mathbf{s}_{\text{goal}} = \{p_1, p_2, \ldots, p_k\}

여기서 각 p_i는 목표 상태에서 참이어야 하는 명제이다. 예를 들어, 물류 임무의 목표는 다음과 같이 표현될 수 있다.

\mathbf{s}_{\text{goal}} = \{\text{at}(\text{package}_1, \text{destination}_A), \text{at}(\text{package}_2, \text{destination}_B)\}

목표 기반 명세의 장점은 높은 추상화 수준에서의 간결한 표현이 가능하다는 것이며, 단점은 임무 수행의 과정이나 중간 조건에 대한 제약을 직접적으로 표현하기 어렵다는 것이다.

2.2 시간 논리 기반 명세(Temporal Logic-Based Specification)

시간 논리(Temporal Logic)를 활용하면 목표의 달성뿐 아니라 시간에 따른 행동의 순서, 지속 조건, 안전 조건 등을 풍부하게 표현할 수 있다. 로봇 임무 명세에 주로 사용되는 시간 논리 체계는 다음과 같다.

선형 시간 논리(LTL, Linear Temporal Logic): 시간의 흐름에 따른 명제의 진리값 변화를 기술한다. 주요 연산자는 다음과 같다.

LTL 수식의 예시를 통해 다양한 임무 유형을 표현할 수 있다.

순찰 임무: 여러 지점을 반복적으로 방문해야 하는 임무이다.

\Box \Diamond \text{visit}(A) \wedge \Box \Diamond \text{visit}(B) \wedge \Box \Diamond \text{visit}(C)

“항상 결국 A를 방문하고, 항상 결국 B를 방문하고, 항상 결국 C를 방문한다.”

안전 조건 하의 도달 임무: 위험 구역을 회피하면서 목표에 도달해야 하는 임무이다.

(\Box \neg \text{in\_danger\_zone}) \wedge (\Diamond \text{at\_goal})

“항상 위험 구역에 있지 않으며, 결국 목표에 도달한다.”

순차적 과업 수행: 정해진 순서대로 과업을 수행해야 하는 임무이다.

\Diamond (\text{inspect}(A) \wedge \Diamond (\text{inspect}(B) \wedge \Diamond \text{report}))

“A를 점검한 후 B를 점검하고, 마지막으로 보고한다.”

계산 트리 논리(CTL, Computation Tree Logic): 분기하는 미래 경로를 고려한 명세가 가능하다. CTL은 경로 한정자(Path Quantifier) \forall(모든 경로에서)와 \exists(어떤 경로에서)를 포함하여 LTL보다 풍부한 표현력을 제공한다.

2.3 제약 기반 명세(Constraint-Based Specification)

제약 기반 명세는 임무를 수학적 제약 조건의 집합으로 표현하는 방식이다. 목표보다는 임무 수행 과정에서 반드시 준수해야 하는 조건에 초점을 맞춘다.

\mathcal{M}_{\text{constraint}} = \{\phi_1(\mathbf{x}, t), \phi_2(\mathbf{x}, t), \ldots, \phi_m(\mathbf{x}, t)\}

여기서 \phi_i는 상태 벡터 \mathbf{x}와 시간 t의 함수로 표현된 제약 조건이다. 제약 기반 명세는 최적화 기반 계획기와 자연스럽게 통합되며, 동차적으로 연속 제약과 이산 제약을 모두 표현할 수 있다.

2.4 온톨로지 기반 명세(Ontology-Based Specification)

온톨로지(Ontology)를 활용하여 임무 관련 개념, 관계, 속성을 체계적으로 정의하고, 이를 기반으로 임무를 명세하는 방식이다. 온톨로지는 다음과 같은 구성 요소를 가진다.

\mathcal{O} = (\mathcal{C}, \mathcal{R}, \mathcal{I}, \mathcal{A})

여기서 \mathcal{C}는 클래스(Class) 집합, \mathcal{R}은 관계(Relation) 집합, \mathcal{I}는 인스턴스(Instance) 집합, \mathcal{A}는 공리(Axiom) 집합이다.

예를 들어, 로봇 임무 온톨로지에서 “순찰 임무(Patrol Mission)“는 다음과 같이 정의될 수 있다.

• 클래스: PatrolMission ⊆ Mission
• 속성: hasWaypoint(PatrolMission, Waypoint), hasCyclePeriod(PatrolMission, Duration)
• 공리: PatrolMission → ∃hasWaypoint.Waypoint (순찰 임무는 반드시 하나 이상의 경유점을 가진다)

온톨로지 기반 명세는 이기종 로봇 시스템 간의 임무 상호 운용성(Interoperability) 확보에 유리하며, 추론 엔진(Reasoning Engine)을 통한 자동 일관성 검사가 가능하다.

3. 고수준 명세에서 저수준 실행으로의 변환

3.1 계획 수립을 통한 정제(Refinement via Planning)

고수준 명세를 실행 가능한 과업 시퀀스로 변환하는 과정은 자동 계획 수립(Automated Planning) 기법에 의하여 수행된다. 이 과정은 다음과 같이 형식화된다.

\text{Planner}: (\mathcal{M}_{\text{high}}, \mathbf{s}_{\text{init}}, \mathcal{A}_{\text{available}}) \rightarrow \pi^*

여기서 \mathcal{M}_{\text{high}}는 고수준 명세, \mathbf{s}_{\text{init}}는 초기 상태, \mathcal{A}_{\text{available}}은 로봇이 수행 가능한 행동의 집합, \pi^*는 최적 행동 시퀀스(계획)이다.

3.2 LTL 명세의 오토마톤 변환

LTL로 표현된 고수준 명세를 실행 가능한 형태로 변환하는 표준적인 방법은 LTL 수식을 뷰치 오토마톤(Büchi Automaton)으로 변환하는 것이다.

\varphi_{\text{LTL}} \xrightarrow{\text{translation}} \mathcal{B}_\varphi

뷰치 오토마톤 \mathcal{B}_\varphi = (Q, \Sigma, \delta, q_0, F)에서 Q는 상태 집합, \Sigma는 알파벳(로봇 행동), \delta는 전이 함수, q_0는 초기 상태, F는 수용 상태 집합이다. 이 오토마톤과 로봇의 전이 시스템(Transition System)을 곱(Product)하여 명세를 만족하는 실행 경로를 탐색한다(Kress-Gazit et al., 2009).

\mathcal{T}_{\text{product}} = \mathcal{T}_{\text{robot}} \otimes \mathcal{B}_\varphi

3.3 심볼 접지(Symbol Grounding)

고수준 명세에서 사용되는 추상적 심볼(예: “목표 지점”, “장애물”, “안전한 속도”)을 로봇의 센서 데이터와 제어 명령에 대응시키는 과정이다. 접지 함수 \gamma는 다음과 같이 정의된다.

\gamma: \mathcal{S}_{\text{symbolic}} \rightarrow \mathcal{S}_{\text{continuous}}

예를 들어, “목표 지점 A“라는 심볼을 GPS 좌표 (37.5665, 126.9780)으로, “안전한 속도“를 v \leq 1.5 \, \text{m/s}로 접지한다.

4. 고수준 명세의 설계 원칙

효과적인 고수준 임무 명세를 위하여 다음과 같은 설계 원칙을 준수해야 한다.

4.1 추상화 적정성(Appropriate Abstraction)

명세의 추상화 수준은 사용자의 의도를 정확하게 전달하되, 로봇 시스템에 불필요한 구현 세부 사항을 강제하지 않을 정도로 적정해야 한다. 과도한 추상화는 모호성을 유발하며, 과도한 구체화는 유연성을 저해한다.

4.2 조합 가능성(Composability)

고수준 명세의 개별 요소들이 독립적으로 정의되고, 이들의 조합을 통하여 복잡한 임무를 구성할 수 있어야 한다. 이를 위하여 명세 요소 간의 인터페이스가 명확히 정의되어야 한다.

\mathcal{M}_{\text{composite}} = \mathcal{M}_1 \oplus \mathcal{M}_2 \oplus \cdots \oplus \mathcal{M}_k

여기서 \oplus는 명세 합성 연산자이다.

4.3 실현 가능성 보장(Realizability Guarantee)

고수준 명세가 주어진 로봇 시스템과 환경에서 실현 가능한(Realizable) 것인지를 검증할 수 있어야 한다. 실현 가능성 판정 문제는 다음과 같이 정의된다.

\exists \pi: \mathcal{T}_{\text{robot}} \models \varphi_{\text{LTL}}

“로봇의 전이 시스템 \mathcal{T}_{\text{robot}}에서 LTL 명세 \varphi를 만족하는 전략 \pi가 존재하는가?”

이 판정 문제는 게임 이론(Game Theory)의 관점에서 합성(Synthesis) 문제로 환원될 수 있다(Piterman et al., 2006).

5. 고수준 명세의 비교 분석

각 명세 패러다임의 특성을 비교하면 다음과 같다.

6. 참고 문헌

• 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.
• Piterman, N., Pnueli, A., & Sa’ar, Y. (2006). “Synthesis of reactive(1) designs.” In International Conference on Verification, Model Checking, and Abstract Interpretation (pp. 364–380). Springer.
• Menghi, C., Tsigkanos, C., Berger, T., & Pelliccione, P. (2019). “PsALM: specification of dependable robotic missions.” In IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings (pp. 99–102). IEEE.
• Ghallab, M., Nau, D., & Traverso, P. (2016). Automated Planning and Acting. Cambridge University Press.
• Baier, C., & Katoen, J. P. (2008). Principles of Model Checking. MIT Press.

v0.1.0