Marius Bozga
email: marius.bozga@univ-grenoble-alpes.fr

Radu Iosif
email: radu.iosif@univ-grenoble-alpes.fr

Joseph Sifakis
email: joseph.sifakis@univ-grenoble-alpes.fr

Verification of Component-based Systems with Recursive Architectures

Keywords: Resource Logic, Component-based Distributed Systems, Parameterized Verification

We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical section are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invariants allowing the proof of general safety properties. The invariants are defined using the WSκS fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection, thus reducing a verification problem to checking satisfiability of a WSκS formula.

Introduction

Mastering the complexity of a distributed system requires a deep understanding of its coordination mechanisms. We distinguish between endogenous coordination, that explicitly uses synchronization primitives in the code describing the behavior of the components (e.g. semaphores, monitors, compare-andswap, etc.) and exogenous coordination, that defines global rules describing how the components interact. These two orthogonal paradigms play different roles in the design of a system: exogenous coordination is used during high-level model building, whereas endogenous coordination is considered at a later stage of development, to implement the model using low-level synchronization.

In this paper we focus on (high-level) exogenous coordination of distributed systems, consisting of a finite yet unbounded number of interconnected components. Communication is assumed to be correct, i.e. we abstract from packet losses and corruptions. Components behave according to a small set of finitestate abstractions of sequential programs, whose transitions are labeled with events. They communicate via interactions (handshaking) modeled as sets of events that occur simultaneously in multiple components. For instance, Figure 1(a) shows a token-ring system, whose components are depicted by gray boxes containing state machines that represent their behavior and whose architecture is the set of connectors between components depicted by solid lines.

The separation between behavior and coordination is a fundamental principle in the design of large-scale distributed systems [START_REF] Kramer | Analysing dynamic change in distributed software architectures[END_REF]. This modular view of a distributed system, in which the internal computation and the state changes of each component are encapsulated in a well defined interface, is key to scalable design methods that exploit a conceptual hierarchy. For instance, a ring is a chain whose final output port is connected to the initial input port, whereas a chain consists of a (head) component linked to a separate (tail) chain as shown in Figure 1(b). Moreover, system designers are accustomed to using architectural patterns, such as rings, pipelines, stars, trees, etc., that define interactions between (unboundedly large) sets of components. Such high-level models of reallife distributed systems are suitable for reasoning about correctness in the early stages of system design, when details related to network reliability or the implementation of coordination by means of low-level synchronization mechanisms (e.g. semaphores, monitors, compare-and-swap, etc.) are abstracted away.

Running Example

