Compositional Verification of Almost-Sure Büchi Objectives in MDPs

This paper studies the verification of almost-sure Büchi 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üchi 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üchi state are a sufficient and necessary statistic for the compositional verification of almost-sure Büchi 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.