무한 상태 네트워크의 정량적 검증

많은 네트워크 프로토콜과 분산 시스템은 재귀성(recursion), 무한 로컬 상태(unbounded local state), 그리고 비용(cost), 지연 시간(latency), 또는 신뢰성(reliability)과 같은 정량적 동작을 결합합니다. 푸시다운 시스템(pushdown systems)의 네트워크에 대한 기존 결정 가능성 결과는 대체로 정성적이며, 트레이스(traces)와 가중치(weights)를 공동으로 추적해야 하는 정량적 분석까지 확장되지 못하고 있습니다. 본 논문에서는 가중치가 부여된 푸시다운 시스템의 비순환(acyclic) 네트워크에 대한 정량적 검증 프레임워크를 제시합니다. 재귀적인 네트워크 구성 요소를 유한하게 요약하려면, 그 중첩 루프(nested loops)를 펌핑하여 얻은 무한한 실행(runs) 계열을 붕괴시켜야 하는데, 이를 과대 근사(over-approximation)가 아닌 방식으로 extit{정확히} 수행하는 것이 오랜 난제였습니다. 본 논문에서는 이 작업이 가능한 가중치 도메인(weight domains)의 한 클래스를 제시합니다: 이러한 계열에 의해 축적된 가중치가 닫힌 형식으로 붕괴되는 '펌핑 반환 구조'(pumping semirings)입니다. 비공식적으로 말해, 해당 도메인은 반복 횟수를 셀 수 없어야 합니다. 이 클래스는 북극 반환 구조(arctic semiring)나 아래로 닫힌 언어(downward-closed languages)와 같이 무한 상승 사슬(infinite ascending chains)을 허용하는 도메인을 포함합니다. 본 논문에서는 이러한 도메인 위에서 정량적 도달 가능성(quantitative reachability)을 정확하게 계산하는 종료 알고리즘을 제공하며, 이는 두 가지 아이디어에 기반합니다: 실행의 구성적 표현인 세그먼트 트리 대수(segment tree algebras), 그리고 추가적인 가속이 여전히 정확하도록 가중치를 기호적으로 분리하는 열적 확장(thermal extensions)입니다. 우리는 이를 사용하여 문맥 자유 언어(context-free languages)의 상향 및 하향 폐포(upward and downward closures)를 균일하게 계산하고, 이 알고리즘을 '얇은'(thin) 펌핑 반환 구조를 갖는 비순환 네트워크로 확장하여 푸시다운 시스템 네트워크에 대한 최초의 정량적 안전성(safety) 및 도달 가능성 분석 결과를 얻었습니다.