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

2025/08/18 by van der Vegt, Marck, Watanabe, Kazuki, Hasuo, Ichiro +1
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2508.13087

Abstract

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.

Citations

• Pareto Fronts for Compositionally Solving String Diagrams of Parity Games
• Tools at the Frontiers of Quantitative Verification
• Compositional Value Iteration with Pareto Caching
• Composing Reinforcement Learning Policies, with Formal Guarantees
• Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
• Compositional Probabilistic Model Checking with String Diagrams of MDPs
• Compositional Solution of Mean Payoff Games by String Diagrams
• A Practitioner's Guide to MDP Model Checking Algorithms
• Abstraction-Refinement for Hierarchical Probabilistic Models
• Verifiable and Compositional Reinforcement Learning Systems
• Hierarchical Solution of Markov Decision Processes using Macro-actions

Related

• Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
• Compositional Value Iteration with Pareto Caching
• Modular Mix-and-Match Complementation of Büchi Automata (Technical Report)
• Compositional Probabilistic Model Checking with String Diagrams of MDPs
• Advanced Automata Minimization