IA159 Formal Verification Methods
Partial Order Reduction
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
Focus
stuttering principle
theory of partial order reduction
heuristics for efficient implementation
Source
Chapter 10 of E. M. Clarke, O. Grumberg, and D. A. Peled:
Model Checking, MIT, 1999.
IA159 Formal Verification Methods: Partial Order Reduction 2/72
Basic facts on partial order reduction
compatible with model checking of finite systems against
LTL formulae without X operator
size of the reduced system is 3–99% of the original size
model checking process for reduced systems is faster and
consumes less memory
best suited for asynchronous systems
also known as model checking using representatives
IA159 Formal Verification Methods: Partial Order Reduction 3/72
Modified definition of Kripke structure
We consider only deterministic systems.
A Kripke structure is a tuple M = (S, T, S0, L), where
S is a finite set of states
T is a set of transitions, each α ∈ T is a partial function
α : S → S.
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 transition α is enabled in s if α(s) is defined
α is disabled in s otherwise
enabled(s) denotes the set of transitions enabled in s
IA159 Formal Verification Methods: Partial Order Reduction 4/72
More definitions
Let ϕ be an LTL formula and K = (S, T, S0, L) be a Kripke
structure.
AP(ϕ) is the set of atomic propositions occurring in ϕ
a path in K starting from a state s ∈ S is an infinite
sequence π = s0, s1, . . . of states such that s0 = s and for
each i there is a transition αi ∈ T such that αi(si) = si+1
a path starting in a fixed state can be identified with a
sequence of transitions
a path π satisfies ϕ, written π |= ϕ, if w |= ϕ, where the
word w = w(0)w(1) . . . is defined as w(i) = L(si) ∩ AP(ϕ)
for all i ≥ 0
K satisfies ϕ, written K |= ϕ, if all paths starting from initial
states of K satisfy ϕ
IA159 Formal Verification Methods: Partial Order Reduction 5/72
Goal of partial order reduction
LTL−X denotes LTL formulae without X operator.
Goal
Given a finite Kripke structure K and an LTL−X formula ϕ, we
want to find a smaller Kripke structure K such that
K |= ϕ ⇐⇒ K |= ϕ.
IA159 Formal Verification Methods: Partial Order Reduction 6/72
Reduction method
K arises from K by disabling some transitions in some
states
as a result, some states may become unreachable in K
for each state s, ample(s) denotes the set of transitions
that are enabled in s in K , ample(s) ⊆ enabled(s)
calculation of ample sets needs to satisfy three goals
1 K given by ample sets has to satisfy
K |= ϕ ⇐⇒ K |= ϕ
2 K should be substantially smaller than K
3 the overhead in calculating ample sets must be small
IA159 Formal Verification Methods: Partial Order Reduction 7/72
A base of partial order reduction
Stuttering principle
IA159 Formal Verification Methods: Partial Order Reduction 8/72
Stuttering on words
let w = w(0)w(1)w(2) . . . be an infinite word
a letter w(i) is called redundant iff w(i) = w(i + 1) and
there is j > i such that w(i) = w(j)
canonical form of w is the word obtained by deleting all
redundant letters from w
infinite words w1, w2 are stutter equivalent, written
w1 ∼ w2, iff they have the same canonical form
Example
canonical form of kk k oooo o m k k.nω is komk.nω
canonical form of k oo o mmmmm m kkk k.nω is komk.nω
hence kkkooooomkk.nω ∼ kooommmmmmkkkk.nω
IA159 Formal Verification Methods: Partial Order Reduction 9/72
Stuttering principle
Theorem (Lamport 1983)
Let ϕ be an LTL−X formula and w1, w2 be two stutter equivalent
words. Then
w1 |= ϕ ⇐⇒ w2 |= ϕ.
IA159 Formal Verification Methods: Partial Order Reduction 10/72
Stuttering on paths
Paths π = s0s1 . . . and π = s0s1 . . . are stutter equivalent with
respect to a set AP ⊆ AP, written π ∼AP π , iff w ∼ w , where
w, w are defined as w(i) = L(si) ∩ AP and w (i) = L(si ) ∩ AP
for each i.
Kripke structures K, K are stutter equivalent with respect to
AP , written K ∼AP K , iff
K and K have the same set of initial states and
for each path π of K starting in an initial state s there exists
a path π of K starting in the same initial state such that
π ∼AP π and vice versa.
IA159 Formal Verification Methods: Partial Order Reduction 11/72
Stuttering principle for Kripke structures
Corollary
Let ϕ be an LTL−X formula and K, K be Kripke structures such
that K ∼AP(ϕ) K . Then
K |= ϕ ⇐⇒ K |= ϕ.
IA159 Formal Verification Methods: Partial Order Reduction 12/72
Stuttering principle for Kripke structures
Corollary
Let ϕ be an LTL−X formula and K, K be Kripke structures such
that K ∼AP(ϕ) K . Then
K |= ϕ ⇐⇒ K |= ϕ.
Hence, for every set of stutter equivalent paths (with respect to
AP(ϕ)) of K it is sufficient to keep at least one representant of
these paths in K .
IA159 Formal Verification Methods: Partial Order Reduction 13/72
Example

