Verification of Parametric Markov Automata under Time-bounded Reachability

기술 요약: 시간 제한적 도달 가능성 하에서의 파라메트릭 마르코프 오토마타 검증

문제 정의
마르코프 오토마타(MA)는 비결정론적이고 연속적인 시간을 갖는 확률적 시스템을 위한 구성적 모델로, 일반화된 확률적 페트리 넷(Generalized Stochastic Petri Nets) 및 동적 결함 트리(Dynamic Fault Trees)와 같은 모델의 의미론 역할을 합니다. 그러나 기존의 모델 체킹 알고리즘은 모든 전이율과 확률이 정확하게 알려진 완전 지정된 모델을 필요로 합니다. 이러한 가정은 매개변수가 환경적 불확실성이나 미지의 상태에 놓일 수 있는 실제 시스템에서는 실현 불가능한 경우가 많습니다.

본 논문은 전이율과 확률적 후속 분포가 고정된 상수가 아닌 파라메트릭 함수로 정의되는 **파라메트릭 마르코프 오토마타(pMA)**의 검증 문제를 다룹니다. 저자들은 시간 제한적 도달 가능성 속성(예: "시간 $t$ 이내에 목표 상태에 도달할 확률이 $\theta$ 보다 큰가?")에 초점을 맞춥니다. 두 가지 특정 문제가 다뤄집니다:

1. 만족 검증(Satisfaction Verification): 주어진 영역 내에 속성을 만족하거나 위반하는 매개변수 값(valuation)이 존재하는지 결정합니다.
2. 합성(Synthesis): 매개변수 공간을 속성을 만족하는 영역과 속성을 위반하는 영역으로 분할합니다.

분석은 시스템의 스케줄러(비결정론적 선택을 수행)와 "자연"(매개변수 값을 할당) 사이의 상호작용에 기초한 네 가지 구별된 만족 관계(Feasibility, Angelic-aid, Robust, Demonic)를 고려해야 합니다.

방법론
제안된 접근 방식은 연속적인 파라메트릭 모델을 기존의 합성 기술에 적합한 이산 모델로 변환하는 2단계 과정을 통해 이 문제들을 해결하며, 이 과정에서 도입된 오차를 제한합니다.

1. 이산화 및 변환:

   • pMA는 먼저 단계 크기 $\delta$를 사용하여 이산화되어, 연속 시간 모델을 **파라메트릭 마르코프 결정 과정(pMDP)**으로 변환합니다. 이 단계는 비파라메트릭 MA에 대한 기존의 이산화 결과를 일반화합니다.
   • 시간 경과 없이 발생하는 확률적 상태(Probabilistic States, PS)의 즉각적인 전이를 처리하기 위해, 저자들은 상태 제거(state-elimination) 기법을 사용하여 PS를 마르코프 상태(Markovian States, MS)로 병합하고, 이를 통해 모델을 표준적인 pMDP 상의 단계 제한적 도달 가능성 문제로 변환합니다.
   • 이산화가 심볼릭 매개변수 합성에 다루기 어려운 지수 항($e^{-\lambda \delta}$)을 도입하므로, 저자들은 이 항들을 **부분 테일러 전개(partial Taylor expansions)**를 사용하여 근사합니다. 이를 통해 전이 확률이 유리스 함수(rational functions)로 표현되고 상한 및 하한에 의해 제한되는 "근사 이산화 pMA"를 얻습니다.

2. 매개변수 리프팅(Parameter Lifting, PL) 및 검증:

   • 변환된 pMDP는 **매개변수 리프팅(PL)**을 통해 분석됩니다. 이 기법은 매개변수 선택을 확률적 게임 내의 두 번째 플레이어인 "자연"의 비결정론적 선택으로 취급함으로써 상태 간 의존성을 추상화합니다.
   • PL 방법은 도달 가능 확률의 상한과 하한을 계산합니다. 이 경계값들은 사용자가 지정한 임계값 $\theta$와 비교됩니다.
   • 이 접근 방식은 정교화(refinement) 체계를 활용합니다: 만약 경계값이 결정적이지 않다면(즉, 구간이 임계값을 가로지르는 경우), 매개변수 영역을 분할하고 과정을 반복합니다.
   • 총 오차는 세 가지 항, 즉 이산화 오차($\epsilon_\delta$), 테일러 근사로 인한 오차, 그리고 PL 추상화로 인해 도입된 오차에 의해 제어됩니다. 저자들은 이산화 오차가 지배적인 요인임을 입증합니다.

