Model Checking Action- and State-Labelled Markov Chains

Christel BaierChristel Baier, Lucia ClothLucia Cloth, Boudewijn R. HaverkortBoudewijn R. Haverkort, Matthias KuntzMatthias Kuntz, Markus SiegleMarkus Siegle

DOI Link

Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Matthias Kuntz, Markus Siegle
Model Checking Action- and State-Labelled Markov Chains
International Conference on Dependable Systems and Networks (DSN), 701--710, 2004. IEEE Computer Society

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BCHKS2004,
  author    = {Christel Baier and Lucia Cloth and Boudewijn R. Haverkort and
               Matthias Kuntz and Markus Siegle},
  title     = {Model Checking Action- and State-Labelled Markov Chains},
  booktitle = {International Conference on Dependable Systems and Networks (DSN)},
  publisher = {IEEE Computer Society},
  year      = {2004},
  pages     = {701--710},
  doi       = {10.1109/DSN.2004.1311941}
}