230
M. Bozga et al.
tures, in which processes are indistinguishable, and the system can be described by
one single Petri Net with an infinite family of initial markings. Here, for the first time,
we show that the trap technique can be extended to pipelines, token rings and trees,
where the system is defined by an infinite family of Petri Nets, each with a different
structure. These systems cannot be analyzed using the techniques of [31,1,29], because
they do not yield well-structured transition systems. Contrary to [18,27,26,7,34], our
approach does not require a manual cut-off proof. Contrary to regular model checking
and automata learning [2,19], it does not require any symbolic state-space exploration.
Finally, our approach produces an explanation of why the property holds in terms of the
trap invariant and 1-invariants used. Summarizing, our approach provides a comparatively cheap technique for parameterized verification, that succeeds in numerous cases.
It is ideal as preprocessing step that can very quickly lead to success with a very clear
explanation of why the property holds, and otherwise provides at least a strong invariant
that can be used for further analysis.
(succ(k))
w
e
g
p
p(k) g(k)
f
b
t
Philosopher(k)
Fork(k)
Fork((k + 1) mod N)
Γ philo = (g(i) ∧ t(i) ∧ t(succ(i))) ∨ (p(i) ∧ (i) ∧ (succ(i)))
f
b
t
(k)
t(k)
t(succ(k))
Fig. 1: Parameterized Dining Philosophers
Running Example. Consider the dining philosophers system in Fig. 1, consisting of
n ≥ 2 components of type Fork and Philosopher respectively, placed in a ring of size 2n.
The k-th philosopher has a left fork, of index k, and a right fork, of index (k + 1) mod n.
Each component is an instance of a finite state automaton with states f (ree) and b(usy)
for Fork, respectively w(aiting) and e(ating) for Philosopher. A fork goes from state f
to b via a t(ake) transition and from f to b via a (eave) transition. A philosopher goes
from w to e via a g(et) transition and from e to w via a p(ut) transition. The g action of the
k-th philosopher is executed jointly with the t actions of the k-th and [(k + 1) mod n]-th
forks, in other words, the philosopher takes both its left and right forks simultaneously.
Similarly, the p action of the k-th philosopher is executed simultaneously with the
action of the k-th and [(k + 1) mod n]-th forks, i.e. each philosopher leaves both its
left and right forks at the same time. We describe these interactions by the interaction
formula:
Γ philo = (g(i) ∧ t(i) ∧ t(succ(i))) ∨ (p(i) ∧ (i) ∧ (succ(i)))
(1)
where the free variable i refers at some arbitrary component index.
M. Bozga et al.
tures, in which processes are indistinguishable, and the system can be described by
one single Petri Net with an infinite family of initial markings. Here, for the first time,
we show that the trap technique can be extended to pipelines, token rings and trees,
where the system is defined by an infinite family of Petri Nets, each with a different
structure. These systems cannot be analyzed using the techniques of [31,1,29], because
they do not yield well-structured transition systems. Contrary to [18,27,26,7,34], our
approach does not require a manual cut-off proof. Contrary to regular model checking
and automata learning [2,19], it does not require any symbolic state-space exploration.
Finally, our approach produces an explanation of why the property holds in terms of the
trap invariant and 1-invariants used. Summarizing, our approach provides a comparatively cheap technique for parameterized verification, that succeeds in numerous cases.
It is ideal as preprocessing step that can very quickly lead to success with a very clear
explanation of why the property holds, and otherwise provides at least a strong invariant
that can be used for further analysis.
(succ(k))
w
e
g
p
p(k) g(k)
f
b
t
Philosopher(k)
Fork(k)
Fork((k + 1) mod N)
Γ philo = (g(i) ∧ t(i) ∧ t(succ(i))) ∨ (p(i) ∧ (i) ∧ (succ(i)))
f
b
t
(k)
t(k)
t(succ(k))
Fig. 1: Parameterized Dining Philosophers
Running Example. Consider the dining philosophers system in Fig. 1, consisting of
n ≥ 2 components of type Fork and Philosopher respectively, placed in a ring of size 2n.
The k-th philosopher has a left fork, of index k, and a right fork, of index (k + 1) mod n.
Each component is an instance of a finite state automaton with states f (ree) and b(usy)
for Fork, respectively w(aiting) and e(ating) for Philosopher. A fork goes from state f
to b via a t(ake) transition and from f to b via a (eave) transition. A philosopher goes
from w to e via a g(et) transition and from e to w via a p(ut) transition. The g action of the
k-th philosopher is executed jointly with the t actions of the k-th and [(k + 1) mod n]-th
forks, in other words, the philosopher takes both its left and right forks simultaneously.
Similarly, the p action of the k-th philosopher is executed simultaneously with the
action of the k-th and [(k + 1) mod n]-th forks, i.e. each philosopher leaves both its
left and right forks at the same time. We describe these interactions by the interaction
formula:
Γ philo = (g(i) ∧ t(i) ∧ t(succ(i))) ∨ (p(i) ∧ (i) ∧ (succ(i)))
(1)
where the free variable i refers at some arbitrary component index.