Model Checking Markov Chains with Actions and State Labels
Baier, Christel and Cloth, Lucia and Haverkort, Boudewijn R. and Kuntz, Matthias and Siegle, Markus (2007) Model Checking Markov Chains with Actions and State Labels. IEEE Transactions on Software Engineering, 33 (4). pp. 209224. ISSN 00985589

PDF
2MB 
Abstract:  In the past, logics of several kinds have been proposed for reasoning about discrete or continuoustime 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 stateproperties and actionsequences. 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 statebased logic asCSL (continuous stochastic logic).
In asCSL, path properties are characterized by regular expressions over actions and stateformulas. Thus, the truth value of pathformulas 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 statebased fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automatonbased 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 asCSLformulas, and checked using the new procedure. 
Item Type:  Article 
Additional information:  Protocol verification, performance of systems, model checking, automata, Markov processes 
Copyright:  © 2007 IEEE 
Faculty:  Electrical Engineering, Mathematics and Computer Science (EEMCS) 
Research Group:  
Link to this item:  http://purl.utwente.nl/publications/66558 
Official URL:  http://dx.doi.org/10.1109/TSE.2007.36 
Export this item as:  BibTeX EndNote HTML Citation Reference Manager 
Repository Staff Only: item control page
Metis ID: 241568