397.46 도달 가능성(Reachability) 분석

로봇 임무 계획에서 도달 가능성(reachability) 분석은 로봇이 현재 상태에서 특정 목표 상태에 도달할 수 있는지를 형식적으로 판별하는 과정이다. 이 분석은 임무 달성 가능성 검사의 핵심 구성 요소이며, 임무 명세의 실현 가능성 판단, 계획 탐색 공간의 축소, 그리고 안전성 검증에 근본적으로 활용된다.

1. 도달 가능성의 형식적 정의

1.1 상태 전이 시스템에서의 도달 가능성

상태 전이 시스템 \mathcal{M} = (S, A, \delta, s_0)에서 상태 s_g \in S가 초기 상태 s_0으로부터 **도달 가능(reachable)**하다는 것은, 행동의 유한 시퀀스 \pi = \langle a_1, a_2, \ldots, a_n \rangle이 존재하여 다음이 성립함을 의미한다.

s_0 \xrightarrow{a_1} s_1 \xrightarrow{a_2} \cdots \xrightarrow{a_n} s_n = s_g

여기서 \delta: S \times A \rightarrow S는 상태 전이 함수이며, 각 행동 a_i는 상태 s_{i-1}에서 적용 가능(applicable)해야 한다. 초기 상태 s_0에서 도달 가능한 모든 상태의 집합을 **도달 가능 집합(reachable set)**이라 하며, 다음과 같이 정의된다.

\text{Reach}(s_0) = \{s \in S \mid \exists \pi: s_0 \xrightarrow{\pi} s\}

1.2 목표 도달 가능성 문제

목표 조건 G \subseteq S에 대한 도달 가능성 문제는 다음을 판별하는 것이다.

\text{Reach}(s_0) \cap G \neq \emptyset

이것이 참이면 목표는 도달 가능(reachable)하고, 거짓이면 도달 불가능(unreachable)하다.

2. 도달 가능성 분석의 계산 방법

2.1 순방향 도달 가능성 분석(Forward Reachability)

순방향 도달 가능성 분석은 초기 상태로부터 출발하여 가능한 모든 후속 상태를 계산하는 방법이다. 너비 우선 탐색(Breadth-First Search, BFS) 기반의 고정점(fixpoint) 연산으로 수행된다.

알고리즘: Forward Reachability Analysis
입력: 상태 전이 시스템 M = (S, A, δ, s₀), 목표 집합 G
출력: reachable 또는 unreachable

