Stochastic Model Checking
by Marta Kwiatkowska, Gethin Norman, David Parker
Section 4: Model Checking Continuous Time Markov Chains The CTMC Model
Subsection 4.1: Paths and Probability Measures of Paths Paths
Cylinder sets
Probability measure (on paths)
Subsection 4.2: Steady-State and Transient Behaviour
We just introduced path probabilities in Subsection 4.1 We now introduce two additional notions:
- transient probabilites - steady state probabilities
Transient probability:
Steady-state probability:
Subsection 4.3: Continuous Stochastic Logic (CSL) Syntax
Semantics
Derived Operators (actually definitions)
Transient probabilities can be expressed using steady state:
Examples:
Subsection 4.5: CTMC and CSL with Rewards
Introducing rewards (or costs) give us the ability to determine quantitative aspects of the behaviour of systems.
A reward structure for a CTMC D=(S,s,R,L) has two components:
the state reward (or cumulative reward) gives the cost of staying in a given state measured per time unit
the transition reward (or instantaneous or impulse reward) gives the cost of a transition from one state to another
This definition is almost as for DTMC and PCTL.
Example Reward Structures
Extensions of CSL with Rewards Syntax
Semantics
Examples
Subsection 4.4 (& 4.5): CSL Model Checking (with rewards) The overall process is as for PCTL - but details differ and will not be covered here
Simple Example: Model Checking on C
observe that the formula does not talk about real-time hence the formula can be modelled checked using the embedded DTMC emb(C)
Subsection 4.6: Complexity of CSL Model Checking
