IA169 System Verification and Assurance
Verification of Systems with Probabilities
Vojtěch Řehák
Jiří Barnat
Motivation Example
Fail-repair system
idle working done
repair error
start end
bug
service
ok
reset
What are the properties of the model?
G(working =⇒ F done)
G(working =⇒ F error)
FG(working ∨ error ∨ repair)
IA169 System Verification and Assurance – 10 2/28
Motivation Example
Fail-repair system
idle working done
repair error
start end
bug
service
ok
reset
What are the properties of the model?
G(working =⇒ F done) NO
G(working =⇒ F error)
FG(working ∨ error ∨ repair)
IA169 System Verification and Assurance – 10 2/28
Motivation Example
Fail-repair system
idle working done
repair error
start end
bug
service
ok
reset
What are the properties of the model?
G(working =⇒ F done) NO
G(working =⇒ F error) NO
FG(working ∨ error ∨ repair)
IA169 System Verification and Assurance – 10 2/28
Motivation Example
Fail-repair system
idle working done
repair error
start end
bug
service
ok
reset
What are the properties of the model?
G(working =⇒ F done) NO
G(working =⇒ F error) NO
FG(working ∨ error ∨ repair) NO
IA169 System Verification and Assurance – 10 2/28
Motivation Example
Fail-repair system
idle working done
repair error
start
0.95
end
bug
0.05
service
ok
reset
What is the probability of reaching “done” from “working”
with no visit of “error”?
with at most one visit of “error”?
with arbitrary many visits of “error”?
IA169 System Verification and Assurance – 10 3/28
Motivation Example
Fail-repair system
idle working done
repair error
start
0.95
end
bug
0.05
service
ok
reset
What is the probability of reaching “done” from “working”
with no visit of “error”? 0.95
with at most one visit of “error”?
with arbitrary many visits of “error”?
IA169 System Verification and Assurance – 10 3/28
Motivation Example
Fail-repair system
idle working done
repair error
start
0.95
end
bug
0.05
service
ok
reset
What is the probability of reaching “done” from “working”
with no visit of “error”? 0.95
with at most one visit of “error”? 0.95 + (0.05*0.95)
with arbitrary many visits of “error”?
IA169 System Verification and Assurance – 10 3/28
Motivation Example
Fail-repair system
idle working done
repair error
start
0.95
end
bug
0.05
service
ok
reset
What is the probability of reaching “done” from “working”
with no visit of “error”? 0.95
with at most one visit of “error”? 0.95 + (0.05*0.95)
with arbitrary many visits of “error”? 1
IA169 System Verification and Assurance – 10 3/28
Section
Discrete-time Markov Chains (DTMC)
IA169 System Verification and Assurance – 10 4/28
Probabilistic Models
Discrete-time Markov Chains (DTMC)
Standard modeling formalism for probabilistic systems.
A finite diagram of states and state-changing transitions.
Each transition is annotated with a probability p (p ∈ [0, 1]).
The probabilities over transitions from a single state sum to 1.
(They form discrete probability distribution.)
Observation
Markov property (“memoryless structure”) — only the current state
determines the successors (the past states are irrelevant).
Each state has at least one outgoing edge (“no deadlock”).
IA169 System Verification and Assurance – 10 5/28
DTMC Examples
Task: create DTMC modeling the following scenario
A queue for at most 4 items.
States of the graph encode how many items are enqueued.
Every transitions encodes that either an item has arrived in the
queue or one item has been consumed from the queue (exclusive or).
Arrival of an item happens with the probability of 1/3, while the
dequeue operation happens with the probability of 2/3.
Solution
IA169 System Verification and Assurance – 10 6/28
DTMC Examples
Task: create DTMC modeling the following scenario
A queue for at most 4 items.
States of the graph encode how many items are enqueued.
Every transitions encodes that either an item has arrived in the
queue or one item has been consumed from the queue (exclusive or).
Arrival of an item happens with the probability of 1/3, while the
dequeue operation happens with the probability of 2/3.
Solution
0 1 2 3 4
1/3 1/3 1/3 1/3
2/32/32/32/3
2/3 1/3
IA169 System Verification and Assurance – 10 6/28
DTMC examples
Task: create DTMC modeling the following scenario - continued
If the actions of item arrival and item removal are independent, they
both have their own probability of appearance with every time tick.
A new item comes with probability p = 1/2, an item is removed
with probability q = 2/3?
With every time tick, one of the actions may occur, both actions
may occur simultaneously, or none of them may occur at all.
Solution
IA169 System Verification and Assurance – 10 7/28
DTMC examples
Task: create DTMC modeling the following scenario - continued
If the actions of item arrival and item removal are independent, they
both have their own probability of appearance with every time tick.
A new item comes with probability p = 1/2, an item is removed
with probability q = 2/3?
With every time tick, one of the actions may occur, both actions
may occur simultaneously, or none of them may occur at all.
Solution
0 1 2 3 4
p p(1 − q) p(1 − q) p(1 − q)
qq(1 − p)q(1 − p)q(1 − p)
1 − p 1 − q
(1−p)(1−q)
+ pq
(1−p)(1−q)
+ pq
(1−p)(1−q)
+ pq
IA169 System Verification and Assurance – 10 7/28
DTMC – Formal Definition
Discrete-time Markov Chain is given by
a set of states S,
an initial state s0 of S,
a probability matrix P : S × S → [0, 1], and
an interpretation of atomic propositions I : S → AP.
IA169 System Verification and Assurance – 10 8/28
DTMC – Formal Definition
Discrete-time Markov Chain is given by
a set of states S,
an initial state s0 of S,
a probability matrix P : S × S → [0, 1], and
an interpretation of atomic propositions I : S → AP.
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







IA169 System Verification and Assurance – 10 8/28
Section
Property Specification
IA169 System Verification and Assurance – 10 9/28
Property specification languages
Recall some non-probabilistic specification languages:
LTL formulae
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | X ϕ | ϕ U ϕ
CTL formulae
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | EG ϕ
Syntax of CTL∗
state formula ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | E ψ
path formula ψ ::= ϕ | ¬ψ | ψ ∨ ψ | X ψ | ψ U ψ
IA169 System Verification and Assurance – 10 10/28
Property specification languages
We need to quantify probability that a certain behaviour will occur.
Probabilistic Computation Tree Logic (PCTL)
Syntax of PCTL
state formula ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | P bψ
path formula ψ ::= X ϕ | ϕ U ϕ | ϕ U≤k
ϕ
where
b ∈ [0, 1] is a probability bound,
∈ {≤, <, ≥, >}, and
k ∈ N is a bound on the number of steps.
IA169 System Verification and Assurance – 10 11/28
Property specification languages
We need to quantify probability that a certain behaviour will occur.
Probabilistic Computation Tree Logic (PCTL)
Syntax of PCTL
state formula ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | P bψ
path formula ψ ::= X ϕ | ϕ U ϕ | ϕ U≤k
ϕ
where
b ∈ [0, 1] is a probability bound,
∈ {≤, <, ≥, >}, and
k ∈ N is a bound on the number of steps.
A PCTL formula is always a state formula.
α U≤k
β is a bounded until saying that α holds until β within k steps.
For k = 3 it is equivalent to β ∨ (α ∧ X β) ∨ (α ∧ X (β ∨ α ∧ X β)).
Some tools also supports P=?ψ asking for the probability that the
specified behaviour will occur.
IA169 System Verification and Assurance – 10 11/28
PCTL examples
We can also use derived operators like G, F, ∧, ⇒, etc.
idle working done
repair error
1 0.95
0.05
1
1
1
Probabilistic reachability P≥1( F done )
probability of reaching the state done is equal to 1
Probabilistic bounded reachability P>0.99( F≤6 done )
probability of reaching the state done in at most 6 steps is > 0.99
Probabilistic until P<0.96( (¬error) U (done) )
probability of reaching done with no visit of error is less than 0.96
IA169 System Verification and Assurance – 10 12/28
Qualitative vs. quantitative properties
Qualitative PCTL properties
P b ψ where b is either 0 or 1
Quantitative PCTL properties
P b ψ where b ∈ (0, 1)
IA169 System Verification and Assurance – 10 13/28
Selected Qualitative PCTL Properties
In DTMC where zero probability edges are erased, it holds that
P>0( X ϕ) is equivalent to EX ϕ
there is a next state satisfying ϕ
P≥1( X ϕ) is equivalent to AX ϕ
the next states satisfy ϕ
P>0( F ϕ) is equivalent to EF ϕ
there exists a finite path to a state satisfying ϕ
but
P≥1( F ϕ) is not equivalent to AF ϕ
(see, e.g., AF done on our running example)
IA169 System Verification and Assurance – 10 14/28
Selected Qualitative PCTL Properties
In DTMC where zero probability edges are erased, it holds that
P>0( X ϕ) is equivalent to EX ϕ
there is a next state satisfying ϕ
P≥1( X ϕ) is equivalent to AX ϕ
the next states satisfy ϕ
P>0( F ϕ) is equivalent to EF ϕ
there exists a finite path to a state satisfying ϕ
but
P≥1( F ϕ) is not equivalent to AF ϕ
(see, e.g., AF done on our running example)
There is no CTL formula equivalent to P≥1( F ϕ),
and no PCTL formula equivalent to AF ϕ.
IA169 System Verification and Assurance – 10 14/28
Section
Analysis of Discrete-time Markov Chains
IA169 System Verification and Assurance – 10 15/28
DT Markov Chain Analysis - General Approaches
Transient analysis
probability distribution after k-steps
probability of reaching a state within k-steps
Long run analysis
states visited infinitely often with probability one
stationary (invariant) distribution
Model Checking
model checking DTMCs
model checking MDPs
IA169 System Verification and Assurance – 10 16/28
Section
Transient Analysis
IA169 System Verification and Assurance – 10 17/28
Quantitative - forward reachability
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







