Structural Invariants for Parameterized Architectures
239
Fig. 3: Alternating Dining Philosophers
¬zero(x) ∧ [(g(x) ∧ g(x)) ∨ (gr(x) ∧ g(s(x))) ∨ (p(x) ∧ (x) ∧ (s(x)))]
f
b
get
leave
w
e
h
put
getright
getleft
w
e
h
put
getleft
getright
g(0)
gr(0) g(0)
gr(2) g(2)
Philosopher lr (2)
Fork(0)
Fork(1)
Philosopher lr (1)
Philosopher rl (0)
Fork(2)
(0)
p(0)
p(2)
Γ alt
philo
= zero(x) ∧ [(g(x) ∧ g(x)) ∨ (gr(x) ∧ g(s(x))) ∨ (p(x) ∧ (x) ∧ (s(x)))] ∨
f
b
get
leave
f
b
get
leave
w
e
h
put
getleft
getright
g(1)
gr(1) g(1)
g(2)
(1)
p(1)
(2)
Proposition 1. Consider an instance of the alternating dining philosophers system in
Fig. 3, consisting of components Fork(0), Philosopher rl (0), Fork(1), Philosopher lr (1),
Fork(2) and Philosopher lr (2) placed in a ring, in this order. Then each nonempty trap
of this system contains one of the places b, 0, h, 0, b, 1, w, 1, f, 2 or e, 2.
However, the configuration is unreachable by a real execution of the PN, started in
the initial configuration that marks f, i and w, i, for all i = 0, 1, 2. An intuitive reason
is that, in any reachable configuration, each fork is in state f (ree) only if none of its
neighboring philosophers is in state e(ating). In order to prove deadlock freedom, one
must learn this and other similar constraints. Next, we present a heuristic method for
strengthening the trap invariant that infers such universal constraints.
4.1 One Invariants
As shown by the example above, trap constraints do sometimes fail to prove interesting
properties. Hence, it is desirable to refine the overapproximation of viable markings to
exclude more spurious counterexamples. In order to do so, we consider a special class
of linear invariants, called 1-invariants in the following. Although linear invariants are
not structural and rely on the set of reachable markings of a marked Petri Net, the set of
1-invariants can be sufficiently under-approximated by structural conditions.
Definition 1. Given a marked PN N = ((S , T, E), m 0 ), with S = {s 1 ,..., s n }, a vector
a = (a 1 ,..., a n ) ∈ {0, 1} n is a 1-invariant of N if and only if, for each reachable marking
m ∈ R(N), we have
n
i=1 a i · m(s i ) = 1.
The following lemma relates 1-invariants to some structural properties. However,
there are 1-invariants not captured by these conditions. Taking the intersection of this set
of 1-invariants defines a weaker invariant, which is sound for our verification purposes.
Lemma 3. Given a marked PN N = ((S, T, E), m 0 ), a set of places F ⊆ S is a 1invariant if the following hold:
1.
s∈F
m 0 (s) = 1,
2. either ||F ∩ • t || = ||F ∩ t • || = k with k ∈ {0, 1} or ||F ∩ • t || > 1 for every t ∈ T .
239
Fig. 3: Alternating Dining Philosophers
¬zero(x) ∧ [(g(x) ∧ g(x)) ∨ (gr(x) ∧ g(s(x))) ∨ (p(x) ∧ (x) ∧ (s(x)))]
f
b
get
leave
w
e
h
put
getright
getleft
w
e
h
put
getleft
getright
g(0)
gr(0) g(0)
gr(2) g(2)
Philosopher lr (2)
Fork(0)
Fork(1)
Philosopher lr (1)
Philosopher rl (0)
Fork(2)
(0)
p(0)
p(2)
Γ alt
philo
= zero(x) ∧ [(g(x) ∧ g(x)) ∨ (gr(x) ∧ g(s(x))) ∨ (p(x) ∧ (x) ∧ (s(x)))] ∨
f
b
get
leave
f
b
get
leave
w
e
h
put
getleft
getright
g(1)
gr(1) g(1)
g(2)
(1)
p(1)
(2)
Proposition 1. Consider an instance of the alternating dining philosophers system in
Fig. 3, consisting of components Fork(0), Philosopher rl (0), Fork(1), Philosopher lr (1),
Fork(2) and Philosopher lr (2) placed in a ring, in this order. Then each nonempty trap
of this system contains one of the places b, 0, h, 0, b, 1, w, 1, f, 2 or e, 2.
However, the configuration is unreachable by a real execution of the PN, started in
the initial configuration that marks f, i and w, i, for all i = 0, 1, 2. An intuitive reason
is that, in any reachable configuration, each fork is in state f (ree) only if none of its
neighboring philosophers is in state e(ating). In order to prove deadlock freedom, one
must learn this and other similar constraints. Next, we present a heuristic method for
strengthening the trap invariant that infers such universal constraints.
4.1 One Invariants
As shown by the example above, trap constraints do sometimes fail to prove interesting
properties. Hence, it is desirable to refine the overapproximation of viable markings to
exclude more spurious counterexamples. In order to do so, we consider a special class
of linear invariants, called 1-invariants in the following. Although linear invariants are
not structural and rely on the set of reachable markings of a marked Petri Net, the set of
1-invariants can be sufficiently under-approximated by structural conditions.
Definition 1. Given a marked PN N = ((S , T, E), m 0 ), with S = {s 1 ,..., s n }, a vector
a = (a 1 ,..., a n ) ∈ {0, 1} n is a 1-invariant of N if and only if, for each reachable marking
m ∈ R(N), we have
n
i=1 a i · m(s i ) = 1.
The following lemma relates 1-invariants to some structural properties. However,
there are 1-invariants not captured by these conditions. Taking the intersection of this set
of 1-invariants defines a weaker invariant, which is sound for our verification purposes.
Lemma 3. Given a marked PN N = ((S, T, E), m 0 ), a set of places F ⊆ S is a 1invariant if the following hold:
1.
s∈F
m 0 (s) = 1,
2. either ||F ∩ • t || = ||F ∩ t • || = k with k ∈ {0, 1} or ||F ∩ • t || > 1 for every t ∈ T .