x=2
β0

x:=x+1
11
x=2
β1

x:=x+1
11
x=2
β0
x=2
x:=x+1
11
x=2
β1
x=2

Let AP(ϕ) contain just x = 2.
IA159 Formal Verification Methods: Partial Order Reduction 14/72
Example

x=2
β0

x:=x+1
11
x=2
β1

x:=x+1
11
x=2
β0
x=2
x:=x+1
11
x=2
β1
x=2

Let AP(ϕ) contain just x = 2.
x=2 x=2 x=2 x=2 . . .
x=2 x=2 x=2 x=2 . . .
x=2 x=2 x=2 x=2 . . .
IA159 Formal Verification Methods: Partial Order Reduction 15/72
Example

x=2
β0

x:=x+1
11
x=2
β1

x:=x+1
11
x=2
β0
x=2
x:=x+1
11
x=2
β1
x=2

Let AP(ϕ) contain just x = 2.
x=2 x=2 x=2 x=2 . . .
IA159 Formal Verification Methods: Partial Order Reduction 16/72
Theory of partial order reduction
Conditions on ample sets
IA159 Formal Verification Methods: Partial Order Reduction 17/72
Terminology: (in)visibility and full expansion
A transition α ∈ T is invisible if for each pair of states s, s ∈ S
such that α(s) = s it holds that
L(s) ∩ AP(ϕ) = L(s ) ∩ AP(ϕ).
A transition is visible if it is not invisible.
IA159 Formal Verification Methods: Partial Order Reduction 18/72
Terminology: (in)visibility and full expansion
A transition α ∈ T is invisible if for each pair of states s, s ∈ S
such that α(s) = s it holds that
L(s) ∩ AP(ϕ) = L(s ) ∩ AP(ϕ).
A transition is visible if it is not invisible.
A state s is fully expanded when ample(s) = enabled(s).
IA159 Formal Verification Methods: Partial Order Reduction 19/72
Terminology: (in)dependence
s
α
~~
β
22
s1
β 22
s2
α
~~
r
An independence relation I ⊆ T × T is a symmetric and
antireflexive relation satisfying the following two conditions for
each state s ∈ S and for each (α, β) ∈ I:
1 enabledness: if α, β ∈ enabled(s) then α ∈ enabled(β(s))
2 commutativity: if α, β ∈ enabled(s) then α(β(s)) = β(α(s))
The dependency relation D is the complement of I.
IA159 Formal Verification Methods: Partial Order Reduction 20/72
Condition C0
If all ample sets satisfy the following conditions C0, C1, C2, and
C3, then K ∼AP(ϕ) K.
IA159 Formal Verification Methods: Partial Order Reduction 21/72
Condition C0
If all ample sets satisfy the following conditions C0, C1, C2, and
C3, then K ∼AP(ϕ) K.
C0
ample(s) = ∅ ⇐⇒ enabled(s) = ∅.
IA159 Formal Verification Methods: Partial Order Reduction 22/72
Condition C1
C1
Along every path in the original structure that starts in s, the
following condition holds: a transition outside ample(s) and
dependent on a transition in ample(s) cannot be executed
without a transition in ample(s) occuring first.
IA159 Formal Verification Methods: Partial Order Reduction 23/72
Condition C1
C1
Along every path in the original structure that starts in s, the
following condition holds: a transition outside ample(s) and
dependent on a transition in ample(s) cannot be executed
without a transition in ample(s) occuring first.
Lemma
If C1 holds, then the transitions in enabled(s) ample(s) are
all independent of those in ample(s).
IA159 Formal Verification Methods: Partial Order Reduction 24/72
Condition C1
C1
Along every path in the original structure that starts in s, the
following condition holds: a transition outside ample(s) and
dependent on a transition in ample(s) cannot be executed
without a transition in ample(s) occuring first.
Thanks to C1, all paths of K starting in a state s and not
included in K have one of the following two forms:
the path has a prefix β0β1 . . . βmα, where α ∈ ample(s)
and each βi is independent of all transitions in ample(s)
including α.
the path is an infinite sequence of transitions β0β1 . . .
where each βi is independent of all transitions in ample(s).
IA159 Formal Verification Methods: Partial Order Reduction 25/72
Condition C1: consequences
s
β0
ÖÖ
α
$$
s1
β1
ÕÕ
α
$$
r0
β0
ÖÖ
s2
β2
ÕÕ
α
%%
r1
β1
ÖÖ
βm
ÕÕ
r2
β2
ÕÕsm
α
%%
βm
ÕÕ
rm
Due to C1, after execution of a sequence
β0β1 . . . βm of a transitions
not in ample(s) from s, all the transitions
in ample(s) remain enabled.
Further, the sequence β0β1 . . . βmα
executed from s leads to the same
state as the sequence αβ0β1 . . . βm.
As the sequence β0β1 . . . βmα is not
included in the reduced system, we
want β0β1 . . . βmα and αβ0β1 . . . βm
to be prefixes of stutter equivalent
paths. This is quaranteed if α is in-
visible.
IA159 Formal Verification Methods: Partial Order Reduction 26/72
Condition C2
C2 (invisibility)
If s is not fully expanded, then every α ∈ ample(s) is invisible.
IA159 Formal Verification Methods: Partial Order Reduction 27/72
Condition C3: motivation
Conditions C0, C1, and C2 are not yet sufficient to guarantee
that K is stutter equivalent to K. There is a possibility that
some transition will be delayed forever because of a cycle.

