IA159 Formal Verification Methods
Model Checking: An Overview
Jan Strejˇcek
Department of Computer Science
Faculty of Informatics
Masaryk University
Focus and sources
Focus
model checking in general
specifications, linear temporal logic (LTL), Büchi automata
models, Kripke structure, process rewrite systems (PRS)
model checking problems and decidability
LTL model checking of finite systems
state explosion problem
Sources
Chapters 1, 2, 3 and 9 of E. M. Clarke, O. Grumberg, and
D. A. Peled: Model Checking, MIT, 1999.
R. Mayr: Decidability and Complexity of Model Checking
Problems for Infinite-State Systems. PhD thesis, 1998.
IA159 Formal Verification Methods: Model Checking: An Overview 2/38
Model checking schema
model M
""
specification S
yy
model checking
algorithm

""
YES,
M satisfies S
NO,
M does not satisfy S
(+ counterexample)
IA159 Formal Verification Methods: Model Checking: An Overview 3/38
Model checking
Specification
IA159 Formal Verification Methods: Model Checking: An Overview 4/38
Specification
a finite formal description of some property that should be
satisfied by all behaviours of the system
usually does not fully specify the system
typically given by a formula of some temporal logic
Linear Temporal Logic (LTL) (linear time)
Computational Tree Logic (CTL) (branching time)
CTL∗
, Hennessy–Milner logic, µ calculus, . . .
can be given also by a Büchi automaton, etc.
IA159 Formal Verification Methods: Model Checking: An Overview 5/38
The hierarchy of basic temporal logics.
modal µ-calculus
CTL∗
CTL LTL
Hennessy-Milner logic
The hierarchy of selected temporal logics according to their
expressive power.
IA159 Formal Verification Methods: Model Checking: An Overview 6/38
State-based vs. action-based logics
state-based These logics talk about properties of states of a
system. Properties of a single state are reflected
by validity of atomic propositions in the state.
State-based logic are interpreted over behaviours
of the system represented by sequences (or trees)
of sets of valid atomic propositions.
action-based Every transition of a system is labelled with an
action. Action-based logic are interpreted over
behaviours of the system represented only by
sequences (or trees) of actions.
We provide definition of both state-based and action-based LTL.
IA159 Formal Verification Methods: Model Checking: An Overview 7/38
Syntax of state-based LTL
State-based Linear Temporal Logic (LTL) is defined by
ϕ ::= | a | ¬ϕ | ϕ1 ∧ ϕ2 | Xϕ | ϕ1 U ϕ2
where stands for true and a ranges over a countable set AP
of atomic propositions.
Abbreviations ⊥ ≡ ¬ Fϕ ≡ U ϕ Gϕ ≡ ¬F¬ϕ
Terminology and intuitive meaning
Xa next • a • • • . . .
a U b until a a . . . a b • • • . . .
Fa eventually • • . . . • a • • • . . .
Ga always a a a a . . .
IA159 Formal Verification Methods: Model Checking: An Overview 8/38
Semantics of state-based LTL
Let Σ = 2AP , where AP ⊆ AP is a finite subset. We interpret
LTL on infinite words w = w(0)w(1) . . . ∈ Σω. By wi we denote
the suffix of w of the form w(i)w(i + 1)w(i + 2) . . ..
The validity of an LTL formula ϕ for w ∈ Σω, written w |= ϕ, is
defined as
w |=
w |= a iff a ∈ w(0)
w |= ¬ϕ iff w |= ϕ
w |= ϕ1 ∧ ϕ2 iff w |= ϕ1 ∧ w |= ϕ2
w |= Xϕ iff w1 |= ϕ
w |= ϕ1 U ϕ2 iff ∃i ∈ N0 : wi |= ϕ2 ∧ ∀ 0 ≤ j < i : wj |= ϕ1
Given an alphabet Σ, an LTL formula ϕ defines the language
LΣ
(ϕ) = {w ∈ Σω
| w |= ϕ}.
IA159 Formal Verification Methods: Model Checking: An Overview 9/38
Action-based LTL
Differences between action-based and state-based LTL
In the syntax, a ranges over countable set of actions Act.
Formulae of action-based LTL are then interpreted over
infinite sequences w of actions from a finite subset
Act ⊆ Act.
Semantics of formula a is defined as follows:
w |= a iff a = w(0)
IA159 Formal Verification Methods: Model Checking: An Overview 10/38
Examples of LTL formulae
G¬error - safety property
G(p =⇒ Fq) - response property
GFp - liveness property
IA159 Formal Verification Methods: Model Checking: An Overview 11/38
Büchi automata
A Büchi automaton (BA) is a tuple A = (Σ, Q, δ, q0, F), where
Σ is a finite alphabet,
Q is a finite set of states,
δ : Q × Σ → 2Q is a transition function,
q0 ∈ Q is an initial states,
F ⊆ Q is a set of accepting states.
A run of A on inifnite word w = w(0)w(1)... ∈ Σω is an infinite
sequence of states σ = σ(0)σ(1)..., where σ(0) = q0 and
σ(i + 1) ∈ δ(σ(i), w(i)) holds for all i.
A run σ is accepting if Inf(σ) ∩ F = ∅, where Inf(σ) is the set of
the states appearing in σ infinitely often. An automaton A
accepts a word w if there is an accepting run of A on w. We set
L(A) = {w ∈ Σω
| A accepts w}.
IA159 Formal Verification Methods: Model Checking: An Overview 12/38
Example of a Büchi automaton
q1 q2
b
a
a b
IA159 Formal Verification Methods: Model Checking: An Overview 13/38
Example of a Büchi automaton
q1 q2
b
a
a b
Accepts the words with infinitely many occurences of a.
IA159 Formal Verification Methods: Model Checking: An Overview 14/38
Model checking
Model
IA159 Formal Verification Methods: Model Checking: An Overview 15/38
Model
a finite formal description of all possible behaviours of the
system to be verified
behaviour is a sequence (or a tree) of states/actions
state is an image of the system in a certain moment
(current values of variables, program counter, etc.)
a state is characterized by validity of atomic propositions
(e.g. PC == start, x > 5)
many possible formalisms
standard languages C, Java, VHDL, . . .
dedicated languages, e.g. ProMeLa (Process or Protocol
Meta Language)
process rewrite systems (infinite-state systems)
BPA, BPP, PA, pushdown processes, Petri nets, . . .
low-level formalisms: Kripke structure (for state-based
approach) and labelled transition systems (for action-based
approach)
IA159 Formal Verification Methods: Model Checking: An Overview 16/38
Example: mutual exclusion in ProMeLa
byte cnt = 0; // number of processes in critical sections
byte turn = 0; // token for entering a critical section
init {
run(P0); run(P1); // parallel execution of P0 a P1
}
proctype P0() proctype P1()
{ {
// s0 //s1
do do
// NC0 (noncritical section) // NC1 (noncritical section)
:: do :: do
:: (turn == 0) -> break; :: (turn == 1) -> break;
:: else; :: else;
od; od;
// CS0 (critical section) // CS1 (critical section)
cnt = cnt + 1; cnt = cnt + 1;
cnt = cnt - 1; cnt = cnt - 1;
turn = 1; turn = 0;
od; od;
} }
IA159 Formal Verification Methods: Model Checking: An Overview 17/38
Kripke structure
Let AP be a countable set of atomic propositions.
A Kripke structure is a tuple M = (S, R, S0, L), where
S is a set of states
R ⊆ S × S is transitions relation
S0 ⊆ S is a set of initial states
L : S → 2AP is a labelling function associating to each state
s ∈ S the set of atomic propositions that are true in s.
A path in M starting in a state s is an infinite sequence
π = s0s1s2... of states such that s0 = s and (si, si+1) ∈ R holds
for every i.
IA159 Formal Verification Methods: Model Checking: An Overview 18/38
Example: mutual exclusion as a Kripke structure
turn = 0
s0, NC1
turn = 0
NC0, s1
turn = 0
CS0, s1NC0, NC1
turn = 0
CS0, NC1
s0, CS1
turn = 1
s0, NC1
turn = 1 turn = 1
NC0, s1
turn = 1
NC0, NC1
turn = 1
NC0, CS1
⊥, ⊥
turn = 0
s0, s1
turn = 1
⊥, ⊥
turn = 1
s0, s1
turn = 0
turn = 0
IA159 Formal Verification Methods: Model Checking: An Overview 19/38
Process rewrite systems: motivation
finite-state systems have very limited expressive power
there are some classes of infinite-state systems with
decidable LTL model checking problem
many standard classes of infinite-state systems are
definable uniformly as subslasses of Process Rewrite
Systems (PRS)
IA159 Formal Verification Methods: Model Checking: An Overview 20/38
Process rewrite systems: process terms
Let Const = {A, B, C, . . .} be a countably infinite set of process
constants. Process terms are defined by the abstract syntax
t ::= ε | A | t1.t2 | t1 t2,
where
ε is the empty term,
A ∈ Const is a process constant (used as an atomic
process),
’ ’ means a parallel composition, and
’.’ means a sequential composition.
We always work with equivalence classes of terms modulo
commutativity and associativity of ’ ’ ((A B) C = B (A C))
and modulo associativity of ’.’ ((A.B).C = A.(B.C)).
IA159 Formal Verification Methods: Model Checking: An Overview 21/38
Process rewrite systems: classes of process terms
We distinguish four classes of process terms as:
“1” terms consisting of a single process constant only
(i.e. ε ∈ 1), e.g. A.
“S” sequential terms without parallel composition, e.g. A.B.C.
“P” parallel terms without sequential composition. e.g. A B C.
“G” general terms with arbitrarily nested sequential and parallel
compositions.
IA159 Formal Verification Methods: Model Checking: An Overview 22/38
Process rewrite systems: syntax
Let Act = {a, b, · · · } be a countably infinite set of atomic
actions and α, β ∈ {1, S, P, G} such that α ⊆ β. An (α, β)-PRS
(process rewrite system) is a pair ∆ = (R, t0), where
R ⊆ ((α {ε}) × Act × β) is a finite set of rewrite rules, and
t0 ∈ β is an initial term.
We write (t1
a
→ t2) ∈ R instead of (t1, a, t2) ∈ R.
IA159 Formal Verification Methods: Model Checking: An Overview 23/38
Process rewrite systems: semantics
An (α, β)-PRS ∆ = (R, t0) defines a labelled transition system
where
states are process terms of β,
t0 is the initial state,
the transition relation −→ is the least relation satisfying the
following inference rules:
(t1
a
→ t2) ∈ R
t1
a
−→ t2
t1
a
−→ t2
t1 t
a
−→ t2 t
t1
a
−→ t2
t1.t
a
−→ t2.t
IA159 Formal Verification Methods: Model Checking: An Overview 24/38
Process rewrite systems: example

