Structural Invariants for Parameterized Architectures
237
form (4), we define the WSκS formulae:
intersects-pre C
S
(X, x 1 ,..., x ) =
j=1 X• p j (x j ) ∨
+m
j=+1 ∃x j . Tr(ψ j ) ∧ X• p j (x j ) and
intersects-post C
S
(X, x 1 ,..., x ) =
j=1 X p j
• (x j ) ∨
+m
j=+1 ∃x j . Tr(ψ j ) ∧ X p j
• (x j ).
Now we can define trap-pred S (X) as the conjunction of the following formulae, one for
each clause C (in the form described in (4)) of Γ
∀x 1 ...∀x .
Tr(ϕ) ∧ intersects-pre C
S
(X, x 1 ,..., x )
→ intersects-post C
S
(X, x 1 ,..., x ).
(5)
So, intuitively, trap-pred S (X) states that for every transition of the Petri Net, if the set
X of places intersects the preset of the transition, then it also intersects its postset. This
is the condition for the set of places to be a trap. Formally, we obtain:
Lemma 2. Given a component-based system S = C
1
,..., C
N
,Γ and a structure I =
(U,ι), where ι is an interpretation of the set variables X, the set P = {{s, u ∈
N
k=1 S
k
×U |
u ∈ ι(X s )} is a trap of N U
S
if and only if (U,ι) | = WSκS trap-pred S (X).
Parameterized Trap Invariants in WSκS. Loosely speaking, the intended meaning
of trap-pred S (X) is “the set of places X is a trap”. Our goal is to construct a formula
stating: “the marking m marks all initially marked traps”.
Recall that the Petri Nets obtained from component-based systems are always 1safe, and so a marking is also a set of places. Recall, however, that all reachable markings have the property that they place exactly one token in the set of places modeling the
set of states of a component (loosely speaking, the set of places of the k-th philosopher
is (w, k) and (e, k), and there is always one token in the one or the other). So we define
a formula marking S (X) with intended meaning “the set of places X is a legal marking”,
and another one, trap-invariant S (X) with intended meaning “the set of places X marks
every initially marked trap”.
In addition to the tuple of set variables X defined above, we consider now the “copy”
tuple X
def
= X
s s∈S i ,1≤i≤N . Intuitively, X and X represent one set of places each. First,
we define a (1-safe) marking as a set of places that marks exactly one state of each copy
of each component:
marking S (X) = ∀x .
1≤i≤N
s∈S i
⎛
⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ X s (x) ∧
s ∈S i \ {s}
¬X s (x)
⎞
⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ .
Second, we give a formula describing the intersection of two sets of places:
intersection S (X, X ) = ∃x .
s∈
1≤i≤N S i
(X s (x) ∧ X
s (x)).
Finally, to actually capture IMTs we need to determine if a trap is initially marked.
However, this can be easily described by the formula:
initially-marked S (X) = ∃x .
1≤i≤N
X s 0
i (x).
So we can define the trap-invariant by the WSκS formula:
trap-invariant S (X) = ∀X .
trap-pred S (X ) ∧ initially-marked S (X )
→ intersection S (X, X ).
(6)
237
form (4), we define the WSκS formulae:
intersects-pre C
S
(X, x 1 ,..., x ) =
j=1 X• p j (x j ) ∨
+m
j=+1 ∃x j . Tr(ψ j ) ∧ X• p j (x j ) and
intersects-post C
S
(X, x 1 ,..., x ) =
j=1 X p j
• (x j ) ∨
+m
j=+1 ∃x j . Tr(ψ j ) ∧ X p j
• (x j ).
Now we can define trap-pred S (X) as the conjunction of the following formulae, one for
each clause C (in the form described in (4)) of Γ
∀x 1 ...∀x .
Tr(ϕ) ∧ intersects-pre C
S
(X, x 1 ,..., x )
→ intersects-post C
S
(X, x 1 ,..., x ).
(5)
So, intuitively, trap-pred S (X) states that for every transition of the Petri Net, if the set
X of places intersects the preset of the transition, then it also intersects its postset. This
is the condition for the set of places to be a trap. Formally, we obtain:
Lemma 2. Given a component-based system S = C
1
,..., C
N
,Γ and a structure I =
(U,ι), where ι is an interpretation of the set variables X, the set P = {{s, u ∈
N
k=1 S
k
×U |
u ∈ ι(X s )} is a trap of N U
S
if and only if (U,ι) | = WSκS trap-pred S (X).
Parameterized Trap Invariants in WSκS. Loosely speaking, the intended meaning
of trap-pred S (X) is “the set of places X is a trap”. Our goal is to construct a formula
stating: “the marking m marks all initially marked traps”.
Recall that the Petri Nets obtained from component-based systems are always 1safe, and so a marking is also a set of places. Recall, however, that all reachable markings have the property that they place exactly one token in the set of places modeling the
set of states of a component (loosely speaking, the set of places of the k-th philosopher
is (w, k) and (e, k), and there is always one token in the one or the other). So we define
a formula marking S (X) with intended meaning “the set of places X is a legal marking”,
and another one, trap-invariant S (X) with intended meaning “the set of places X marks
every initially marked trap”.
In addition to the tuple of set variables X defined above, we consider now the “copy”
tuple X
def
= X
s s∈S i ,1≤i≤N . Intuitively, X and X represent one set of places each. First,
we define a (1-safe) marking as a set of places that marks exactly one state of each copy
of each component:
marking S (X) = ∀x .
1≤i≤N
s∈S i
⎛
⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ X s (x) ∧
s ∈S i \ {s}
¬X s (x)
⎞
⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ .
Second, we give a formula describing the intersection of two sets of places:
intersection S (X, X ) = ∃x .
s∈
1≤i≤N S i
(X s (x) ∧ X
s (x)).
Finally, to actually capture IMTs we need to determine if a trap is initially marked.
However, this can be easily described by the formula:
initially-marked S (X) = ∃x .
1≤i≤N
X s 0
i (x).
So we can define the trap-invariant by the WSκS formula:
trap-invariant S (X) = ∀X .
trap-pred S (X ) ∧ initially-marked S (X )
→ intersection S (X, X ).
(6)