IA169 System Verification and Assurance
LTL Model Checking
(continued)
Jiří Barnat
Model Checking – Schema
Requirements
Specification
Property
Formalization
System
System Model
Model Checking
Simulation
Counterexample
Invalid
Valid
ErrorModelling
IA169 System Verification and Assurance – 05 str. 2/46
Where are we now?
Property Specification
English text.
Formulae of Linear Temporal Logic.
System Description
Source code in programming language.
Source code in modelling language.
Kripke structure representing the state space.
Problem
Kripke structure M
LTL formula ϕ
M |= ϕ ?
IA169 System Verification and Assurance – 05 str. 3/46
Section
Automata-Based Approach to LTL Model Checking
IA169 System Verification and Assurance – 05 str. 4/46
Languages of infinite words
Observation One
System is a set of (infinite) runs.
Also referred to as formal language of infinite words.
Observation Two
Two different runs are equal with respect to an LTL
formula if they agree in the interpretation of atomic
propositions (need not agree in the states).
Let π = s0, s1, . . ., then I(π)
def
⇐⇒ I(s0), I(s1), I(s2), . . ..
Observation Three
Every run either satisfies an LTL formula, or not.
Every LTL formula defines a set of satisfying runs.
IA169 System Verification and Assurance – 05 str. 5/46
Reduction to Language Inclusion
Reformulation as Language Problem
Let Σ = 2AP
be an alphabet.
Language Lsys of all runs of system M is defined as
follows.
Lsys = {I(π) | π is a run in M}.
Language Lϕ of runs satisfying ϕ is defined as follows.
Lϕ = {I(π) | π |= ϕ}.
Observation
M |= ϕ ⇐⇒ Lsys ⊆ Lϕ
IA169 System Verification and Assurance – 05 str. 6/46
Lsys and Lϕ expressed by Büchi automaton
Theorem
For every LTL formula ϕ we can construct Büchi
automaton Aϕ such that Lϕ = L(Aϕ).
[Vardi and Wolper, 1986]
Theorem
For every Kripke structure M = (S, T, I, s0) we can
construct Büchi automaton Asys such that Lsys = L(Asys).
Construction of Asys
Let AP be a set of atomic propositions.
Then Asys = (S, 2AP
, s0, δ, S), where q ∈ δ(p, a) if and
only if (p, q) ∈ T ∧ I(p) = a.
IA169 System Verification and Assurance – 05 str. 7/46
Where we are now?
Property Specification
English text.
Formulae ϕ of Linear Temporal Logic.
Buchi automaton accepting Lϕ.
System Description
Source code in programming language.
Source code in modelling language.
Kripke structure M representing the state space.
Buchi automaton accepting Lsys.
Problem Reformulation
M |= ϕ ⇐⇒ Lsys ⊆ Lϕ
IA169 System Verification and Assurance – 05 str. 8/46
Reduction to Büchi Emptiness Problem
Notation
co−L denotes complement of L with respect to ΣAP
.
Lemma
co−L(Aϕ) = L(A¬ϕ) for every LTL formula ϕ.
Reduction of M |= ϕ to the emptiness of L(Asys × A¬ϕ)
M |= ϕ ⇐⇒ Lsys ⊆ Lϕ
M |= ϕ ⇐⇒ L(Asys) ⊆ L(Aϕ)
M |= ϕ ⇐⇒ L(Asys) ∩ co−L(Aϕ) = ∅
M |= ϕ ⇐⇒ L(Asys) ∩ L(A¬ϕ) = ∅
M |= ϕ ⇐⇒ L(Asys × A¬ϕ) = ∅
IA169 System Verification and Assurance – 05 str. 9/46
Synchronous Product of Büchi Automata
Theorem
Let A = (SA, Σ, sA, δA, FA) and B = (SB, Σ, sB, δB, FB) be
Büchi automata over the same alphabet Σ. Then we can
construct Büchi automaton A × B such that
L(A × B) = L(A) ∩ L(B).
Construction of A × B
A × B =
(SA × SB × {0, 1}, Σ, (sA, sB, 0), δA×B, FA × SB × {0})
(p , q , j) ∈ δA×B((p, q, i), a) for all
p ∈ δA(p, a)
q ∈ δB(q, a)
j = (i + 1) mod 2 if (i = 0 ∧ p ∈ FA) ∨ (i = 1 ∧ q ∈ FB)
j = i otherwise
IA169 System Verification and Assurance – 05 str. 10/46
Synchronous Product of Büchi Automata – Simplification
Observation
For the purpose of LTL model checking, we do not need
general synchronous product of Büchi automata, since
Büchi automaton Asys is constructed in such a way that
FA = SA, i.e. it has all states accepting.
For such a special case the construction of product
automata can be significantly simplified.
Construction of A × B when FA = SA
A × B = (SA × SB, Σ, (sA, sB), δA×B, SA × FB)
(p , q ) ∈ δA×B((p, q), a) for all
p ∈ δA(p, a)
q ∈ δB(q, a)
IA169 System Verification and Assurance – 05 str. 11/46
Reduction to Accepting Cycle Detection
Observation
Any finite automaton may visit accepting state infinitely
many times only if it contains a cycle through that
accepting state.
Decision Procedure for M |= ϕ?
Build a product automaton (Asys × A¬ϕ).
Check the automaton for presence of an accepting cycle.
If there is a reachable accepting cycle then M |= ϕ.
Otherwise M |= ϕ.
IA169 System Verification and Assurance – 05 str. 12/46
Section
Detection of Accepting Cycles
IA169 System Verification and Assurance – 05 str. 13/46
Detection of Accepting Cycles
Reachability in Directed Graph
Depth-first or breadth-first search algorithm.
O(|V | + |E|).
Algorithmic Solution to Accepting Cycle Detection
Compute the set of accepting states in time O(|V | + |E|).
Detect self-reachability for every accepting state in
O(|F|(|V | + |E|)).
Overall time O(|V | + |E| + |F|(|V | + |E|)).
Can we do better?
Yes, with Nested DFS algorithm in O(|V | + |E|).
IA169 System Verification and Assurance – 05 str. 14/46
Depth-First Search Procedure
proc Reachable(V ,E,v0)
Visited = ∅
DFS(v0)
return (Visited)
end
proc DFS(vertex)
if vertex ∈ Visited
then /∗ Visits vertex ∗/
Visited := Visited ∪ {vertex}
foreach { v | (vertex,v)∈ E } do
DFS(v)
od
/∗ Backtracks from vertex ∗/
fi
IA169 System Verification and Assurance – 05 str. 15/46
Colour Notation in DFS
Observation
When running DFS on a graph all vertices can be
classified into one of the three following categories
(denoted with colours).
Colour Notation for Vertices
White vertex – Has not been visited yet.
Gray vertex - Visited, but yet not backtracked.
Black vertex - Visited and backtracked.
Recursion Stack
Gray vertices form a path from the initial vertex to the
vertex that is currently processed by the outer procedure.
IA169 System Verification and Assurance – 05 str. 16/46
Properties of DFS, G = (V , E) a v0 ∈ V
Observation
If two distinct vertices v1, v2 satisfy that
(v0, v1) ∈ E∗
,
(v1, v1) ∈ E+
,
(v1, v2) ∈ E+
.
Then procedure DFS(v0) backtracks from vertex v2 before
it backtracks from vertex v1.
DFS post-order
If (v, v) ∈ E+
and (v0, v) ∈ E∗
, then upon the
termination of sub-procedure DFS(v), called within
procedure DFS(v0), all vertices u such that (v, u) ∈ E+
are visited and backtracked.
IA169 System Verification and Assurance – 05 str. 17/46
Detection of Accepting Cycles in O(|V | + |E|)
Observation
If a sub-graph reachable from a given accepting vertex
does not contain accepting cycle, then no accepting cycle
starting in an accepting state outside the sub-graph can
reach the sub-graph.
The Key Idea
Execute the inner procedures in a bottom-up manner.
The inner procedures are called in the same order in which
the outer procedure backtracks from accepting states, i.e.
the ordering of calls follows a DFS post-order.
IA169 System Verification and Assurance – 05 str. 18/46
Detection of Accepting Cycles in O(|V | + |E|)
proc Detection_of_accepting_cycles
Visited := ∅
DFS(v0)
end
proc DFS(vertex)
if (vertex) ∈ Visited
then Visited := Visited ∪ {vertex}
foreach {s | (vertex,s) ∈ E} do
DFS(s)
od
if IsAccepting(vertex)
then DetectCycle(vertex)
fi
fi
end
IA169 System Verification and Assurance – 05 str. 19/46
Detection of Accepting Cycles in O(|V | + |E|)
Assumption On Early Termination
The inner procedure reports the accepting cycle and
terminates the whole algorithm if called for an accepting
vertex that lies on an accepting cycle.
Consequences
If the inner procedure called for an accepting vertex v
reports no accepting cycle, then there is no accepting
cycle in the graph reachable from vertex v.
IA169 System Verification and Assurance – 05 str. 20/46
Detection of Accepting Cycles in O(|V | + |E|)
Linear Complexity of Nested DFS Algorithm
Employing DFS post-order it follows that vertices that
have been visited by previous invocation of inner
procedure may be safely skipped in any later invocation of
the inner procedure.
O(|V | + |E|) Algorithm
1) Nested procedures are called in DFS post-order as given
by the outer procedure, and are limited to vertices not yet
visited by inner procedure.
2) All vertices are visited at most twice.
IA169 System Verification and Assurance – 05 str. 21/46
Detecting Cycles in Inner Procedures
Theorem
If the immediate successor to be processed by an inner
procedure is grey (on the stack of the outer procedure),
then the presence of an accepting cycle is guaranteed.
Application
It is enough to reach a vertex on the stack of the outer
procedure in the inner procedure in order to report the
presence of an accepting cycle.
IA169 System Verification and Assurance – 05 str. 22/46
O(|V | + |E|) Algorithm
proc Detection_of_accepting_cycles
Visited := Nested := in_stack := ∅
DFS(v0)
Exit("Not Present")
end
proc DFS(vertex)
if (vertex) ∈ Visited
then Visited := Visited ∪ {vertex}
in_stack := in_stack ∪ {vertex}
foreach {s | (vertex,s) ∈ E} do
DFS(s)
od
if IsAccepting(vertex)
then DetectCycle(vertex)
fi
in_stack := in_stack \ {vertex}
fi
end
proc DetectCycle (vertex)
if vertex ∈ Nested
then Nested := Nested ∪ {vertex}
foreach {s | (vertex,s) ∈ E} do
if s ∈ in_stack
then WriteOut(in_stack)
Exit("Present")
else DetectCycle(s)
fi
od
fi
end
IA169 System Verification and Assurance – 05 str. 23/46
Time and Space Complexity
Outer Procedure
Time: O(|V | + |E|)
Space: O(|V |)
Inner Procedures
Time (overall): O(|V | + |E|)
Space: O(|V |)
Complexity
Time: O(|V | + |E| + |V | + |E|) = O(|V | + |E|)
Space: O(|V | + |V |) = O(|V |)
IA169 System Verification and Assurance – 05 str. 24/46
Nested DFS – Example
IA169 System Verification and Assurance – 05 str. 25/46
Section
Classification of Büchi Automata
IA169 System Verification and Assurance – 05 str. 26/46
Sub-Classes of Büchi Automata
Terminal Büchi Automata
All accepting cycles are self-loops on accepting states
labelled with true.
Weak Büchi Automata
Every strongly connected component of the automaton is
composed either of accepting states, or of non-accepting
states.
IA169 System Verification and Assurance – 05 str. 27/46
Impact on Verification Procedure
Automaton A¬ϕ
For a number of LTL formulae ϕ, A¬ϕ is terminal or weak.
A¬ϕ is typically quite small.
Type of A¬ϕ can be pre-computed prior verification.
Types of components of A¬ϕ
Non-accepting – Contains no accepting cycles.
Strongly accepting – Every cycle is accepting.
Partially accepting – Some cycles are accepting and some are
not.
Product Automaton
The graph to be analysed is a graph of product
automaton AS × A¬ϕ.
Types of components of AS × A¬ϕ are given by the
corresponding components of A¬ϕ.
IA169 System Verification and Assurance – 05 str. 28/46
Impact on Verification Procedure – Terminal BA
A¬ϕ is terminal Büchi automaton
For the proof of existence of accepting cycle it is enough
to proof reachability of any state that is accepting in A¬ϕ
part.
Verification process is reduced to the reachability problem.
„Safety” Properties
Those properties ϕ for which A¬ϕ is a terminal BA.
Typical phrasing: „Something bad never happens.”
Reachability is enough to proof the property.
IA169 System Verification and Assurance – 05 str. 29/46
Impact on Verification Procedure – Weak BA
A¬ϕ is weak Büchi automaton
Contains no partially accepting components.
For the proof of existence of accepting cycle it is enough
to proof existence of reachable cycle in a strongly
accepting component.
Can be detected with a single DFS procedure.
Time-optimal algorithm exists that does not rely on DFS.
„Weak” LTL Properties
Those properties ϕ for which A¬ϕ is a weak BA.
Typically, responsiveness: G (a =⇒ F (b)).
IA169 System Verification and Assurance – 05 str. 30/46
Classification of LTL Properties
Classification
Every LTL formula belongs to one of the following classes:
Reactivity, Recurrence, Persistance, Obligation, Safety, Guarantee
Interesting Relations
Guarantee class properties can be described with a terminal
Büchi automaton.
Persistance, Obligation, and Safety class properties can be
described with a weak Büchi automaton.
Negation in Verification Process (ϕ → A¬ϕ)
ϕ ∈ Safety ⇐⇒ ¬ϕ ∈ Guarantee.
ϕ ∈ Recurrence ⇐⇒ ¬ϕ ∈ Persistance.
IA169 System Verification and Assurance – 05 str. 31/46
Classification of LTL Properties
Guarantee
Obligation
Safety
PersistenceRecurrence
Reactivity
General BA
Weak BA
Terminal BA
IA169 System Verification and Assurance – 05 str. 32/46
Section
Fighting State Space Explosion
IA169 System Verification and Assurance – 05 str. 33/46
State Space Explosion Problem
What is State Space Explosion
System is usually given as a composition of parallel
processes.
Depending on the order of execution of actions of parallel
processes various intermediate states emerge.
The number of reachable states may be up to
exponentially larger than the number of lines of code.
Consequence
Main memory cannot store all states of the product
automaton as they are too many.
Algorithms for accepting cycle detection suffer for lack of
memory.
IA169 System Verification and Assurance – 05 str. 34/46
Some Methods to Fight State Space Explosion
State Compression
Lossless compression.
Lossy compression – Heuristics.
On-The-Fly Verification
Symbolic Representation of State Space
Reduced Number of States of the Product Automaton
Introduction of atomic blocks.
Partial order on execution of process actions.
Avoid exploration of symmetric parts.
Parallel and Distributed Verification
IA169 System Verification and Assurance – 05 str. 35/46
On-The-Fly Verification
Observation
Product automaton graph is defined implicitly with:
|F|_init() — Returns initial state of automaton.
|F|_succs(s) — Gives immediate successors of a given state.
|Accepting|(s) — Gives whether a state is accepting or not.
On-The-Fly Verification
Some algorithms may detect the presence of accepting
cycle without the need of complete exploration of the
graph.
Hence, M |= ϕ can be decided without the full
construction of Asys × A¬ϕ.
This is referred to as on-the-fly verification.
IA169 System Verification and Assurance – 05 str. 36/46
Partial Order Reduction
Example
Consider a system made of processes A and B.
A can do a single action α, while B is a sequence of
actions β, e.g. β1, . . . , βm.
Unreduced State Space:
βm
α α α
β1 β2
βm
α
β1 β2
s
r
Property to be verifed: Reachability of state r.
IA169 System Verification and Assurance – 05 str. 37/46
Partial Order Reduction
Observation
Runs (αβ1β2 . . . βm), (β1αβ2 . . . βm), . . . , (β1β2 . . . βmα)
are equivalent with respect to the property.
It is enough to consider only a representative from the
equivalence class, say, e.g. (β1β2 . . . βmα).
βm
α α α
β1 β2
βm
α
β1 β2
s
r
The representative is obtained by postponing of action α.
IA169 System Verification and Assurance – 05 str. 38/46
Partial Order Reduction
Reduction Principle
Do not consider all immediate successor during state
space exploration, but pick carefully only some of them.
Some states are never generated, which results in a
smaller state space graph.
Technical Realisation
To pick correct but optimal subset of successors is as
difficult as to generate the whole state space. Hence,
heuristics are used.
The reduced state space must contain an accepting cycle
if and only if the unreduced state space does so.
LTL formula must not use X operator (subclass of LTL).
IA169 System Verification and Assurance – 05 str. 39/46
Distributed and Parallel Verification
Principle
Employ aggregate power of multiple CPUs.
Increased memory and computing power.
Problem of Nested DFS
Typical implementation relies on hashing mechanism,
hence, the main memory is accessed extremely randomly.
Should memory demands exceeds the amount of available
memory, thrashing occurs.
Mimicking serial Nested DFS algorithm in a
distributed-memory setting is extremely slow.
(Token-based approach).
It is unknown whether the DFS post-order can be
computed by a time-optimal scale-able parallel algorithm
(Still an open problem.)
IA169 System Verification and Assurance – 05 str. 40/46
Parallel Algorithms for Distributed-Memory Setting
Observation
Instead of DFS other graph procedures are used.
Tasks such as breadth-first search, or value propagation
can be efficiently computed in parallel.
Parallel algorithms do not exhibit optimal complexity.
Complexity Optimal On-The-Fly
Nested DFS O(V+E) Yes Yes
OWCTY
general Büchi automata O(V.(V+E)) No No
weak Büchi automata O(V+E) Yes No
MAP O(V.V.(V+E)) No Partially
OWCTY+MAP
general Büchi automata O(V.(V+E)) No Partially
weak Büchi automata O(V+E) Yes Partially
IA169 System Verification and Assurance – 05 str. 41/46
Section
Model Checking – Summary
IA169 System Verification and Assurance – 05 str. 42/46
Decision Procedure and State Space Explosion
Properties Validity
Property to be verified may be violated by a single
particular (even extremely unlikely) run of the system
under inspection.
The decision procedure relies on exploration of state space
graph of the system.
State Space Explosion
Unless there are other reasons, all system runs have to be
considered.
The number of states, that system can reach is up to
exponentially larger than the size of the system
description.
Reasons: Data explosion, asynchronous parallelism.
IA169 System Verification and Assurance – 05 str. 43/46
Advantages of Model Checking
General Technique
Applicable to Hardware, Software, Embedded Systems,
Model-Based Development, . . .
Mathematically Rigorous Precision
The decision procedure results with M |= ϕ, if and only
if, it is the case.
Tool for Model Checking – Model Checkers
The so called "Push-Button" Verification.
No human participation in the decision process.
Provides users with witnesses and counterexamples.
IA169 System Verification and Assurance – 05 str. 44/46
Disadvantages of Model Checking
Not Suitable for Everything
Not suitable to show that a program for computing
factorial really computes n! for a given n.
Though it is perfectly fine to check that for a value of 5 it
always returns the value of 120.
Often Relies on Modelling
Need for model construction.
Validity of a formula is guaranteed for the model, not the
modelled system.
Size of the State Space
Applicable mostly to system with finite state space.
Due to state space explosion, practical applicability is
limited.
Verifies Only What Has Been Specified
Issues not covered with formulae need not be discovered.
IA169 System Verification and Assurance – 05 str. 45/46
Self-study
Challenge yourself and perform ...
... analysis of some C source code (e.g. a task from
course on secure coding) with DIVINE model checker.
IA169 System Verification and Assurance – 05 str. 46/46