Probability distribution after k steps when starting in 1
IA169 System Verification and Assurance – 10 18/28
Quantitative - forward reachability
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







Probability distribution after k steps when starting in 1
1 0 0 0 0 × P = 0 1 0 0 0
IA169 System Verification and Assurance – 10 18/28
Quantitative - forward reachability
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







Probability distribution after k steps when starting in 1
1 0 0 0 0 × P = 0 1 0 0 0
1 0 0 0 0 × P2 = 0 0 0.05 0 0.95
IA169 System Verification and Assurance – 10 18/28
Quantitative - forward reachability
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







Probability distribution after k steps when starting in 1
1 0 0 0 0 × P = 0 1 0 0 0
1 0 0 0 0 × P2 = 0 0 0.05 0 0.95
1 0 0 0 0 × P3 = 0 0 0 0.05 0.95
IA169 System Verification and Assurance – 10 18/28
Quantitative - forward reachability
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







Probability distribution after k steps when starting in 1
1 0 0 0 0 × P = 0 1 0 0 0
1 0 0 0 0 × P2 = 0 0 0.05 0 0.95
1 0 0 0 0 × P3 = 0 0 0 0.05 0.95
1 0 0 0 0 × P4 = 0 0.05 0 0 0.95
IA169 System Verification and Assurance – 10 18/28
Quantitative - forward reachability
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







Probability distribution after k steps when starting in 1
1 0 0 0 0 × P = 0 1 0 0 0
1 0 0 0 0 × P2 = 0 0 0.05 0 0.95
1 0 0 0 0 × P3 = 0 0 0 0.05 0.95
1 0 0 0 0 × P4 = 0 0.05 0 0 0.95
1 0 0 0 0 × P5 = 0 0 0.0025 0 0.9975
IA169 System Verification and Assurance – 10 18/28
Quantitative - backward reachability
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







Prob. of being in states 2 or 5 after k steps, i.e. P=?F=k(2 ∨ 5)
IA169 System Verification and Assurance – 10 19/28
Quantitative - backward reachability
1 2 5
4 3
1 0.95
0.05
1
1 1
P =







0 1 0 0 0
0 0 0.05 0 0.95
0 0 0 1 0
0 1 0 0 0
0 0 0 0 1







