IA169 Model Checking
Abstraction and CEGAR
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Motivation
Abstraction is one of the most important techniques for reducing the state
explosion problem.
[CGKPV18]
original
system
properties
verification impossible
IA169 Model Checking: Abstraction and CEGAR 2/96
Motivation
Abstraction is one of the most important techniques for reducing the state
explosion problem.
[CGKPV18]
original
system
properties
abstract
model
verification
IA169 Model Checking: Abstraction and CEGAR 3/96
Motivation
Abstraction is one of the most important techniques for reducing the state
explosion problem.
[CGKPV18]
original
system
properties
abstract
model
verification
large finite systems −→ smaller finite systems
infinite-state systems −→ finite systems
IA169 Model Checking: Abstraction and CEGAR 4/96
Intuition
x = 0
x = 1
x = 2
x = 3
IA169 Model Checking: Abstraction and CEGAR 5/96
Intuition
x = 0
x = 1
x = 2
x = 3
IA169 Model Checking: Abstraction and CEGAR 6/96
Intuition
x = 0
x = 1
x = 2
x = 3
x = 0
x > 0
IA169 Model Checking: Abstraction and CEGAR 7/96
Intuition
x = 0
x = 1
x = 2
x = 3
x = 0
x > 0
equivalent with respect to F(x > 0)
nonequivalent with respect to GF(x = 0)
IA169 Model Checking: Abstraction and CEGAR 8/96
Agenda and sources
agenda
simulation
exact abstractions
non-exact abstractions, in particular predicate abstraction
abstraction in practice
CEGAR: counterexample-guided abstraction refinement
sources
Chapter 13 of E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith:
Model Checking, Second Edition, MIT, 2018.
R. Pelánek: Reduction and Abstraction Techniques for Model Checking, PhD
thesis, FI MU, 2006.
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith: Counterexample-guided
Abstraction Refinement for Symbolic Model Checking, J. ACM 50(5), 2003.
IA169 Model Checking: Abstraction and CEGAR 9/96
Simulation
Simulation
Definition (simulation)
Given two Kripke structures M = (S, →, S0, L) and M′ = (S′, →′, S′
0, L′), we say
that M′ simulates M, written M ≤ M′, if there exists a relation R ⊆ S × S′ such
that:
∀s0 ∈ S0 . ∃s′
0 ∈ S′
0 . (s0, s′
0) ∈ R
(s, s′) ∈ R =⇒ L(s) = L′(s′)
(s, s′) ∈ R ∧ s → p =⇒ ∃p′ ∈ S′ . s′ →′ p′ ∧ (p, p′) ∈ R
IA169 Model Checking: Abstraction and CEGAR 11/96
Simulation
Definition (simulation)
Given two Kripke structures M = (S, →, S0, L) and M′ = (S′, →′, S′
0, L′), we say
that M′ simulates M, written M ≤ M′, if there exists a relation R ⊆ S × S′ such
that:
∀s0 ∈ S0 . ∃s′
0 ∈ S′
0 . (s0, s′
0) ∈ R
(s, s′) ∈ R =⇒ L(s) = L′(s′)
(s, s′) ∈ R ∧ s → p =⇒ ∃p′ ∈ S′ . s′ →′ p′ ∧ (p, p′) ∈ R
Lemma
If M ≤ M′, then for every path σ = s1s2 . . . of M starting in an initial state there is a
run σ′ = s′
1s′
2 . . . of M′ starting in an initial state and satisfying
L(s1)L(s2) . . . = L′
(s′
1)L′
(s′
2) . . . .
IA169 Model Checking: Abstraction and CEGAR 12/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A
M ≤ A =⇒ all behaviours of M are also in A
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 13/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A A |= φ
M ≤ A =⇒ all behaviours of M are also in A
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 14/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A A |= φ
M |= φ
M ≤ A =⇒ all behaviours of M are also in A
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 15/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A A ̸|= φ
M ≤ A =⇒ all behaviours of M are also in A
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 16/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A A ̸|= φ
???
If A has a behaviour violating φ (i.e. A ̸|= φ), then either
1 M has this behaviour as well (i.e. M ̸|= φ), or
2 M does not have this behaviour, which is then called false positive
or spurious counterexample
(M |= φ or M ̸|= φ due to another behaviour violating φ).
IA169 Model Checking: Abstraction and CEGAR 17/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≥ A
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 18/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≥ A A ̸|= φ
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 19/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≥ A A ̸|= φ
M ̸|= φ
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 20/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≥ A A |= φ
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 21/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≥ A A |= φ
???
M ≥ A =⇒ all behaviours of A are also in M
(but not vice versa)
IA169 Model Checking: Abstraction and CEGAR 22/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A
M ≥ A
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐≠
IA169 Model Checking: Abstraction and CEGAR 23/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A
M ≥ A
A |= φ
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐≠
IA169 Model Checking: Abstraction and CEGAR 24/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A
M ≥ A
A |= φ
M |= φ
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐≠
IA169 Model Checking: Abstraction and CEGAR 25/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A
M ≥ A
A ̸|= φ
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐≠
IA169 Model Checking: Abstraction and CEGAR 26/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A
M ≥ A
A ̸|= φ
M ̸|= φ
M ≤ A ≤ M =⇒ A and M have tha same behaviours
A is an exact abstraction of M
note: A and M are bisimilar =⇒ M ≤ A ≤ M
⇐≠
IA169 Model Checking: Abstraction and CEGAR 27/96
Relations between original and abstract systems
original
system
M
abstract
model
A
property
φ ∈ LTL
M ≤ A
M ≥ A
A ̸|= φ
M ̸|= φ
All these relations hold even for φ ∈ ACTL∗
,
where ACTL∗
is a fragment of CTL∗
without any
existential quantifier (and negation above quantifiers).
IA169 Model Checking: Abstraction and CEGAR 28/96
Exact abstractions
Cone of influence (aka dead variables)
Idea
We eliminate the state variables that do not influence the variables in the
specification.
IA169 Model Checking: Abstraction and CEGAR 30/96
Cone of influence (aka dead variables)
assume that our system is a program
let V be the set of variables appearing in specification
cone of influence C of V is the minimal set of variables such that
V ⊆ C
if v occurs in a test affecting the control flow, then v ∈ C
if there is an assignment v := e for some v ∈ C, then all variables occurring in
the expression e are also in C
C can be computed by the source code analysis
variables that are not in C can be eliminated from the code together with all
commands they participate in
IA169 Model Checking: Abstraction and CEGAR 31/96
Cone of influence: example
S: v = getinput();
x = getinput();
y = 1;
z = 1;
while (v > 0) {
z = z * x;
x = x - 1;
y = y * v;
v = v - 1;
}
z = z * y;
E:
specification: F(pc = E)
IA169 Model Checking: Abstraction and CEGAR 32/96
Cone of influence: example
S: v = getinput();
x = getinput();
y = 1;
z = 1;
while (v > 0) {
z = z * x;
x = x - 1;
y = y * v;
v = v - 1;
}
z = z * y;
E:
specification: F(pc = E)
V = ∅, C = {v}
IA169 Model Checking: Abstraction and CEGAR 33/96
Cone of influence: example
S: v = getinput();
x = getinput();
y = 1;
z = 1;
while (v > 0) {
z = z * x;
x = x - 1;
y = y * v;
v = v - 1;
}
z = z * y;
E:
S: v = getinput();
skip;
skip;
skip;
while (v > 0) {
skip;
skip;
skip;
v = v - 1;
}
skip;
E:
specification: F(pc = E)
V = ∅, C = {v}
IA169 Model Checking: Abstraction and CEGAR 34/96
Other exact abstractions
symmetry reduction
in systems with more identical parallel components, their order is not
important
equivalent values
if the set of behaviours starting in a state s is the same for values a, b of a
variable v, then the two values can be replaced by one
applicable to larger sets of values as well
used in timed automata for timer values
IA169 Model Checking: Abstraction and CEGAR 35/96
Non-exact abstractions, in particular predicate abstraction
Concept
we face two problems
1 to find a suitable set of abstract states (called abstract domain) and a
mapping between the original states and the abstract ones
2 to compute a transition relation on abstract states
IA169 Model Checking: Abstraction and CEGAR 37/96
Finding abstract states
abstract states are usually defined in one of the following ways
1 for each variable x, we replace the original variable domain Dx by an abstract
variable domain Ax and we define a total function hx : Dx → Ax
a state s = (v1, . . . , vm) ∈ Dx1
× . . . × Dxm given by values of all variables
corresponds to an abstract state
h(s) = (hx1
(v1), . . . , hxm (vm)) ∈ Ax1
× . . . × Axm
2 predicate abstraction - we choose a finite set Φ = {ϕ1, . . . , ϕn} of predicates
over the set of variables;
we have several choices of an abstract domain
The first approach can be seen as a special case the latter one.
IA169 Model Checking: Abstraction and CEGAR 38/96
Popular abstract domains for integers
sign abstraction
Ax = {a+, a−, a0}
hx (v) =



