Model Checking Markov Chains with Actions and State Labels

Christel Baier, L. Cloth, Boudewijn R.H.M. Haverkort, G.W.M. Kuntz, Markus Siegle

Research output: Contribution to journalArticleScientificpeer-review

Abstract

In the past, logics of several kinds have been proposed for reasoning about discrete- or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state-properties and action-sequences. For this purpose, we introduce the logic asCSL which provides powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic asCSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state-formulas. Thus, the truth value of path-formulas does not only depend on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated by through an elaborate model of a scalable cellular communication system for which several properties are formalized by means of asCSL-formulas, and checked using the new procedure.
Original languageEnglish
Pages (from-to)209-224
Number of pages16
JournalIEEE Transactions on Software Engineering
Volume33
Issue number1/4
DOIs
Publication statusPublished - 2007
Externally publishedYes

Fingerprint

Model checking
Markov processes
Labels
Cellular radio systems
Communication systems

Keywords

  • IR-66558
  • EWI-7867
  • METIS-241568

Cite this

Baier, Christel ; Cloth, L. ; Haverkort, Boudewijn R.H.M. ; Kuntz, G.W.M. ; Siegle, Markus. / Model Checking Markov Chains with Actions and State Labels. In: IEEE Transactions on Software Engineering. 2007 ; Vol. 33, No. 1/4. pp. 209-224.
@article{ea2eb9b6e36043b68a60b26c9128f47c,
title = "Model Checking Markov Chains with Actions and State Labels",
abstract = "In the past, logics of several kinds have been proposed for reasoning about discrete- or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state-properties and action-sequences. For this purpose, we introduce the logic asCSL which provides powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic asCSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state-formulas. Thus, the truth value of path-formulas does not only depend on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated by through an elaborate model of a scalable cellular communication system for which several properties are formalized by means of asCSL-formulas, and checked using the new procedure.",
keywords = "IR-66558, EWI-7867, METIS-241568",
author = "Christel Baier and L. Cloth and Haverkort, {Boudewijn R.H.M.} and G.W.M. Kuntz and Markus Siegle",
note = "Imported from research group DACS (ID number 429) M1 - 10.1109/TSE.2007.36",
year = "2007",
doi = "10.1109/TSE.2007.36",
language = "English",
volume = "33",
pages = "209--224",
journal = "IEEE Transactions on Software Engineering",
issn = "0098-5589",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
number = "1/4",

}

Model Checking Markov Chains with Actions and State Labels. / Baier, Christel; Cloth, L.; Haverkort, Boudewijn R.H.M.; Kuntz, G.W.M.; Siegle, Markus.

In: IEEE Transactions on Software Engineering, Vol. 33, No. 1/4, 2007, p. 209-224.

Research output: Contribution to journalArticleScientificpeer-review

TY - JOUR

T1 - Model Checking Markov Chains with Actions and State Labels

AU - Baier, Christel

AU - Cloth, L.

AU - Haverkort, Boudewijn R.H.M.

AU - Kuntz, G.W.M.

AU - Siegle, Markus

N1 - Imported from research group DACS (ID number 429) M1 - 10.1109/TSE.2007.36

PY - 2007

Y1 - 2007

N2 - In the past, logics of several kinds have been proposed for reasoning about discrete- or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state-properties and action-sequences. For this purpose, we introduce the logic asCSL which provides powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic asCSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state-formulas. Thus, the truth value of path-formulas does not only depend on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated by through an elaborate model of a scalable cellular communication system for which several properties are formalized by means of asCSL-formulas, and checked using the new procedure.

AB - In the past, logics of several kinds have been proposed for reasoning about discrete- or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state-properties and action-sequences. For this purpose, we introduce the logic asCSL which provides powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic asCSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state-formulas. Thus, the truth value of path-formulas does not only depend on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated by through an elaborate model of a scalable cellular communication system for which several properties are formalized by means of asCSL-formulas, and checked using the new procedure.

KW - IR-66558

KW - EWI-7867

KW - METIS-241568

U2 - 10.1109/TSE.2007.36

DO - 10.1109/TSE.2007.36

M3 - Article

VL - 33

SP - 209

EP - 224

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

SN - 0098-5589

IS - 1/4

ER -