DocumentCode :
1226147
Title :
Model Checking Markov Chains with Actions and State Labels
Author :
Baier, Christel ; Cloth, Lucia ; Haverkort, Boudewijn R. ; Kuntz, Matthias ; Siegle, Markus
Author_Institution :
Inst. for Theor. Comput. Sci., Technische Univ. Dresden
Volume :
33
Issue :
4
fYear :
2007
fDate :
4/1/2007 12:00:00 AM
Firstpage :
209
Lastpage :
224
Abstract :
In the past, logics of several kinds have been proposed for reasoning about discrete-time 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 as CSL which provides a 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 CSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state formulas. Thus, the truth value of path formulas depends not only 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 with 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 :
Markov processes; automata theory; formal verification; temporal logic; Markov chain; automaton-based technique; continuous stochastic logic; model checking; regular expression; state label; transition label; Algebra; Automata; Embedded system; Law; Legal factors; Markov processes; Petri nets; Power system modeling; Probabilistic logic; Stochastic processes; Markov processes.; Protocol verification; automata; model checking; performance of systems;
fLanguage :
English
Journal_Title :
Software Engineering, IEEE Transactions on
Publisher :
ieee
ISSN :
0098-5589
Type :
jour
DOI :
10.1109/TSE.2007.36
Filename :
4123324
Link To Document :
بازگشت