IA169 System Verification and Assurance
Verification of Systems with Probabilities
Vojtěch Řehák
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/25
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”?
What is the probability of reaching “done” from “working” with at
most one visit of “error”?
What is the probability of reaching “done” from “working”?
IA169 System Verification and Assurance – 10 3/25
Section
Discrete-time Markov Chains (DTMC)
IA169 System Verification and Assurance – 10 4/25
Probabilistic models
Discrete-time Markov Chains (DTMC)
Standard model for probabilistic systems.
State-based model with probabilities on branching.
Based on the current state, the succeeding state is given by a
discrete probability distribution.
Markov property (“memorylessness”) — only the current state
determines the successors (the past states are irrelevant).
Probabilities on outgoing edges sums to 1 for each state.
Hence, each state has at least one outgoing edge (“no deadlock”).
IA169 System Verification and Assurance – 10 5/25
DTMC examples
Model of a queue
0 1 2 3 4
1/3 1/3 1/3 1/3
2/32/32/32/3
2/3 1/3
Queue for at most 4 items. In every time tick, a new item comes with
probability 1/3 and an item is consumed with probability 2/3.
What if a new item comes with probability p = 1/2 and an item is
consumed with probability q = 2/3?
IA169 System Verification and Assurance – 10 6/25
DTMC examples
Model of the new queue
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/25
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/25
Back to our questions
Fail-Repair System
idle working done
repair error
1 0.95
0.05
1
1
1
What is the probability of reaching “done” from “working”
with no visit of “error”?
What is the probability of reaching “done” from “working”
with at most one visit of “error”?
What is the probability of reaching “done” from “working”?
IA169 System Verification and Assurance – 10 9/25
Markov chain analysis
Transient analysis
distribution after k-steps
reaching/hitting probability
hitting time
Long run analysis
probability of infinite hitting
stationary (invariant) distribution
mean inter visit time
long run limit distribution
IA169 System Verification and Assurance – 10 10/25
Section
Property Specification
IA169 System Verification and Assurance – 10 11/25
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 12/25
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 13/25
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 14/25
Qualitative vs. quantitative properties
Qualitative PCTL properties
P b ψ where b is either 0 or 1
Quantitative PCTL properties
P b ψ where b is in (0, 1)
IA169 System Verification and Assurance – 10 15/25
Qualitative 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 16/25
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 17/25
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 18/25
"Up to" reachability
Computing P=? F≤6 3.
Is it 6
i=0 P=? F=i 3 ? 1 2 5
4 3
1 0.95
0.05
1
1 1
No, we are summing probabilities of repeated visits.
It is true when the model is changed such that repeated visits are
not possible. Alternativelly, we can make the target state
absorbing.
1 2 5
T 3
1 0.95
0.05
1
1
1
and it is 6
i=0 P=? F=i 3
1 2 5
4 3
1 0.95
0.05
1 1
1
and it is P=? F=6 3
IA169 System Verification and Assurance – 10 19/25
Unbounded reachability - optional slide
Unbounded reachability
Let p(s, A) be the probability of reaching a state in A from s.
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/25
Section
Long Run Analysis
IA169 System Verification and Assurance – 10 21/25
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 22/25
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 23/25
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 24/25
DTMC extensions - communication and nondeterminism
Last remark on some DTMC extensions.
Modules and synchronisation
modules
actions
rewards
Decision extension
Markov Decision Processes (MDP)
Pmin and Pmax properties
IA169 System Verification and Assurance – 10 25/25