236
M. Bozga et al.
order variables (also called set variables), denoted as X, Y,... in the following. The syntax of WSκS is:
t := | x | succ 0 (t) | ... | succ κ (t)
terms
φ := t 1 = t 2 | pr(t) | X(t) | φ 1 ∧ φ 2 | ¬φ 1 | ∃x . φ 1 | ∃X . φ 1 formulae
So WSκS extends ILκ with the constant symbol , atoms X(t) and monadic second
order quantifiers ∃X . φ. We can consider w.l.o.g. equality atoms t 1 = t 2 instead of the
inequalities t 1 ≤ t 2 in ILκ, because the latter can be defined in WSκS as usual:
x ≤ y
def
= ∀X . closed(X) ∧ X(x) → X(y) closed(X)
def
= ∀x . X(x) →
κ−1
i=0 X(succ i (x))
Like ILκ, the formulae of WSκS are interpreted on ordered trees of arity κ. The
models of WSκS are structures (U,ι), where ι assigns the root of the tree to , a node
ι(x) to each variable x ∈ Var and a set ι(X) ⊆ U to each set variable X ∈ SVar. The
satisfaction relation (U,ι) | = WSκS φ is defined as for ILκ, with one difference: in ILκ, the
successor of a leaf of a tree is the root of the tree, while in WSκS the successor of leaf
is, by convention, the leaf itself [37, Example 2.10.3]. This is the only reason why ILκ
is not just a fragment of WSκS.
We define an embedding of ILκ formulae, without occurrences of predicates and
set variables, into WSκS. W.l.o.g. we consider ILκ formulae that have been previously flattened, i.e the successor function occurs only within atomic propositions of
the form succ i (x) = y. This is done by replacing each atomic proposition of the form
succ i 1 (...succ i n (x) ...) = y by the formula ∃x 1 ...∃x n . x n = succ i n (x) ∧ y = succ i 1 (x 1 ) ∧
n−1
j=1 x j = succ i j (x j+1 ). The translation of an ILκ formula φ into WSκS is the formula
Tr(φ), defined recursively on the structure of φ such that Tr simply preserves first-order
connectives and, secondly, yields:
Tr(succ i (x) = y)
def
= (¬ max(x) ∧ succ i (x) = y) ∨ (max(x) ∧ y = ).
We show that a formula φ of ILκ and its WSκS counterpart Tr(φ) are equivalent:
Lemma 1. Given an ILκ formula φ, for any structure I = (U,ι), we have I | = IL φ ⇐⇒
I | = WSκS Tr(φ).
3.2 Defining Parameterized Trap Invariants in WSκS
Fix a component-based system S = C
1
,..., C
N
,Γ and recall that every universe U induces a Petri Net N U
S
whose set of places is
N
k=1 S
k
× U. For every state s ∈
N
i=1 S
i , let
X s be a monadic second-order variable, and let X be the tuple of these variables in an
arbitrary but fixed order. We define a formula trap-pred S (X), with X as set of free variables, that characterizes the traps of the infinitely many Petri Nets N U
S
corresponding to
S. Formally, trap-pred S (X) has the following property:
For every universe U and for every set P ⊆
N
k=1 S
k
× U of places of N U
S
:
P is a trap of N U
S
iff the assignment X q → {u ∈ U | (q, u) ∈ P} satisfies trap-pred S (X).
Observe that every assignment to X encodes a set of places, and vice versa. So, abusing
language, we can speak of the set of places X.
We define auxiliary predicates that capture the intersection of the set of places X
with the pre ( • t) and postset (t • ) of a transition t in N U
S
. For every clause C of Γ, of the
M. Bozga et al.
order variables (also called set variables), denoted as X, Y,... in the following. The syntax of WSκS is:
t := | x | succ 0 (t) | ... | succ κ (t)
terms
φ := t 1 = t 2 | pr(t) | X(t) | φ 1 ∧ φ 2 | ¬φ 1 | ∃x . φ 1 | ∃X . φ 1 formulae
So WSκS extends ILκ with the constant symbol , atoms X(t) and monadic second
order quantifiers ∃X . φ. We can consider w.l.o.g. equality atoms t 1 = t 2 instead of the
inequalities t 1 ≤ t 2 in ILκ, because the latter can be defined in WSκS as usual:
x ≤ y
def
= ∀X . closed(X) ∧ X(x) → X(y) closed(X)
def
= ∀x . X(x) →
κ−1
i=0 X(succ i (x))
Like ILκ, the formulae of WSκS are interpreted on ordered trees of arity κ. The
models of WSκS are structures (U,ι), where ι assigns the root of the tree to , a node
ι(x) to each variable x ∈ Var and a set ι(X) ⊆ U to each set variable X ∈ SVar. The
satisfaction relation (U,ι) | = WSκS φ is defined as for ILκ, with one difference: in ILκ, the
successor of a leaf of a tree is the root of the tree, while in WSκS the successor of leaf
is, by convention, the leaf itself [37, Example 2.10.3]. This is the only reason why ILκ
is not just a fragment of WSκS.
We define an embedding of ILκ formulae, without occurrences of predicates and
set variables, into WSκS. W.l.o.g. we consider ILκ formulae that have been previously flattened, i.e the successor function occurs only within atomic propositions of
the form succ i (x) = y. This is done by replacing each atomic proposition of the form
succ i 1 (...succ i n (x) ...) = y by the formula ∃x 1 ...∃x n . x n = succ i n (x) ∧ y = succ i 1 (x 1 ) ∧
n−1
j=1 x j = succ i j (x j+1 ). The translation of an ILκ formula φ into WSκS is the formula
Tr(φ), defined recursively on the structure of φ such that Tr simply preserves first-order
connectives and, secondly, yields:
Tr(succ i (x) = y)
def
= (¬ max(x) ∧ succ i (x) = y) ∨ (max(x) ∧ y = ).
We show that a formula φ of ILκ and its WSκS counterpart Tr(φ) are equivalent:
Lemma 1. Given an ILκ formula φ, for any structure I = (U,ι), we have I | = IL φ ⇐⇒
I | = WSκS Tr(φ).
3.2 Defining Parameterized Trap Invariants in WSκS
Fix a component-based system S = C
1
,..., C
N
,Γ and recall that every universe U induces a Petri Net N U
S
whose set of places is
N
k=1 S
k
× U. For every state s ∈
N
i=1 S
i , let
X s be a monadic second-order variable, and let X be the tuple of these variables in an
arbitrary but fixed order. We define a formula trap-pred S (X), with X as set of free variables, that characterizes the traps of the infinitely many Petri Nets N U
S
corresponding to
S. Formally, trap-pred S (X) has the following property:
For every universe U and for every set P ⊆
N
k=1 S
k
× U of places of N U
S
:
P is a trap of N U
S
iff the assignment X q → {u ∈ U | (q, u) ∈ P} satisfies trap-pred S (X).
Observe that every assignment to X encodes a set of places, and vice versa. So, abusing
language, we can speak of the set of places X.
We define auxiliary predicates that capture the intersection of the set of places X
with the pre ( • t) and postset (t • ) of a transition t in N U
S
. For every clause C of Γ, of the