loading...
Model Checking Action- and State-Labelled Markov Chains
Florence, Italy June 28-July 01
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DSN.2004.13119412004 International Conference on Depe ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Christel Baier, Universit?t Bonn
Lucia Cloth, University of Twente
Boudewijn Haverkort, University of Twente
Matthias Kuntz, University of the Federal Armed Forces Munich
Markus Siegle, University of the Federal Armed Forces Munich
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.
Citation:
Christel Baier, Lucia Cloth, Boudewijn Haverkort, Matthias Kuntz, Markus Siegle, "Model Checking Action- and State-Labelled Markov Chains," dsn, pp.701, 2004 International Conference on Dependable Systems and Networks (DSN'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions