Model Checking Algorithms for Markov Automata

Abstract

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.