Model checking action- and state-labelled Markov chains

In this paper we introduce the logic asCSL, an extension of continuous stochastic logic (CSL), which provides powerful means to characterise execution paths of action- and state-labelled Markov chains. In asCSL, path properties are characterised by regular expressions over actions and state-formulas. Thus, the executability of a path not only depends on the available actions but also on the validity of certain state formulas in intermediate states. Our main result is that the model checking problem for asCSL can be reduced to CSL model checking on a modified Markov chain, which is obtained through a product automaton construction. We provide a case study of a scalable cellular phone system which shows how the logic asCSL and the model checking procedure can be applied in practice.