β


α1
((
α3
ff
α2
oo

β

α1
((
β

α3
ff
β

α2
oo
α1
((
α3
ff
α2
oo

α1
((
α3
ff
α2
oo
β is visible, α1, α2, α3 are invisible, β is independent of
α1, α2, α3, and α1, α2, α3 are interdependent
IA159 Formal Verification Methods: Partial Order Reduction 28/72
Condition C3
C3 (cycle condition)
A cycle in reduced structure is not allowed if it contains a state
in which some transition is enabled, but is never included in
ample(s) for any state s on the cycle.
IA159 Formal Verification Methods: Partial Order Reduction 29/72
Partial order reduction
Correctness
IA159 Formal Verification Methods: Partial Order Reduction 30/72
Statement
Theorem
Let ϕ be an LTL−X formula and K be a Kripke structure. If K is
a reduction of K satisfying C0–C3, then
K ∼AP(ϕ) K .
IA159 Formal Verification Methods: Partial Order Reduction 31/72
Terminology
since now a path can be finite or infinite
σ ◦ η the concatenation of a finite path σ and a (finite or
infinite) path η (◦ is applicable if the last state last(σ) of σ is
the same as the first state of η)
tr(π) denote the sequence of transitions on a path π
for a (finite or infinite) sequence v of transitions, vis(v)
denotes its projection onto the visible transitions
IA159 Formal Verification Methods: Partial Order Reduction 32/72
Construction
For every infinite path π of K starting in some initial state we
construct an infinite sequence of paths
π = π0, π1, π2, π3, . . .
where, for each i, πi = σi ◦ ηi such that |σi| = i.
IA159 Formal Verification Methods: Partial Order Reduction 33/72
Construction
For every infinite path π of K starting in some initial state we
construct an infinite sequence of paths
π = π0, π1, π2, π3, . . .
where, for each i, πi = σi ◦ ηi such that |σi| = i.
π = π0 = s0
α0
GG s1
α1
GG s2
α2
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 34/72
Construction
For every infinite path π of K starting in some initial state we
construct an infinite sequence of paths
π = π0, π1, π2, π3, . . .
where, for each i, πi = σi ◦ ηi such that |σi| = i.
π = π0 = s0
α0
GG s1
α1
GG s2
α2
GG . . .
π0 = σ0 ◦ η0
s0 s0
α0
GG s1
α1
GG s2
α2
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 35/72
Construction of πi+1
Let s0 be the last state of σi.
The construction of πi+1 depends on α0.
πi = oo σi GG ◦ oo ηi
• GG . . . GG s0
α0
GG •
α1
GG •
α2
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 36/72
Construction of πi+1
Case A α0 ∈ ample(s0).
πi = oo σi GG ◦ oo ηi
• GG . . . GG s0
α0
GG •
α1
GG •
α2
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 37/72
Construction of πi+1
Case A α0 ∈ ample(s0).
πi = oo σi GG ◦ oo ηi
• GG . . . GG s0
α0
GG •
α1
GG •
α2
GG . . .
πi+1 = oo
σi+1
GG ◦ oo
ηi+1
• GG . . . GG s0
α0
GG •
α1
GG •
α2
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 38/72
Construction of πi+1
Case B α0 ∈ ample(s0).
By C2, all transitions in ample(s0) must be invisible.
Due to C0 and C1, there are two cases.
πi = oo σi GG ◦ oo ηi
• GG . . . GG s0
α0
GG •
α1
GG •
α2
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 39/72
Construction of πi+1
Case B1 α0 ∈ ample(s0).
Some β ∈ ample(s0) appears on ηi after a finite
sequence of independent transitions α0α1 . . . αk−1.
πi = oo σi GG ◦ oo ηi
• GG . . . GG s0
α0
GG . . .
αk−1
GG • β
77
. . . •
αk+1
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 40/72
Construction of πi+1
Case B1 α0 ∈ ample(s0).
Some β ∈ ample(s0) appears on ηi after a finite
sequence of independent transitions α0α1 . . . αk−1.
πi = oo σi GG ◦ oo ηi
• GG . . . GG s0
α0
GG
β 88
. . .
αk−1
GG • β
77
• α0
GG . . . αk−1
GG •
αk+1
GG . . .
πi+1 = oo
σi+1
GG ◦ oo
ηi+1
• GG . . . GG s0 β
77
•
α0
GG . . .
αk−1
GG •
αk+1
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 41/72
Construction of πi+1
Case B2 α0 ∈ ample(s0).
Some β ∈ ample(s0) is independent
of all transitions in ηi.
πi = oo σi GG ◦ oo ηi
• GG . . . GG s0
α0
GG
β 77
•
α1
GG •
α2
GG . . .
•
IA159 Formal Verification Methods: Partial Order Reduction 42/72
Construction of πi+1
Case B2 α0 ∈ ample(s0).
Some β ∈ ample(s0) is independent
of all transitions in ηi.
πi = oo σi GG ◦ oo ηi
• GG . . . GG s0
α0
GG
β 77
•
α1
GG
66
•
α2
GG
77
. . .
• α0
GG • α1
GG • α2
GG . . .
πi+1 = oo
σi+1
GG ◦ oo
ηi+1
• GG . . . GG s0 β
77
•
α0
GG •
α1
GG •
α2
GG . . .
IA159 Formal Verification Methods: Partial Order Reduction 43/72
Properties of π0, π1, π2, . . .
Lemma
For all πi, πj, it holds:
πi ∼AP(ϕ) πj
vis(tr(πi)) = vis(tr(πj))
if ξi, ξj are prefixes of πi, πj satisfying
vis(tr(ξi)) = vis(tr(ξj)), then
L(last(ξi)) ∩ AP(ϕ) = L(last(ξj)) ∩ AP(ϕ).
(It is sufficient to prove it for πi and πi+1. And this is easy.)
IA159 Formal Verification Methods: Partial Order Reduction 44/72
Definition of σ
We define an infinite path σ as the limit of the finite paths σi.
To prove correctness of the reduction, we have to show that:
1 σ belongs to the reduced structure K
2 σ ∼AP(ϕ) π
(The first item follows directly from the construction of σi.)
IA159 Formal Verification Methods: Partial Order Reduction 45/72
Properties of σ
”Every transition of π eventually appears in σ.”
Lemma
Let α be the first transition of ηi. There exists j > i such that α
is the last transition of σj and, for all i ≤ k < j, α is the first
transition of ηk .
(This is a consequence of C3.)
IA159 Formal Verification Methods: Partial Order Reduction 46/72
Properties of σ
”Only invisible transitions are added to σ.
Visible transitions of π keep their order.”
Lemma
Let γ be the first visible transition on ηi and prefixγ(ηi) be the
maximal prefix of tr(ηi) that does not contain γ. Then one of the
following holds:
γ is the first action of ηi and the last transition of σi+1, or
γ is the first visible transition of ηi+1, the last transition of
σi+1 is invisible, and prefixγ(ηi+1) prefixγ(ηi).
v w denotes that v = w or v can be obtained from w by
erasing one or more transitions.
IA159 Formal Verification Methods: Partial Order Reduction 47/72
Properties of σ
Lemma
Let v be a prefix of vis(tr(π)). Then there exists a path σi such
that v = vis(tr(σi)).
Lemma
σ ∼AP(ϕ) π.
Hence, K ∼AP(ϕ) K .
IA159 Formal Verification Methods: Partial Order Reduction 48/72
Calculating ample sets
Complexity of checking conditions C0–C3
IA159 Formal Verification Methods: Partial Order Reduction 49/72
Conditions C0 and C2
C0
ample(s) = ∅ ⇐⇒ enabled(s) = ∅.
C2 (invisibility)
If s is not fully expanded, then every α ∈ ample(s) is invisible.
conditions C0 and C2 are local: their validity depends just
on enabled(s) and ample(s), not on the whole structure
C0 can be checked in constant time
C2 can be checked in linear time with respect to |ample(s)|
IA159 Formal Verification Methods: Partial Order Reduction 50/72
Condition C1
C1
Along every path in the original structure that starts in s, the
following condition holds: a transition outside ample(s) and
dependent on a transition in ample(s) cannot be executed
without a transition in ample(s) occuring first.
checking C1 for a state s and a set T ⊆ enabled(s) is at
least as hard as checking reachability for K (reachability
problem can be reduced to checking C1)
we give a procedure computing a set of transitions that is
guaranteed to satisfy C1
computed sets do not have to be optimal: tradeoff
efficiency Vs. amount of reduction
IA159 Formal Verification Methods: Partial Order Reduction 51/72
Condition C3
C3 (cycle condition)
A cycle in reduced structure is not allowed if it contains a state
in which some transition is enabled, but is never included in
ample(s) for any state s on the cycle.
C3 is also non-local
in contrast to C1, C3 refers only to the reduced structure
instead of checking C3, we formulate a stronger condition
which is easier to check
IA159 Formal Verification Methods: Partial Order Reduction 52/72
Condition C3
Lemma
Assume that C1 holds for all ample sets along a cycle in a
reduced structure. If at least one state along the cycle is fully
expanded, then C3 hold for this cycle.
C1 implies that each α ∈ enabled(s) ample(s) is
independent of transitions in ample(s)
α ∈ enabled(s) ample(s) is also enabled in the next
state on the cycle in K
if the cycle contains a fully expanded state, then it surely
satisfies C3
IA159 Formal Verification Methods: Partial Order Reduction 53/72
Condition C3’
If K is generated using depth-first search strategy, then every
cycle in K has to contain a back edge (i.e. an edge going to a
state on the search stack)
C3’
If s is not fully expanded, then no transition in ample(s) may
reach a state that is on the search stack.
C3’ can be checked efficiently during nestedDFS algorithm
IA159 Formal Verification Methods: Partial Order Reduction 54/72
Calculating ample sets
Algorithm
IA159 Formal Verification Methods: Partial Order Reduction 55/72
Basic information
Reduced system is constructed on-the-fly: ample(s) is
computed only when a model checking algorithm needs to
know successors of s.
Algorithm computing ample sets depends on the model of
computation. We consider processes with
shared variables and
message passing with queues.
IA159 Formal Verification Methods: Partial Order Reduction 56/72
Notation
pci(s) denotes the program counter of process Pi in a
state s
pre(α) is a set including all transitions β such that there
exists a state s for which α ∈ enabled(s) and
α ∈ enabled(β(s))
dep(α) is the set of all transitions that are dependent on α
Ti is the set of transitions of process Pi
Ti(s) = Ti ∩ enabled(s)
currenti(s) is the set of all transitions of Pi that are enabled
in some s such that pci(s) = pci(s )
(note that Ti(s) ⊆ currenti(s))
IA159 Formal Verification Methods: Partial Order Reduction 57/72
Tradeoff
We do not compute the sets pre(α) and dep(α) precisely.
We preffer to efficiently compute over-approximations of these
sets.
IA159 Formal Verification Methods: Partial Order Reduction 58/72
Computing pre(α)
pre(α) includes the transitions of the processes that
contain α and that can change a program counter to a
value from which α can execute
if the enabling condition for α involves shared variables,
then pre(α) includes all other transitions that can change
these shared variables
if α sends or receives messages on some queue q, then
pre(α) includes transitions of other processes that receive
or send data through q, respectively
IA159 Formal Verification Methods: Partial Order Reduction 59/72
Computing dep(α)
pairs of transitions that share a variable, which is changed
by at least one of them, are dependent
pairs of transitions belonging to the same process are
dependent
two receive transitions that use the same message queue
are dependent
two send transitions are also dependent (sending a
message may cause the queue to fill)
Note that a pair of send and receive transitions in different
processes are independent as they can potentially enable each
other, but not disable.
IA159 Formal Verification Methods: Partial Order Reduction 60/72
Sketch of the algorithm
C1 implies that transitions in enabled(s) ample(s) are
independent on those in ample(s)
as transitions in Ti(s) are interdependent, it holds
Ti(s) ⊆ ample(s) ∨ Ti(s) ∩ ample(s) = ∅
hence, Ti(s) is a good candidate for ample(s)
IA159 Formal Verification Methods: Partial Order Reduction 61/72
Sketch of the algorithm
C1 implies that transitions in enabled(s) ample(s) are
independent on those in ample(s)
as transitions in Ti(s) are interdependent, it holds
Ti(s) ⊆ ample(s) ∨ Ti(s) ∩ ample(s) = ∅
hence, Ti(s) is a good candidate for ample(s)
Idea of the algorithm
We check whether some Ti(s) = ∅ satisfies the conditions C1,
C2, and C3’. If there is no such Ti(s), we set
ample(s) = enabled(s).
IA159 Formal Verification Methods: Partial Order Reduction 62/72
Checking C1
C1
Along every path in the original structure that starts in s, the
following condition holds: a transition outside ample(s) and
dependent on a transition in ample(s) cannot be executed
without a transition in ample(s) occuring first.
If ample(s) = Ti(s) violates C1, then there is a path
s
β0
GG
}}  33
•
β1
GG . . .
βn
GG •
α GG . . .
where
α ∈ Ti(s) and α is dependent on Ti(s),
β0, . . . , βn are independent on Ti(s).
IA159 Formal Verification Methods: Partial Order Reduction 63/72
Checking C1
s
β0
GG
~~  22
•
β1
GG . . .
βn
GG s
α∈Ti (s)
GG . . .
There are two cases.
Case A α ∈ Tj for some i = j. Then dep(Ti(s)) ∩ Tj = ∅.
IA159 Formal Verification Methods: Partial Order Reduction 64/72
Checking C1
s
β0
GG
~~  22
•
β1
GG . . .
βn
GG s
α∈Ti (s)
GG . . .
There are two cases.
Case A α ∈ Tj for some i = j. Then dep(Ti(s)) ∩ Tj = ∅.
Case B α ∈ Ti.
β0, . . . , βn are independent on Ti(s) and hence
β0, . . . , βn ∈ Ti (all transitions of Pi are considered as
interdependent).
Therefore pci(s) = pci(s ) and thus α ∈ currenti(s) Ti(s).
As α ∈ Ti(s), some transition of β0, . . . , βn has to be
included in pre(α).
Hence, pre(currenti(s) Ti(s)) ∩ Tj = ∅ for some j = i.
IA159 Formal Verification Methods: Partial Order Reduction 65/72
Algorithm checking C1
function checkC1(s, Pi)
forall Pi = Pj do
if dep(Ti(s)) ∩ Tj = ∅ ∨ pre(currenti(s) Ti(s)) ∩ Tj = ∅ then
return false
return true
end function
If the function returns true, then C1 holds. It may return false
even if Ti(s) satisfies C1.
IA159 Formal Verification Methods: Partial Order Reduction 66/72
Algorithm
function checkC2(X)
forall α ∈ X do
if visible(α) then
return false
return true
end function
function checkC3’(s, X)
forall α ∈ X do
if onStack(α(s)) then
return false
return true
end function
function ample(s)
forall Pi such that Ti(s) = ∅ do
if checkC1(s, Pi) ∧ checkC2(Ti(s)) ∧ checkC3’(s, Ti(s)) then
return Ti(s)
return enabled(s)
end function
IA159 Formal Verification Methods: Partial Order Reduction 67/72
Partial order reduction
Example
IA159 Formal Verification Methods: Partial Order Reduction 68/72
Example: code
P :: m : cobegin P0 P1 coend
P0 :: s0 : while true do
NC0 : wait(turn = 0);
CS0 : turn := 1;
endwhile;
P1 :: s1 : while true do
NC1 : wait(turn = 1);
CS1 : turn := 0;
endwhile;
Specification formula ϕ = G¬((pc0 = CS0) ∧ (pc1 = CS1))
IA159 Formal Verification Methods: Partial Order Reduction 69/72
Example
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: Partial Order Reduction 70/72
Example
turn = 0
s0, NC1 NC0, s1
turn = 0
CS0, s1
turn = 0
NC0, 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: Partial Order Reduction 71/72
Coming next week
Abstraction
How to verify large systems?
How to find a good abstraction?
When is an abstraction considered to be good?
IA159 Formal Verification Methods: Partial Order Reduction 72/72