In this paper we present a stochastic extension of the modal logic PDL (propositional dynamic logic), SPDL, that is interpreted over labelled continuous time Markov chains (CTMC). We define the syntax and semantics of SPDL. SPDL provides, like PDL, powerful means to specify path properties. In general paths can be characterised by regular expressions, where the executability of a regular expression can depend on the validity of guard or test formulae. Such regular expressions enriched with test formulae are called programs. In order to model check SPDL path formulae it is necessary to derive from the programs a variant of deterministic finite automata and to build the product automaton between the labelled CTMC and this automaton. We describe two different ways to model check SPDL, at first via solving an integral equation system and secondly by transient analysis. We show that a variant of Markov bisimulation preserves the validity of SPDL formulae, finally we give the worst case complexity for model checking SPDL formulae by means of uniformisation.     «

In this paper we present a stochastic extension of the modal logic PDL (propositional dynamic logic), SPDL, that is interpreted over labelled continuous time Markov chains (CTMC). We define the syntax and semantics of SPDL. SPDL provides, like PDL, powerful means to specify path properties. In general paths can be characterised by regular expressions, where the executability of a regular expression can depend on the validity of guard or test formulae. Such regular expressions enriched with...    »