Structural Invariants for Parameterized Architectures
233
Loosely speaking, (4) states that in an interaction components can simultaneously
engage in a multiparty rendez-vous, together with a broadcast to the ports q 1 ,...,q m of
the components whose indices satisfy the constraints ψ 1 , . . . , ψ m , respectively. An example of peer-to-peer rendez-vous with no broadcast is the dining philosophers system
in Fig. 1, whereas examples of broadcast are found among the benchmarks in §5. In
the next section we show that, despite this generality, it is possible to construct a trap
invariant for any interaction formula in a purely syntactic way.
Observe that the interaction formula does not explicitly specify that every other
process remains idle. Formally, as we will see in the next section, the system has an
interaction for each minimal model of (4), which allows us not to have to specify idleness. Given structures I 1 = (U,ι 1 ) and I 2 = (U,ι 2 ) sharing the same universe U, we say
I 1 I 2 if and only if ι 1 (pr) ⊆ ι 2 (pr) for every pr ∈ Pred. Given a formula φ, a structure
I is a minimal model of φ if I | = φ and, for all structures I such that I I and I I,
we have I | = φ.
2.1 Execution Semantics of Component-based Systems
The semantics of a component-based system S = C
1
,..., C
N
,Γ is an infinite family of
Petri Nets, one for each universe of Γ. The reachable markings and actions of the Petri
Net characterize the reachable global states and transitions of the system, respectively.
To fix notations, we recall several basic definitions.
Preliminaries: Petri Nets. A Petri Net (PN) is a tuple N = S , T, E, where S is a set
of places, T is a set of transitions, S ∩ T = ∅, and E ⊆ (S × T ) ∪ (T × S ) is a set of arcs.
The elements of S ∪ T are called nodes. Given nodes x, y ∈ S ∪ T , we write E(x, y)
def
= 1
if (x, y) ∈ E and E(x, y)
def
= 0, otherwise. For a node x, let • x
def
= {y ∈ S ∪ T | E(y, x) = 1},
x • def
= {y ∈ S ∪ T | E(x, y) = 1} and lift these definitions to sets of nodes.
A marking of N is a function m : S → N. A transition t is enabled in m if and only if
m(s) > 0 for each place s ∈ • t. For all markings m, m and transitions t, we write m
t
−
→ m
whenever t is enabled in m and m (s) = m(s) − E(s, t) + E(t, s), for all s ∈ S . Given two
markings m and m , a finite sequence of transitions σ = t 1 ,..., t n is a firing sequence,
written m
σ
− → m if and only if either (i) n = 0 and m = m , or (ii) n ≥ 1 and there exist
markings m 1 ,..., m n−1 such that m
t 1
− → m 1 ...m n−1
tn
− → m .
A marked Petri Net is a pair N = (N, m 0 ), where m 0 is the initial marking of N.
A marking m is reachable in N if there exists a firing sequence σ such that m 0
σ
− → m.
We denote by R(N) the set of reachable markings of N. A marked PN N is 1-safe if
m(s) ≤ 1, for each s ∈ S and m ∈ R(N). All PNs considered in the following will be
1-safe and we shall silently blur the distinction between a marking m : S → {0, 1} and
the boolean valuation β m : S → {⊥, } defined as β m (s) = ⇐⇒ m(s) = 1. A set of
markings M is an inductive invariant of N = (N, m 0 ) if and only if m 0 ∈ M and for each
m
t
−
→ m such that m ∈ M, we have m ∈ M.
Petri Net Semantics of Component-Based Systems. We define the semantics of a
component-based system as an infinite family of 1-safe Petri Nets. For k = 1,..., N let
C
k
= P
k
, S
k
, s 0
k
,Δ
k
be a component type and, then, let S = C
1
,..., C
N
,Γ be a system.
Fix a universe U of Γ. We define a marked Petri Net N U
S
def
= (S , T, E, m 0 ) as follows:
233
Loosely speaking, (4) states that in an interaction components can simultaneously
engage in a multiparty rendez-vous, together with a broadcast to the ports q 1 ,...,q m of
the components whose indices satisfy the constraints ψ 1 , . . . , ψ m , respectively. An example of peer-to-peer rendez-vous with no broadcast is the dining philosophers system
in Fig. 1, whereas examples of broadcast are found among the benchmarks in §5. In
the next section we show that, despite this generality, it is possible to construct a trap
invariant for any interaction formula in a purely syntactic way.
Observe that the interaction formula does not explicitly specify that every other
process remains idle. Formally, as we will see in the next section, the system has an
interaction for each minimal model of (4), which allows us not to have to specify idleness. Given structures I 1 = (U,ι 1 ) and I 2 = (U,ι 2 ) sharing the same universe U, we say
I 1 I 2 if and only if ι 1 (pr) ⊆ ι 2 (pr) for every pr ∈ Pred. Given a formula φ, a structure
I is a minimal model of φ if I | = φ and, for all structures I such that I I and I I,
we have I | = φ.
2.1 Execution Semantics of Component-based Systems
The semantics of a component-based system S = C
1
,..., C
N
,Γ is an infinite family of
Petri Nets, one for each universe of Γ. The reachable markings and actions of the Petri
Net characterize the reachable global states and transitions of the system, respectively.
To fix notations, we recall several basic definitions.
Preliminaries: Petri Nets. A Petri Net (PN) is a tuple N = S , T, E, where S is a set
of places, T is a set of transitions, S ∩ T = ∅, and E ⊆ (S × T ) ∪ (T × S ) is a set of arcs.
The elements of S ∪ T are called nodes. Given nodes x, y ∈ S ∪ T , we write E(x, y)
def
= 1
if (x, y) ∈ E and E(x, y)
def
= 0, otherwise. For a node x, let • x
def
= {y ∈ S ∪ T | E(y, x) = 1},
x • def
= {y ∈ S ∪ T | E(x, y) = 1} and lift these definitions to sets of nodes.
A marking of N is a function m : S → N. A transition t is enabled in m if and only if
m(s) > 0 for each place s ∈ • t. For all markings m, m and transitions t, we write m
t
−
→ m
whenever t is enabled in m and m (s) = m(s) − E(s, t) + E(t, s), for all s ∈ S . Given two
markings m and m , a finite sequence of transitions σ = t 1 ,..., t n is a firing sequence,
written m
σ
− → m if and only if either (i) n = 0 and m = m , or (ii) n ≥ 1 and there exist
markings m 1 ,..., m n−1 such that m
t 1
− → m 1 ...m n−1
tn
− → m .
A marked Petri Net is a pair N = (N, m 0 ), where m 0 is the initial marking of N.
A marking m is reachable in N if there exists a firing sequence σ such that m 0
σ
− → m.
We denote by R(N) the set of reachable markings of N. A marked PN N is 1-safe if
m(s) ≤ 1, for each s ∈ S and m ∈ R(N). All PNs considered in the following will be
1-safe and we shall silently blur the distinction between a marking m : S → {0, 1} and
the boolean valuation β m : S → {⊥, } defined as β m (s) = ⇐⇒ m(s) = 1. A set of
markings M is an inductive invariant of N = (N, m 0 ) if and only if m 0 ∈ M and for each
m
t
−
→ m such that m ∈ M, we have m ∈ M.
Petri Net Semantics of Component-Based Systems. We define the semantics of a
component-based system as an infinite family of 1-safe Petri Nets. For k = 1,..., N let
C
k
= P
k
, S
k
, s 0
k
,Δ
k
be a component type and, then, let S = C
1
,..., C
N
,Γ be a system.
Fix a universe U of Γ. We define a marked Petri Net N U
S
def
= (S , T, E, m 0 ) as follows: