기술 요약: 사이버-물리 시스템의 보수적 이산 추상화 구축을 위한 실용적 가이드

문제 정의

사이버-물리 시스템(CPS)은 실패가 인명과 재산을 위협할 수 있는 안전 필수 환경에서 작동한다. 심볼릭 모델 체킹(Symbolic Model Checking)은 복잡한 시제 논리(Temporal-logic) 속성을 검증하는 효과적인 방법이지만, 유한 상태 모델을 필요로 한다. 그러나 실제 CPS는 연속적인 상태 공간 위에서 진화한다. 모델 체킹을 적용하기 위해 엔지니어들은 이러한 연속 역학을 유한 상태 추상체로 이산화해야 한다.

핵심 과제는 **건전성(Soundness)**을 확보하는 것이다. 즉, 추상 모델에서 도출된 검증 보증이 구체적인 시스템으로 전달되어야 한다. 이를 위해서는 추상화가 구체적인 상태 공간 및 동작의 **보수적 과대 근사(Conservative over-approximation)**가 되어야 한다. 실제로 모델 구축자들은 건전성을 해치거나 과도한 비관론을 초래하는 네 가지 함정에 자주 직면한다:

1. 구체적 상태 공간의 미달 커버링(Under-covering).
2. 전이 관계의 과소 근사(Under-approximating) (실행 가능한 동작 누락).
3. "퇴화된(Degenerate)" 동작의 불건전한 제거 (예: 인증 없이 셀프 루프를 제거함).
4. 부적절한 명세 리프팅(Specification lifting) (추상적 만족이 구체적 만족으로 이어지는 논리적 함축을 보존하지 못함).

이러한 문제들은 추상 모델이 실제 시스템이 만족하는 명세를 위반하는 것으로 나타나는 "가짜(Spurious)" 반례를 생성하여, 검증을 무용지물로 만든다.

방법론

본 논문은 보수적인 이산 추상화를 구축하기 위한 4단계의 모듈형 워크플로우를 제안한다. 이 워크플로우는 "구성 과정에서 보수성(Conservative-by-construction)"을 갖도록 설계되었으며, 이는 특정 수학적 보증을 통해 모든 단계에서 건전성이 유지됨을 의미한다.

1단계: 상태 공간 추상화

연속 상태 공간 $X$는 균일한 직교 격자(Uniform rectilinear grid)를 사용하여 유한한 추상 상태 집합 $\hat{X}$로 분할된다. 양자화 함수 $\psi: X \to \hat{X}$는 구체적 상태를 추상 셀(Cell)로 매핑한다. 역 매핑 $\Psi(\hat{x})$는 각 추상 상태의 구체적 영역(Preimage)을 정의한다. 이 단계는 모든 구체적 상태와 초기 조건이 추상 모델 내에 대표성을 갖도록 보장한다.

2단계: 보수적 전이 구성

본 논문은 모든 구체적 전이가 추상 모델에 표현되도록 보장하면서 전이 관계 $\hat{f}$(즉, 어떤 추상 상태가 다음 상태가 될 수 있는지 결정하는 것)를 계산하는 세 가지 교체 가능한 방법을 제시한다:

• 축 정렬 바운딩 박스 (AABB): 구체적 셀의 이미지가 시스템 역학 하에서 가지는 바운딩 박스를 계산한다. 이 박스와 교차하는 모든 추상 셀을 후속 상태로 추가한다. 계산 효율적이지만 비선형 시스템에 대해서는 지나치게 보수적일 수 있다.
• 폴리토프 전파 (Polytope Propagation): 구체적 셀의 이미지를 과대 근사하기 위해 폴리토프(Convex hull)를 사용한다. 비선적 역학에 대해 AABB보다 더 정밀하지만 계산 비용이 높다. 이 방법은 고비용의 폴리토프 교차 테스트를 수행하기 전에 후보를 필터링하기 위해 AABB 컬링(Culling)을 활용한다.
• PAC 인증을 이용한 샘플링: 블랙박스 또는 고도의 비선형 시스템의 경우, 상태 공간을 샘플링하여 전이를 발견한다. 결정론적 보증 대신, 이 방법은 아마도 대략적으로 정확한(Probably Approximately Correct, PAC) 보증을 제공한다. 이 방법은 구성된 전이 관계가 모든 "유의미한" 전이(확률 $\ge \beta$로 발생하는 전이)를 포함한다는 것을 높은 신뢰도($1-\delta$)로 인증하며, 관찰되지 않은 전이의 "누락된 질량(Missing mass)"을 제한한다.

3단계: 퇴화된 동작의 완화

보수적 추상화는 종종 가짜 전이(구체적 시스템에서는 불가능한 전이)와 셀프 루프(상태에서 자기 자신으로의 전이)를 도입한다. 이는 특히 생존성(Liveness) 속성에 대해 검증 결과에 부정적인 영향을 줄 수 있다.

• 가짜 전이: **반례 유도 추상화 정밀화(CEGAR)**를 통해 해결한다. 추상 모델에서 반례 궤적이 발견되면, 알고리즘은 이를 구체적 역학에 대해 검증한다. 만약 해당 궤적이 가짜라면(도달 가능 집합이 공집합이 되면), 가짜 전이를 제거하기 위해 상태 공간을 정밀화(분할)한다.
• 셀프 루프: **인증된 셀프 루프 제거(Certified Self-Loop Erasure)**를 통해 해결한다. 셀프 루프는 모든 구체적 궤적이 유한한 단계($K$) 내에 해당 셀을 벗어날 수 있음이 인증될 때만 제거된다. 이는 도달 가능 집합 전파를 반복하거나 PAC 보증을 가진 샘플링 전략을 통해 검증된다.