a− if v < 0
a0 if v = 0
a+ if v > 0
parity abstraction
Ax = {ae, ao}
hx (v) =
ae if v is even
ao if v is odd
good for verification of properties related to the last bit of binary representation
IA169 Model Checking: Abstraction and CEGAR 39/96
Popular abstract domains for integers
congruence modulo an integer
Ax = {0, 1, . . . , m − 1} for some m > 1
hx (v) = v mod m
nice properties
((x mod m) + (y mod m)) mod m = (x + y) mod m
((x mod m) − (y mod m)) mod m = (x − y) mod m
((x mod m) · (y mod m)) mod m = (x · y) mod m
representation by logarithm
hx (v) = ⌈log2(v + 1)⌉
the number of bits needed to represent v
good for verification of properties related to overflow problems
IA169 Model Checking: Abstraction and CEGAR 40/96
Popular abstract domains for integers
single bit abstraction
Ax = {0, 1}
hx (v) =the i-th bit of v for a fixed i
single value abstraction
Ax = {0, 1}
hx (v) =
1 if v = c
0 otherwise
...and others
IA169 Model Checking: Abstraction and CEGAR 41/96
Predicate abstraction
Let Φ = {ϕ1, . . . , ϕn} be a set of predicates over the set of variables.
abstract domain {0, 1}n
a state s = (v1, . . . , vm) corresponds to an abstract state given by a vector of
truth values of {ϕ1, . . . , ϕn}, i.e.,
h(s) = (ϕ1(v1, . . . , vm), . . . , ϕn(v1, . . . , vm)) ∈ {0, 1}n
example: ϕ1 = (x1 > 3) ϕ2 = (x1 < x2) ϕ3 = (x2 > 10)
s = (5, 7)
h(s) = (1, 1, 0)
IA169 Model Checking: Abstraction and CEGAR 42/96
Abstract structures
assume that
we have an original Kripke structure M = (S, →, S0, L)
we have an abstract domain A and a mapping h : S → A
we define an abstract model as a Kripke structure (A, →′, A0, LA), where
A0 = {h(s0) | s0 ∈ S0}
LA : A → 2AP has to be correctly defined, i.e.,
for abstraction based on variable domains, validity of atomic propositions is
determined by abstract states in Ax1
× . . . × Axm
for predicate abstraction, validity of atomic propositions is determined by
abstraction predicates {ϕ1, . . . , ϕn} (AP is typically a subset of it)
and LA has to agree with L, i.e., L(s) = LA(h(s))
→′ is defined in one of the following ways
IA169 Model Checking: Abstraction and CEGAR 43/96
May abstraction
may abstraction produces Mmay = (A, →may , A0, LA)
a1 →may a2 iff there exist s1, s2 ∈ S such that h(s1) = a1, h(s2) = a2, s1 → s2
IA169 Model Checking: Abstraction and CEGAR 44/96
May abstraction
may abstraction produces Mmay = (A, →may , A0, LA)
a1 →may a2 iff there exist s1, s2 ∈ S such that h(s1) = a1, h(s2) = a2, s1 → s2
example: construct Mmay for the following system using predicate abstraction
with predicates ϕ1 = (x > 0) and ϕ2 = (x > 2) and abstract domain {0, 1}2
x = 0 x = 1 x = 2 x = 3 x = 4 x = 5 · · ·
· · ·
IA169 Model Checking: Abstraction and CEGAR 45/96
May abstraction
may abstraction produces Mmay = (A, →may , A0, LA)
a1 →may a2 iff there exist s1, s2 ∈ S such that h(s1) = a1, h(s2) = a2, s1 → s2
example: construct Mmay for the following system using predicate abstraction
with predicates ϕ1 = (x > 0) and ϕ2 = (x > 2) and abstract domain {0, 1}2
x = 0 x = 1 x = 2 x = 3 x = 4 x = 5 · · ·
· · ·
(0, 0) (1, 0) (1, 1)
IA169 Model Checking: Abstraction and CEGAR 46/96
Must abstraction
must abstraction produces Mmust = (A, →must , A0, LA)
a1 →must a2 iff for each s1 ∈ S satisfying h(s1) = a1 there exists s2 ∈ S
such that h(s2) = a2 and s1 → s2
IA169 Model Checking: Abstraction and CEGAR 47/96
Must abstraction
must abstraction produces Mmust = (A, →must , A0, LA)
a1 →must a2 iff for each s1 ∈ S satisfying h(s1) = a1 there exists s2 ∈ S
such that h(s2) = a2 and s1 → s2
example: construct Mmust for the following system using predicate abstraction
with predicates ϕ1 = (x > 0) and ϕ2 = (x > 2) and abstract domain {0, 1}2
x = 0 x = 1 x = 2 x = 3 x = 4 x = 5 · · ·
· · ·
IA169 Model Checking: Abstraction and CEGAR 48/96
Must abstraction
must abstraction produces Mmust = (A, →must , A0, LA)
a1 →must a2 iff for each s1 ∈ S satisfying h(s1) = a1 there exists s2 ∈ S
such that h(s2) = a2 and s1 → s2
example: construct Mmust for the following system using predicate abstraction
with predicates ϕ1 = (x > 0) and ϕ2 = (x > 2) and abstract domain {0, 1}2
x = 0 x = 1 x = 2 x = 3 x = 4 x = 5 · · ·
· · ·
(0, 0) (1, 0) (1, 1)
IA169 Model Checking: Abstraction and CEGAR 49/96
Relations between M, Mmust, and Mmay
Lemma
For every Kripke structure M, abstract domain A with a mapping function h it holds
Mmust ≤ M ≤ Mmay .
IA169 Model Checking: Abstraction and CEGAR 50/96
Relations between M, Mmust, and Mmay
Lemma
For every Kripke structure M, abstract domain A with a mapping function h it holds
Mmust ≤ M ≤ Mmay .
computing Mmust or Mmay requires constructing M first (recall that M can be
very large or even infinite)
we rather compute an under-approximation M′
must of Mmust or an
over-approximation M′
may of Mmay directly from the implicit representation of M
it holds that M′
must ≤ Mmust ≤ M ≤ Mmay ≤ M′
may
IA169 Model Checking: Abstraction and CEGAR 51/96
Abstraction in practice
Predicate abstraction: abstracting sets of states
Abstract domain {0, 1}n can lead to too many transitions =⇒ it is sometimes
better to assign a single abstract state to a set of original states.
abstract domain 2{0,1}n
let ⃗b = ⟨b1, . . . , bn⟩ be a vector of bi ∈ {0, 1}
we set [⃗b, Φ] = b1 · ϕ1 ∧ . . . ∧ bn · ϕn, where 0 · ϕi = ¬ϕi and 1 · ϕi = ϕi
let X denote the set of original states
h(X) = {⃗b ∈ {0, 1}n | ∃s ∈ X : s |= [⃗b, Φ]}
example: ϕ1 = (x1 > 3) ϕ2 = (x1 < x2) ϕ3 = (x2 > 10)
X = {(5, 7), (4, 5), (2, 9)}
h(X) = {(1, 1, 0), (0, 1, 0)}
nice theoretical properties
not used in practice (this abstract domain grows too fast)
IA169 Model Checking: Abstraction and CEGAR 53/96
Predicate abstraction: abstracting sets of states
abstract domain {0, 1, ∗}n (predicate-cartesian abstraction)
let ⃗b = ⟨b1, . . . , bn⟩ be a vector of bi ∈ {0, 1, ∗}
we set [⃗b, Φ] = b1 · ϕ1 ∧ . . . ∧ bn · ϕn, where 0 · ϕi = ¬ϕi, 1 · ϕi = ϕi, ∗ · ϕi = ⊤
h(X) = min{⃗b ∈ {0, 1, ∗}n | ∀s ∈ X : s |= [⃗b, Φ]}, where min means “the most
specific”
example: ϕ1 = (x1 > 3) ϕ2 = (x1 < x2) ϕ3 = (x2 > 10)
X = {(5, 7), (4, 5), (2, 9)}
h(X) = (∗, 1, 0)
this one is sometimes used in practice
IA169 Model Checking: Abstraction and CEGAR 54/96
Guarded command language
syntax
let V be a finite set of integer variables
Act is a set of action names
model is a pair M = (V, E), where E = {t1, . . . , tm} is a finite set of transitions
of the form ti = (ai, gi, ui), where
ai ∈ Act
gi is a first-order formula called guard and built with V, integers, standard binary
operations (+, −, ·, . . .) and relations (=, <, >, . . .)
ui is a finite sequence of assignments x := e, where x ∈ V and e is an
expression built with V, integers, and standard binary operations (+, −, ·, . . .)
IA169 Model Checking: Abstraction and CEGAR 55/96
Guarded command language
syntax
let V be a finite set of integer variables
Act is a set of action names
model is a pair M = (V, E), where E = {t1, . . . , tm} is a finite set of transitions
of the form ti = (ai, gi, ui), where
ai ∈ Act
gi is a first-order formula called guard and built with V, integers, standard binary
operations (+, −, ·, . . .) and relations (=, <, >, . . .)
ui is a finite sequence of assignments x := e, where x ∈ V and e is an
expression built with V, integers, and standard binary operations (+, −, ·, . . .)
semantics
M defines a labelled transition system where
states are valuations of variables S = 2V→Z
initial state is the zero valuation s0(v) = 0 for all v ∈ V
s
ai
→ s′
whenever s |= gi and s′
arises from s by applying the assignments in ui
M can also describe a Kripke structure if we add a labelling function
IA169 Model Checking: Abstraction and CEGAR 56/96
Example
x = 0 x = 1 x = 2 x = 3 x = 4 x = 5 · · ·
a a a a a a
b
c
c
d d d · · ·
implicit description in guarded command language by model (V, E), where
V = {x}
E = {(a, ⊤, x := x + 1),
(b, ¬(x > 0), x := 0),
(c, (x > 0) ∧ (x ≤ 2), x := 0),
(d, (x > 2), x := 0)}
IA169 Model Checking: Abstraction and CEGAR 57/96
Abstraction in practice
we use predicate abstraction with domain {0, 1, ∗}n
given a formula φ with free variables ⃗x from V, we set
pre(ai, φ) = (gi =⇒ φ[⃗x/ui(⃗x)])
where φ[⃗x/ui(⃗x)] denotes the formula φ with each free variable x replaced by
ui(x), which is the expression representing the value of x after the
assignments in ui
intuitively, pre(ai, φ) transforms the condition φ to the situation before taking
the transition (ai, gi, ui)
we use a sound (potentially not complete) decision procedure is_valid, i.e.,
is_valid(φ) = ⊤ =⇒ φ is a tautology
IA169 Model Checking: Abstraction and CEGAR 58/96
Abstraction in practice
for every abstract state ⃗b ∈ {0, 1, ∗}n and for every transition ti = (ai, gi, ui), we
compute an over-approximation of a may-successor of ⃗b under ti as
if is_valid([⃗b, Φ] =⇒ ¬gi) then there is no successor
otherwise, the successor ⃗b′ is given by
b′
j =



