Sciweavers

DSN
2004
IEEE

Model Checking Action- and State-Labelled Markov Chains

13 years 7 months ago
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.
Christel Baier, Lucia Cloth, Boudewijn R. Haverkor
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where DSN
Authors Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Matthias Kuntz, Markus Siegle
Comments (0)