# (15)Example Reward Structures (16)Extensions of CSL with Rewards Syntax (17)Semantics (18)Examples (19)Subsection 4.4 (&amp

## Full text

(1)

Stochastic Model Checking

by Marta Kwiatkowska, Gethin Norman, David Parker

Section 4: Model Checking Continuous Time Markov Chains The CTMC Model

(2)
(3)
(4)
(5)

Subsection 4.1: Paths and Probability Measures of Paths Paths

(6)

Cylinder sets

(7)

Probability measure (on paths)

(8)

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:

(9)

(10)

Subsection 4.3: Continuous Stochastic Logic (CSL) Syntax

(11)

Semantics

(12)

Derived Operators (actually definitions)

Transient probabilities can be expressed using steady state:

(13)

Examples:

(14)

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.

(15)

Example Reward Structures

(16)

Extensions of CSL with Rewards Syntax

(17)

Semantics

(18)

Examples

(19)

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)

(20)

Subsection 4.6: Complexity of CSL Model Checking

Updating...

## References

Related subjects :