Compositional Verification of Almost-Sure B\"uchi Objectives in MDPs
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.
Cite
@article{arxiv.2508.13087,
title = {Compositional Verification of Almost-Sure B\"uchi Objectives in MDPs},
author = {Marck van der Vegt and Kazuki Watanabe and Ichiro Hasuo and Sebastian Junges},
journal= {arXiv preprint arXiv:2508.13087},
year = {2025}
}