B
b

B C
coo
b

A.B
a //
(A.B) C
a //
c
oo (A.B) C C
a //
c
oo · · ·
c
oo
(S, G)-PRS (R, B C) with rewrite rules
R = { B
b
→ A.B, A.B
a
→ (A.B) C, C
c
→ ε }
IA159 Formal Verification Methods: Model Checking: An Overview 25/38
Process rewrite systems: power of rewrite rules
(1, 1)-PRS finite-state systems
m
x:=x+1
→ n simple sequential programs
without procedures
(1, S)-PRS basic process algebra
m
call p
→ p0.n programs with procedure calls
no global variables and return values
(S, S)-PRS pushdown systems
g.m
call p
→ g.p0.n sequential programs with procedures
global variables, return values
IA159 Formal Verification Methods: Model Checking: An Overview 26/38
Process rewrite systems: power of rewrite rules
(1, P)-PRS basic parallel processes
m
creat thread f
→ n f0 programs with simple parallel threads
no communication
(P, P)-PRS Petri nets
m p
synchronize
→ n q programs with parallel threads
communication between threads
IA159 Formal Verification Methods: Model Checking: An Overview 27/38
Process rewrite systems hierarchy (PRS-hierarchy)
The hierarchy compares expressive power of many classes of
infinite-state systems including BPA, BPP, PA, Petri nets (PN),
and pushdown processes (PDA). FS stands for finite systems.
PRS
(G,G)-PRS
PAD
(S,G)-PRS
PAN
(P,G)-PRS
PDA
(S,S)-PRS
PA
(1,G)-PRS
PN
(P,P)-PRS
BPA
(1,S)-PRS
BPP
(1,P)-PRS
FS
(1,1)-PRS
IA159 Formal Verification Methods: Model Checking: An Overview 28/38
Model checking
Decidability of model checking
IA159 Formal Verification Methods: Model Checking: An Overview 29/38
Model checking
Model checking problem is to decide whether all behaviours of
a given system satisfy a given specification.
specific problems for specific input
state-based LTL model checking of finite systems
action-based CTL model checking of finite systems
state-based LTL model checking of pushdown processes
action-based LTL model checking of pushdown processes
. . .
model checking problem is not decidable for some kinds of
input (e.g. action-based LTL model checking of PA
processes)
even small changes of the problem can be important:
action-based LTL model checking of PN is decidable, while
state-based LTL model checking of PN in undecidable
all model checking problems are decidable for finite
systems
IA159 Formal Verification Methods: Model Checking: An Overview 30/38
The decidability boundary
The decidability boundary of the action-based LTL model
checking in the PRS-hierarchy.
PRS
PAD PAN
↑undecidable
↓decidable PDA PA PN
BPA BPP
FS
IA159 Formal Verification Methods: Model Checking: An Overview 31/38
Model checking
Automata-based LTL model checking of finite systems
IA159 Formal Verification Methods: Model Checking: An Overview 32/38
Automata-based LTL model checking of finite systems
Kripke structure M
with finitely many states

