Compositional Verification of Almost-Sure B\"uchi Objectives in MDPs

TL;DR

This paper introduces compositional methods for verifying almost-sure B"uchi objectives in Markov Decision Processes, providing algorithms that improve efficiency in complex systems with structured components.

Contribution

It establishes proper exit sets as a key statistic for compositional verification and presents two algorithms, including a polynomial-time iterative method, for verifying B"uchi objectives.

Findings

Proper exit sets are necessary and sufficient for verification.

The bottom-up algorithm computes verification recursively.

The iterative algorithm achieves polynomial-time complexity.

Abstract

This paper studies the verification of almost-sure B\"uchi objectives in MDPs with a known, compositional structure based on string diagrams. In particular, we ask whether there is a strategy that ensures that a B\"uchi objective is almost-surely satisfied. We first show that proper exit sets -- the sets of exits that can be reached within a component without losing locally -- together with the reachability of a B\"uchi state are a sufficient and necessary statistic for the compositional verification of almost-sure B\"uchi objectives. The number of proper exit sets may grow exponentially in the number of exits. We define two algorithms: (1) A straightforward bottom-up algorithm that computes this statistic in a recursive manner to obtain the verification result of the entire string diagram and (2) a polynomial-time iterative algorithm which avoids computing all proper exit sets by performing iterative strategy refinement.