Prob. of being in states 2 or 5 after k steps, i.e. P=?F=k(2 ∨ 5)
P × 0 1 0 0 1
T
= 1 0.95 0 1 1
T
P2 × 0 1 0 0 1
T
= 0.95 0.95 1 0.95 1
T
P3 × 0 1 0 0 1
T
= 0.95 1 0.95 0.95 1
T
P4 × 0 1 0 0 1
T
= 1 0.9975 0.95 1 1
T
P5 × 0 1 0 0 1
T
= 0.9975 0.9975 1 0.9975 1
T
IA169 System Verification and Assurance – 10 19/28
Unbounded reachability
Unbounded reachability
Let p(s, A) be the probability of reaching a state in A from s.
Observation: It holds that:
p(s, A) = 1 for s ∈ A
p(s, A) = s ∈succ(s) P(s, s ) ∗ p(s , A) for s ∈ A
where succ(s) is a set of successors of s and P(s, s ) is the
probability on the edge from s to s .
Theorem
The minimal non-negative solution of the above equations
equals to the probability of unbounded reachability.
IA169 System Verification and Assurance – 10 20/28
"Up to" reachability
Task
For the given DTMC compute the probability of reaching
state 3 within 6 steps.
Compute P=? F≤6 3.
1 2 5
4 3
1 0.95
0.05
1
1 1
Wrong Solution
BEWARE!
We cannot sum the probabilities of repeated visits!
P=? F≤6
3 =
6
i=0
P=? F=i
3
IA169 System Verification and Assurance – 10 21/28
"Up to" reachability – continued
Possible Solution 1
We may only sum the probabilities if we make sure, that no
revisit of a state is possible.
We have to modify the DTMC.
P=? F≤6 3 = 6
i=0 P=? F=i 3
1 2 5
T 3
1 0.95
0.05
1
1
1
Possible Solution 2
Alternativelly, we can make the target state absorbing.
P=? F≤6 3 = P=? F=6 3
1 2 5
4 3
1 0.95
0.05
1 1
1
IA169 System Verification and Assurance – 10 22/28
Section
Long Run Analysis
IA169 System Verification and Assurance – 10 23/28
Long run analysis
1 2 5
4 3
1 0.95
0.05
1
1 1
Recall that we reach the state 5(done) with probability 1.
IA169 System Verification and Assurance – 10 24/28
Long run analysis
1 2 5
4 3
1 0.95
0.05
1
1 1
Recall that we reach the state 5(done) with probability 1.
1 2 5
4 3
1 0.95
0.05
1
1
0.5
0.5
What are the states visited infinitely often with probability 1?
IA169 System Verification and Assurance – 10 24/28
States visited infinitely often
Decompose the graph
representation onto
strongly connected
components.
1
This holds only in DTMC models with finitely many states.
IA169 System Verification and Assurance – 10 25/28
States visited infinitely often
Decompose the graph
representation onto
strongly connected
components.
Theorem 1
A state is not visited or visited infinitely often with
probability 1 if and only if it is in a bottom strongly
connected component.
All other states are visited finitely many times with
probability 1.
1
This holds only in DTMC models with finitely many states.
IA169 System Verification and Assurance – 10 25/28
Frequency of visits
How often is a state visited
among the states visited
infinitely many times?
1 2 5
4 3
1 0.95
0.05
1
1
0.5
0.5
Theorem
limn→∞E
# visits of state i during the first n steps
n
= πi
where π is a so called stationary (or steady-state or invariant or
equilibrium) distribution satisfying π × P = π.
IA169 System Verification and Assurance – 10 26/28
Section
DTMC Extensions
IA169 System Verification and Assurance – 10 27/28
Markov Decision Processes
Markov Decision Processes (MDP)
Extends DTMC with non-determinism.
For a given state, there is a choice of probability distribution
we may use to proceed to the next state (non-deterministic
choice of action, every action represents one probability
distribution over the successors).
Model Checking MDPs
Satisfaction of a property ranges between Pmin and Pmax
depending on the resolution of the non-determinism.
By resolving the non-determinism in MDP we get DTMC.
PRISM – Probabilistic model checker
Other DTMC, MDP Extensions
Rewards
Partial observability
IA169 System Verification and Assurance – 10 28/28