Model Checking Algorithms for Markov Automata
Hassan Hatefi, Holger Hermanns · Technische Universität Berlin – Universitätsbibliothek · 2024
Markov automata constitute a compositional modeling formalism spanning as special cases the models of discrete and continuous time Markov chains, as well as interactive Markov chains and probabilistic automata. This paper discusses the core algorithmic ingredients of a numerical model checking procedure for Markov automata with respect to a PCTL or CSL like temporal logic. The main challenge lies in the computation of time-bounded reachability probabilities, for which we provide a stable approximation scheme.