4단계: LTL 명세의 건전한 리프팅

구체적 공간에 정의된 LTL 명세 $\phi$를 추상 명세 $\hat{\phi}$로 리프팅해야 한다. 본 논문은 **May-Must 의미론(May-must semantics)**을 채택한다:

• Must 술어: 원자적 명제가 추상 상태에서 참이라는 것은 해당 셀 내의 모든 구체적 상태에서 참일 때를 의미한다.
• May 술어: 원자적 명제가 참이라는 것은 해당 셀 내의 적어도 하나의 구체적 상태에서 참일 때를 의미한다.
  리프팅 연산자 $\rho$는 원자적 명제를 "Must"(안전성(Safety)을 위해) 또는 "May"(논리 구조에 따라 적절하게)로 강화하거나 약화함으로써 $\phi$를 $\hat{\phi}$로 변환하며, 이를 통해 $\hat{s} \models \hat{\phi} \implies s \models \phi$를 보장한다.

주요 기여

1. 실용적인 워크플로우: 상태 분할, 전이 구성, 퇴화된 동작 완화, 명세 리프팅을 하나의 건전한 프레임워크로 통합한 단일한 4단계 파이프라인을 제공한다.
2. 교체 가능한 서브루틴: 본 방법론은 전이 구성을 위한 다양한 접근 방식(AABB, Polytope, Sampling)과 퇴화된 동작 제거(CEвAR, Certified Erasure)를 지원하여, 사용자가 계산 비용과 추상화 정밀도 사이의 균형을 맞출 수 있게 한다.
3. 샘플링을 위한 PAC 보증: 분석적 과대 근사가 어려운 시스템을 위해, 데이터 기반 접근 방식을 도입하여 엄격한 확률적 커버리지 인증(Good-Turing 추정량 및 McAllester-Schapire 경계 활용)을 제공한다.
4. 퇴화 현상의 체계적 처리: 인증된 제거 및 CEGAR를 통해 가짜 셀프 루프와 전이를 명시적으로 처리함으로써, 일반적으로 보수적 추상화에서 발생하는 비관론을 방지한다.

실험 결과

저자들은 합성 선형 시스템, Mountain Car 벤치마크(비선형, 학습된 정책), 그리고 자율 유니사이클(Dubins 모델)의 세 가지 사례 연구를 통해 파이프라인을 평가하였다.

• 전이 구성: 샘플링 기반 방법은 특히 비선형 시스템에서 AABB 및 Polytope 방법과 비교했을 때, 더 적은 셀프 루프와 낮은 후속 상태 수 변동성을 가진 더 희소한(Sparser) 전이 관계를 생성했다. 이는 더 높은 참 양성률(True Positive Rate, TPR)로 이어졌다.
• 셀프 루프 제거: 셀프 루프를 제거하는 것은 검증 결과를 크게 개선했다. 유니사이클 사례의 경우, 제거 후 TPR이 약 0.19에서 0.63으로 증가했다. Mountain Car 사례에서는 TPR이 약 0.83에서 0.93으로 향상되었다.
• CEGAR: CEGAR는 모델 크기와 구축 시간을 상당히 증가시켰지만, 셀프 루프 비율(SLP)을 일관되게 감소시켰다. 이는 Mountain Car 시스템에서 뚜렷한 TPR 향상을 가져왔으나, 타겟팅된 제거 없이는 제거하기 어려운 사소한 반례들로 인해 유니사이클 시스템에서는 영향이 미미했다.
• 정밀도(Granularity): 더 미세한 상태 공간 정밀도는 일관되게 더 높은 TPR을 나타냈으며, 이는 모델 크기와 검증 정확도 사이의 트레이드오프를 확인시켜 주었다.

의의

본 논문은 CPS를 위한 추상화를 구축하는 엔지니어와 연구자들을 위한 실용적 가이드로서의 의의를 갖는다. 저자들은 다음과 같은 방식으로 이론적 추상화 기법과 실제 구현 사이의 간극을 메운다:

• 건전하지 않은 검증을 초래하는 일반적인 오류를 방지하는 구성 과정에서 건전한(Sound-by-construction) 워크플로우를 제공한다.
• 사용자가 시스템 복잡도와 가용 계산 자원에 따라 결정론적(AABB/Polytope) 방법과 확률적(Sampling) 방법 중 선택할 수 있도록 모듈형 도구를 제공한다.
• 퇴화된 동작(가짜 전이 및 셀프 루프)을 완화하는 것이 단순한 최적화가 아니라, 특히 생존성(Liveness) 속성에 대해 의미 있는 검증 결과를 얻기 위한 필수 단계임을 입증한다.

저자들은 심볼릭 모델 체킹이 강력한 도구이지만, 그 효용성은 전적으로 추상의 품질에 달려 있다고 결론짓는다. 본 워크플로우는 비관론과 실행 가능성 사이의 균형을 맞추면서 그러한 품질을 달성할 수 있는 엄격하고 적응 가능한 프레임워크를 제공한다.