주요 기여

• pMA의 정의: 본 논문은 전이율 및 확률 함수를 파라메트릭하게 확장한 pMA를 공식적으로 도입합니다.
• 시간 제한적 도달 가능성 알고리즘: 저자들은 시간 제한적 제약 조건 하에서 pMA의 만족 검증 및 매개변수 합성을 수행할 수 있는 최초의 알고리즘을 제시합니다.
• 일반화된 이산화: Guck 등[17]의 이산화 결과를 파라메트릭 설정으로 일반화하여, 이산화된 pMA가 실제 pMA의 도달 가능 확률을 경계 지음을 증명합니다.
• 근사 이산화: 유리스 함수 기반의 합성을 가능하게 하기 위해 테일러 전개를 사용하여 이산화 모델의 지수 항을 처리하는 방법을 도입합니다.
• 구현: 이 접근 방식은 Storm 모델 체커(Stormpy 인터페이스를 통해)로 구현되었으며, pMA와 파라메트릭 CTMC를 모두 지원합니다.

실험 결과
저자들은 flexible-manufacturing, polling, kanban과 같은 QCOMP 벤치마크 세트의 모델들을 포함한 벤치마크 제품군을 통해 구현을 평가했습니다.

• 검증: 만족 검증의 경우, 도구는 테스트된 모든 벤치마크에 대해 결정적인 답을 성공적으로 제공했으며, 종종 수 초 내에 완료되었습니다.
• 합성: 매개변수 합성을 위해, 도구는 작은 모델들에 대해 매개변수 공간을 성공적으로 분할했습니다. 그러나 더 크거나 복잡한 모델의 경우, 빈번하게 15분 타임아웃에 도달했습니다.
• 성능 병목 현의: 실험적 분석은 **이산화(discretization)**를 주요 성능 병목 현상으로 식별했습니다. 계산 비용은 이산화 단계 $\delta$가 감소하거나(오차를 줄이기 위해) 모델의 최대 체류율(sojourn rate)이 증가함에 따라 크게 증가합니다.
• 비교: 파라메트릭 CTMC에 대한 PRISM-PSY와 비교했을 때(PRISM-PSY는 이산화가 필요하지 않음), 제안된 방법이 더 느렸습니다. 그러나 제안된 방법은 PRISM-PSY가 실패하는 지점에서도 성공합니다. 즉, tandem 벤치마크와 같이 (단순히 전이율뿐만 아니라) 파라메트릭 전이 확률을 가진 pMA를 분석할 수 있습니다.

의의 및 주장
본 논문은 신뢰성 공학에서 널리 사용되지만 이전에는 완전 지정된 인스턴스로 제한되었던 모델 클래스인 마르코프 오토마타의 불확실성 분석을 가능하게 함으로써, 형식 검증의 간극을 메운다고 주장합니다. 저자들은 충분히 작은 이산화 단계를 제공한다면, 이 접근 방식이 임의의 정밀도까지 검증 및 합성을 해결할 수 있음을 강조합니다.

저자들은 확장성 문제에 대해 겸허한 태도를 유지하며, 현재의 구현이 이산화 비용에 의해 제한된다는 점을 인정합니다. 그들은 성능 병목 현상의 주된 원인이 pMA의 이산화에서 비롯된다고 명시적으로 밝힙니다. 따라서 향-연구로서 이산화를 완전히 피하는 접근 방식, 예를 들어 연속 시간 확률 게임을 직접 분석하거나 유니포미제이션(uniformization) 기법을 활용하는 방안을 조사할 것을 제안하지만, 이러한 대안들이 자체적인 계산적 어려움을 초래할 수 있음도 언급합니다. 이 연구는 연속 시간 비결정론적 시스템의 파라메트릭 분석을 위한 기초적인 프레임워크를 구축하며, 기존의 Storm과 같은 도구의 능력을 더 넓은 범위의 모델에서 파라메트릭 불확실성을 다룰 수 있도록 확장합니다.