LTL formula ϕ

Büchi automaton AM
accepts paths of M starting in initial
states and projected by L to 2AP(ϕ)
%%
Büchi automaton A¬ϕ
words over 2AP(ϕ) violating ϕ
zz
product Büchi automaton B
L(B) = L(AM ) ∩ L(A¬ϕ)

L(B)
?
= ∅
e.g. nested DFS algorithm
xx
$$
YES
NO
+ counterexample
IA159 Formal Verification Methods: Model Checking: An Overview 33/38
Complexity notes
Complexity
Time and space complexity of the LTL model checking
algorithm is O(|M| · 2O(|ϕ|)), where |M| is the number of states
and transitions in the Kripke structure M.
LTL model checking problem is PSPACE-complete.
state explosion problem - |M| is often exponential in the
size of implicit description of the system due to
parallelism
large data domains
dynamically allocated memory
. . .
IA159 Formal Verification Methods: Model Checking: An Overview 34/38
State explosion problem - an example
byte x = 0;
byte y = 0;
proctype A() { proctype B() { proctype C() {
x = x + 1; x = x + 2; y = y + 5;
} } }
x = 0
y = 0
x=x+1;
vv
x=x+2;

y=y+5;
((x = 1
y = 0
x=x+2;

y=y+5;
((
x = 2
y = 0
x=x+1;vv
y=y+5;
((
x = 0
y = 5
x=x+1;vv
x=x+2;

x = 3
y = 0
y=y+5;
((
x = 1
y = 5
x=x+2;

x = 2
y = 5
x=x+1;
vvx = 3
y = 5
IA159 Formal Verification Methods: Model Checking: An Overview 35/38
Partial solutions of the state explosion problem
abstraction
partial order reduction
symmetry reduction
on-the-fly algorithms
symbolic model checking
distributed algorithms
. . .
IA159 Formal Verification Methods: Model Checking: An Overview 36/38
Our topics
translation LTL→BA (via alternating 1-weak BA)
partial order reduction
state-based LTL model checking of pushdown processes
abstraction
counterexample guided abstraction refinement (CEGAR)
IA159 Formal Verification Methods: Model Checking: An Overview 37/38
Coming next week
LTL model checking of pushdown system
How can I denote an infinite-state system?
Can I verify an infinite-state system?
What are pushdown processes good for?
Can I do LTL model checking for them?
IA159 Formal Verification Methods: Model Checking: An Overview 38/38