*For the most recent entries see the
Petri Nets Newsletter.*

## Model Checking Markov Chains with Actions and State Labels.

Baier, Christel;
Cloth, Lucia;
Haverkort, Boudewijn R.;
Kuntz, Matthias;
Siegle, Markus
In:
*IEEE Transactions on Software Enginering, Volume 33, 04*, pages 209-224.
2007.

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 asCSL 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.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*