IA169 System Verification and Assurance
LTL Model Checking
(continued)
Jiří Barnat
Reminder
Problem
Kripke structure M
LTL formula ϕ
M |= ϕ ?
Solution Based on Büchi Automata
Asys – automaton accepting all system runs
A¬ϕ – automaton accepting all runs violating ϕ
L(Asys) ∩ L(A¬ϕ) = L(Asys × A¬ϕ)
L(Asys × A¬ϕ) = ∅ ⇐⇒ system exhibits invalid run
L(Asys × A¬ϕ) = ∅ ⇐⇒ M |= ϕ
IA169 System Verification and Assurance – 06 str. 2/38
Algorithm for Detection of Accepting Cycles
Algorithm Input
Product Büchi automaton given implicitly
|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.
Algorithm Output
Present/ Not present
Counterexample.
Algorithm
Two nested depth-first search procedures – Nested DFS.
Outer procedure detects accepting states, inner procedure
checks for each accepting state if it is self-reachable (lies
on a cycle).
IA169 System Verification and Assurance – 06 str. 3/38
Section
Detection of Accepting Cycles
IA169 System Verification and Assurance – 06 str. 4/38
Detection of Accepting Cycles
Problem
Let A = (S, Σ, δ, s0, F) be a Büchi automaton.
Is the language accepted by A non-empty?
Reduction to Accepting Cycle Detection Problem
Let G = (S, E), where
E = {(u, v) ∈ S × S | ∃a ∈ Σ such that v ∈ δ(u, a)}
be a graph of a Büchi automaton.
L(A) is non-empty if and only if the graph of the
automaton A contains reachable accepting cycle, i.e. a
cycle whose at least one vertex v corresponds to an
accepting state (v ∈ F), and is, at the same time,
reachable from the initial state ((s0, v) ∈ E∗
).
IA169 System Verification and Assurance – 06 str. 5/38
Detection of Accepting Cycles
Algorithmic Solution
1) Identify all reachable accepting states in the graph of
Büchi automaton. (Outer procedure.)
2) Check for every such the state that is not self-reachable
(Inner procedure.)
Reachability in Directed Graph
The standard graph algorithm.
To compute the set of reachable vertices (or accepting
vertices) can be done in in time O(|V | + |E|).
Using the standard algorithm, accepting cycle detection
can be done in time O(|V | + |E| + |F|(|V | + |E|)).
Clever techniques can employ depth-first search post-order
to reduce the time complexity to O(|V | + |E|).
IA169 System Verification and Assurance – 06 str. 6/38
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 – 06 str. 7/38
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 – 06 str. 8/38
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 – 06 str. 9/38
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 – 06 str. 10/38
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 – 06 str. 11/38
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 – 06 str. 12/38
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 – 06 str. 13/38
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 – 06 str. 14/38
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
of
fi
end
IA169 System Verification and Assurance – 06 str. 15/38
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 – 06 str. 16/38
Nested DFS – Example
IA169 System Verification and Assurance – 06 str. 17/38
Section
Classification of Büchi Automata
IA169 System Verification and Assurance – 06 str. 18/38
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 – 06 str. 19/38
Impact on Verification Procedure
Automaton A¬ϕ
For a number of LTL formulae ϕ is A¬ϕ 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 – 06 str. 20/38
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 – 06 str. 21/38
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 – 06 str. 22/38
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 – 06 str. 23/38
Classification of LTL Properties
Guarantee
Obligation
Safety
PersistenceRecurrence
Reactivity
General BA
Weak BA
Terminal BA
IA169 System Verification and Assurance – 06 str. 24/38
Section
Fighting State Space Explosion
IA169 System Verification and Assurance – 06 str. 25/38
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 – 06 str. 26/38
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 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 – 06 str. 27/38
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 to on-the-fly verification.
IA169 System Verification and Assurance – 06 str. 28/38
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 – 06 str. 29/38
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 – 06 str. 30/38
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 – 06 str. 31/38
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 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 – 06 str. 32/38
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 – 06 str. 33/38
Section
Model Checking – Summary
IA169 System Verification and Assurance – 06 str. 34/38
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 thee 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 – 06 str. 35/38
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 – 06 str. 36/38
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 – 06 str. 37/38
Practicals and Homework – 06
Practicals
Code-based reachability analysis with DIVINE model
checker.
Verify ring.cpp.
Find error in fifo.cpp.
Homework
Analysis with DIVINE model checker on a more complex
example (some homework from previous course on secure
coding).
IA169 System Verification and Assurance – 06 str. 38/38