238
M. Bozga et al.
Relying on Lemma 2 we are assured that the set represented by X intersects all IMTs.
Now, let ϕ(X) be any formula that defines a set of good global states of the componentbased systems (or, equivalently, a good set of markings of their corresponding Petri
nets), with the intuition that, at any moment during execution, the current global state of
the component-based system should be good. We can now state the following theorem,
that captures the soundness of the verification method based on trap invariants:
Theorem 1. Given a component-based system S and a WSκS formula ϕ(X), if the
formula
∃X . marking S (X) ∧ trap-invariant S (X) ∧ ¬ϕ(X)
(7)
is unsatisfiable, then for every universe U, the property defined by the formula ϕ(X)
holds in every reachable marking of N U
S
.
In the light of the above theorem, verifying the correctness of a component-based
system with any number of active components boils down to deciding the satisfiability
of a WSκS formula. The latter problem is known to be decidable, albeit with nonelementary worst-case complexity. A closer look at the verification conditions of the
form (7) generated by our method suffices to see that the quantifier alternation is finite,
which implies that the time needed to decide the (un)satisfiability of (7) is elementary.
Moreover, our experiments show that these checks are very fast (less than 1 second on
an average machine) for a non-trivial set of examples.
4 Refining Trap Invariants
Since the safety verification problem is undecidable for parameterized systems [6], the
verification method based on trap invariants cannot be complete. As an example, consider the alternating dining philosophers system, of which an instance (for n = 3) is
shown in Fig. 3. The system consists of two philosopher component types, namely
Philosopher rl , which takes its right fork before its left fork, and Philosopher lr , taking the left fork before the right one. Each philosopher has two interaction ports for
taking the forks, namely g (get left) and gr (get right) and one port for releasing the
forks p (put). The ports of the Philosopher rl component type are overlined, in order
to be distinguished. The Fork component type is the same as in Fig. 1. The interaction
formula for this system Γ alt
philo
, shown in Fig. 3, implicitly states that only the 0-index
philosopher component is of type Philosopher rl , whereas all other philosophers are of
type Philosopher lr . Note that the interactions on ports g, gr and p are only allowed if
zero(x)
def
= ∀y . x ≤ y holds, in other words if x is interpreted as the root of the universe
(in our case, 0 since U = {0,..., n − 1}).
It is well-known that any instance of the parameterized alternating dining philosophers system consisting of at least one Philosopher rl and one Philosopher lr is deadlockfree. However, trap invariants are not enough to prove deadlock freedom, as shown by
the global state {{b, 0, h, 0, b, 1, w, 1, f, 2, e, 2}, marked with thick red lines in
Fig. 3. Note that no interaction is enabled in this state. Moreover, this state intersects
with any trap of the marked PN that defines the executions of this particular instance, as
proved below. Consequently, the trap invariant contains a deadlock configuration, and
the system cannot be proved deadlock-free by this method.
M. Bozga et al.
Relying on Lemma 2 we are assured that the set represented by X intersects all IMTs.
Now, let ϕ(X) be any formula that defines a set of good global states of the componentbased systems (or, equivalently, a good set of markings of their corresponding Petri
nets), with the intuition that, at any moment during execution, the current global state of
the component-based system should be good. We can now state the following theorem,
that captures the soundness of the verification method based on trap invariants:
Theorem 1. Given a component-based system S and a WSκS formula ϕ(X), if the
formula
∃X . marking S (X) ∧ trap-invariant S (X) ∧ ¬ϕ(X)
(7)
is unsatisfiable, then for every universe U, the property defined by the formula ϕ(X)
holds in every reachable marking of N U
S
.
In the light of the above theorem, verifying the correctness of a component-based
system with any number of active components boils down to deciding the satisfiability
of a WSκS formula. The latter problem is known to be decidable, albeit with nonelementary worst-case complexity. A closer look at the verification conditions of the
form (7) generated by our method suffices to see that the quantifier alternation is finite,
which implies that the time needed to decide the (un)satisfiability of (7) is elementary.
Moreover, our experiments show that these checks are very fast (less than 1 second on
an average machine) for a non-trivial set of examples.
4 Refining Trap Invariants
Since the safety verification problem is undecidable for parameterized systems [6], the
verification method based on trap invariants cannot be complete. As an example, consider the alternating dining philosophers system, of which an instance (for n = 3) is
shown in Fig. 3. The system consists of two philosopher component types, namely
Philosopher rl , which takes its right fork before its left fork, and Philosopher lr , taking the left fork before the right one. Each philosopher has two interaction ports for
taking the forks, namely g (get left) and gr (get right) and one port for releasing the
forks p (put). The ports of the Philosopher rl component type are overlined, in order
to be distinguished. The Fork component type is the same as in Fig. 1. The interaction
formula for this system Γ alt
philo
, shown in Fig. 3, implicitly states that only the 0-index
philosopher component is of type Philosopher rl , whereas all other philosophers are of
type Philosopher lr . Note that the interactions on ports g, gr and p are only allowed if
zero(x)
def
= ∀y . x ≤ y holds, in other words if x is interpreted as the root of the universe
(in our case, 0 since U = {0,..., n − 1}).
It is well-known that any instance of the parameterized alternating dining philosophers system consisting of at least one Philosopher rl and one Philosopher lr is deadlockfree. However, trap invariants are not enough to prove deadlock freedom, as shown by
the global state {{b, 0, h, 0, b, 1, w, 1, f, 2, e, 2}, marked with thick red lines in
Fig. 3. Note that no interaction is enabled in this state. Moreover, this state intersects
with any trap of the marked PN that defines the executions of this particular instance, as
proved below. Consequently, the trap invariant contains a deadlock configuration, and
the system cannot be proved deadlock-free by this method.