For starters, we consider the following recursive definition of a token-ring architecture, composed of a finite but unbounded number of stations that are instances of the same component type S, connected via transfer connectors, of interaction type T. The behavior of each station is a machine with two states, indicating whether the station has a token (t) or not (n). The number of tokens is constant and equal to the number of stations that are initially in state t. Each station not having a token may receive a token from the left, via the in port (that triggers the transition n in -→ t) and send its token to the right, via the out port (that triggers the transition t Intuitively, rule 1 states that a token-ring consists of a chain of components and an interaction between the out port of the last and the in port of the first component in the chain. A chain consists of either two components and an interaction between their out and in ports, respectively (rule 2), or a component and an interaction between its out port and the in port of the first component of a distinct chain [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. The rules (4) and [START_REF] O'hearn | Resources, concurrency, and local reasoning[END_REF] intuitively say that a component has type S and can be in state n or in state t, respectively. The star symbol * used in the rules 1-5 is a commutative and associative logical connective that composes sub-systems with disjoint sets of components and interactions; for instance, in rule 2, the two components declared as Comp(x 1 ) and Comp(x 2 ) are necessarily different, meaning that x 1 and x 2 cannot be mapped to the same value. The rules 2 and 3 correspond to the base and the inductive case of a recursive definition of finite chains of length at least two. We refer to Figure 1(b) for a depiction of the recursive unfolding of the above rules.

Note that no transfer of tokens is possible if the number of tokens in the system is either zero (there is no token to be transfered) or equals the number of components (there is no room to place a token). In this case, we say that a system is in a deadlock. The decision problem "can a token-ring started in a nondeadlock actually reach a deadlock?" is challenging, because it requires a proof that holds for systems of any size, i.e. number of components and interactions.

We show that, even if such problems are undecidable, in general, a large number of instances of these problems can be handled by the methods developed in this paper.

Contributions of this Work

The parameterized verification method presented in this paper relies on an idea reported in [START_REF] Bozga | Specification and safety verification of parametric hierarchical distributed systems[END_REF]. In addition to a complete development of the technical results, previously omitted for space reasons, here we apply the verification method to a specification language based on a resource logic, that resembles Separation Logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], instead of the recursive term algebra introduced in [START_REF] Bozga | Specification and safety verification of parametric hierarchical distributed systems[END_REF]. An extension of this resource logic has been recently developed for Hoare-style reasoning about the safety properties of programmed reconfiguration in distributed systems [START_REF] Ahrens | Local reasoning about parameterized reconfigurable distributed systems[END_REF], to which the work presented here provides a push-button verification back-end. In combination with the proof system reported in [START_REF] Ahrens | Local reasoning about parameterized reconfigurable distributed systems[END_REF], the verification method presented in this paper can automatically prove the correctness of a distributed system after the reconfiguration of its coordinating architecture. Since various dialects of (Concurrent) Separation Logic are being commonly used to specify and reason about concurrent systems [START_REF] O'hearn | Resources, concurrency, and local reasoning[END_REF][START_REF] Sergey | Hoare-style specifications as correctness conditions for non-linearizable concurrent objects[END_REF][START_REF] Farka | On algebraic abstractions for concurrent separation logics[END_REF], we expect this new logic to be easily accepted by the research and development community. The contribution of this paper is three-fold:

1. We introduce a logic-based language, called Configuration Logic (CL), to describe the sets of configurations (i.e. architectures and local states of components) of distributed systems parameterized by (i) the number of components of each type that are active in the system, e.g. a system with n readers and m writers, in which n and m are not known a priori and (ii) the pattern in which the interactions occur (e.g. a pipeline, ring, star or more general hypergraph structures). The language uses predicate symbols to hierarchically break the architecture into specific patterns. The interpretation of these predicate symbols is defined inductively by rewriting rules consisting of formulae that contain predicate atoms, in a way that recalls the usual definitions of algebraic datatypes [START_REF] Barrett | An abstract decision procedure for a theory of inductive data types[END_REF] or heaps [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF].

2. We tackle a parametric safety problem concerning systems described in this language, which is essentially checking that the reachable states of every instance stays clear of a set of global error configurations, such as deadlocks or critical section violations. In particular, we show that both the parametric deadlock freedom and critical section violation problems are undecidable, even for architectures as simple as a chain of components.

3. We develop a verification method that synthesizes parametric invariants from the syntactic description of the architecture (in CL) and from the behavior of its components (finite-state machines). The invariants and the set of error configurations are both described using a decidable fragment of Monadic Second Order Logic (MSO), that enables the use of off-the-shelf solvers for checking the resulting verification conditions.

The stages of the synthesis of verification conditions are depicted in Figure 2. The starting point is a set of inductive definitions (SID) and a CL formula describing the initial configurations of the system, together with a description of component behavior by finite-state machines. The CL formula uses inductively defined predicate symbols defined by sets of rewriting trees, describing the unfoldings of their inductive definitions. In particular, these rewriting trees describe architectures, up to a permutation of the indices of components of each type.

We use rewriting trees as the backbones of architecture encoding, from which we derive a MSO flow formula, that essentially describes the operational semantics induced by the interactions of the architecture, relying on (i) a static description of the profile of the interactions (how they glue component types), and (ii) the transition systems describing the behavior of component types in the architecture. The main technical problem in building flow formulae is tracking the identities and values of the variables that occur within predicate symbols, which, in turn, are recursively replaced by their definitions, in a rewriting tree. For instance, the y 2 variable introduced by rule (1) using existential quantification substitutes the x 2 variable from the definition of a Chain predicate, in rules ( 2) and (3) several times, before the same variable (y 2 ) substitutes the x 1 variable in rule (4) or (5) ( §1.1). This is achieved by defining a path automaton that traverses the rewriting tree downwards tracking the introduction of a variable by existential quantification in a rule to the rule where it is instantiated in a component atom.

The flow formula is subsequently used to define invariants, i.e. over-approximations of the sets of states reachable from some initial configuration, in a system defined by some unfolding (rewriting) of the predicate symbols in CL specifications. In contrast with the classical approach of invariant inference using, e.g. abstract interpretation [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF], our technique generates invariants as MSO formulae obtained directly from the flow formulae, by a syntactic translation. Analogously, the set of error configurations (deadlocks and critical section violations) is obtained directly from the flow formula of the system. The verification condition asks that the conjunction of the MSO formulae describing the invariant and error configurations, respectively, is unsatisfiable; a satisfiable verification condition might indicate the presence of a spurious error caused by the overapproximation introduced by the invariant synthesis. Since we represent the configurations of a system by rewriting trees, we use a decidable fragment of MSO, interpreted over trees to answer the verification condition automatically.

The paper is structured as follows. Section 2 introduces the definitions of component-based systems and their operational semantics, Section 3 describes the resource logic used to define sets of configurations, Section 4 describes the parametric decision problems and gives the general undecidability results, Section 5 defines rewriting trees formally, together with a notion of a canonical model, induced by a rewriting tree of a logical formula, Section 6 describes the invariant synthesis and the encoding of the verification conditions in MSO, Section 7 reports on related work and Section 8 gives concluding remarks and sketches directions for future work.

Component-based Systems

Definitions

This section introduces the definitions needed to formally describe our model of component-based systems. We denote by N the set of natural numbers. Given integers i and j, we write [i, j] for the set {i, i + 1, . . . , j}, assumed to be empty if i > j. For a set A and an integer i ≥ 1, we denote by A i the i-times Cartesian product of A with itself. By pow(A) we denote the powerset of A. For a finite set A, we denote by ||A|| its cardinality.

Let P be a countable set of ports. We consider classes of component-based systems that share the same signature Σ = (C, I, P), where: W.l.o.g., we assume that N i=1 P(C i ) = P and P(C i ) ∩ P(C j ) = ∅, for all 1 ≤ i < j ≤ N , i.e. each port p belongs to the interface of exactly one component type, denoted by comp(p). We denote by I (k) the subset of interaction types of arity k, formally

• C = {C 1 , . . . , C N } is
I (k) def = {I ∈ I | #(I) = k}, for any k ≥ 1.
Example 1 (contd. from §1.1). The signature for the token-ring example from Figure 1a is Σ = {S}, {T}, P , where P(S) = {in, out} and P(T) = out, in , i.e. the interaction type T connects an out port to an in port.

The component and interaction types are interpreted as sets and relations over a countably infinite universe U of indices. The particular nature of indices is not important at this point; we assume that two indices can only be compared for equality, with no other associated relation or function. An architecture α over the signature Σ = (C, I, P) associates each component type C i a set α(C i ) ⊆ U and each interaction type I j a relation α(I j ) ⊆ U #(Ij ) , defining:

• components C i [u], for some u ∈ α(C i ), and

• interactions I j [u 1 , . . . , u #(Ij ) ], for some u 1 , . . . , u #(Ij ) ∈ α(I j ).
Intuitively, an architecture is a description of the static structure of a system. Note that an index u ∈ U can refer two (or more) different components C

(S) = [1, n] and α(T) = { 1, 2 , 2, 3 , . . . , n, 1 } , for some n ≥ 2.
A behavior is described by a finite state machine M = (Q, P, -→), where Q is a finite set of states, P ⊆ P is a finite set of ports and -→⊆ Q × P × Q is a transition relation; we write q p -→ q instead of (q, p, q ) ∈-→. Let B be the set of finite-state machines with ports from P. The behavior map β :

C → B associates each component type C ∈ C with a state machine β(C) = (Q C , P(C), - → C ),
whose set of states is denoted by For a port p we denote by T β (p) the set of transitions labeled by p in the finite-state machine associated by β to comp(p). We extend this notation to tuples of ports by taking

states β (C) def = Q C . In the following, we consider w.l.o.g. that states β (C i ) ∩ states β (C j ) = ∅, for all 1 ≤ i < j ≤ N and define Q β def = N i=1 states β (C i ).
T β ( p 1 , . . . , p n ) def = T β (p 1 ) × • • • × T β (p n ).
That is, the set T β ( p 1 , . . . , p n ) contains n-tuples of transitions t 1 , . . . , t n labeled respectively with ports p 1 , . . . , p n . For an interaction I we use T β (I) as a shortcut for T β (P(I)). In particular, T β (I) contains the set of tuples of component's transitions that are synchronizing by interaction I.

A system S is a tuple (Σ, α, β), where α is an architecture and β is a behavior associated with the signature Σ. When Σ is clear from the context, we omit it and denote a system as (α, β).

Operational Semantics

We represent the operational semantics of a system as a Petri net, recalled below for self-containment reasons. A Petri net 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 × A marked Petri net is a pair N = (N, m 0 ), where m 0 is the initial marking of N. A firing sequence is initial if it starts in m 0 . A marking m is reachable in N if there exists an initial firing sequence ending in m. Let Reach(N ) (resp. Step(N )) be the set of markings reachable (in one step) in N . For simplicity, we write Reach(N, m 0 ) and Step(N, m 0 ) instead of Reach((N, m 0 )) and

T ) ∪ (T × S) is a set of edges. Given x, y ∈ S ∪ T , we write E(x, y) def = 1 if (x, y) ∈ E and E(x, y) def = 0, otherwise. Let • x def = {y ∈ S ∪ T | E(y, x) = 1}, x • def = {y ∈ S ∪ T | E(x, y) = 1}
Step((N, m 0 )), respectively. A marked Petri net N is boolean2 if m(s) ≤ 1, for each s ∈ S and m ∈ Reach(N ). All marked Petri nets considered in the following will be boolean and we blur the distinction between a marking m : S → {0, 1} and the set {s ∈ S | m(s) = 1}, by writing s ∈ m (resp. s ∈ m) instead of m(s) = 1 (resp. m(s) = 0). Definition 1. The operational semantics of a system S = (Σ, α, β) with signature Σ = (C, I, P) is represented by the Petri net N(S) = (S, T, E), where:

S def = C∈C { q[u] | q ∈ states β (C), u ∈ α(C) } T def = I∈I { (I[u 1 , . . . , u #(I) ], t 1 , . . . , t #(I) ) | p 1 , . . . , p #(I) = P(I), u 1 , . . . , u #(I) ∈ α(I), t 1 , . . . , t #(I) ∈ T β (I), ∀i, j ∈ [1, #(I)]. i = j ⇒ u i = u j or comp(p i ) = comp(p j ) } E def = I∈I { (q[u i ]
), q [u i ]) | t i = (q pi -→ q ), i ∈ [1, #(I)] }
The places, transitions and edges of N(S) are defined jointly by the architecture α and the behavior β. For every component C[u] in α, the Petri net contains the places q[u], for each state q in states β (C). For every interaction I[u 1 , . . . , u #(I) ] in α, the Petri net contains one transition for every tuple t 1 , . . . , t #(I) of transitions of component types behavior, which are synchronizing according to I, that is, where their labeling ports p 1 , . . . , p #(I) form the tuple P(I). Moreover, a transition corresponding to an interaction I[u 1 , . . . , u #(I) ] involves pairwise distinct components; the last condition in the definition of T above requires that u i = u j or comp(p i ) = comp(p j ). Finally, edges are defined according to the tuple of synchronizing transitions t 1 , . . . , t #(I) and connect to pre-and post-places, respectively q[u i ] and q [u i ], for each involved component C[u i ]. For the sake of clarity we omit writing the tuple t 1 , . . . , t #(I) when it is determined by I, namely for those behaviors where a port labels exactly one transition, in each state machine, as it is the case in the example below: Example 4 (contd. from Example 3). The Petri net describing the execution semantics of the token-ring system from Figure 1(a) is given in Figure 3. Consider the marking of this Petri net depicted in dashed lines. From this marking, the sequence of interactions T [START_REF] Kramer | Analysing dynamic change in distributed software architectures[END_REF][START_REF] Bozga | Specification and safety verification of parametric hierarchical distributed systems[END_REF], T[2, 3], . . . , T[n-1, n], T[n, 1] can be fired any number of times, in this order. These interactions correspond to the joint execution of the transitions labeled by the ports out and in, from any two adjacent components i and (i mod n) + 1 of the ring, respectively.

T[1, 2] t[1] n[2] t[2] n[n] t[n] T[n -1, n] T[2, 3] T[n, 1] . . . T[n, 1] n[1]
The executions of a system S = (Σ, α, β) can be represented by the firing sequences of a marked Petri net involving only those boolean markings of N(S), that contain exactly one state q ∈ states β (C) per component C[u], such that u ∈ α(C). We formalize and prove this fact below: Definition 2. Given a system S = (Σ, α, β) with signature Σ = (C, I, P), a marking m of the Petri net N(S) = (S, T, E) is precise if and only if, for each C ∈ C and each u ∈ α(C), we have ||m ∩ {q[u] | q ∈ states β (C)}|| = 1.

Proposition 1. Given a system S and a precise initial marking m 0 of N(S), every marking m ∈ Reach(N(S), m 0 ) is precise.

Proof. Let S = (Σ, α) and m ∈ Reach(N(S), m 0 ) be a marking. The proof goes by the length n ≥ 0 of the firing sequence taking m 0 into m . For the base case n = 0, we have that m = m 0 is precise, by hypothesis. For the inductive step n ≥ 1, let m be the predecessor of m in the sequence, hence m is precise for S, by the inductive hypothesis. Then, by Def. 1, there exists a transition (I[u 1 , . . . , u #(I) ], t 1 , . . . , t

#(I) ) in T , such that m = (m \ {q 1 [u 1 ], . . . , q #(I) [u #(I) ]}) ∪ {q 1 [u 1 ], . . . , q #(I) [u #(I) ]} (6)
where P(I) = p 1 , . . . , p #(I) and

t i = (q i pi -→ q i ) ∈-→ comp(pi) for all i ∈ [1, #(I)] and moreover u i = u j or comp(p i ) = comp(p j ) for all distinct i, j ∈ [1, #(I)].
Let C ∈ C be a component type and let u ∈ α(C) be an index. Since m is precise, we have m ∩ {q[u] | q ∈ states β (C)} = {q * [u]}, for some state q * . We distinguish the following cases:

• u = u i for some i ∈ [1, #(I)] and q * = q i In this case, we have:

m ∩ {q[u] | q ∈ states β (C)} = {q i [u]}, by definition of m in (6)
• u = u i for some i ∈ [1, #(I)] and q * = q i . In this case, as the transition (I[u 1 , . . . , u #(I) ], t 1 , . . . , t #(I) ) fires in m it follows that q i [u] ∈ m. But

then q i [u] ∈ m ∩ {q[u] | q ∈ states β (C)} = {q * [u]} implies q i = q * ,
which is a contradiction.

• u ∈ {u 1 , . . . , u #(I) }. In this case, we have:

m ∩ {q[u] | q ∈ states β (C)} = m ∩ {q[u] | q ∈ states β (C)}
In all non-contradictory cases, we obtain that ||m ∩ {q[u] | q ∈ states β (C)}|| = 1.

Because C ∈ C and u ∈ α(C) are arbitrary, m is precise for S.

The Configuration Logic

By configuration of a system, we understand the architecture describing the components and interactions from the system, together with a snapshot of its current state. Configurations are used to reason about parametric systems, that share a common architectural pattern (style) and differ in the number of instances of a certain component type. For instance, a token-ring (Figure 1) applies the same architectural pattern (the output of each component is connected to its right neighbor in a round-robin fashion) to any number of components, greater or equal to two.

We introduce the configuration logic (CL) to describe (possibly infinite) sets of configurations, via inductive definitions. Let Σ = (C, I, P) be a signature and β : C → B be a behavior map, fixed for the rest of this section. Definition 3. A configuration of a system S = (Σ, α, β) is a pair (α, m), where α is an architecture over the signature Σ and m is a precise marking of N(S).

We aim at describing sets of configurations recursively (i.e. configurations with more complex structure being obtained by composing simpler ones), using the following definition of composition: Definition 4. Two architectures α 1 and α 2 , over the signature Σ = (C, I, P), are disjoint if and only if α 1 (C) ∩ α 2 (C) = ∅, for all C ∈ C and α 1 (I) ∩ α 2 (I) = ∅, for all I ∈ I. If α 1 and α 2 are disjoint, the composition of configurations

(α 1 , m 1 ) and (α 2 , m 2 ) is (α 1 , m 1 ) • (α 2 , m 2 ) def = (α 1 ∪ α 2 , m 1 ∪ m 2 )
, where α 1 ∪ α 2 denotes the pointwise union of the architectures α 1 and α 2 :

• (α 1 ∪ α 2 )(C) = α 1 (C) ∪ α 2 (C), for each C ∈ C, • (α 1 ∪ α 2 )(I) = α 1 (I) ∪ α 2 (I), for each I ∈ I. The composition (α 1 , m 1 ) • (α 2 , m 2 ) is undefined if α 1 and α 2 are not disjoint.
It is easy to check that the composition of configurations (α 1 , m 1 ) and (α 2 , m 2 ) with disjoint architectures is again a configuration, in particular m 1 ∩ m 2 = ∅ and m 1 ∪ m 2 is a precise marking of the Petri net N(Σ, α 1 ∪ α 2 , β).

Let X 1 be a set of first-order variables and A be a countably infinite set of predicate symbols, where #(A) ≥ 0 denotes the arity of a predicate symbol A ∈ A. The formulae of CL are inductively defined by the following syntax:

φ ::= emp | C(x) | C q (x) | I(x 1 , . . . , x #(I) ) | A(x 1 , . . . , x #(A) ) | φ * φ | ∃x . φ
where C ∈ C are component types, q ∈ states β (C) are states, I ∈ I are interaction types, A ∈ A are predicate symbols and x 1 , x 2 , . . . ∈ X 1 denote firstorder variables. Atomic formulae of the form C(x) or C q (x), I(x 1 , . . . , x #(I) ) and A(x 1 , . . . , x #(A) ) are called component, interaction and predicate atoms, respectively. The logical connective * is an associative and commutative separating conjunction operator.

By fv(φ) we denote the set of free variables that do not occur within the scope of a quantifier; φ is called quantifier-free (q.f.) if and only if it has no quantifiers and a sentence if and only if fv(φ) = ∅, respectively. A substitution is a partial mapping θ : X 1 → X 1 and φθ is the formula obtained by replacing each variable

x ∈ fv(φ) ∩ dom(θ) by θ(x) in φ, where dom(θ)

def = {x ∈ X 1 | θ is defined at x}.
We denote by [x 1 /y 1 , . . . , x k /y k ] the substitution that replaces x i with y i , for all i ∈ [1, k] and is undefined everywhere else. This notation is extended to tuples of variables of equal length as [x/y], where x = x 1 , . . . , x k and y = y 1 , . . . , y k .

Intuitively, a formula emp describes configurations with empty architecture, C(x) (resp. C q (x)) describes configurations with architectures consisting of a single instance of the component type C, indexed by the value of x (resp. in state q), and I(x 1 , . . . , x k ) describes a single interaction of type I, between components indexed by x 1 , . . . , x k , respectively. The formula C q1 (x 1 ) * . . . * C q k (x k ) * I(x 1 , . . . , x k ) describes an architecture consisting of k pairwise distinct instances of the component type C, in states q 1 , . . . , q k , respectively, joined by an interaction of type I. The formula I(x 1 , . . . , x k ) * I(x 1 , . . . , x k ) states the existence of two interactions of type I, with distinct tuples of indices, given by the values of x 1 , . . . , x k and x 1 , . . . , x k , respectively, i.e. the values of x i and x i must differ for at least one i ∈ [1, k].

The semantics of CL formulae is given by a satisfaction relation |= s ∆ between configurations and formulae. This relation is parameterized by: • a store s : X 1 → U, i.e. a function mapping variables to indices, and • a set of inductive definitions (SID) ∆ consisting of rules of the form A(x 1 , . . . , x #(A) ) ← φ, where φ is a CL formula such that fv(φ) = {x 1 , . . ., x #(A) }. The satisfaction relation is defined inductively on the structure of the formulae:

(α, m) |= s ∆ emp ⇐⇒ α(C) = ∅, for all C ∈ C, α(I) = ∅, for all I ∈ I and m = ∅ (α, m) |= s ∆ C(x) ⇐⇒ α(C) = {s(x)}, α(C ) = ∅, for all C ∈ C {C}, α(I) = ∅, for all I ∈ I and m = {q[s(x)]} , for some q ∈ states β (C) (α, m) |= s ∆ C q (x) ⇐⇒ α(C) = {s(x)}, α(C ) = ∅, for all C ∈ C {C}, α(I) = ∅, for all I ∈ I and m = {q[s(x)]} (α, m) |= s ∆ I(x 1 , . . . , x #(I k ) ) ⇐⇒ α(C) = ∅, for all C ∈ C, α(I) = { s(x 1 ), . . ., s(x #(I k ) ) }, α(I ) = ∅, for all I ∈ I {I} and m = ∅ (α, m) |= s ∆ A(x 1 , . . . , x #(A) ) ⇐⇒ (α, m) |= s ∆ φ[y 1 /x 1 , . . . , y #(A) /x #(A) ], for some rule A(y 1 , . . . , y #(A) ) ← φ ∈ ∆ (α, m) |= s ∆ φ 1 * φ 2 ⇐⇒ there exist configurations (α 1 , m 1 ), (α 2 , m 2 ) such that (α, m) = (α 1 , m 1 ) • (α 2 , m 2 ) and (α i , m i ) |= s ∆ φ i , for i = 1, 2. (α, m) |= s ∆ ∃x . φ 1 ⇐⇒ (α, m) |= s ∆ φ 1
, for some store s that agrees with s on all variables from X 1 {x} To simplify the notation, we consider that ∆ is fixed and omit the ∆ subscript in the following. If the formula φ is a sentence, we can omit the store s from the satisfaction relation |= s and write (α, m) |= φ. In this case, (α, m) is said to be a model of φ and denote by [[φ]] the set of models of the sentence φ. For two sentences φ and ψ, we say that

φ entails ψ if [[φ]] ⊆ [[ψ]], written φ |= ψ.
Example 5 (contd. from §1.1). The SID consisting of the rules 1-5 ( §1.1) defines systems with token-ring architectures. On the other hand, the rules below define chains of S and T components, with at least n, t ∈ N components in state n and t, respectively:

Chain 0,0 (x, x) ← S(x) Chain 0,1 (x, x) ← S t (x) Chain 1,0 (x, x) ← S n (x) Chain n,t (x, z) ← ∃y. S t (x) * T(x, y) * Chain n,t -1 (y, z) Chain n,t (x, z) ← ∃y. S n (x) * T(x, y) * Chain n -1,t (y, z) where k -1 def = max(k -1, 0), k ∈ N.
Below we show that CL sentences define indeed system configurations.

Proposition 2. Given a sentence φ of CL, if (α, m) ∈ [[φ]] then m is a precise marking of the Petri net N(Σ, α, β).
Proof. We prove a more general statement: for each formula φ and each store s, if (α, m) |= s φ then m is a precise marking of N(Σ, α, β). The proof is by induction on the definition of the |= s relation, by distinguishing the following cases:

• φ ∈ {emp, I(x 1 , . . . , x #(I) )}: m = ∅ and α(C) = ∅, for all C ∈ C, thus m is trivially precise for N(Σ, α, β). • φ = C(x): m = {q[s(x)]}, for some q ∈ states β (C), α(C) = {s(x)} and α(C ) = ∅, for all C ∈ C {C}, hence m is precise for N(Σ, α, β). • φ = C q (x): m = {q[s(x)]}, α(C) = {s(x)} and α(C ) = ∅, for all C ∈ C {C}, hence m is precise for N(Σ, α, β). • φ = A(x 1 , . . . , x #(A) ): (α, m) |= s ψ[y 1 /x 1 , . . . , y #(A) /x #(A)
], for some rule A(y 1 , . . . , y #(A) ) ← ψ ∈ ∆ and apply the inductive hypothesis.

• φ = φ 1 * φ 2 : if (α, m) |= s φ 1 * φ 2 then there exists configurations (α i , m i ) |= s φ i , for i = 1, 2, such that α 1 and α 2 are disjoint, α = α 1 ∪ α 2 and m = m 1 ∪ m 2 . By the inductive hypothesis, m i is a precise marking of N(Σ, α i , β), for i = 1, 2. Let C ∈ C be a component type and let u ∈ α(C) be an index. Then either u ∈ α 1 (C) or u ∈ α 2 (C), but not both. Let us consider the case u ∈ α 1 (C) α 2 (C), the other case being symmet- ric. Then m ∩ {q[u] | q ∈ states(C)} = m 1 ∩ {q[u] | q ∈ states(C)}, hence ||m ∩ {q[u] | q ∈ states(C)}|| = ||m 1 ∩ {q[u] | q ∈ states(C)}|| = 1.
Since the choices of C and u were arbitrary, we obtain that m is precise.

• φ = ∃x . φ 1 : by an application of the inductive hypothesis.

Decision Problems

A decision problem is a class of yes/no queries of the same kind, that differ only in their input. All decision problems considered in this paper are parameterized by a given signature Σ = (C, I, P). The queries take as input a sentence φ, a SID ∆, a behavior map β : C → B and a tuple of states q 1 , . . . , q n ∈ Q n β for some n ∈ N. They are defined as follows:

• deadlock (φ, ∆, β): is there a configuration (α, m), such that (α, m) |= ∆ φ and Reach(N(Σ, α, β), m) ∩ Dead (N(Σ, α, β)) = ∅ ? • reach(φ, q 1 , . . . , q k , ∆, β): are there configurations (α, m), (α, m ) and indices u 1 , . . . , u k ∈ U, such that (α, m) |= ∆ φ, m ∈ Reach(N(Σ, α, β), m) and {q i [u i ] | i ∈ [1, k]} ⊆ m , with q 1 [u 1 ], . . . , q k [u k ] pairwise distinct?
The above queries occur typically as correctness conditions in system verification. For instance, proving that, in every system described by a formula φ, no freeze configuration is reachable means showing that deadlock (φ, ∆, β) does not hold. Similarly, proving that each system described by φ stays clear of a set of error configurations e.g., at most one component is in some critical state q crit at any time amounts to proving that reach(φ, q crit , q crit , ∆, β) does not hold.

Undecidability Results for Linear Systems

We show that the problems defined by the sets of queries above, taken over all inputs, but parameterized by a fixed given signature, are undecidable. In fact, we shall prove stronger results, in which the input formulae define sets of configurations with linear architectures. Definition 5. Given a signature Σ = ({C}, I, P), a sentence φ, interpreted over a SID ∆, is linear if and only if φ |= ∆∪Λ φ L , where Λ consists of the rules:

L(x, x) ← C(x) * * I∈I (1) I(x) L(x, y) ← ∃z . C(x) * * I∈I (1) I(x) * * I∈I (2) I(x, z) * L(z, y)
where L is a binary predicate symbol and φ L is the sentence ∃x∃y . L(x, y).

For example, the sentences ∃x∃y.Chain(x, y) ( §1.1) and ∃x∃y.Chain n,t (x, y) for n, t ≥ 0 (Example 5) are linear, when taking C = {S} and I = {T}.

Below we show that undecidability occurs for classes of queries taking linear sentences as input, over a fixed signature consisting of only one component type and a fixed set of interaction types, which is not part of the input of a query.

Theorem 1. The following problems are undecidable:

LinearDeadlock def = {deadlock (φ, ∆, β) | φ |= ∆∪Λ φ L } LinearReachability def = {reach(φ, q 1 , ∆, β) | φ |= ∆∪Λ φ L }
The idea of the proof is to build a component-based system with linear architecture that simulates the execution of a Post-Turing machine. We present the construction in §4.2 and complete the proof in §4.3.

Simulation of Post-Turing Machines by Linear Systems

A Post-Turing machine [START_REF] Post | Finite Combinatory Processes-Formulation 1[END_REF][START_REF] Davis | What is a computation?[END_REF] executes sequential deterministic programs M of the form 1 : stmt 1 ; 2 : stmt 2 ; . . . ; m : stmt m , where each statement stmt i is one of following: write 0, write 1, go right, go left, goto step j if read 0, goto step j if read 1, stop, for some j ∈ [1, m]. The machine operates on an infinite tape of zeroes and ones. Initially, the head is pointing at some position on the tape and the program control is at the first statement. At any step, the current statement is executed and the tape content, the head position and control are updated according to that statement.

We simulate a Post-Turing machine by a component-based system with linear architecture. Its signature Σ P T = (C P T , I P T , P P T ) is presented in Figure 4(a) and consists of one component type C P T and ten interaction types I P T , with associated ports as presented in the figure. In particular, the signature does not depend on the program executed by the machine.

The linear system that simulates a Post-Turing machine is depicted in Figure 4(b). First of all, the machine program M is encoded in the behavior β M of the component type C P T . In particular, this behavior includes three disjoint state machines, as described in Table 1, labeled with the same set of ports. Second, in the linear system, each component plays a different role depending on its position, i.e. it runs according to one of the three state machines below:

• the leftmost ctrl component behaves according to the control state machine derived from the program M : it issues the commands to be executed by the tape components depending on the current statement, and proceeds further according to the control flow of M . In case of read commands, it goes to an intermediate state, waiting to receive either read 0 or read 1 answers. In case of left! commands, it goes to an error state signaling the overflow of the tape on the left side. The complete definition is given in Table 1 (top). • the middle tape components behave according to the tape state machine and mimic the behavior of a single tape cell: the k-th component state records the k-th symbol of the tape γ k and the presence ( ) or absence (⊥) of the machine head at that cell. They react to commands (received through in-ports) by changing their state and/or further issuing commands to their neighbors (sent through out-ports). The complete defini-440 tion is given in Table 1 (middle).

• the rightmost sink component behaves according to the sink state machine and detects the overflow of the tape on the right side and signals it as an error. This happens when this component receives the right! command. The complete definition is given in Table 1 (bottom). Let M be the program of a Post-Turing machine and let w = γ 1 γ 2 . . . γ n be a finite word in {0, 1} n , assuming moreover wlog 3 that n ≥ 2. Consider the signature Σ P T and the behavior β M as defined in the previous section. Furthermore, consider the following set ∆ w of rules, where

I 1 def = I (1) P T , I 2 def = I (2) P T : Zeroes(x, x) ← C (0,⊥) P T (z) * * I∈I1 I(x) Zeroes(x, y) ← ∃z . C (0,⊥) P T (x) * * I∈I1 I(x) * * I∈I2 I(x, z) * Zeroes(z, y)
3 w can be augmented with extra zeroes on the right control state machine

Q M ctrl def = {i, (i, ) | i ∈ [1, m + 1]} represents the program M i : write 0 i out write 0 -------→ i+1 i : write 1 i out write 1 -------→ i+1 i : go right i out right ------→ i+1 i : go left i out lef t -----→ i+1, i out lef t! -----→ (i, ), (i, ) out err -----→ (i, ) i : goto step j if read 0 i out read -----→ (i, ), (i, ) in read 0 ------→ j, (i, ) in read 1 ------→ i+1 i : goto step j if read 1 i out read -----→ (i, ), (i, ) in read 1 ------→ j, (i, ) in read 0 ------→ i+1 i : stop / * nothing * / tape state machine Qtape def = {(γ, π), (γ, π, a) | γ ∈ {0, 1}, π ∈ {⊥, }, a ∈ IP T {err }} (γ, ⊥) in a --→ (γ, ⊥, a) (γ, ⊥, a) out a ---→ (γ, ⊥) ∀a = right!, left!, err (γ, ⊥) in right! -----→ (γ, ) (γ, ⊥, left) out lef t! -----→ (γ, ) (γ, ) in write γ -------→ (γ , ) (γ, ) in read -----→ (γ, , read ) (γ, , read ) out read γ -------→ (γ, ) (γ, ) in right -----→ (γ, , right) (γ, , right) out right! ------→ (γ, ⊥) (γ, ) in lef t! -----→ (γ, ⊥) sink state machine with states Q sink def = {idle, busy} idle in right! -----→ busy busy out err -----→ busy
(x) * * I∈I1 I(x) * * I∈I2 I(x, z 2 ) * C (γ2,⊥) P T (z 2 ) * * I∈I1 I(z 2 ) * * I∈I2 I(z 2 , z 3 ) * C (γ3,⊥) P T (z 3 ) * * I∈I1 I(z 3 ) * ... * I∈I2 I(z n-1 , y) * C (γn,⊥) P T (y) * * I∈I1 I(y)
Tape w (x, y) ← ∃z 1 ∃w 1 ∃z 2 ∃w 2 . Zeroes(x, z 1 ) * and let φ w def = ∃x ∃y . Init w(x, y). Intuitively, φ w is a linear sentence which defines the valid (initial) configurations of the linear system encoding the Post-Turing machine, where moreover w is written on the tape and the machine head is pointing at the beginning w. We prove the following two assertions equivalent:

2. the answer to deadlock (φ w , ∆ w , β M ) is yes "1 ⇒ 2": If the machine terminates then it terminates by visiting finite portions of the tape to the left and to the right, with respect to the initial placement of w on the tape. Henceforth, if the linear component-based system is started with the amount of tape cells needed on both sides, it will run without errors (that is, neither left or right tape overflow) until termination as well. "2 ⇒ 1": First of all, if the linear system reaches a deadlock from its initial configuration, it means that neither left or right overflow occur (otherwise, the unary err interactions are enabled and run in an endless loop). Henceforth, the computation of the linear system involved only the allocated tape components and followed the execution of the statements in M . Moreover, by construction of the linear system, the relationship between the control and the tape state machines ensures that no blocking can occur between them: tape cells are continuously ready to receive the commands from the control and to execute them, in order. Therefore, the system stops in a deadlock only if no more commands are sent, i.e. when the control machine reaches a stop statement and all tape components are "idle", that is, no other commands are pending for completion.

The termination problem of Post-Turing machines being undecidable [START_REF] Davis | What is a computation?[END_REF], it implies that the LinearDeadlock problem is also undecidable. Moreover, we can use a similar argument to show that the LinearReachability problem is undecidable as well. Actually, we can restrict without loss of generality to programs M containing a unique stop statement moreover occurring as the last statement m in M . Then, for such programs we can prove the equivalence of the previous assertions to the following one:

3. the answer to reach(φ w , m , ∆ w , β M ) is yes that is, the linear system reaches some configuration where a component is in state m. In fact, by construction, the only component that could reach the m state is the leftmost control component, and therefore we can map back any execution of the linear component-based system reaching m in the control component, to a terminating execution of the Post-Turing machine.

Translating CL Specifications into Rewriting Trees

The inductive interpretation of predicate symbols in the CL logic, by means of a finite set of definitions, supports the idea of designing systems hierarchically (top-down). For instance, in §1.1, we specify a ring system first by a chain of components, with an interaction between the out port of the last to the in port of the first component (rule 1). Then a chain consists of one component and an interaction between the out port of that component and the in port of the first component of a separate chain (rule 3), or of two components (rule 2). Intuitively, one can view these stages of the definition as rewriting steps, in which a predicate atom is replaced by one of the rules defining it. In this section, we formalize this idea by introducing rewriting trees, i.e. trees labeled with rules, that define a partial order in which the rules are applied.

Moreover, the verification method described in §6 uses rewriting trees as backbones for the encoding of sets of configurations in MSO interpreted over trees [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of second-order logic[END_REF]. In particular, the component indices from the set U are going to be interpreted as nodes of rewriting trees. As will be shown below, this interpretation of logical variables loses no generality, because component indices can only be compared for equality; their particular nature is of no importance from the point of view of the verification problems considered. Furthermore, the interpretation of component indices as tree nodes enables the use of a decidable fragment of MSO, to encode verification conditions.

The mapping of variables to the nodes of a rewriting tree is uniquely defined by the occurrences of the component atoms in the tree. More precisely, because all atomic propositions that occur in the rewriting tree are joined by separating conjunctions, the variables of all component atoms C(x) with the same component type C must be interpreted as different indices, or else the formula corresponding to the tree would not be satisfiable. Hence, a rewriting tree uniquely defines an architecture α over a given signature Σ and, implicitly, a Petri net N(Σ, α, β), for a given behavior map β (Def. 1).

Rewriting Trees

Trees play an important role in the subsequent developments, hence we introduce a few formal definitions, for self-containment reasons. Let κ ≥ 1 be an integer constant and let [1, κ] * denote the set of finite sequences of integers between 1 and κ, called nodes in the following. We denote the concatenation of nodes w, u ∈ [1, κ] * as w • u or simply wu, when no confusion arises. A set of nodes T ⊆ [1, κ] * is said to be:

1. prefix-closed if wi ∈ T , for some i ∈ [1, κ], only if w ∈ T , and 2. complete if wi ∈ T , for some i ∈ [1, κ], only if wj ∈ T , for all j ∈ [1, i -1]. A κ-ary tree T is a function mapping a complete prefix-closed set of nodes nodes(T ) into a finite set of labels. The root of T is the empty sequence , the children of a node w ∈ nodes(T ) are childs T (w)

def = {wi ∈ nodes(T ) | i ∈ [1, κ]} and the parent of a node wi ∈ nodes(T ), where i ∈ [1, κ], is w. The leaves of T are leaves(T ) def = {w ∈ nodes(T ) | w • 1 ∈ nodes(T )}. The subtree of T rooted at w is defined by nodes(T ↓ w ) def = {w | ww ∈ nodes(T )} and T ↓ w (w ) def = T (ww ),
for all w ∈ nodes(T ↓ w ). A prefix of a tree T is the restriction of T to a complete prefix-closed subset of nodes(T ). We say that T is finite if nodes(T ) is finite.

Let ∆ be a fixed SID in the rest of this section. For an arbitrary CL formula φ, we denote by # pred (φ) the number of occurrences of predicate atoms and by pred i (φ) the i-th predicate atom from φ, in some predefined total ordering of the symbols in the syntax tree of φ. A formula φ is said to be predicatefree if # pred (φ) = 0. Without loss of generality, we assume from now on that # pred (φ) ≤ κ, for each CL formula φ considered in the following. We shall also simplify our technical life by considering the following assumption: Assumption 1. For each sentence φ, there exists a rule A φ () ← φ in ∆, where A φ is a predicate symbol of zero arity, not occurring in φ or elsewhere in ∆.

This assumption loses no generality because each query in a decision problem ( §4) considers finitely many sentences, for which finitely many rules of the above form are added to ∆. Definition 6. Given a CL formula φ, a rewriting tree for φ is a tree T with labels from ∆, such that T ( ) = A(x 1 , . . . , x #(A) ) ← φ , for some predicate symbol A and, for each w ∈ nodes(T ) such that T (w) = A 0 (x 1 , . . . , x #(A0) ) ← ψ 0 , the following hold:

1.

for all i ∈ [1, # pred (ψ 0 )], if pred i (ψ 0 ) = A i (y i 1 , . . . , y i #(Ai) ), then wi ∈ nodes(T ) and T (wi) = A i (x 1 , . . . , x #(Ai) ) ← ψ i is a rule from ∆, 2. wi ∈ nodes(T ), for all i > # pred (ψ i ).
We denote by T(φ) the set of rewriting trees for φ.

By slight abuse of notation, we write φ[ψ 1 /ϕ 1 . . . ψ n /ϕ n ] for the result of replacing each subformula ψ i of φ by the formula ϕ i , for all i ∈ [1, n]. We associate each rewriting tree T ∈ T(φ) a characteristic formula F(T ), defined inductively on the structure of T , as follows:

F(T ) def =      φ, if nodes(T ) = { } φ [A 1 (y 1 )/F(T ↓ 1 )[x 1 /y 1 ] . . . A n (y n )/F(T ↓ n )[x n /y n ]] , if n = # pred (φ) ≥ 1 and pred i (φ) = A i (y i ), for all i ∈ [1, n]
Intuitively, the characteristic formula of a rewriting tree is the predicate-free formula obtained by replacing each predicate atom occurring in a node of the tree by the characteristic formula of its corresponding subtree, recursively. In the process of building a characteristic formula, the free variables of the characteristic formulae of the subtrees are substituted with the parameters of their corresponding predicate atoms.

Let M(T ) def = η denote the matrix of the characteristic formula F(T ) i.e., the largest quantifier-free formula of F(T ) = ∃x 1 . . . ∃x n . η written in prenex form.

Since the separating conjunction and the existential quantifier distribute, every characteristic formula has a prenex form that is unique, modulo the commutativity and associativity of the separating conjunction. Example 6. Let Σ = ({N, L}, {R, I}, P) be a signature, where P(N) = {req, reply}, P(L) = {reply, in, out}, P(R) = req, reply, reply and P(I) = out, in . Consider a behavior map β, such that states β (N) = {q 0 , q 1 } and states β (L) = {s 0 , s 1 , s 2 }. The SID below defines tree-shaped architectures, whose leaves are

Leaf (x) ← L s 0 (x) Leaf (x) ← L s 0 (x) Leaf (x) ← L s 0 (x) Leaf (x) ← L s 0 (x) Leaf (x) ← L s 0 (x) Leaf (x) ← L s 0 (x) (a)
N(n 1 1 ) in out req N(n 1 2 ) L(l 1 ) L(r 1 1 ) L(l 1 2 ) Node(n 1 1 , l 1 , r 1 1 ) Node(n 1 2 , l 1 2 , r 1 )
Root() ← ∃r∃n 1 ∃ 1 ∃r 1 ∃n 2 ∃ 2 ∃r 2 . N q0 (r) * R(r, n 1 , n 2 ) * I(r 1 , 2 ) * I(r 2 , 1 ) * Node(n 1 , 1 , r 1 ) * Node(n 2 , 2 , r 2 ) (7) Node(n, , r) ← ∃n 1 ∃r 1 ∃n 2 ∃ 2 . N q0 (n) * R(n, n 1 , n 2 ) * I(r 1 , 2 ) * Node(n 1 , , r 1 ) * Node(n 2 , 2 , r) (8)
Node(n, , r) ← N q0 (n) * R(n, , r) * Leaf ( ) * I( , r) * Leaf (r) (9) Leaf (x) ← L s0 (x) (10)
Figure 5(a) shows an unfolding tree for φ = ∃r∃n

1 ∃ 1 ∃r 1 ∃n 2 ∃ 2 ∃r 2 . N q0 (r) * R(r, n 1 , n 2 ) * I(r 1 , 2 ) * I(r 2 , 1 ) * Node(n 1 , 1 , r 1 ) * Node(n 2 , 2 , r 2 ), with A φ =
Root, and Figure 5(b) shows a model of the characteristic formula of this unfolding tree. To avoid name clashes, we annotate existentially quantified variables in the characteristic formula with the node of the unfolding tree where they are introduced, for instance r , n 1 and n 2 are introduced at the root, whereas

n 1 1 , n 1 2 , 1 2 , r 1 1 (n 2 1 , n 2 2 , 2 2 , r 2 1
) occur first at the left (right) child of the root.

The following result shows that each model of a sentence is the model of the characteristic formula of some rewriting tree for that sentence, that represents the way in which the model is "produced" by unfolding the rules in ∆. In general, such rewriting trees are not unique, as different rewriting trees can have equivalent characteristic formulae.

Lemma 1. For each CL sentence φ, we have

[[φ]] = T ∈T(φ) [[F(T )]].
Proof. We prove a slightly more general statement: for each formula φ, each rule A(x 1 , . . . , x #(A) ) ← φ from ∆, each configuration (α, m) and each store s:

(α, m) |= s φ ⇐⇒ (α, m) |= s F(T ), for some T ∈ T(φ), such that T ( ) = A(x 1 , . . . , x #(A) ) ← φ
"⇒" By induction on the definition of the satisfaction relation |=, considering the following cases:

• φ ∈ {emp, C q (x
F(T ) = φ, thus (α, m) |= s F(T ). • φ = ∃y 1 . . . ∃y n . φ 0 * * k i=1 A i (z i 1 , . . . , z i #(Ai) )
, where φ 0 is quantifier-and predicate-free: since (α, m) |= s ∃y 1 . . . ∃y n . φ 0 * * k i=1 A i (z i 1 , . . . , z i #(Ai) ), there exists a store s that agrees with s over X 1 \ {y 1 , . . . , y n } and configurations (α i , m i ), such that (α, m) = (α 0 , m 0 ) • . . .

• (α k , m k ), (α 0 , m 0 ) |= s φ 0 and (α i , m i ) |= s A i (z i 1 , . . . , z i #(Ai) ), for all i ∈ [1, k]. For each i ∈ [1, k], since (α i , m i ) |= s A i (z i 1 , . . . , z i #(Ai) ), there exists A i (x 1 , . . . , x #(Ai) ) ← ψ i in ∆, such that (α i , m i ) |= s ψ i [x 1 /z i 1 , . . . , x #(Ai) /z i #(Ai) ], by the defini- tion of |=. Let s i def = s • [x 1 /z i 1 , . . . , x #(Ai) /z i #(Ai)
] be a store. We have (α i , m i ) |= s i ψ i and, by the induction hypothesis, there exists a rewrit-

ing tree T i ∈ T(ψ i ), such that T i ( ) = A i (x 1 , . . . , x #(Ai) ) ← ψ i and (α i , m i ) |= s i F(T i ), hence (α i , m i ) |= s F(T i )[x 1 /z i 1 , . . . , x #(Ai) /z i #(Ai)
]. We define the rewriting tree T as:

-nodes(T ) = { } ∪ k i=1 i • nodes(T i ), -T ( ) = A(x 1 , . . . , x #(A) ) ← φ, -T (iw) = T i (w), for each i ∈ [1, k] and each w ∈ nodes(T i ).
We obtain

F(T ) = ∃y 1 . . . ∃y n . φ 0 * * k i=1 F(T i )[x 1 /z i 1 , . . . , x #(Ai) /z i #(Ai) ], leading to (α, m) |= s F(T ).
"⇐" By induction on the structure of T ∈ T(φ), such that moreover T ( ) = A(x 1 , . . . , x #(A) ) ← φ , by distinguishing the following cases:

• nodes(T ) = { }: since T ( ) = A(x 1 , . . . , x #(A) ) ← φ , we have F(T ) = φ, hence (α, m) |= s φ.
• childs T ( ) = {1, . . . , k}, for some k ≥ 1: assume w.l.o.g. that φ =

∃y 1 . . . ∃y n . φ 0 * * k i=1 A i (z i 1 , . . . , z i #(Ai) )
, where φ 0 is a quantifier-and predicate-free formula. By the definition of characteristic formulae, we have

F(T ) = ∃y 1 . . . ∃y n . φ 0 * * k i=1 F(T ↓ i )[x 1 /z i 1 , . . . , x #(Ai) /z i #(Ai) ], where T (i) = A i (x 1 , . . . , x #(Ai) ) ← ψ i , hence T ↓ i ∈ T(ψ i ). Since (α, m)
|= s F(T ), there exists a store s that agrees with s over X 1 \ {y 1 , . . . , y n } and configurations (α 0 , m 0 ), . . . , (α k , m k ), such that (α 0 , m 0 ) |= s φ 0 and

(α i , m i ) |= s F(T ↓ i )[x 1 /z i 1 , . . . , x #(Ai) /z i #(Ai) ], for all i ∈ [1, m]. Consider an arbitrary index i ∈ [1, m] and let s i def = s • [x 1 /z i 1 , . . . , x #(Ai) /z i #(Ai) ], hence (α i , m i ) |= s i F(T ↓ i ). By the inductive hypothesis, we have (α i , m i ) |= s i ψ i , hence (α i , m i ) |= s i A i (x 1 , . . . , x #(Ai) ) and (α i , m i ) |= s A i (z i 1 , . . ., z i #(Ai) ) follows.
Because the above holds for all i ∈ [1, k], we conclude that (α, m) |= s φ.

Canonical Models

In the following, we shall equate the universe of indices U with the set [1, κ] * of tree nodes, i.e. finite sequences of integers between 1 and κ. This is without loss of generality, because both sets are infinitely countable and the nature of indices plays no role in the interpretation of CL formulae. In this setting, we define the canonical model (α T , m T ) of the characteristic formula F(T ) of a rewriting tree T . In order to simplify its definition, we proceed under the following assumption: Assumption 2. Each rule of ∆ is of one of the forms:

A(x 1 ) ← φ, such that φ = emp (I) A(x 1 , . . . , x #(A) ) ← ∃y 1 . . . ∃y n . φ * ψ * * p i=1 A i (z i 1 , . . . , z i #(Ai) ) (II)
for some n ≥ 0 and p ≥ 1, where:

• φ ∈ {C q (x 1 ) | C ∈ C, q ∈ states β (C)} ∪ {emp},
• ψ is a separating conjunction of interaction atoms, • p i=1 {z i 1 , . . . , z i #(Ai) } = {x 1 , . . . , x #(A) } \ fv(φ) ∪ {y 1 , . . . , y n }, and • {z i 1 , . . . , z i #(Ai) } ∩ {z j 1 , . . . , z j #(Aj ) } = ∅, for all 1 ≤ i < j ≤ p. The above assumption is not without loss of generality. On the positive side, all examples considered in this paper can be written using only rules of this form, for instance, the definition of the Chain n,t predicates, for constant integers n, t ≥ 0 (Example 5) or the definition of the Root, Node and Leaf predicates (Example 6).

A direct consequence of the above assumption is that, each variable that occurs in a characteristic formula of a rewriting tree, occurs in exactly one component atom, in a rule that labels exactly one node from the rewriting tree. This fact is proved below: Lemma 2. Let φ be a CL formula and T ∈ T(φ) be a rewriting tree for φ. For each variable x, that occurs free or existentially quantified in F(T ), there exists exactly one node w ∈ nodes(T ) and one component atom C q (x) in T (w).

Proof. It is sufficient to prove the statement for the case where x occurs in the label of the root of T . If it is introduced at some node w ∈ nodes(T ) \ { } by an existential quantifier, the same proof can be done taking T ↓ w instead of T . The proof goes by induction on the structure of T . For the base case nodes(T ) = { }, the only possibility is that T ( ) is a rule of the form (I) and the proof is immediate. For the inductive step, let T ( ) be the following rule:

A(x 1 , . . . , x #(A) ) ← ∃y 1 . . . ∃y n . φ * ψ * * p i=1 A i (z i 1 , . . . , z i #(Ai) )
If φ is of the form C q (x 1 ) and x = x 1 , then is the unique node such that x occurs in a component atom. Else, x ∈ {x 1 , . . . , x #(A) } ∪ {y 1 , . . . , y n } \ fv(φ), thus x ∈ {z i 1 , . . . , z i #(Ai) }, for exactly one i ∈ [1, p], by Assumption 2. In this case the inductive hypothesis applies, thus x occurs in exactly one component atom C q (x) in T (w), for exactly one w ∈ nodes(T ↓ i ).

The canonical model of a characteristic formula F(T ) is obtained by instantiating each variable x that occurs free or existentially quantified in F(T ) by the unique node w ∈ nodes(T ), such that x occurs in a single component atom C q (x) in T (w) (Lemma 2). Formally, let φ = ∃y 1 . . . ∃y n . ψ * * p i=1 A i (z i 1 , . . . , z i #(Ai) ) be a formula, where ψ is quantifier-and predicate-free, and define, for each rewriting tree T ∈ T(φ), a store s T : fv(ψ) ∪ p i=1 {z i 1 , . . . , z i #(Ai) } → nodes(T ), as follows:

s T (x) def =    if x occurs in a component atom from ψ i • s T↓i (x j ) if x = z i j , for some j ∈ [1, #(A i )],
where

T (i) = A i (x 1 , . . . , x #(Ai) ) ← ϕ i , for all i ∈ [1, p]
Note that, because the rules of the SID meet the conditions of Assumption 2, the two cases of the definition of s T above are exclusive and, moreover, s T (x) is defined for all free variables of the matrix ψ * * p i=1 A i (z i 1 , . . . , z i #(Ai) ) of φ. Recall that M(T ) denotes the quantifier-free matrix of the characteristic formula F(T ). We extend the store s T to a store s T : fv(M(T )) → nodes(T ) mapping all variables (free or existentially quantified) that occur in the characteristic formula F(T ):

s T (x) def = s T (x) if x ∈ fv(F(T )) w • s T↓w (x) if x is existentially quantified at w ∈ nodes(T ) (11)
In the above definition, we have assumed that all existentially quantified variables have pairwise distinct names (this is w.l.o.g. as quantified variables can be α-renamed, if necessary). Note that s T is uniquely defined, for each given rewriting tree T and induces a unique canonical model, defined below:

Definition 7.
The canonical model of a rewriting tree T is the configuration (α T , m T ), defined as follows:

• α T (C) def = {s T (x) | C q (x) occurs in M(T )}, • α T (I) def = { s T (x 1 ), . . . , s T (x #(I) ) | I(x 1 , . . . , x #(I)
) occurs in M(T )}, and

• m T def = {q[s T (x)] | C q (x) occurs in M(T )}.
Lemma 3. Given a sentence φ, for each rewriting tree T ∈ T(φ), we have (α T , m T ) |= F(T ).

Proof. We prove a more general statement, namely if φ is a formula, not necessarily a sentence, then (α T , m T ) |= s T M(T ). The proof goes by induction on the structure of T , distinguishing the cases below:

• nodes(T ) = { } and T ( ) = (A(x) ← C q (x)) is a rule of type (I): then

α T (C) = {s T (x)} = { }, m T = {q[s T (x)]} = {q[ ]}, α T (C ) = ∅, for all C ∈ C \ {C} and α T (I) = ∅, for all I ∈ I, thus (α T , m T ) |= s T C q (x).
• nodes(T ) = { } and T ( ) = A(x 1 , . . . , x #(A) ) ← ∃y 1 . . .

∃y n . φ * ψ * * p i=1 A i (z i 1 , . . . , z i #(Ai)
) is a rule of type (II). By the definition of s T , we have s T (x) = i • s T↓i (x), for all x ∈ fv(M(T ↓ i )) and i ∈ [1, p]. We define the structures (α 0 , m 0 ), (α 1 , m 1 ), . . . , (α p , m p ) as follows:

-

α 0 (C) def = {s T (x)} = { } and m 0 def = {q[s T (x)]} = {q[ ]} if φ = C q (x 1 ),
else α 0 (C) = ∅ and m 0 = ∅ and, moreover, α 0 (I)

def = { s T (x 1 ), . . ., s T (x #(I) ) | I(x 1 , . . . , x #(I) ) occurs in ψ}, thus we have (α 0 , m 0 ) |= s T φ * ψ. -α i (C) def = {s T (x) | C q (x) occurs in M(T ↓ i )}, α i (I) def = { s T (x 1 ), . . ., s T (x #(I) ) | I(x 1 , . . . , x #(I) ) occurs in M(T ↓ i )} and m i def = {q[s T (x)] | C q (x) occurs in M(T ↓ i )}, for each i ∈ [1, p]. Since s T (x) = i • s T↓i (x), for all x ∈ η i and i ∈ [1, p], we have α i (C) = {i • u | u ∈ α T↓i (C)}, for all C ∈ C, m i = {q[i • u] | q[u] ∈ m T↓i } and α i (I) = { i•u 1 , . . ., i•u #(I)
| u 1 , . . . , u #(I) ∈ α T↓i (I)}, for all I ∈ I. By the inductive hypothesis, we have (α T↓i , m T↓i ) |= s T↓ i η i , thus (α i , m i ) |= s T η i , for all i ∈ [1, p].

Since the sets of indices of α 0 , . . . , α p and m 0 , . . . , m p are pairwise disjoint, their composition is defined and, moreover, we have (α T , m T ) = (α 0 , m 0 ) • . . . • (α p , m p ). Consequently, we obtain (α T , m T ) |= s T φ * ψ * * p i=1 A i (z i 1 , . . . , z i #(Ai) ), as required. Example 7. Since T is a rewriting tree for a sentence, each variable occurs bound in F(T ) and is mapped by the store s T into the unique node of T that contains a unique component atom in which that variable occurs:

s T (r ) = s T (n 1 ) = 1 s T (n 2 ) = 2 s T (n 1 1 ) = 11 s T (n 1 2 ) = 12 s T (n 2 1 ) = 21 s T (n 2 2 ) = 22 s T ( 1 ) = 111 s T (r 1 1 ) = 112 s T ( 1 2 ) = 121 s T (r 1 ) = 122 s T ( 2 ) = 211 s T (r 2 1 ) = 212 s T ( 2 2 ) = 221 s T (r 2 ) = 222
The configuration (α T , m T ) corresponding to the rewriting tree T from Fig-

α T (N) = { , 1,
T = {q 0 [ ], q 0 [1], q 0 [2], q 0 [11], q 0 [12], q 0 [21], q 0 [22], s 0 [111], s 0 [112], s 0 [121], s 0 [122], s 0 [211], s 0 [212], s 0 [221], s 0 [222]}

Symmetry Reduction

As shown in Lemma 1, each model of a sentence is a model of the characteristic formula of some rewriting tree for that sentence. In this section, we prove a symmetry property of the models of a characteristic formula corresponding to a given rewriting tree, that makes them indistinguishable from the point of view of the decision problems considered previously ( §4). Let us fix a signature Σ, with component types C = {C 1 , . . . , C N } and interaction types I = {I 1 , . . . , I M }, and a behavior map β, in the rest of this section.

Intuitively, two architectures are symmetric if they differ only by a renaming of indices used to interpret the component and interaction types. For instance, the architectures α 1 and α 2 , where α

1 (C 1 ) = α 1 (C 2 ) = {1}, α 1 (I 1 ) = { 1, 1 } and α 2 (C 1 ) = {1}, α 2 (C 2 ) = {2}, α 2 (I 1 ) = { 1, 2 }
have the same shape (assuming N = 2 and M = 1). However, this isomorphism cannot be captured by a global permutation of indices, as it is usually the case4 in the literature [START_REF] Emerson | Symmetry and model checking[END_REF], because the sets α 1 (C 1 ) ∪ α 1 (C 2 ) and α 2 (C 1 ) ∪ α 2 (C 2 ) have different cardinalities. For this reason, our definition of symmetry considers one permutation per component type.

Formally, given an architecture α over Σ and a tuple of bijections f = f 1 , . . . , f N , where each f i : U → U renames the indices of the component type C i , for all i ∈ [1, N ], we define:

(f (α))(C i ) def = f i (α(C i )), for all i ∈ [1, N ] (f (α))(I) def = { f i1 (u 1 ), . . . , f i #(I) (u #(I) ) | u 1 , . . . , u #(I) ∈ α(I), ∀k ∈ [1, #(I)] . comp( P(I) k ) = C i k }
For a marking m of the Petri net N(Σ, α, β), we define, moreover:

f (m) def = {q[f i (u)] | q[u] ∈ m, q ∈ states β (C i ), i ∈ [1, N ]}
Since the sets states β (C i ), for i ∈ [1, N ], are assumed to be pairwise disjoint, for each state q there is exactly one component type C i , such that q ∈ states β (C i ).

Definition 8. Two configurations are symmetric, denoted (α 1 , m 1 ) ∼ (α 2 , m 2 ), if and only if there exists a tuple of bijections f = f 1 , . . . , f N , where f i : U → U,

for all i ∈ [1, N ], such that f (α 1 ) = α 2 and f (m 1 ) = m 2 .
The main idea of using symmetries is to prove that models of the same characteristic formula F(T ) of some rewriting tree T are symmetric and, in particular, symmetric with the canonical model (α T , m T ). This proof is greatly simplified by considering only those architectures in which all interactions are tightly connected to components, in the following sense: Note that the interactions from an architecture α having unconnected ports cannot fire in the Petri net N(Σ, α, β) (Def. 1), thus having no impact on the answer of a decision problem (deadlock, reachability). However, such interactions are important for the definition of the composition operation (Def. 4). For instance, the tight architecture from Example 1 can only be decomposed into loose non-empty architectures. Consequently, the syntax of CL formulae does not impose any restriction that guarantee tightness of the architectures defined. This is achieved by an easy-to-check condition below (Def. 10). In general, the tightness problem is decidable and its complexity has been studied for several fragments of CL [START_REF] Bozga | Decision problems in a logic for reasoning about reconfigurable distributed systems[END_REF]. Definition 10. A profile is a function λ : A → i≥1 C i , that associates each predicate symbol A(x 1 , . . . , x #(A) ) of non-zero arity with a tuple of component types of length #(A) ≥ 1. A formula φ is tight for a profile λ if and only if it contains, for each interaction atom I(x 1 , . . . , x #(I) ) and each k ∈ [1, #(I)]:

• a component atom C q (x k ), such that P(I) k ∈ P(C), or • a predicate atom A(y 1 , . . . , y #(A) ), such that x k = y and P(I) k ∈ P( λ(A) ), for some ∈ [1, #(A)]. A SID ∆ is tight if and only if there exists a profile λ ∆ , such that, for each rule A(x 1 , . . . , x #(A) ) ← φ from ∆, the formula φ is tight for λ ∆ and contains, for

each k ∈ [1, #(A)]: • a component atom C q (x k ), such that λ ∆ (A) k = C, or • a predicate atom B(y 1 , . . . , y #(A) ), such that x k = y and λ ∆ (A) k = λ ∆ (B) , for some ∈ [1, #(B)]. A formula φ, interpreted over a tight SID ∆, is tight if and only if it is tight for the profile λ ∆ .
For instance, one can check that the predicate atoms Chain n,t (x, y) are tight, by taking the profile λ ∆ (Chain n,t ) = S, S , for all constants n, t ≥ 0 (Example 5). Analogously, the predicate atoms Node(n, , r) are tight, by taking the profile λ ∆ (Node) = N, L, L and λ ∆ (Leaf ) = L (Example 6). The above conditions guarantee the tightness of architectures described by tight formulae: Lemma 4. For each model (α, m) of a tight sentence, the architecture α is tight.

Proof. Let φ be a tight sentence, such that (α, m) |= φ. By Lemma 1, there exists a rewriting tree T ∈ T(φ), such that (α, m) |= F(T ). Let I(z 1 , . . . , z #(I) ) be an interaction atom from F(T ) and k ∈ [1, #(I)]. Also, let w ∈ nodes(T ) be the node where this interaction atom was introduced, such that T (w) = A(x 1 , . . . , x #(A) ) ← ϕ and I(y 1 , . . . , y #(I) ) occurs in ϕ, where y 1 , . . . , y #(I) are substituted by z 1 , . . . , z #(A) , respectively, during the construction of F(T ). Since the SID ∆, that interprets the formula φ, is tight, the rule body ϕ is tight, hence one of the following holds:

• there exists a component atom C q (y k ) in ϕ, such that P(I) k = C, or • there exists a predicate atom B(ξ 1 , . . . , ξ #(B) ) in ϕ, such that y k = ξ and

P(I) k = λ ∆ (B)
, where λ ∆ is the profile from Def. 10. In this case, we apply induction to prove the existence of a component atom C q (ξ k ) in F(T ↓ i ), such that P(I) k = C, where i ∈ [1, # pred (ϕ)] is the child of w corresponding to B(ξ 1 , . . . , ξ #(B) ) in T . In both cases, F(T ) contains a component atom C q (z k ), such that P(I) k = C, hence (α, m) is tight, by Def. 9.

The next result proves that each model of a tight sentence is necessarily symmetric to a canonical model of that sentence:

Proposition 3. Given a tight sentence φ, for each T ∈ T(φ), if (α, m) |= F(T ), then (α, m) ∼ (α T , m T ). Proof. Since (α T , m T ) |= F(T ), by Lemma 3, it is sufficient to prove that (α 1 , m 1 ) ∼ (α 2 , m 2 ), for any two configurations (α i , m i ), such that (α i , m i ) |= F(T ). Let F(T ) def = ∃x 1 . . . ∃x n . η,
where η is a quantifier-and predicate-free formula. Then (α i , m i ) |= F(T ) if and only if there exist stores s i , such that (α i , m i ) |= si η, for i = 1, 2. We define the sets U i j def = {s i (x) | C q j (x) occurs in η} and the bijections f j : U 1 j → U 2 j as f j (s 1 (x)) = s 2 (x), for all variables x, such that C q j (x) occurs in η. These bijections are extended to bijections f j : U → U, by the following fact:

Fact 1. Given finite sets U 1 , U 2 ⊆ U, such that f : U 1 → U 2 is a bijection, there exists a bijection f : U → U, such that f (u) = f (u), for all u ∈ U 1 . Proof. Since f is a bijection, we have ||U 1 || = ||U 2 || and, since ||U i || = ||U i \ U 3-i ||+ ||U 1 ∩ U 2 ||, for i = 1, 2, we obtain ||U 1 \ U 2 || = ||U 2 \ U 1 ||. Hence there exists a bijection f : U → U, such that f (u) = f (u), for all u ∈ U 1 , f (U 2 \ U 1 ) = U 1 \ U 2 and f (U \ (U 1 ∪ U 2 )) = f (U \ (U 1 ∪ U 2 )). For f def = f 1 , . . . , f N ,
we prove the following points:

• f (α 1 ) = α 2 : by the definition of f j , we have f j (α 1 (C j )) = α 2 (C j ), for all j ∈ [1, N ]. Let I ∈ I and we prove α 2 (I) = { f i1 (u 1 ), . . . , f i #(I) (u #(I) ) | u 1 , . . . , u #(I) ∈ α 1 (I), ∀k ∈ [1, #(I)] . comp( P(I) k ) = C i k }. "⊆" Let u 1 , . . . , u #(I) ∈ α 2 (I).
Then there exists an interaction atom I(x 1 , . . ., x #(I) ) in η, such that

u i = s 2 (x i ), for i ∈ [1, #(I)].
u k ∈ α 1 (C i k ), such that f i k (u k ) = u k = s 2 (x k )
. By the definition of f i k , we have u k = s 1 (x k ), hence u 1 , . . . , u #(I) ∈ α 1 (I).

(x k ) = u k ∈ α 1 (C i k ). By the definition of f i k , we have s 2 (x k ) = f i k (u k ), for all k ∈ [1, #(I)], hence f i1 (u 1 ), . . . , f i #(I) (u #(I) ) ∈ α 2 (I). • f (m 1 ) = m 2 : we prove m 2 = {q[f i (u)] | q[u] ∈ m 1 , q ∈ states β (C i ), i ∈ [1, N ]}. "⊆" Let q[u] ∈ m 2 . Since (α 2 , m 2 ) |= s2 η, there exists a component atom C q i (x) in η, such that u = s 2 (x) ∈ α 2 (C i
) and C i is the unique component type, such that q ∈ states β (C i ). By the definition of f i , we have

s 1 (x) ∈ α 1 (C i ) and s 2 (x) = f i (s 1 (x)). Moreover, since (α 1 , m 1 ) |= s1 η, we have q[s 1 (x)] ∈ m 1 . "⊇" Let q[u] ∈ m 1 and q ∈ states β (C i ), for some i ∈ [1, N ]. Since (α 1 , m 1 ) |= s1 η, there exists a component atom C q (x) in η, such that u = s 1 (x). By the definition of f i , we have f i (s 1 (x)) = s 2 (x), hence q[f i (u)] = q[s 2 (x)] ∈ m 2 , since (α 2 , m 2 ) |= s2 η.
Moreover, the symmetry relation is preserved by the Petri net describing the operational semantics of the system (Def. 1): Lemma 5. Given a tight architecture α and a behavior β, over a signature Σ = ({C 1 , . . . , C N }, I, P), for any tuple of bijections f = f 1 , . . . , f N , where f i : U → U, for all i ∈ [1, N ], the following hold:

1. m ∈ Reach(N(Σ, α, β), m) ⇐⇒ f (m ) ∈ Reach(N(Σ, f (α), β), f (m)), 2. m ∈ Dead (N(Σ, α, β)) ⇐⇒ f (m) ∈ Dead (N(Σ, f (α), β)),
for any two markings m, m of the Petri net N(Σ, α, β).

Proof. By Def. 1, let N(Σ, f (α), β) be the Petri net (S f , T f , E f ), where:

S f = N i=1 {q[u] | q ∈ states(C i ), u ∈ (f (α))(C i )} = N i=1 {q[f i (u)] | q ∈ states(C i ), u ∈ α(C i )} T f = I∈I { (I[u 1 , . . . , u #(I) ], t 1 , . . . , t #(I) ) | p 1 , . . . , p #(I) = P(I), u 1 , . . . , u #(I) ∈ (f (α))(I), t 1 , . . . , t #(I) ∈ T β (I), ∀i, j ∈ [1, #(I)]. i = j ⇒ u i = u j or comp(p i ) = comp(p j ) } = I∈I { (I[f k1 (u 1 ), . . . , f k #(I) (u #(I) )], t 1 , . . . , t #(I) ) | p 1 , . . . , p #(I) = P(I), ∀i ∈ [1, #(I)]. C ki = comp(p i ), u 1 , . . . , u #(I) ∈ α(I), t 1 , . . . , t #(I) ∈ T β (I), ∀i, j ∈ [1, #(I)]. i = j ⇒ f ki (u i ) = f kj (u j ) or comp(p i ) = comp(p j ) } E f = I∈I { (q[f ki (u i )], (I[f k1 (u 1 ), . . . , f k #(I) (u #(I) )], t 1 , . . . , t #(I) )), ((I[f k1 (u 1 ), . . . , f k #(I) (u #(I) )], t 1 , . . . , t #(I) ), q [f ki (u i )]) | t i = (q pi -→ comp(pi) q ), i ∈ [1, #(I)] }
We obtain the following equivalence:

m (I[u1,...,u #(I) ], t1,...,t #(I) ) -----------------→ m in N(Σ, α, β) ⇐⇒ f (m) (I[f k 1 (u1),...,f k #(I) (u #(I) )], t1,...,t #(I) ) -------------------------→ f (m ) in N(Σ, f (α), β)
where

k 1 , . . . , k #(I) ∈ [1, N ] are such that C ki = comp( P(I) i ), for all i ∈ [1, #(I)].
Point (1) uses this fact inductively, on the length of the firing sequence leading from m to m . For point (2) we use, moreover, that

q[u] ∈ m ⇐⇒ q[f i (u)] ∈ f (m) and q[u] ∈ • (I[u 1 , . . . , u #(I) ], t 1 , . . . , t #(I) ) ⇐⇒ q[f i (u)] ∈ • (I[f k1 (u 1 ), . . . , f k #(I) (u #(I) )], t 1 , . . . , t #(I) )
, where C i is the unique component type such that q ∈ states β (C i ).

Theorem 2. Given a tight sentence φ, interpreted over a SID ∆, a behavior map β and a tuple of states q 1 , . . . , q k , the following equivalences hold:

deadlock t (φ, ∆, β) ⇐⇒ deadlock (φ, ∆, β) reach t (φ, q 1 , . . . , q k , ∆, β) ⇐⇒ reach(φ, q 1 , . . . , q k , ∆, β)
where deadlock t (φ, ∆, β) and reach t (φ, q 1 , . . . , q k , ∆, β) are defined below:

• deadlock t (φ, ∆, β): does there exist rewriting tree T ∈ T(φ), such that Reach(N(Σ, α T , β), m T ) ∩ Dead (N(Σ, α T , β)) = ∅?

• reach t (φ, q 1 , . . . , q k , ∆, β): does there exist a rewriting tree T ∈ T(φ) and a configuration

(α T , m) ∈ Reach(N(Σ, α T , β), m T ), such that {q i [u i ] | i ∈ [1, k]} ⊆ m, with q 1 [u 1 ], . . . , q k [u k ] pairwise distinct?
Proof. We prove the following points:

• deadlock t (φ, ∆, β) ⇒ deadlock (φ, ∆, β): assume that deadlock t (φ, ∆, β)
has a positive answer and let T ∈ T(φ) be a rewriting tree, such that Reach(N(Σ, α T , β), m T ) ∩ Dead (N(Σ, α T , β)) = ∅, the existence of which is stated by deadlock t (φ, ∆, β). By Lemma 3, (α T , m T ) |= F(T ) and, by Lemma 1, we obtain (α T , m T ) |= φ, thus deadlock (φ, ∆, β) has a positive answer. • deadlock (φ, ∆, β) ⇒ deadlock t (φ, ∆, β): assume that deadlock (φ, ∆, β) has a positive answer and let (α, m) be a model of φ and m be a marking such that m ∈ Reach(N(Σ, α, β), m) ∩ Dead (N(Σ, α, β)). By Lemma 1, there exists a rewriting tree T ∈ T(φ), such that (α, m) |= F(T ). By Lemma 3, since φ is a tight sentence, we obtain that (α, m) ∼ (α T , m T ) and let f = f 1 , . . . , f N be the bijections from Def. 8, such that (α T , m T ) = (f (α), f (m)). By Lemma 5, we obtain that

f (m ) ∈ Reach(N(Σ, f (α), β), f (m)) ∩ Dead (N(Σ, f (α), β)), thus deadlock t (φ, ∆, β)
has a positive answer.

• reach t (φ, q 1 , . . . , q k , ∆, β) ⇒ reach(φ, q 1 , . . . , q k , ∆, β): assume that reach t (φ, q 1 , . . . , q k , ∆, β) has a positive answer and let T ∈ T(φ) be a rewriting tree and m be a marking of

N(Σ, α T , β), such that (α T , m) ∈ Reach(N(Σ, α T , β), m T ) and {q i [u i ] | i ∈ [1, k]} ⊆ m, where q 1 [u 1 ], . . ., q k [u k ] are pairwise distinct places. By Lemma 3, (α T , m T ) |= F(T ) and,
by Lemma 1, we obtain (α T , m T ) |= φ, thus reach(φ, q 1 , . . . , q k , ∆, β)

has a positive answer. • reach(φ, q 1 , . . . , q k , ∆, β) ⇒ reach t (φ, q 1 , . . . , q k , ∆, β): assume that reach(φ, q 1 , . . . , q k , ∆, β) has a positive answer and let (α, m) be a model of φ and m ∈ Reach(N(Σ, α, β), m) be a marking, such that

{q i [u i ] | i ∈ [1, k]} ⊆ m , where q 1 [u 1 ], . . . , q k [u k ] are pairwise distinct places of N(Σ, α, β)
. By Lemma 1, there exists a rewriting tree T ∈ T(φ), such that (α, m) |= F(T ). By Lemma 3, since φ is a tight sentence, we obtain that (α, m) ∼ (α T , m T ) and let f = f 1 , . . . , f N be the bijections from Def. 8, such that (α T , m T ) = (f (α), f (m)). By Lemma 5, we obtain that f (m ) ∈

Reach(N(Σ, f (α), β), f (m)). Moreover, if C i is the unique component type, such that q i ∈ states β (C i ), for all i ∈ [1, k], since {q i [u i ] | i ∈ [1, k]} ⊆ m , we obtain {q i [f i (u i )] | i ∈ [1, k]} ⊆ f (m ) and reach t (φ, q 1 , . . . , q k , ∆, β)
has a positive answer.

Parametric Verification using Structural Invariants

In this section we present a sound (but necessarily incomplete) method to address practical instances of the (undecidable) decision problems of deadlock and reachability (Theorem 1). The method proceeds by synthesizing a sufficient verification condition as a formula in a decidable fragment of MSO, interpreted over trees of bounded arity κ, with second-order set variables ranging over finite sets. This logic is known as the Weak Second-order calculus of κ Successors (WSκS). Well-known automata-theoretic decision procedures exist for WSκS [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of second-order logic[END_REF] and we rely on optimized provers [START_REF] Henriksen | Mona: Monadic second-order logic in practice[END_REF] to check the verification conditions.

During the unfolding of the predicate symbols, according to the structure of a rewriting tree T , an existentially quantified variable introduced by a rule might be renamed several times (the renaming occurs when replacing a predicate atom A(y 1 , . . . , y #(A) ) with one of its definitions ϕ[x 1 /y 1 . . . x #(A) /y #(A) ], for some rule A(x 1 , . . . , x #(A) ) ← ϕ from the SID) before it is instantiated by a component atom C q (x), that occurs in some node w ∈ nodes(T ). Due to Assumption 2 on the syntax of the rules in the SID, this node is unique and the canonical store s T maps the variable to that node, i.e. s T (x) = w. In order to determine this value, we must track x along the path in the rewriting tree that leads from the node where it was introduced (by an existential quantifier, or the root of the tree if the variable is a top-level parameter) to the node where the component atom C q (x) occurs.

Example 8. Let us consider the rewriting tree T depicted in Fig. 5(a). The variable 1 introduced by an existential quantifier at the root of the tree replaces the parameter of the rule that labels the left successor of the root, i.e. the node 1, that replaces the parameter of the label of the node 11, which finally replaces the x parameter of the label of the node 111, that contains a component atom Leaf s0 (x). Hence, the value of 1 in the canonical store is s T ( 1 ) = 111. The path from the node where the variable has been introduced by existential quantification and the node where its value is assigned by an instance atom is shown in dashed lines in Fig. 5.

Tracking variables is done by path automata that traverse the tree downwards, following the substitutions of a particular variable. A path automaton is then transformed into an equivalent WSκS path formula, that defines the set of trees over which the automaton has an accepting run. The path formula is used to define a flow formula that describes the pre-and post-sets for each transition of the Petri net N(Σ, α T , β) corresponding to the canonical architecture α T , defined by the rewriting tree T , and the given behavior map β. Moreover, path formulae allow to define WSκS formulae describing the initial and final configurations of the system.

In particular, the flow formula is used to derive invariants (i.e. over-approximations of the set of reachable configurations) directly from the structure of the Petri net N(Σ, α T , β). These invariants are defined by the sets of places of N(Σ, α T , β) that do not lose (trap invariants) or generate extra tokens (mutex invariants), respectively. All verification conditions for the problems considered in this paper boil down to checking the satisfiability of a WSκS formula.

Weak Second Order Calculus of κ Successors

We define the logic WSκS, which is a fragment of MSO interpreted over a finite prefix of an infinite κ-ary tree. As a remainder, the prefix of a tree T is the restriction of T to a prefix-closed and complete subset of nodes(T ) ( §5.1).

Let X 2 = {X, Y, Z, . . .} be a countably infinite set of second-order variables, ranging over subsets of [1, κ] * . The formulae of WSκS are defined inductively by the following syntax:

τ ::= | x | τ.i terms ξ ::= τ = τ | X(τ ) | ξ ∧ ξ | ¬ξ | ∃x . ξ | ∃X . ξ formulae where x ∈ X 1 , X ∈ X 2 and i ∈ [1, κ]. As usual, we write x = y def = ¬x = y, ξ 1 ∨ ξ 2 def = ¬(¬ξ 1 ∧ ¬ξ 2 ), ξ 1 → ξ 2 def = ¬ξ 1 ∨ ξ 2 , ξ 1 ↔ ξ 2 def = (ξ 1 → ξ 2 ) ∧ (ξ 2 → ξ 1 ), ∀x . ξ def = ¬∃x . ¬ξ and ∀X . ξ def = ¬∃X . ¬ξ. For a constant n ∈ N, we define: X = {y 1 , . . . , y n } ⇐⇒ ∀x . X(x) ↔ n i=1 x = y i (12)
||X|| ≥ n ⇐⇒ ∃y 1 . . . ∃y n .

1≤i<j≤n

y i = y j ∧ n i=1 X(y i ) (13)
||X|| = n ⇐⇒ ||X|| ≥ n ∧ ¬||X|| ≥ n + 1 (14)
The variables of a WSκS formula are interpreted by a store ν :

X 1 ∪ X 2 → [1, κ] * ∪ 2 [1,κ] * , such that ν(x) ∈ [1, κ] * , for each x ∈ X 1 and ν(X) ⊆ [1, κ] * is a finite set, for each X ∈ X 2 .
The terms of WSκS are interpreted inductively, as ν( ) def = and ν(τ.i) def = ν(τ ) • i. We denote by |= ν wsks ξ the fact that the WSκS formula ξ is valid for the valuation ν. This relation defined below, by induction on the structure of the formulae:

|= ν wsks τ 1 = τ 2 ⇐⇒ ν(τ 1 ) = ν(τ 2 ) |= ν wsks X(τ ) ⇐⇒ ν(τ ) ∈ ν(X) |= ν wsks ξ 1 ∧ ξ 2 ⇐⇒ |= ν wsks ξ 1 and |= ν wsks ξ 2 |= ν wsks ¬ξ ⇐⇒ not |= ν wsks ξ |= ν wsks ∃x . ξ ⇐⇒ |= ν[x←w] wsks ξ, for some node w ∈ [1, κ] * |= ν wsks ∃X . ξ ⇐⇒ |= ν[X←S] wsks ξ, for some finite set S ⊆ [1, κ] *
A WSκS formula ξ is satisfiable if and only if there exists a store ν, such that |= ν wsks ξ. Such a store is said to be a model of ξ. Note that, because we have assumed the successor functions .i to be total, for all i ∈ [1, κ], formulae defining infinite sets, such as e.g. ∀x . X(x) → X(x.1), are unsatisfiable, under the interpretation of second-order variables as finite sets.

Rewriting Trees and Configurations

We begin by building a WSκS formula that describes an infinite κ-ary tree, whose finite prefix is a rewriting tree T ∈ T(φ), for a CL formula φ. Let ∆ = {ρ 1 , . . . , ρ P } be a fixed SID in the following, such that ρ 1 is the rule that labels the root of T , by convention. We use a designated tuple of second order variables R = R 1 , . . . , R P , where each variable R i is interpreted as the set of tree nodes labeled with the rule ρ i in some rewriting tree, for all i ∈ [1, P ].

With this convention, the RewrTree ∆ (R) formula (Figure 6) defines rewriting trees:

• line [START_REF] Henriksen | Mona: Monadic second-order logic in practice[END_REF] states that the sets that interpret the second-order variables R are pairwise disjoint and that R 1 is a singleton containing the root of the rewriting tree,

• line [START_REF] Bojańczyk | Tree-walking automata[END_REF] states that the union of the sets R is prefix-closed, i.e. the parent of each node from the interpretation of a variable R i belongs to the interpretation of some variable R j , for i, j ∈ [1, P ],

• lines ( 17) and ( 18) encode the conditions 1 and 2 of Def. 6, respectively, i.e. for that every predicate atom A (y 1 , . . . , y #(A ) ) from a rule that labels a node w in the rewriting tree there is exactly one child of that node, labeled with a rule A (x 1 , . . . , x #(A ) ) ← ψ and w has no other children.

It is not very hard to show that, for each model ν of RewrTree ∆ (R) there exists a unique rewriting tree, denoted by T R ν , such that nodes(T

R ν ) = P i=1 ν(R i ) and T R ν (w) = ρ i ⇐⇒ w ∈ ν(R i ), for all i ∈ [1, P ] and w ∈ nodes(T R ν ).
As discussed in §5, a rewriting tree T defines a canonical configuration (α T , m T ), where α T is the architecture consisting of the components and interactions corresponding to the atoms of F(T ) and m T is a marking of the Petri

RewrTree ∆ (R) def = ∀x . 1≤i<j≤P ¬R i (x) ∨ ¬R j (x) ∧ R 1 (x) ↔ x = ∧ (15)
∀x .

P i=1 κ =1 R i (x. ) → P j=1 R j (x) ∧ (16)
∀x .

i:ρi=(A(x1,...,x #(A) )←ϕ)

# pred (ϕ) j=1 R i (x) → j:pred j (ϕ)=A (y1,...,y #(A ) ) :ρ =(A (x1,...,x #(A ) )←ψ) R (x.j) ∧ (17)
∀x .

i:ρi=(A(x1,...,x #(A) )←ϕ) In the rest of this section, we consider Σ and β to be fixed and recall that Q β denotes the finite set of states used to describe the behaviors β(C 1 ), . . . , β(C N ). Our next concern is defining the precise markings of N(Σ, α T , β) (Def. 2) by a WSκS formula. We define sets of places of N(Σ, α T , β) by means of a tuple of second-order variables X def = X q | q ∈ Q β . Any valuation ν of the variables X corresponds to a set of places σ X ν def = {q[u] | u ∈ ν(X q )}. When needed, we shall use distinct copies of X, such as

κ j=# pred (ϕ)+1 R i (x) → P =1 ¬R (x.j) (18)
X def = X q | q ∈ Q β , Y def = Y q | q ∈ Q β and Z def = Z q | q ∈ Q β .
The WSκS formula below defines the precise markings of a Petri net N(Σ, α T , β), assuming that T is the rewriting tree corresponding to some model of RewrTree ∆ (R):

m(X, R) def = ∀x . N i=1 q =q ∈states β (Ci) ¬X q (x) ∨ ¬X q (x) ∧ (19)
q∈states β (Ci)

X q (x) ↔ ρj ∈inst(Ci) R j (x) (20)
Intuitively, line [START_REF] German | Reasoning about systems with many processes[END_REF] above states that a component of type C i may not be in two different states from states β (C i ), and line [START_REF] Browne | Reasoning about networks with many identical finite state processes[END_REF] states that the index of a component of type C i must be a node of the rewriting tree labeled with a rule in which a component atom of the form C q i (x) occurs (see Assumption 2 on the syntax of the rules labeling a rewriting tree). We write inst(C) for the subset of ∆ consisting of those rules that contain a component atom of the form C q (x). The correctness of the encoding is stated and proved below: Lemma 6. For any model ν of RewrTree ∆ (R)∧m(X, R), the set σ X ν is a precise marking of the Petri net N(Σ, α T R ν , β). Proof. Let C ∈ C be a component type and u ∈ α T R ν (C) be an index. We prove that ||σ X ν ∩ {q[u] | q ∈ states β (C)}|| = 1, by proving the following points:

• σ X ν ∩ {q[u] | q ∈ states β (C)} = ∅: since |= ν wsks RewrTree ∆ (R), we have that T R
ν is a rewriting tree, such that nodes(T R ν ) = P i=1 ν(R i ) and ν(R i ) is the set of nodes of T R ν that are labeled with the rule ρ i , for all i ∈

[1, P ]. Since u ∈ α T R ν (C) ⊆ nodes(T R ν )
, there exists a rule ρ i , such that C ∈ inst(ρ i ) and u ∈ ν(R i ), hence by line [START_REF] Browne | Reasoning about networks with many identical finite state processes[END_REF], we have u ∈ ν(X q ), i.e. q[u] ∈ σ X ν , for some q ∈ states β (C). Consequently,

q[u] ∈ σ X ν ∩ {q[u] | q ∈ states β (C)}. • ||σ X ν ∩ {q[u] | q ∈ states β (C)}|| < 2: suppose that q[u], q [u] ∈ σ X
ν , for q = q ∈ states β (C). Hence u ∈ ν(X q ) ∩ ν(X q ), which contradicts line [START_REF] German | Reasoning about systems with many processes[END_REF] and the fact that |= ν wsks m(X, R).

Path Automata

The next step in building WSκS verification conditions that are sufficient for proving deadlock freedom and unreachability of several control states at once ( §4) is tracking the variables that occur in a rule labeling a node of a rewriting tree T , down to the component atoms which set their values, in the canonical architecture α T . These values are used to define the interactions of α T and, in particular, to encode the pre-set ( • t) and post-set (t • ) of a transition (t) from the Petri net N(Σ, α T , β), by a flow formula, described next ( §6.4).

As briefly mentioned (see Example 8) a variable "traverses" the rewriting tree of a given formula downwards, while replacing the formal parameters of the rule labeling the child. This traversal is described by a special type of tree automaton, that walks down the tree, following the identity of the tracked variable. These automata are a restricted version of tree walking automata [START_REF] Bojańczyk | Tree-walking automata[END_REF].

A path in a tree T is a sequence n 1 , . . . , n ∈ nodes(T ), such that n i+1 is a child of n i , for all i ∈ A path automaton A = ({s 1 , . . . , s L }, I, F, δ) corresponds, in the sense of Lemma 7 below, to the formula in Figure 7, which is, moreover, built directly from the syntactic description of A. Here Y = Y 1 , . . . , Y L are second order variables interpreted as the sets of tree nodes labeled by the automaton with the states s 1 , . . . , s L , respectively. Intuitively, the first three conjuncts of the above formula (line 21) encode the facts that Y are disjoint (no tree node is labeled by wsks ∃Y . ∆ A (x, y, Y) . Our purpose is to infer, directly from the syntax of the rules in ∆, path automata that recognize the path between the node where a variable is introduced (either as a formal parameter of a rule or by an existential quantifier) and the node where the variable is instantiated, in each given rewriting tree.

∆ A (x, y, Y) def = 1≤i =j≤L ∀z. ¬Y i (z) ∨ ¬Y j (z) ∧ si∈I Y i (x) ∧ sj ∈F Y j (y) (21) ∧ L i=1 ∀z . z = y ∧ Y i (z) → j:si d -→sj Y j (z.d) ∨ j:si d -→sj ∃z . z .d = z ∧ Y j (z ) (22)
∧ L j=1 ∀z . z = x ∧ Y j (z) → i:si d -→sj ∃z . z .d = z ∧ Y i (z ) ∨ i:si d -→sj Y i (z.d) (23)
Formally, for each rule ρ = (A(x 1 , . . . , x #A ) ← ∃y 1 . . . ∃y m . ψ), such that ψ is a quantifie-free formula, and each variable x ∈ fv(ψ), we consider the path automaton A x ρ = (S, I, F, δ), where:

• S def = {s z ρ | ρ = (A (x 1 , . . . , x #A ) ← ∃y 1 .
. . ∃y m .φ) , φ is q.f., z ∈ fv(φ)}; the intuition is that the automaton visits the state s z ρ while tracking variable z in the body of the rule ρ , that labels the node of the rewriting tree which is currently visited by the automaton,

• the initial and final states are

I def = {s x ρ } and F def = {s z ρ | ρ = A (x 1 , . . . , x #A ) ← ∃y 1 .
. . ∃y m . C q (z) * φ , φ is q.f., C ∈ C, q ∈ states β (C)}; the automaton starts to track x in ρ and moves down in the rewriting tree, finally tracking a variable z that occurs in a component atom in ρ ,

= A (x 1 , . . . , x #(A ) ) ← ϕ from ∆, all directions d ∈ [1, # pred (ϕ)],
such that pred d (ϕ) = A (y 1 , . . . , y #(A ) ), and all j ∈ [1, #(A )]; if ρ labels the parent of the node labeled by ρ in the rewriting tree, the automaton moves down one step, from tracking y j in ρ to tracking x j in ρ .

Example 9. The path automata recognizing the paths to component atoms, for the variables 1 and r 1 in the rewriting tree from Example 6 are depicted in Figure 8. The initial states are s 1 7 and s r1 7 , respectively, and the final state is s n 10 for both automata. The rule labels are the ones from Example 6.

The lemma below shows that these automata recognize the set of paths corresponding to the recursive substitutions of a given variable down to the node where it occurs in a component atom, in all rewriting trees built using the rules from the given SID: Lemma 8. Given a rule ρ = A(x 1 , . . . , x #(A) ) ← ∃y 1 . . . ∃y m . φ , such that φ is a quantifier-free formula, and a variable x ∈ fv(φ), for each sequence w ∈ [1, κ] * , the following are equivalent:

1. there exists a rewriting tree T and nodes n, m ∈ nodes(T ), such that T (n) = ρ, m = n • w and s T (x) = m (see 11 for the definition of s T ). 2. w ∈ L(A x ρ ).

Proof. (1) ⇒ (2) By the definition of s T , we have s T (x) = s T↓n (x) and s T↓n (x) = m if there exist:

• a sequence of nodes n = n 1 , n 2 , . . . , n p = m ∈ nodes(T ), such that n i+1 = n i • d i , for some d i ∈ [1, κ], for all i ∈ [1, p -1], • a sequence of variables x = z 1 , . . . , z p ∈ X 1 , such that z i replaces z i+1 in the construction of the characteristic formula F(T ), for all i ∈ [1, p -1],
and occurs in a component atom from T (m). By the definition of rewriting trees, each node n i is labeled by a rule ρ i = A i (x 1 , . . . , x #(Ai) ) ← ∃y 1 . . . ∃y m . φ i , where φ i is quantifier-free, and there exists j ∈ [1, #(A i )] such that z i occurs on the j-th position in pred di (φ i ) and z i+1 occurs j-th within the head A i+1 (x 1 , . . . , x #(Ai+1) ) of ρ i+1 . By the definition of A x ρ , there exist transitions s zi The path automata A z ρ are used to define the Path z ρ (x, y, R) formulae below:

Path z ρ (x, y, R) def = ∃Y . ∆ A z ρ (x, y, Y) ∧ Υ(Y, R) Υ(Y, R) def = i:ρi=(A (x1,...,x #(A ) )←ϕ ) z∈fv(ϕ ) ∀x . Y z ρi (x) → R i (x)
The formula Υ(Y, R) above states that all nodes labeled with a state q z ρi during the run must be also labeled with ρ i in the rewriting tree given as input to the path automaton. Here we denote by Y z ρi the second-order variable corresponding to the state q z ρi in a path automaton A x ρ . Intuitively, the formula Path z ρ (x, y, R) states that, in each rewriting tree defined by a model ν of the RewrTree ∆ (R) formula, there exists a path from ν(x) to ν(y), where ν(x) is a node labeled with ρ, in which z occurs free or existentially quantified, and y is the node where a variable necessarily equal to z occurs in a component atom.

Flow Formulae

At this point, we introduce a WSκS formula Φ(X, X , R) that defines the structure of transitions in the Petri net N(Σ, α T R ν , β), where ν is a model of RewrTree ∆ (R). By "structure" here we mean that ν(X) and ν(X ) encode the pre-and post-sets of some transition in N(Σ, α T R ν , β), as explained in §6.2.

Figure 9 shows the flow formula of a given SID, consisting of the rules ρ 1 , . . . , ρ P . We denote by inter (ρ) the set of interaction atoms that occur in the body of a rule ρ. Essentially, the formula ( 24) is split into a disjunction of formulae Ψ ,I(x1,...,x #(I) ) , one for each rule ρ ∈ ∆ and each interaction atom I(x 1 , . . . , x #(I) ) that occurs in the body of ρ . To understand the Ψ ,I(x1,...,x #(I) ) formulae, recall that each of the variables x i is mapped to the (unique) node of the rewriting tree containing an instance atom C q (x), such that x i replaces x in the characterizing formula of the rewriting tree T R ν , provided that ν is a model of RewrTree ∆ (R). In order to find this node, we track the variable x i from the node labeled by the rule ρ, to the node where this instance atom occurs. This is done by the Path xi ρ (y 0 , y i , R) formula [START_REF] Konnov | Parameterized systems in BIP: design and model checking[END_REF], that holds whenever y 0 and y i are respectively mapped to the source and the destination of a path from a node ν(y 0 ) ∈ nodes(T R ν ), with label ρ to a node ν(y i ) ∈ nodes(T R ν ), such that the [1, #(I)]. Then there exists a node w 0 ∈ nodes(T R ν ) and an interaction atom

I(x 1 , . . . , x #(I) ) in T R ν (w 0 ), such that s T R ν (x i ) = w i , for all i ∈ [1, #(I)].
Assume w.l.o.g. that T R ν (w 0 ) = ρ , for some ∈ [1, P ] and let ν = ν[y 0 ← w 0 , . . . , y #(I) ← w #(I) ] be a valuation. We prove the following points:

• |= ν wsks R (y 0 ): since |= ν wsks RewrTree ∆ (R), T R ν (w 0 ) = ρ , ν (y 0 ) = w 0 and ν agrees with ν over R.

) i ) = comp( P(I) j ). • |= ν wsks X q = {y i | i ∈ [1, #(I)], τ i = (q i pi -→ q i ), q i = q}, for all q ∈ Q β : be- cause σ X ν = • t = {q 1 , . . . , q #(I) }. • |= ν wsks X q = {y i | i ∈ [1, #(I)], τ i = (q i pi -→ q i ), q i = q}, for all q ∈ Q β : be- cause σ X ν = t • = {q 1 , . . . , q #(I) } We obtain that |= ν wsks Ψ ,I(x1,...,x #(I)
) and, consequently |= ν wsks Φ(X, X , R).

Structural Invariants

An invariant I of a marked Petri net N = (N, m 0 ), where N = (S, T, E) is a Petri net, is a set of markings that over-approximates the reachable states Reach(N ), that is Reach(N ) ⊆ I ⊆ pow(S). The invariant is, moreover, said to be inductive if and only if it is closed under the transition relation of the Petri net, namely that {m | m ∈ I, t ∈ T, m t -→ m } ⊆ I. The synthesis of inductive invariants is a notoriously difficult problem, that has been received much attention in the past. The most common method of infering inductive invariants is the iteration of an abstract (over-approximation) transition relation in an abstract domain, until a fixpoint is reached. Depending on the complexity of the abstract domain, this approach, known as abstract interpretation [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF], can be quite costly. In contrast, we consider inductive invariants that can be synthesized directly from the structure of a Petri net, without iterating (an abstraction of) its transition relation up to a fixpoint. Such invariants are called structural in the literature [START_REF] Sifakis | Structural properties of Petri nets[END_REF]. The next definition introduces two types of structural invariants: Definition 11. Given a marked Petri net N = (N, m 0 ), where N = (S, T, E), a set of places σ ⊆ S is said to be a:

• trap if ||σ ∩ m 0 || ≥ 1 and, for any t ∈ T , if ||σ ∩ • t|| ≥ 1 then ||σ ∩ t • || ≥ 1, • mutex if ||σ ∩ m 0 || = 1 and, for any t ∈ T , we have ||σ ∩ • t|| = ||σ ∩ t • || ≤ 1.
The trap and mutex invariant of N are the below sets of markings, respectively:

• Θ(N ) def = {m marking of N | ||m ∩ σ|| ≥ 1, for each trap σ of N }, • Ω(N ) def = {m marking of N | ||m ∩ σ|| = 1, for each mutex σ of N }.
By substituting the reachable set with the intersection of the trap and mutex invariant, we obtain the following sufficient queries, that allow to prove the absence of deadlocks and unreachability of a tuple of states in a system described by a CL formula: Lemma 10. Given a tight sentence φ, interpreted over a SID ∆, a behavior map β and a tuple of states q 1 , . . . , q n , the following hold: deadlock (φ, ∆, β) ⇒ deadlock t (φ, ∆, β) reach(φ, q 1 , . . . , q n , ∆, β) ⇒ reach t (φ, q 1 , . . . , q n , ∆, β) where deadlock t (φ, ∆, β) and reach t (φ, q 1 , . . . , q n , ∆, β) are defined below:

• deadlock t (φ, ∆, β): does there exist a rewriting tree T ∈ T(φ), such that Θ(N(Σ, α T , β), m T ) ∩ Ω(N(Σ, α T , β), m T ) ∩ Dead (N(Σ, α T , β)) = ∅?

• reach t (φ, q 1 , . . . , q n , ∆, β): does there exist a rewriting tree T ∈ T(φ Given a CL sentence φ that describes the set of initial configurations of a system, Figure 10 introduces WSκS formulae that define the trap and mutex invariants of the marked Petri nets (N(Σ, α T , β), m 0 ), where T ∈ T(φ) are rewriting trees and (α T , m 0 ) |= φ are initial configurations. This construction uses the flow formula (Figure 9) derived from the SID that interprets the predicate symbols from φ and the behavior map β of the system. Here we denote by X (resp. m, with q 1 [u 1 ], . . . , q n [u n ] pairwise distinct coincides with the set {σ X ν | |= ν wsks ErrSet q1,...,qn (X) ∧ m(X, R) ∧ RewrTree ∆ (R)}.

Since the WSκS logic is decidable with non-elementary complexity, in general [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of second-order logic[END_REF], the problem of checking the satisfiability of the verification conditions provided by Theorem 3 is decidable. By inspection of the formulae (1) and ( 2), one can show that checking the verification conditions is in 4EXPTIME, where 4 is the maximum quantifier alternation depth of these formulae. In practice, however, these checks are quite fast, as shown by the preliminary experiments performed on a similar encoding, reported in our previous work [START_REF] Bozga | Specification and safety verification of parametric hierarchical distributed systems[END_REF].

Related Work

This paper reports on a resource logic for the specification of sets of configurations of parametric distributed systems with unbounded numbers of components (processes) and a verification method for safety properties, such as absence of deadlocks and critical section violations.

Traditionally, verification of unbounded networks of parallel processes considers known architectural patterns, typically cliques or rings [START_REF] German | Reasoning about systems with many processes[END_REF][START_REF] Browne | Reasoning about networks with many identical finite state processes[END_REF]. Because the price for decidability is drastic restriction on architecture styles [START_REF] Bloem | Decidability of Parameterized Verification[END_REF], more recent works propose practical semi-algorithms, e.g. regular model checking [START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF][START_REF] Abdulla | Regular model checking without transducers (on efficient verification of parameterized systems)[END_REF] or automata learning [START_REF] Chen | Learning to prove safety over parameterised concurrent systems[END_REF]. Here the architectural pattern is implicitly determined by the class of language recognizers: word automata encode pipelines or rings, whereas tree automata describe trees.

A first attempt at specifying architectures by logic is the interaction logic of Konnov et al. [START_REF] Konnov | Parameterized systems in BIP: design and model checking[END_REF], which is a combination of Presburger arithmetic with monadic uninterpreted function symbols, that can describe cliques, stars and rings. More structured architectures (pipelines and trees) can be described using a second-order extension [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]. As such, these interaction logics are undecidable and have no support for automated verification. Recently, interaction logics that support the verification of safety properties, by structural invariant synthesis have been developed. These logics use fragments of first order logic with interpreted function symbols that implicitly determine the class of architectures, such as cliques [START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF], or pipelines, rings and trees [START_REF] Bozga | Structural invariants for the verification of systems with parameterized architectures[END_REF].

From a theoretical point of view, our resource logic with inductive definitions is strictly more expressive: for instance, a chain of components where a certain component type occurs on all even (odd) positions is provably not expressible in first order logic, but can be easily defined using our language, whose inductive definitions allow to describe second order constructs in a controlled manner (rather than using unrestricted second order quantification, as in [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]). Moreover, first order logic with successor functions can describe at most tree-like architectures, whereas our language describes structures more general than trees6 , using no interpreted function symbols, other than ports involved in interactions [START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF][START_REF] Bozga | Structural invariants for the verification of systems with parameterized architectures[END_REF]. Specifying parameterized component-based systems by inductive definitions is, however, not new. Network grammars [START_REF] Shtadler | Network grammars, communication behaviors and automatic verification[END_REF] use context-free grammar rules to describe systems with linear (pipeline, token-ring) architectures obtained by composition of an unbounded number of processes. In contrast, we use predicate symbols of unrestricted arities to describe architectural patterns that are, in general, more complex than trees. Such complex structures can be specified recursively using graph grammar rules with parameter variables [START_REF] Metayer | Describing software architecture styles using graph grammars[END_REF][START_REF] Hirsch | Graph grammars and constraint solving for software architecture styles[END_REF]. To avoid clashes, these variables must be renamed to unique names and assigned unique indices at each unfolding step. Our specifications use quantifiers to avoid name clashes and separating conjunction to guarantee that the components and interactions obtained by the unfolding of the rules are unique.

Verification of network grammars against safety properties requires the synthesis of network invariants [START_REF] Wolper | Verifying properties of large sets of processes with network invariants[END_REF], computed by rather costly fixpoint iterations [START_REF] Lesens | Automatic verification of parameterized linear networks of processes[END_REF] or by abstracting (forgetting the particular values of indices in) the composition of a small bounded number of instances [START_REF] Kesten | Network invariants in action[END_REF]. Instead, our method uses lightweight structural invariants, that are synthesized with little computational effort and prove to be efficient in many practical examples [START_REF] Bozga | Structural invariants for the verification of systems with parameterized architectures[END_REF][START_REF] Bozga | Specification and safety verification of parametric hierarchical distributed systems[END_REF].

Conclusions and Future Work

The paper proposes a general framework for the practical semi-algorithmic verification of parametric systems. The framework integrates previous work of the authors and extends it through developments in two complementary directions. The first direction is modeling parametric system architectures from instances of predefined component types and interaction types. Configuration logic allows the specification of configurations characterizing architecture styles with snapshots of their component states. Parametric system behavior can be obtained, in the form of Petri nets using operational semantics, from given configuration logic specifications and behaviors of component types. We show that even for very simple linear architectures, essential safety properties such as deadlock-freedom or mutual explosion are undecidable.

The second direction proposes a method that from given configuration logic specifications and the finite-state behavior of its components, leads to formulas of WSκS characterizing two types of structural invariants used to prove deadlock-freedom and mutual exclusion properties. The generation process avoids the complexity of traditional fixpoint computation techniques. It synthesizes constraints on the state space induced by the interactions of the parametric architecture. Verification boils down to checking the satisfiability of WSκS formulae, for which optimized solvers exist. The whole generation process involves transformations from configuration specifications into rewriting trees and then into WSκS through path automata. Proving its soundness requires some tedious technical developments; nonetheless, its implementation does not suffer from the usual limitations due to state space complexity and the number of components. Experimental results show that the proposed verification method is scalable and allows proving safety in a number of non-trivial cases [START_REF] Bozga | Specification and safety verification of parametric hierarchical distributed systems[END_REF].

1 Figure 1 :

 11 Figure 1: Recursive Specification of a Token-Ring System

Figure 2 :

 2 Figure 2: The Synthesis of Verification Conditions

  a finite set of relation symbols of arity one, called component types, • I = {I 1 , . . . , I M } is a finite set of relation symbols of arity #(I j ) ≥ 1, called interaction types, • P : C ∪ I → pow(P) ∪ i≥1 P i is an interface associating each component type C ∈ C a finite set of ports P(C) ∈ pow(P) and each interaction type I ∈ I a finite tuple of ports P(I) ∈ P #(I) .

  Example 3 (contd. from Example 1). The behavior of the component type S in Figure 1a is described by the state machine β(S) = ({t, n}, {in, out}, -→), with transitions n in -→ t and t out --→ n.

  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. 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 and t ∈ T . A 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 t1 -→ m 1 . . . m n-1 tn -→ m . A marking m is a deadlock of a Petri net N = (S, T, E) if and only if no transition t ∈ T is enabled in m and let Dead (N) denote the set of deadlocks of N.

Figure 3 :

 3 Figure 3: The Execution Semantics of a Token-Ring System

Figure 4 :

 4 Figure 4: Undecidability of Deadlock and Reachability for Linear Component-based Systems

445 4 . 3 .

 43 Proof of Theorem 1

2 , l 2 , r 2 )Figure 5 :

 2225 Figure 5: Trees with Leaves Linked in a Token Ring

  ), I(x 1 , . . . , x #(I) )}: we define T by nodes(T ) def = { } and T ( ) def = A(x 1 , . . . , x #(A) ) ← φ . By Def. 6, we have T ∈ T(φ) and

ure 5 (

 5 a) is given below:

Definition 9 .

 9 An architecture α is tight if and only if, for each interaction I[u 1 , . . . , u #(I) ] from α and each k ∈ [1, #(I)], we have u k ∈ α(C) where C = comp( P(I) k )), that is, the unique component type such that P(I) k ∈ P(C).

"⊇" Let u 1

 1 , . . . , u #(I) ∈ α 1 (I), such that comp( P(I) k ) = C i k , for all k ∈ [1, #(I)]. Then there exists an interaction atom I(x 1 , . . . , x #(I) ) in η, such that u k = s 1 (x k ), for all k ∈ [1, #(I)]. Since φ is a tight sentence and (α 1 , m 1 ) |= φ, by Lemma 4, the architecture α 1 is tight, thus s 1

Figure 6 :

 6 Figure 6: Rewriting Trees

[ 1 ,

 1 -1]. If m is a descendant of n, we denote by π(n, m) the unique path starting in n and ending in m. Note that π(n, m) is determined by n and the sequence of directions d 1 , . . . , d p ∈ [1, κ], such that m = n•d 1 •. . .•d p . A path automaton is a tuple A = (S, I, F, δ), where S is a set of states, I, F ⊆ S are the sets of initial and final states, respectively, and δ ⊆ S × [1, κ] × S is a set of transitions s d -→ s , where s, s ∈ S are states and d ∈ [1, κ] is a direction. A run of A over the path π(n, m), where m = n • d 1 • . . . • d p , is a sequence of states s 1 , . . . , s p+1 ∈ S, such that s 1 ∈ I and s i di -→ s i+1 , for all i ∈ [1, p]. The run is accepting if and ony if s p+1 ∈ F . The language L(A) of A is the set of paths in T over which A has an accepting run.

Figure 7 :Lemma 7 .

 77 Figure 7: Definition of the Path Automaton formula ∆ A (x, y, Y)

9 Figure 8 : 6 •

 986 Figure 8: Path Automata Recognizing the Paths to Component Atoms from Example 6

  all i ∈ [1, p -1]. Moreover, s x ρ = s z1 ρ1 and s zp ρp are initial state and final states of A x ρ , respectively. Since m = n • d 1 . . . d p = n • w, we obtain that w = d 1 . . . d p ∈ L(A x ρ ). (2) ⇒ (1) Let w = d 1 . . . d p , where d 1 , . . . , d p ∈ [1, κ], and s zi ρi di -→ s zi+1 ρi+1 , for all i ∈ [1, p -1], be transitions of A x ρ , such that s z1 ρ1 = s x ρ is the initial state and s zp ρp is a final state of A x ρ . Then, by the definition of A x ρ , the nodes w i def = n • d 1 . . . d i are labeled by rules ρ i def = A i (x 1 , . . . , x #(Ai) ) ← ϕ i , such that z i occurs in pred di (ϕ i ) on the same position as z i+1 , which occurs in A i+1 (x 1 , . . . , x #(Ai+1) ). Then, there exists a rewriting tree T and nodes n, m ∈ nodes(T ), such that m = n • d 1 . . . d o and A x ρ has an accepting run over d 1 . . . d p . By the definition of s T , we have s T (x) = s T↓n (x) = m.

  ) and a configuration (α T , m) ∈ Θ(N(Σ, α T , β), m T ) ∩ Ω(N(Σ, α T , β), m T ), such that {qi [u i ] | i ∈ [1, n]} ⊆ m, with q 1 [u 1 ], . . . , q n [u n ] pairwise distinct?Proof. We show first that the trap Θ(N ) and mutex Ω(N ) invariants of a marked Petri net N are invariants of N . If m 0 = ∅ then N has no traps nor mutexes and Reach(N ) = Θ(N ) = Ω(N ) = ∅, thus Θ(N ) and Ω(N ) are trivially inductive invariants. So we assume m 0 = ∅.For the set Θ(N ), let σ be an arbitrary trap of N . Since m 0 = ∅, we have||σ ∩ m 0 || ≥ 1, hence m 0 ∈ Θ(N ),by the choice of σ. For each pair of markings m and m , such that m ∈ Θ(N ) and m t -→ m , for some transition t ∈ T , we have m = (m \ • t) ∪ t • . If σ ∩ • t = ∅ then ||m ∩ σ|| ≥ ||m ∩ σ|| and ||m ∩ σ|| ≥ 1, because m ∈ Θ(N ). Otherwise, ||σ ∩ • t|| ≥ 1, thus ||σ ∩ t • || ≥ 1 because σ is a trap of N , hence ||m ∩ σ|| ≥ 1. In both cases, we obtain that ||m ∩ σ|| ≥ 1, hence m ∈ Θ(N ), because σ is an arbitrary trap of N . A similar argument shows that Ω(N ) is an inductive invariant of N . Let σ be an arbitrary mutex of N . Then ||σ ∩ m 0 || = 1, hence m 0 ∈ Ω(N ), by the choice of σ. For each pair of markings m and m , such that m ∈ Θ(N ) and m t -→ m , for some transition t ∈ T , we have m = (m \ • t) ∪ t • and ||σ ∩ • t|| = ||σ ∩ t • || ≤ 1, hence ||m ∩ σ|| = 1 and m ∈ Ω(N ), because σ is an arbitrary mutex of N . Moreover, since inductive invariants are closed under intersection, the set Θ(N ) ∩ Ω(N ) is also an inductive invariant of N . Finally, because Reach(N ) is known to be the least inductive invariant of N , we obtain Reach(N ) ⊆ Θ(N ) ∩ Ω(N ). The rest of the proof follows from Theorem 2 and the above fact.

  1 [u] and C 2 [u] belonging to different component types and similarly, a tuple of indices u can refer two (or more) different interactions I 1 [u] and I 2 [u] of different interaction types, with the same arity; interactions may occur disconnected from components, e.g. I[u 1 , . . . , u #(I) ] does not necessarily mean that each component comp( P(I) i )[u i ], for all i ∈ [1, #(I)] is present in the structure.Example 2 (contd. from Example 1). Letting indices be natural numbers, the structure of Figure1ais described by the architecture α over Σ, such that α

Table 1 :

 1 The behavior β

	(γ1, )
	P T

M of C P T for a Post-Turing machine executing a program M Word w (x, y) ← ∃z 2 . . . ∃z n-1 . C

  Since φ is a tight sentence and (α 2 , m 2 ) |= φ, by Lemma 4, the architecture α 2 is tight (Def. 9). Then, for each k ∈ [1, #(I)], we have u k ∈ α 2 (C i k ), where C i k ∈ C is the unique component type such that P(I) k ∈ P(C i k ). By the previous point, there exists

  • |= ν wsks Path xi ρ (y 0 , y i , R), for all i ∈ [1, #(I)]: since s T R ν (x i ) = w i , we obtain π(w 0 , w i ) ∈ L(A xi ρ ) by Lemma 8 and |= ν wsks Path xi ρ (y 0 , y i , R) follows, by Lemma 7. • |= ν wsks y i = y j , for all 1 ≤ i < j ≤ #(I), such that comp( P(I) i ) = comp( P(I) j ): by Def. 1, w i = w j for all i, j ∈ [1, #(I)], such that comp( P(I

Boolean Petri nets are sometimes called 1-safe or 1-bounded in the literature.

Typically, global permutations suffice when only one component type is considered.

For instance, the tree-shaped architecture with leaves linked in a ring §5.

As future work, we plan on adding support for broadcast in our specification language and develop further the invariant synthesis method to take broadcast into account. We also envisage an extension of the finite-state model of behavior to more complex automata, such as pushdown or timed automata.

Ψ ,I(x1,...,x #(I) ) (X, X , R)

Ψ ,I(x1,...,x #(I) ) (X, X , R) def = ∃y 0 . . . ∃y #(I) . R (y 0 ) ∧ #(I)

Path xi ρ (y 0 , y i , R)∧ [START_REF] Konnov | Parameterized systems in BIP: design and model checking[END_REF] τ1,...,τ #(I) ∈T β (I) q∈Q β X q = {y i | i ∈ [1, #(I)], τ i = (q i pi -→ q i ), q i = q}∧ (26)

1≤i<j≤#(I) y i = y j ∨ comp( P(I) i ) = comp( P(I) j ) [START_REF] Bozga | Structural invariants for the verification of systems with parameterized architectures[END_REF] Figure 9: The Flow Formula component atom that gives the value of x i 5 occurs in T R ν (ν(y i )). Hence, x i is interpreted as ν(y i ) in the canonical model of the characteristic formula of T R ν .

The correctness of the encoding is formalized and proved by the following:

Lemma 9. Given a model ν of RewrTree ∆ (R), we have |= ν wsks Φ(X, X , R) if and only if σ X ν = • t and σ X ν = t • , for some transition t of N(Σ, α T R ν , β). Proof. "⇒" If |= ν wsks Φ(X, X , R) then there exists a rule ρ ∈ ∆ = {ρ 1 , . . . , ρ N } and I(x 1 , . . . , x #(I) ) ∈ inter (ρ ), such that |= ν wsks Ψ ,I(x1,...,x #(I) ) (X, X , R). Then, there exist nodes w 0 , . . . , w n ∈ nodes(T R ν ), such that ν(y i ) = w i , for all i ∈ [0, n] and let ν = ν[y 0 ← w 0 , . . . , y n ← w n ]. Since, moreover, |= ν wsks R (y 0 ), we obtain that T R ν (w 0 ) = ρ , hence the variables x 1 , . . . , x #(I) occur in the body of the rule ρ and are assigned to the unique nodes w 1 , . . . , w #(I) ∈ nodes(T R ν ), for which π(w 0 , w i ) ∈ L(A xi ρ ), for all i ∈ [1, #(I)], by Lemma 8. Since |= ν wsks Path xi ρ (y 0 , y i , R), by Lemma 7, we obtain π(w 0 , w i ) ∈ L(A xi ρ ), thus w i = w i , for all i ∈ [1, #(I)], by the uniqueness of these nodes. Let τ 1 , . . . , τ #(I) be a tuple of transitions from T β (I) synchronizing by I. Since |= ν wsks Ψ ,I(x1,...,x #(I) ) (X, X , R), we have w i = w j , for each 1 ≤ i < j ≤ #(I), such that comp( P(I) i ) = comp( P(I) j ). By Def. 1, we have that t = (I[w 1 , . . . , w

"⇐" Let t = (I[w 1 , . . . , w #(I) ], τ 1 , . . . , τ #(I) ) be a transition of N(Σ, α T R ν , β), where τ i = q i P(I) i ----→ q i is a transition of β(comp( P(I) i )), for each i ∈ 5 In the canonical store s T R ν , see §5.2 for its definition. Y and Z) the tuple of second-order variables

, where the definitions of set union and intersection are standard in MSO and omitted to avoid clutter.

Let ν be a model of RewrTree ∆ (R), meaning that T R ν is a rewriting tree for φ. We recall that, by letting ρ 1 def = (A φ () ← φ) be the first rule in the SID, we capture the fact that T R ν ∈ T(φ), for each model ν of RewrTree ∆ (R) (see the second conjunct in line 15 from Figure 6). The formula Init(Y, R) (29) encodes the fact that σ Y ν is an initial marking of the Petri net N(Σ, α T R ν , β) namely, that each node of the rewriting tree T R ν is the index of a component of type C in state q, if C q (z) occurs in the rule that labels the node.

We assume further that ν is a model of RewrTree ∆ (R) ∧ Init(Y, R). The formulae θ(X, R) (30) and Θ(X, Y, R) (31) define the traps and the trap invariant of the marked Petri net (N(Σ, α T R ν , β), σ Y ν ), respectively. Similarly, ω(X, R) [START_REF] Wolper | Verifying properties of large sets of processes with network invariants[END_REF] and Ω(X, R) (33) define the mutexes and the mutex invariant of (N(Σ, α T R ν , β), σ Y ν ), respectively. We intentionally use the same symbols to denote trap (mutex) invariants and their defining WSκS formulae, the distinction between sets of markings and formulae being clear from the context. The following lemma shows the correctness of the definitions from Figure 10:

We give the proof for point (1), the proof for (2) uses a similar argument and is left for the reader.

) be a marking and ν be a valuation such that σ X ν = m and ν agrees with ν over Y and R. Clearly, such a valuation exists and, in order to show that m ∈ {σ

and we are left with proving |= ν wsks ∀Z . θ(Z, R) ∧ ||Y ∩ Z|| ≥ 1 → ||X ∩ Z|| ≥ 1. To this end, let µ be any valuation that agrees with ν over X, Y and R, such that

) and σ X µ = m. Note that, since µ agrees with ν over X, we also have σ

µ is a trap of the marked Petri net (N(Σ, α T R ν , β), σ Y ν ), which concludes this direction of the proof. "⊇" Let ν be a valuation that agrees with ν over Y and R, such that |=

Let θ be such a trap and let µ be a valuation that agrees with ν over X, Y and R, such

which concludes this direction of the proof.

Verification Conditions

The final step in generating sufficient verification conditions for the deadlock and reachability problems ( §4) is the encoding of the sets of error configurations in WSκS. This is done separately, for the two kinds of errors considered, by the formulae in Figure 11. The convention here is to use X to represent the configurations in the error sets. However, none of the formulae from Figure 11 constrains X to be a marking, i.e. by conjunction with m(X), since the latter formula is already included in the definition of the structural invariants, by the formulae Θ(X, Y, R) and Ω(X, Y, R) (Figure 10).

We recall that a marking m is a deadlock of a Petri net N = (S, T, E) if and only if • t ⊆ m, for all transitions t ∈ T (if • t ⊆ m for some transition t, then that transition could be fired from m). This condition is captured by the DeadLock (X, R) formula [START_REF] Kesten | Network invariants in action[END_REF], where Φ(Y, Z, R) is the flow formula that defines the pre-and post-sets, for some transition in the Petri net N(Σ, α T R ν , β), where ν is a model of RewrTree ∆ (R) (Lemma 9). Here we write Y ⊆ X as a shorthand for ∀x . q∈Q β Y q (x) → X q (x), denoting the fact that the set of places defined by Y is included in the one defined by X.

ErrSet q1,...,qn (X) The set defined by the ErrSet q1,...,qn (X) formula (35) captures the fact that each configuration encoded by X contains pairwise distinct places q 1 [w 1 ], . . ., q n [w n ] which is, essentially, the condition required by a reachability query. Note that, because the tuple of states q 1 , . . . , q n is part of the input of the query, the number ||{i ∈ [1, k] | q i = q}|| of occurrences of each state q in the tuple is constant, hence the cardinality of each set X q is compared to a constant [START_REF] Emerson | Symmetry and model checking[END_REF].

The following theorem states the soundness of the verification conditions built throughout this section: Theorem 3. Given a tight sentence φ, interpreted over a SID ∆, a behavior map β and a tuple of states q 1 , . . . , q n , the following hold:

is unsatisfiable only if deadlock (φ, ∆, β) has a negative answer.

ErrSet

is unsatisfiable only if reach(φ, q 1 , . . . , q n , ∆, β) has a negative answer. (2) The proof of this point follows a similar argument as for point 1, the only difference being that the set of markings containing a set {q i [u i ] | i ∈ [1, n]} ⊆