2020/08/24 by Nathalie Bertrand, Patricia Bouyer, Bertrand, Nathalie +6
Computer Science · Engineering · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling #Safety Systems Engineering in Autonomy
paper · pdf · doi:10.48550/arxiv.2008.10426
openalex publication_date 2020/08/24 · openalex created_date 2022/07/26 · openalex updated_date 2026/07/28
Markov chains and Markov decision processes (MDPs) are well-established probabilistic models. While finite Markov models are well-understood, analysing their infinite counterparts remains a significant challenge. Decisiveness has proven to be an elegant property for countable Markov chains: it is general enough to be satisfied by several natural classes of countable Markov chains, and it is a sufficient condition for simple qualitative and approximate quantitative model-checking algorithms to exist. In contrast, existing works on the formal analysis of countable MDPs usually rely on ad hoc techniques tailored to specific classes. We provide here a general framework to analyse countable MDPs by extending the notion of decisiveness. Compared to Markov chains, MDPs exhibit extra non-determinism that can be resolved in an adversarial or cooperative way, leading to multiple natural notions of decisiveness. We show that these notions enable the approximation of reachability and safety probabilities in countable MDPs using simple model-checking procedures. We then instantiate our generic approach to two concrete classes of models inducing countable MDPs: non-deterministic probabilistic lossy channel systems and partially observable MDPs. This leads to an algorithm to approximately compute safety probabilities in each of these classes.