1 if is_valid([⃗b, Φ] =⇒ pre(ai, ϕj))
0 if is_valid([⃗b, Φ] =⇒ pre(ai, ¬ϕj))
∗ otherwise
IA169 Model Checking: Abstraction and CEGAR 59/96
Abstraction in practice
for every abstract state ⃗b ∈ {0, 1, ∗}n and for every transition ti = (ai, gi, ui), we
compute an over-approximation of a may-successor of ⃗b under ti as
if is_valid([⃗b, Φ] =⇒ ¬gi) then there is no successor
otherwise, the successor ⃗b′ is given by
b′
j =



1 if is_valid([⃗b, Φ] =⇒ pre(ai, ϕj))
0 if is_valid([⃗b, Φ] =⇒ pre(ai, ¬ϕj))
∗ otherwise
example: consider the abstract state ⃗b = (1, 0) where ϕ1 = (x > 0) and
ϕ2 = (x > 2) and compute the successor corresponding to (a, ⊤, x := x + 1)
(1, 0)
a
→may′ ( , )
IA169 Model Checking: Abstraction and CEGAR 60/96
Abstraction in practice
for every abstract state ⃗b ∈ {0, 1, ∗}n and for every transition ti = (ai, gi, ui), we
compute an over-approximation of a may-successor of ⃗b under ti as
if is_valid([⃗b, Φ] =⇒ ¬gi) then there is no successor
otherwise, the successor ⃗b′ is given by
b′
j =