1. Reach ← {s₀}
2. Frontier ← {s₀}
3. repeat
4.     NewStates ← ∅
5.     for each s ∈ Frontier do
6.         for each a ∈ applicable(s) do
7.             s' ← δ(s, a)
8.             if s' ∉ Reach then
9.                 NewStates ← NewStates ∪ {s'}
10.                if s' ∈ G then return reachable
11.        end for
12.    end for
13.    Reach ← Reach ∪ NewStates
14.    Frontier ← NewStates
15. until Frontier = ∅
16. return unreachable

이 알고리즘의 시간 복잡도는 O(|S| \cdot |A|)이며, 공간 복잡도는 O(|S|)이다.

2.2 역방향 도달 가능성 분석(Backward Reachability)

역방향 도달 가능성 분석은 목표 상태로부터 역방향으로 선행 상태(predecessor states)를 계산하는 방법이다. 행동 a에 대한 역방향 전이 함수 \delta^{-1}(s', a) = \{s \mid \delta(s, a) = s'\}를 사용한다.

\text{BackReach}_0 = G
\text{BackReach}_{k+1} = \text{BackReach}_k \cup \{s \mid \exists a, s' \in \text{BackReach}_k: \delta(s, a) = s'\}

목표가 도달 가능한 것은 s_0 \in \text{BackReach}^*일 때이며, 여기서 \text{BackReach}^* = \bigcup_{k=0}^{\infty} \text{BackReach}_k는 역방향 도달 가능 집합의 고정점이다.

역방향 분석은 목표 상태의 수가 전체 상태 공간에 비해 작을 때 순방향 분석보다 효율적이다.

2.3 양방향 도달 가능성 분석(Bidirectional Reachability)

순방향과 역방향 분석을 동시에 수행하여, 두 도달 가능 집합이 교차하는 시점에 도달 가능성을 판별하는 방법이다.

\text{reachable} \iff \text{Reach}^{\text{fwd}}_k \cap \text{BackReach}^{\text{bwd}}_l \neq \emptyset

양방향 분석은 상태 공간의 크기가 |S|일 때, 탐색해야 하는 상태의 수를 O(\sqrt{|S|}) 수준으로 절감할 수 있는 이론적 이점을 가진다.

3. 기호적 도달 가능성 분석

3.1 BDD(Binary Decision Diagram) 기반 분석

대규모 상태 공간에서의 명시적(explicit) 상태 열거가 비실용적일 때, 기호적(symbolic) 표현을 사용한 도달 가능성 분석이 활용된다. **이진 결정 다이어그램(Binary Decision Diagram, BDD)**은 부울 함수를 압축적으로 표현하는 자료 구조로서, 상태 집합을 특성 함수(characteristic function)로 부호화한다.

상태 집합 R \subseteq S의 특성 함수는 다음과 같다.

\chi_R(\mathbf{x}) = \begin{cases} 1 & \text{if } \mathbf{x} \in R \\ 0 & \text{otherwise} \end{cases}

여기서 \mathbf{x} = (x_1, x_2, \ldots, x_n)은 상태를 부호화하는 부울 변수 벡터이다.

상태 전이 관계 \delta는 전이 관계 특성 함수 T(\mathbf{x}, \mathbf{a}, \mathbf{x}')로 표현되며, 순방향 이미지(forward image) 연산은 다음과 같이 수행된다.

\chi_{\text{img}}(\mathbf{x}') = \exists \mathbf{x}, \mathbf{a}: \chi_R(\mathbf{x}) \wedge T(\mathbf{x}, \mathbf{a}, \mathbf{x}')

이 연산은 BDD의 부울 연산과 양화(quantification)를 통해 수행되며, 상태 공간의 규칙적 구조를 효과적으로 활용하여 기하급수적 상태 수를 다항식 크기의 BDD로 표현할 수 있다.

3.2 SAT 기반 유계 도달 가능성(Bounded Reachability via SAT)

**유계 모델 검사(Bounded Model Checking, BMC)**에서는 k 단계 이내의 도달 가능성을 명제 논리의 만족 가능성(SAT) 문제로 환원한다.

\phi_k = I(s_0) \wedge \bigwedge_{i=0}^{k-1} T(s_i, a_i, s_{i+1}) \wedge G(s_k)

여기서 I(s_0)는 초기 상태 조건, T(s_i, a_i, s_{i+1})는 전이 관계, G(s_k)는 목표 조건이다. 명제 \phi_k가 만족 가능(satisfiable)하면 k 단계 이내에 목표에 도달할 수 있으며, 만족시키는 할당(satisfying assignment)으로부터 실제 행동 시퀀스를 추출할 수 있다.

4. 연속 시스템의 도달 가능성 분석

4.1 동역학 시스템의 도달 가능 집합

로봇의 물리적 운동을 연속 동역학 시스템으로 모델링할 때, 도달 가능 집합은 다음과 같이 정의된다. 시스템 동역학이 \dot{x} = f(x, u)로 주어질 때, 시간 t에서의 도달 가능 집합은 다음과 같다.

\text{Reach}(t) = \{x(t) \mid x(0) \in X_0,\ u(\cdot) \in \mathcal{U},\ \dot{x} = f(x, u)\}

여기서 X_0는 초기 상태 집합, \mathcal{U}는 허용 제어 입력의 집합이다.

4.2 수치적 도달 가능성 분석 도구

연속 시스템의 정확한 도달 가능 집합 계산은 일반적으로 해석적으로 불가능하므로, 수치적 근사 방법이 사용된다.

Zonotope 기반 근사: Zonotope는 중심 벡터와 생성자(generator) 행렬로 표현되는 볼록 다면체의 특수한 형태이다. 선형 시스템의 도달 가능 집합을 zonotope의 시퀀스로 과대 근사(over-approximation)하는 방법이 효율적으로 활용된다.

\text{Reach}_{\text{approx}}(k+1) = A \cdot \text{Reach}_{\text{approx}}(k) \oplus B \cdot \mathcal{U} \oplus \mathcal{W}

여기서 \oplus는 민코프스키 합(Minkowski sum), \mathcal{W}는 과정 잡음(process noise)의 집합이다.

CORA(Continuous Reachability Analyzer): Althoff(2015)가 개발한 CORA는 선형 및 비선형 동역학 시스템의 도달 가능 집합을 zonotope, 다항식 zonotope, 타원체(ellipsoid) 등으로 계산하는 MATLAB 기반 도구이다.

5. 임무 계획에서의 도달 가능성 분석 활용

5.1 계획 탐색 공간의 축소

도달 가능성 분석은 계획기의 탐색 효율을 향상시키는 데 활용된다. 초기 상태에서 도달 불가능한 목표 조건을 사전에 식별하면, 불필요한 탐색을 방지할 수 있다. GraphPlan 알고리즘에서의 도달 가능성 분석은 계획 그래프의 레벨 확장 과정에서 자연스럽게 수행되며, 도달 불가능한 목표를 조기에 탐지한다.

5.2 안전성 검증

도달 가능성 분석은 로봇 시스템의 안전성(safety) 검증에도 핵심적으로 활용된다. 안전 속성은 “위험 상태 집합 S_{\text{unsafe}}에 도달하지 않는다“는 형태로 표현되며, 이는 다음과 동치이다.

\text{Reach}(s_0) \cap S_{\text{unsafe}} = \emptyset

이 조건이 만족되면 시스템은 안전하고, 그렇지 않으면 안전 위반(safety violation)이 가능함을 의미한다.

5.3 임무 명세 실현 가능성 판단

형식 논리(LTL, CTL 등)로 표현된 임무 명세의 실현 가능성을 판단하기 위해, 도달 가능성 분석이 모델 검사(model checking)와 결합되어 사용된다. 오토마타 기반 접근에서는 시스템 모델과 임무 명세를 동기적으로 합성한 제품 오토마톤(product automaton)에서의 도달 가능성이 임무의 만족 가능성을 결정한다.

6. 도달 가능성 분석의 계산 복잡도

7. 도달 가능성 분석의 한계와 대응

7.1 상태 공간 폭발 문제

명시적 도달 가능성 분석은 상태 공간의 크기에 비례하는 계산 비용이 소요되므로, 대규모 시스템에서는 상태 공간 폭발(state space explosion) 문제에 직면한다. 이를 완화하기 위해 다음 기법들이 활용된다.

• 추상화(Abstraction): 상태 공간을 추상 도메인으로 사상(mapping)하여 축소된 상태 공간에서 분석을 수행한다. 추상화의 정확도와 효율성 사이의 trade-off가 존재한다.
• 대칭 축소(Symmetry Reduction): 시스템의 대칭 구조를 활용하여 동치 클래스(equivalence class) 단위로 상태를 합병한다.
• 부분 순서 축소(Partial Order Reduction): 독립적 행동의 실행 순서에 의한 중복 탐색을 제거한다.

7.2 근사적 도달 가능성

정확한 도달 가능성 분석이 비실용적일 때, 과대 근사(over-approximation) 또는 **과소 근사(under-approximation)**를 사용한다.

• 과대 근사: \text{Reach}(s_0) \subseteq \text{Reach}_{\text{over}}(s_0). 안전성 검증에 적합하며, \text{Reach}_{\text{over}} \cap S_{\text{unsafe}} = \emptyset이면 원래 시스템도 안전하다.
• 과소 근사: \text{Reach}_{\text{under}}(s_0) \subseteq \text{Reach}(s_0). 도달 가능성 확인에 적합하며, \text{Reach}_{\text{under}} \cap G \neq \emptyset이면 목표는 도달 가능하다.

8. 요약

도달 가능성 분석은 로봇 임무 계획에서 목표의 달성 가능성, 시스템의 안전성, 임무 명세의 실현 가능성을 형식적으로 판별하는 핵심 도구이다. 순방향·역방향·양방향 탐색, BDD 기반 기호적 분석, SAT 기반 유계 분석, 그리고 연속 시스템을 위한 zonotope 기반 근사 등 다양한 계산 방법이 활용된다. 상태 공간 폭발 문제에 대해서는 추상화, 대칭 축소, 부분 순서 축소 등의 기법이 적용되며, 정확한 분석이 불가능한 경우 과대/과소 근사를 통해 실용적인 판별이 수행된다.

9. 참고 문헌

• Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model Checking. MIT Press.
• Biere, A., Cimatti, A., Clarke, E. M., & Zhu, Y. (1999). “Symbolic model checking without BDDs.” Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 193–207.
• Althoff, M. (2015). “An introduction to CORA 2015.” Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH), pp. 120–151.
• LaValle, S. M. (2006). Planning Algorithms. Cambridge University Press.
• Ghallab, M., Nau, D., & Traverso, P. (2004). Automated Planning: Theory and Practice. Morgan Kaufmann.

v1.0 | 로봇공학 서적 – Volume 9, Part 53, Chapter 397, Section 46