1 if is_valid([⃗b, Φ] =⇒ pre(ai, ϕj))
0 if is_valid([⃗b, Φ] =⇒ pre(ai, ¬ϕj))
∗ otherwise
example: consider the abstract state ⃗b = (1, 0) where ϕ1 = (x > 0) and
ϕ2 = (x > 2) and compute the successor corresponding to (a, ⊤, x := x + 1)
(1, 0)
a
→may′ (1, )
(x > 0) ∧ (x ≤ 2) =⇒ (⊤ =⇒ (x + 1 > 0)) is true
IA169 Model Checking: Abstraction and CEGAR 61/96
Abstraction in practice
for every abstract state ⃗b ∈ {0, 1, ∗}n and for every transition ti = (ai, gi, ui), we
compute an over-approximation of a may-successor of ⃗b under ti as
if is_valid([⃗b, Φ] =⇒ ¬gi) then there is no successor
otherwise, the successor ⃗b′ is given by
b′
j =



1 if is_valid([⃗b, Φ] =⇒ pre(ai, ϕj))
0 if is_valid([⃗b, Φ] =⇒ pre(ai, ¬ϕj))
∗ otherwise
example: consider the abstract state ⃗b = (1, 0) where ϕ1 = (x > 0) and
ϕ2 = (x > 2) and compute the successor corresponding to (a, ⊤, x := x + 1)
(1, 0)
a
→may′ (1, ∗ )
(x > 0) ∧ (x ≤ 2) =⇒ (⊤ =⇒ (x + 1 > 0)) is true
(x > 0) ∧ (x ≤ 2) =⇒ (⊤ =⇒ (x + 1 > 2)) is not true
(x > 0) ∧ (x ≤ 2) =⇒ (⊤ =⇒ (x + 1 ≤ 2)) is not true
IA169 Model Checking: Abstraction and CEGAR 62/96
Abstraction in practice
for every transition, we compute successors of all abstract states
based on the successors, we transform the original implicit representation of a
system into a Boolean program
it is very similar to a model in guarded command language, but instead of
integers it uses only Boolean variables ⃗b representing the validity of
abstraction predicates Φ
Boolean program is an implicit representation of an over-approximation of
Mmay
Boolean program can be used as an input for a suitable model checker (of
finite-state systems)
IA169 Model Checking: Abstraction and CEGAR 63/96
Example
consider the model (V, E), where
V = {x}
E = {(a, ⊤, x := x + 1),
(b, ¬(x > 0), x := 0),
(c, (x > 0) ∧ (x ≤ 2), x := 0),
(d, (x > 2), x := 0)}
using the predicates ϕ1 = (x > 0), ϕ2 = (x > 2), we get the following Boolean
program defining an over-approximation of Mmay
V = {b1, b2}, where b1, b2 represents the validity of ϕ1, ϕ2
E = {(a, ⊤, b1 := if b1 then 1 else ∗;
b2 := if b2 then 1 else if b1 then ∗ else 0),
(b, ¬b1, b1 := 0; b2 := 0),
(c, b1 ∧ ¬b2, b1 := 0; b2 := 0),
(d, b2, b1 := 0; b2 := 0)}
IA169 Model Checking: Abstraction and CEGAR 64/96
Example of a real NQC code and its absraction
task light_sensor_control() {
int x = 0;
while (true) {
if (LIGHT > LIGHT_THRESHOLD) {
PlaySound(SOUND_CLICK);
Wait(30);
x = x + 1;
} else {
if (x > 2) {
PlaySound(SOUND_UP);
ClearTimer(0);
brick = LONG;
} else if (x > 0) {
PlaySound(SOUND_DOUBLE_BEEP);
ClearTimer(0);
brick = SHORT;
}
x = 0;
}
}
}
IA169 Model Checking: Abstraction and CEGAR 65/96
Example of a real NQC code and its absraction
task light_sensor_control() {
int x = 0;
while (true) {
if (LIGHT > LIGHT_THRESHOLD) {
PlaySound(SOUND_CLICK);
Wait(30);
x = x + 1;
} else {
if (x > 2) {
PlaySound(SOUND_UP);
ClearTimer(0);
brick = LONG;
} else if (x > 0) {
PlaySound(SOUND_DOUBLE_BEEP);
ClearTimer(0);
brick = SHORT;
}
x = 0;
}
}
}
task A_light_sensor_control() {
bool b = false;
while (true) {
if (*) {
b = b ? true : * ;
} else {
if (b) {
brick = LONG;
} else if (b ? true : *) {
brick = SHORT;
}
b = false;
}
}
}
IA169 Model Checking: Abstraction and CEGAR 66/96
CEGAR: counterexample-guided abstraction refinement
Motivation
it is hard to find a small and valuable abstraction
abstraction predicates were originally provided by a user
CEGAR tries to find a suitable abstraction automatically
implemented in SLAM, BLAST, Static Driver Verifier (SDV), and many others
incomplete method, but very successfull in practice
IA169 Model Checking: Abstraction and CEGAR 68/96
Principle of CEGAR
original system M specification φ
IA169 Model Checking: Abstraction and CEGAR 69/96
Principle of CEGAR
original system M specification φ
build a new
abstract model
M′ (M ≤ M′)
AP(φ)
IA169 Model Checking: Abstraction and CEGAR 70/96
Principle of CEGAR
original system M specification φ
build a new
abstract model
M′ (M ≤ M′)
model check
M′ |= φ?
IA169 Model Checking: Abstraction and CEGAR 71/96
Principle of CEGAR
original system M specification φ
build a new
abstract model
M′ (M ≤ M′)
model check
M′ |= φ?
NO BUG!
M |= φ
YES
IA169 Model Checking: Abstraction and CEGAR 72/96
Principle of CEGAR
original system M specification φ
build a new
abstract model
M′ (M ≤ M′)
model check
M′ |= φ?
analyze
counterexample
NO BUG!
M |= φ
YES
NO
IA169 Model Checking: Abstraction and CEGAR 73/96
Principle of CEGAR
original system M specification φ
build a new
abstract model
M′ (M ≤ M′)
model check
M′ |= φ?
analyze
counterexample
NO BUG!
M |= φ
BUG!
M ̸|= φ
YES
NO
real
IA169 Model Checking: Abstraction and CEGAR 74/96
Principle of CEGAR
original system M specification φ
build a new
abstract model
M′ (M ≤ M′)
model check
M′ |= φ?
analyze
counterexample
add new
abstraction
predicates
NO BUG!
M |= φ
BUG!
M ̸|= φ
YES
NO
real
spurious
IA169 Model Checking: Abstraction and CEGAR 75/96
Principle of CEGAR
original system M specification φ
build a new
abstract model
M′ (M ≤ M′)
model check
M′ |= φ?
analyze
counterexample
add new
abstraction
predicates
NO BUG!
M |= φ
BUG!
M ̸|= φ
YES
NO
real
spurious
IA169 Model Checking: Abstraction and CEGAR 76/96
Notes
added abstraction predicates ensure that the new abstract model M′ does not
have the behaviour corresponding to the spurious counterexample of the
previous M′
the analysis of an abstract counterexample and finding new abstract
predicates are nontrivial tasks
the method is sound but incomplete: the algorithm can run in the cycle forever
or fail to find new abstraction predicates
IA169 Model Checking: Abstraction and CEGAR 77/96
Counterexample analysis
an abstract path is a finite or infinite path in an abstract model
an abstract path a1a2 . . . is real if there exists a path s1s2 . . . in the original
system M of the same length such that s1 is initial and si ∈ h−1(ai) for all i
an abstract path that is not real is called spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
IA169 Model Checking: Abstraction and CEGAR 78/96
Analysis of finite counterexamples (e.g. for reachability)
input : a nonempty abstract path a1 . . . an,
an original system M = (S, →, S0, L), an abstraction function h
output: “real” if the path is real; j, R′ otherwise, where j is the length of the
maximal real prefix of the path and R′ is the set of the last states of the
paths in M corresponding to the prefix
R ← h−1(a1) ∩ S0
if R = ∅ then return 0, ∅ // spurious
j ← 1
while R ̸= ∅ ∧ j < n do
j ← j + 1
R′ ← R
R ← {s | ∃s′ ∈ R . s′ → s} ∩ h−1(aj)
if R ̸= ∅ then return real
return j − 1, R′ // spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
IA169 Model Checking: Abstraction and CEGAR 79/96
Analysis of finite counterexamples (e.g. for reachability)
input : a nonempty abstract path a1 . . . an,
an original system M = (S, →, S0, L), an abstraction function h
output: “real” if the path is real; j, R′ otherwise, where j is the length of the
maximal real prefix of the path and R′ is the set of the last states of the
paths in M corresponding to the prefix
R ← h−1(a1) ∩ S0
if R = ∅ then return 0, ∅ // spurious
j ← 1
while R ̸= ∅ ∧ j < n do
j ← j + 1
R′ ← R
R ← {s | ∃s′ ∈ R . s′ → s} ∩ h−1(aj)
if R ̸= ∅ then return real
return j − 1, R′ // spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
IA169 Model Checking: Abstraction and CEGAR 80/96
Analysis of finite counterexamples (e.g. for reachability)
input : a nonempty abstract path a1 . . . an,
an original system M = (S, →, S0, L), an abstraction function h
output: “real” if the path is real; j, R′ otherwise, where j is the length of the
maximal real prefix of the path and R′ is the set of the last states of the
paths in M corresponding to the prefix
R ← h−1(a1) ∩ S0
if R = ∅ then return 0, ∅ // spurious
j ← 1
while R ̸= ∅ ∧ j < n do
j ← j + 1
R′ ← R
R ← {s | ∃s′ ∈ R . s′ → s} ∩ h−1(aj)
if R ̸= ∅ then return real
return j − 1, R′ // spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
IA169 Model Checking: Abstraction and CEGAR 81/96
Analysis of finite counterexamples (e.g. for reachability)
input : a nonempty abstract path a1 . . . an,
an original system M = (S, →, S0, L), an abstraction function h
output: “real” if the path is real; j, R′ otherwise, where j is the length of the
maximal real prefix of the path and R′ is the set of the last states of the
paths in M corresponding to the prefix
R ← h−1(a1) ∩ S0
if R = ∅ then return 0, ∅ // spurious
j ← 1
while R ̸= ∅ ∧ j < n do
j ← j + 1
R′ ← R
R ← {s | ∃s′ ∈ R . s′ → s} ∩ h−1(aj)
if R ̸= ∅ then return real
return j − 1, R′ // spurious
a1 a2 a3 a4
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
produced output: 3, {s9}
IA169 Model Checking: Abstraction and CEGAR 82/96
Analysis of lasso-shaped counterexamples
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA169 Model Checking: Abstraction and CEGAR 83/96
Analysis of lasso-shaped counterexamples
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA169 Model Checking: Abstraction and CEGAR 84/96
Analysis of lasso-shaped counterexamples
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA169 Model Checking: Abstraction and CEGAR 85/96
Analysis of lasso-shaped counterexamples
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA169 Model Checking: Abstraction and CEGAR 86/96
Analysis of lasso-shaped counterexamples
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2 a1
3 a2
2 a2
3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA169 Model Checking: Abstraction and CEGAR 87/96
Analysis of lasso-shaped counterexamples
a1 a2 a3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2 a1
3 a2
2 a2
3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
an abstract loop may correspond to loops of different size and starting at
different stages of the unwinding
the unwinding eventually becomes periodic, the size of the period is the least
common multiple of the size of individual loops
IA169 Model Checking: Abstraction and CEGAR 88/96
Analysis of lasso-shaped counterexamples
Analysis of a lasso-shaped counterexample can be reduced to analysis of a finite
path counterexample.
Theorem
An abstract lasso-shaped path a1 . . . ai(ai+1 . . . an)ω is real iff the abstract path
a1 . . . ai(ai+1 . . . an)m+1 is real, where m = mini+1≤j≤n |h−1(aj)|.
IA169 Model Checking: Abstraction and CEGAR 89/96
Analysis of lasso-shaped counterexamples
Analysis of a lasso-shaped counterexample can be reduced to analysis of a finite
path counterexample.
Theorem
An abstract lasso-shaped path a1 . . . ai(ai+1 . . . an)ω is real iff the abstract path
a1 . . . ai(ai+1 . . . an)m+1 is real, where m = mini+1≤j≤n |h−1(aj)|.
a1 a2 a3
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2 a1
3 a2
2 a2
3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA169 Model Checking: Abstraction and CEGAR 90/96
Analysis of lasso-shaped counterexamples
Analysis of a lasso-shaped counterexample can be reduced to analysis of a finite
path counterexample.
Theorem
An abstract lasso-shaped path a1 . . . ai(ai+1 . . . an)ω is real iff the abstract path
a1 . . . ai(ai+1 . . . an)m+1 is real, where m = mini+1≤j≤n |h−1(aj)|.
a1 a2 a3
•
•
•
•
•
•
•
•
−→
a1 a0
2 a0
3 a1
2 a1
3 a2
2 a2
3
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
IA169 Model Checking: Abstraction and CEGAR 91/96
Abstraction refinement
. . .
. . . aj−1 aj aj+1 . . .
. . .
Sj−1
SB
SI
SD
SB = h−1(aj) ∩ {s | ∃s′ ∈ h−1(aj+1) . s → s′} bad states
SI = h−1(aj) ∖ (SB ∪ SD) irrelevant states
SD = the set produced by the counterexample analysis dead-end states
IA169 Model Checking: Abstraction and CEGAR 92/96
Abstraction refinement
. . .
. . . aj−1 aj aj+1 . . .
. . .
Sj−1
SB
SI
SD
SB = h−1(aj) ∩ {s | ∃s′ ∈ h−1(aj+1) . s → s′} bad states
SI = h−1(aj) ∖ (SB ∪ SD) irrelevant states
SD = the set produced by the counterexample analysis dead-end states
to eliminate the spurious counterexample, we need to refine the abstraction
such that no abstract state contains states from both SB and SD
typically, we add an abstraction predicate that is an interpolant of SB and SD
IA169 Model Checking: Abstraction and CEGAR 93/96
Abstraction refinement
Consider abstract state (3 ≤ x ≤ 5) ∧ (7 ≤ y ≤ 9) and SB, SI, SD:
3 4 5
7 B I I
8 D I B
9 I D D
IA169 Model Checking: Abstraction and CEGAR 94/96
Abstraction refinement
Consider abstract state (3 ≤ x ≤ 5) ∧ (7 ≤ y ≤ 9) and SB, SI, SD:
3 4 5
7 B I I
8 D I B
9 I D D
−→
3 4 5
7 B + I I
8 D + I B
9 D + I D
or
3 4 5
7
B + I D + I
9
8 D B + I
?
there could be more possible abstraction refinements
we want the coarsest refinement (i.e., with the least number of abstract states)
IA169 Model Checking: Abstraction and CEGAR 95/96
Abstraction refinement
Consider abstract state (3 ≤ x ≤ 5) ∧ (7 ≤ y ≤ 9) and SB, SI, SD:
3 4 5
7 B I I
8 D I B
9 I D D
−→
3 4 5
7 B + I I
8 D + I B
9 D + I D
or
3 4 5
7
B + I D + I
9
8 D B + I
?
there could be more possible abstraction refinements
we want the coarsest refinement (i.e., with the least number of abstract states)
Theorem
The problem of finding the coarsest refinement is NP-hard.
there are heuristics that select suitable refinements
IA169 Model Checking: Abstraction and CEGAR 96/96