Denys Dutykh
email: denys.dutykh@univ-savoie.fr

Elena Tobisch
email: elena.tobisch@jku.aturl

RESONANCE ENHANCEMENT BY SUITABLY CHOSEN FREQUENCY DETUNING

Keywords: nonlinear resonance, frequency detuning, 3-wave system, resonance enhancement MSC: [2010]37N10 (primary), 37N05, 76B65 (secondary) PACS: 05.45.-a, 92.10.hf

In this Letter we report new effects of resonance detuning on various dynamical parameters of a generic 3-wave system. Namely, for suitably chosen values of detuning the variation range of amplitudes can be significantly wider than for exact resonance. Moreover, the range of energy variation is not symmetric with respect to the sign of the detuning. Finally, the period of the energy oscillation exhibits non-monotonic dependency on the magnitude of detuning. These results have important theoretical implications where nonlinear resonance analysis is involved, such as geophysics, plasma physics, fluid dynamics. Numerous practical applications are envisageable e.g. in energy harvesting systems.

Introduction

Numerous natural phenomena exhibit linear and nonlinear resonances. In many technical cases occurrence of resonance must to be avoided, the widely known Tacoma Bridge dramatic collapse being an example for this. In other cases, the goal is to approach the state of exact resonance, by reducing resonance detuning, in order to increase the efficiency of a process or device. To give a notion of linear resonance, we consider a linear oscillator (or pendulum) driven by a small force. We say, that the resonance occurs, if the eigenfrequency ω of a system coincides with the frequency of the driving force Ω. In this case, for small enough resonance detuning, Ω-ω > 0, the amplitude of the linear oscillator becomes smaller with increasing detuning.

The simplest case of nonlinear resonance is a set of 3 waves A j e i(k j x j -ω j t) fulfilling resonance conditions of the following form

ω 1 ± ω 2 ± ω 3 = 0, (1.1
)

k 1 ± k 2 ± k 3 = 0, (1.2)
where k j ∈ Z 2 , ω j = ω(k j ) are the wave vectors and frequencies respectively. Drawn from these resonance conditions, resonance detuning in the nonlinear case can be defined in a number of ways, e.g. as a frequency detuning or phase detuning.

In the physical literature, for frequency detuning defined as

ω 1 + ω 2 -ω 3 = ∆ω ≪ min j=1,2,3 {ω j },
the assumption prevails, that bigger detuning results in smaller variation of amplitudes, e.g. [START_REF] Craik | Wave Interactions and Fluid Flows[END_REF]. Quite consistently the study of phase detuning in (1.2) in a 3-wave system demonstrated that the variation range of wave amplitudes becomes smaller with growing dynamical phase [START_REF] Bustamante | Effect of the dynamical phases on the nonlinear amplitudes' evolution[END_REF].

In this Letter we study the effects of frequency detuning in (1.1) by means of the numerical simulation. As an example we take a resonant triad of atmospheric planetary waves from [START_REF] Kartashova | Model of Intraseasonal Oscillations in Earth's Atmosphere[END_REF]. Our numerical simulations show that the detuned system behaviour was correctly understood for ∆ω ≫ δ > 0. However, there exists a transitional range of the detuning magnitude ∆ω where the dynamics of this system is much more complicated. As our results depend only on the general form of the dynamical system given below, they are applicable to a wide class of physical systems.

Model equations

The dynamical system for detuned resonance of three complex-valued amplitudes A i , i = 1, 2, 3 reads (and their complex conjugate equations) where the dot denotes differentiation with respect to the slow time T = t ε, ∆ω ∶= ∆ω ε, ε being a small parameter. The dynamical system for exact resonance is obtained by setting ∆ω ≡ 0. It can be rewritten in amplitude/phase variables as:

N 1 Ȧ1 = -2iZ(N 2 -N 3 )A * 2 A 3 e -i∆ωT , N 2 Ȧ2 = -2iZ(N 3 -N 1 )A * 1 A 3 e -i∆ωT , N 3 Ȧ3 = 2iZ(N 1 -N 2 )A 1 A 2 e i∆ωT ,
N 1 Ċ1 = -2Z(N 2 -N 3 )C 2 C 3 sin ψ, (2.1)
N 2 Ċ2 = -2Z(N 3 -N 1 )C 1 C 3 sin ψ, (2.2)
N 3 Ċ3 = -2Z(N 1 -N 2 )C 1 C 2 sin ψ, (2.3)
ψ = ∆ω -2ZC 1 C 2 C 3 N 2 -N 3 N 1 C -2 1 + N 3 -N 1 N 2 C -2 2 + N 1 -N 2 N 3 C -2 3 cos ψ, (2.4)
where

C i (T ) = A i (T ) is the real amplitude, ψ ∶= θ 1 + θ 2 -θ 3 is the dynamical phase and θ i (T ) = arg A i (T ).
In what follows we will focus on the evolution of the energy of the high-frequency mode E 3 (T ).

Amplitudes

In Fig. 1 we show the energy evolution in the resonant triad given in Table 1 for several values of the frequency detuning ∆ω = ∆ω ε ∈ [-1 2 , 1 2 ]; e.g. in geophysical applications ε ∼ O(10 -2 ). From these graphs it can be seen that the period τ and the range of the energy variation, defined as

∆E (∆ω) ∶= 1 2 max t E -min t E , (3.1)
are non-monotonic functions of the detuning ∆ω.

A graph showing the characteristics of the dependency of the energy variation range ∆E (∆ω) on the frequency detuning ∆ω is shown in Fig. 2. This particular curve was computed for parameters given in Tab. 1. The graph can conveniently be divided into the five regions which are separated by particular values of the frequency detuning ∆ω: ∆ω

(1,2)
max correspond to local maxima, ∆ω st is the position of the local minimum, and ∆ω = 0 corresponds to exact resonance. So, the regions are: (II): ∆ω ∈ ∆ω

(I): ∆ω ∈ -∞, ∆ω (1) max ; Region/Range → ← (I) ∆E +, τ +, ∆ψ-∆E -, τ -, ∆ψ+ (II) ∆E -, τ +, ∆ψ-∆E +, τ -, ∆ψ+ (III) ∆E -, τ +, ∆ψ-∆E +, τ -, ∆ψ+ (IV) ∆E +, τ -, ∆ψ+ ∆E -, τ -, ∆ψ- (V) ∆E -, τ -, ∆ψ+ ∆E +, τ +, ∆ψ-
(1) max , min{0, ∆ω st } ; (III): ∆ω ∈ min{0, ∆ω st }, max{0, ∆ω st } ; (IV): ∆ω ∈ ∆ω st , ∆ω (2) max ; (V): ∆ω ∈ ∆ω (2)
max , +∞ . The reason to regard these regions separately is that the main characteristics (i.e. energy variation ∆E , energy oscillation period τ and the phase variation ∆ψ) behave differently in each region. Our findings are summarized in Table 2, where all the quantities E , τ and ψ are followed by ± sign denoting the their variation in the region (+: increase, -: decrease). The first column corresponds to the direction of increasing values of ∆ω ∈ (-∞ → +∞), while the second column corresponds to the opposite direction ∆ω ∈ (-∞ ← +∞).

The most interesting observation is, that the energy variation range during the system evolution can be significantly larger for a suitable choice of the detuning ∆ω ≠ 0 compared to the exact resonance case ∆ω = 0. There are two values of which provide significant amplifications to ∆E . On Fig. 2 the global maximum is located on the left of ∆ω st , while on Fig. 3 it is on the right of ∆ω st . These two cases differ only by the initial energy distribution among the triad modes (see Tab. 1, initial conditions (a) & (b)).

Similar computations have been performed for other resonant triads and the qualitative behavior of the energy variation has always been similar to Figs. 2 &3. Namely, the global maximum is located on the left of ∆ω st when the high frequency mode ω 3 contains initially most of the energy, and to the right of ∆ω st in the opposite case.

It is important to stress that the energy variation ∆E (∆ω) at the global maximum ∆ω (g) max is always significantly higher than at the point of exact resonance, i.e. ∆E (∆ω (g) max ) > ∆E (0). The highest ratio ∆E (∆ω) ∆E (0) is attained when the local minimum ∆ω st coincides with the point of exact resonance. In this case we can find a ∆ω that the amplification ∆E (∆ω) ∆E (0) is of at least one order of magnitude. A simple phase space analysis allows to locate the local minimum.

Phase space analysis

On Figs. 4 -6 we depict the typical phase portraits of the dynamical system (2.1) -(2.4) in phase-amplitude variables. For illustration we choose the triad given in Tab. 1 with the initial energy distribution (a). In these pictures we represent the high-frequency mode C 3 on the horizontal axis, while the dynamical phase ψ is on the vertical. The main finding is a pronounced asymmetry between the phase portraits for positive and negative values of the detuning ∆ω: the position of the stationary point right on the horizontal axis C 3 (there are other stationary points for ψ ≠ 0) is very different; the shape of the periodic orbit differs (see Figs. A simple phase space analysis reveals the reason for the presence of a local minimum of ∆E in Figs. 2 & 3. Indeed, it can happen that the initial conditions coincide with the system equilibrium point, which depends on ∆ω st .

Conclusions

It was demonstrated that the introduction of frequency detuning significantly enriches the dynamics of a 3-wave resonance system. Moreover, the effects of detuning are highly nonlinear and highly non-monotonic with respect to the detuning parameter. The main findings of this study are outlined hereinbelow:

• The range of values of frequency detuning ∆ω can most conveniently be divided into five regions of different behaviour, not all of them present in any case. The behavior of the main parameters of system (2.1) -(2.4) over those five regions is summarized in Tab. 2. • The amplitude of energy variation (3.1) in a triad with suitably chosen detuning (∆ω ≠ 0) can be significantly higher than in the case of exact resonance, i.e. ∆ω ≡ 0.

The maximal amplification as compared to exact resonance is attained when ∆ω st coincides with the point of exact resonance. In this case one of the zones (III) or (IV) disappears. • The phase portraits along with the shape and size of the periodic cycles are substantially different for ∆ω > 0 and ∆ω < 0. This means that any complete analysis of detuned resonance must include both positive and negative values of the detuning parameter ∆ω.

The notion of resonance enhancement via frequency detuning, as the title of this Letter says, contradicts what we would expect from our physical intuition. However, there exists a simple qualitative explanation for that. Indeed, our intuition comes from a linear pendulum ẍ + ω 2 x = 0 (5.1)

taken usually as a model for a linear wave, and a resonance is regarded due to an action of an external force. On the other hand, the dynamical system for 3-wave resonance can be transformed into the Mathieu equation which describes a particular case of the motion of an elastic pendulum ẍ + [ω 2 penλ cos(ω spr )]x = 0, (

where ω pen and ω str are frequencies of pendulum-and spring-like motions, [START_REF] Kartashova | Nonlinear Resonance Analysis[END_REF]. Regarding resonance detuning ∆ω as a frequency of an external force for (5.2), our findings can be understood in the following way. The detuned 3-wave system has the maximal range of the energy amplitudes variation when the elastic pendulum interacts resonantly with the external forcing. Detailed study of this effect is upcoming, using the approach developed in [START_REF] Gitterman | Spring pendulum: Parametric excitation vs an external force[END_REF] for an elastic pendulum subject to the external force.

Figure 1 .

 1 Figure 1. Energy evolution in the triad given inTable 1, for different values of the detuning ∆ω.

Figure 2 .

 2 Figure 2. Typical dependency of the energy variation range ∆E on the frequency detuning ∆ω for the case when the high frequency mode ω 3 has the maximal energy (initial condition (a)). The vertical red dashed line shows the location of ∆ω

( 1 )

 1 max , while the vertical black solid line shows the location of ∆ω

( 2 )

 2 max . Finally, the blue dash-dotted line shows the amplitude obtained the exact resonance.

Figure 3 .

 3 Figure 3. Typical dependence of the energy variation range ∆E on the frequency detuning ∆ω for the case when the high frequency mode ω 3 has the lowest energy (initial condition (b)).

  4(b) & 5(b)); the transition from closed to snake-like integral curves takes place for different values of ∆ω , e.g. ≈ 0.31 on Fig. 4(c) and ≈ -0.24 on Fig. 5(c); the shape of the integral curves is different; the phase portraits look alike, but differ in size by one order of magnitude. In order to demonstrate how big this difference is for opposite values of ∆ω we depicted on the same Fig. 6 the periodic cycles from Figs. 4(a) & 5(a).

  (a) ∆ω = 0.1 (b) ∆ω = 0.31 (c) ∆ω = 0.315

Figure 4 .

 4 Figure 4. Phase portraits of the dynamical system (2.1) -(2.4) in (C 3 , ψ) variables for the triad from the Tab. 1(a). Positive increasing detuning.

Figure 5 .

 5 Figure 5. Phase portraits of the dynamical system (2.1) -(2.4) in (C 3 , ψ) variables for the triad from the Tab. 1(a). Negative decreasing detuning.

Figure 6 .

 6 Figure 6. Simultaneous plot of two phase portraits and integral curves for the detunings ∆ω = ±0.1 shown at Figs. 4(a) & 5(a) correspondingly.

Table 1 .

 1 Physical parameters used in numerical simulations.

	Parameter	Value
	Resonant wavevectors, [m j , n j ] Resonant frequencies, 2m j n j (n j + 1) 0.0513, 0.0476, 0.0989 [4, 12], [5, 14], [9, 13] Resonant triad parameters, N j 156, 210, 182
	Interaction coefficient, Z	7.82
	Initial energy distribution (a), %	20%, 30%, 50%
	Initial energy distribution (b), %	40%, 40%, 20%
	Initial dynamical phase, ψ	0.0

Table 2 .

 2 Behaviour of physical parameters ∆E , τ and ψ in different regions.

Acknowledgments

This research has been supported by the Austrian Science Foundation (FWF) under projects P22943-N18 and P24671.


Ludovic Henrio

Eric Madelaine

Min Zhang

pNets: an Expressive Model for Parameterised Networks of Processes (Extended Version)

Keywords: Formal methods, Distributed systems, Behavioral semantics, Structured labelled transition systems, Bisimulation

This article studies Parameterised Networks of Automata (pNets) from a theoretical perspective. We illustrate the expressiveness of pNets by showing how to express a wide range of classical constructs of (value-passing) process calculi, but also how we can easily express complex interaction patterns used in modern distributed systems. Our framework can model full systems, using (closed) hierarchies of pNets; we can also build (open) pNet systems expressing composition operators. Concerning more fundamental aspects, we dene a strong bisimulation theory specifically for the pNet model, prove its properties, and illustrate it on some examples. One of the original aspects of the approach is to relate the compositional nature of pNets with the notion of bisimulation; this is exemplied by studying the properties of a attening operator.

This paper contributes to the study of formal modeling languages. In previous research, we dened pNets (Parameterised Networks of Synchronised Automata), an intermediate language targeted towards the behavioural specication of distributed systems. pNets [START_REF] Barros | Behavioural models for distributed fractal components[END_REF] have been used

to provide a behavioural specication formalism in dierent contexts. A (closed) pNet model can be used as the semantics of a program or a system; while open pNets dene the semantics of composition operators in specication or programming languages. The pNet formalism is particularly powerful for expressing the behaviour of distributed objects [START_REF] Boulifa | Behavioural models for group communications[END_REF] and distributed components [START_REF] Barros | Behavioural models for distributed fractal components[END_REF], in particular distributed systems using queues, futures, and one-to-many communications [START_REF] Ameur-Boulifa | Verifying safety of fault-tolerant distributed components[END_REF]. In our previous work, we heavily used pNets in our verication environment, called Vercors.

1 It is a platform that assists the programmer in the specication and the ver- ication of his/her component-based application. From the specication, we generate a pNet representing the application behaviour; from this behavioural model, we are able to verify properties ranging from absence of deadlocks, to reachability of some actions, and any temporal logic property (including safety and liveness) specic to the application. In order to do this, we choose a nite instantiation domain for the parameters of the pNets, and generate a tree of nite labelled transition systems on which we can prove the properties of the application by hierarchical verication, using state-of-the art model-checkers. The long history of research we conducted towards the fully automatised behavioural verication of distributed objects and components has been based on the pNets formalism. The numerous contributions [START_REF] Ameur-Boulifa | Verifying safety of fault-tolerant distributed components[END_REF][START_REF] Barros | Behavioural models for hierarchical components[END_REF][START_REF] Barros | Parameterized Models for Distributed Java Objects[END_REF][START_REF] Boulifa | Behavioural models for group communications[END_REF][START_REF] Boulifa | Finite model generation for distributed Java programs[END_REF] we made in the domain somehow prove the eectiveness of the formalism, but we never studied formally the theoretical foundation of pNets, or their expressiveness. In this report, we will not show any formal expressiveness result (such as an equivalence with a full encoding of CCS or other calculi). Instead we chose to demonstrate the exibility of the model with a range of examples from various calculi, and application domains, into pNets.

Positioning. Our middle-term target is a generic framework for modeling the behaviour of distributed software systems, with synchronous and asynchronous execution and communication.

We do not want to build yet another syntactic language or calculus, but rather provide a semantic level framework, based on (value-passing) transition systems, with a much richer structure.

When building such a framework, we could be tempted to address some features of the dynamic calculi, including dynamic discovery of new objects, channel passing a la π-calculus, or ensembles theories [START_REF] Barnat | Towards Verication of Ensemble-Based Component Systems[END_REF]. In pNets, we chose a dierent approach: we restricted dynamic aspects to the use of parameters; those parameters can however impact the states of the processes, the process topology, but also the communication patterns (see Section 3.4). Expressiveness is lower than in π-calculus as no name passing is allowed, but still the model is more dynamic than nite and static topologies. Bigraph models of Robin Milner [START_REF] Milner | The Space and Motion of Communicating Agents[END_REF] for ubiquitous systems are kinds of general models focusing on describing location and links, whereas pNets focus more on the synchronisation of processes. Bigraphs can encode most dynamic calculi, like e.g., π-calculus, and we consider it too expressive for our purpose. The strength of the pNets resides in the 1 http://www-sop.inria.fr/oasis/index.php?page=vercors RR n°8579 expression of parametric architectures which are more restrictive than fully dynamic features, but easier to verify and still very expressive. Indeed, those architectures are expressive enough to model cloud-oriented applications with dynamic reconguration and group communication, but somehow static enough to allow for model-checking nite abstractions of their models. Our challenge is to nd the best compromise between a model exible enough to encode parametric and dynamic architectures, while allowing automatic model-checking, modulo well-dened data abstractions.

Inspiration for this model clearly comes from early work by Arnold and Nivat on synchronisation vectors [START_REF] Arnold | Finite transition systems[END_REF][START_REF] Arnold | Nivat's processes and their synchronization[END_REF], on top of which we have constructed our pNets. But it is also very close to R. de Simone's work on Meije-SCCS [START_REF] Simone | Higher-level synchronizing devices in Meije-SCCS[END_REF], which provides a notion of Architectural expressions sharing many features with our open pNets. Meije-SCCS has a universality result with respect to calculi dened by some class of operational semantic rules, even if it was based on a more complex synchronisation mechanism (using auxiliary signals and a powerful action monoid) than the one oered by synchronisation vectors. Moreover, even if the semantics of our pNets has a shape similar to the one of Meije-SCCS, it is technically dierent, because the number of holes, and of subnets cooperating in a synchronisation, is unbounded in pNets, while it was nite in Meije-SCCS. As a consequence, we cannot reuse directly the congruence result of [START_REF] Simone | Higher-level synchronizing devices in Meije-SCCS[END_REF], and we will show our own result here.

Contributions. This paper proposes a rst step in the theoretical foundation for pNets. After providing a concise and precise denition of the core of pNets, we express dierent coordination mechanisms that illustrate their expressive capacities. We rst show that it is easy to express in pNets many constructs of classical value-passing algebras, including CCS and Lotos; pNets handle e.g., the usual binding mechanism within CCS communication, as well as the gate negotiation semantics of Lotos. Then we show that pNets allow the expression of more advanced synchronisation patterns. In particular, we show how to express in a simple and natural manner broadcasting interactions, but also indexing, i.e., using an index given in a communication parameter to decide which process should receive the communication, or mechanisms for synchronisation barriers.

Then we dene a strong (early) bisimulation equivalence for closed pNets, and prove that it is a congruence for pNet contexts. This bisimulation is illustrated by two applications: one inspired from value-passing CCS, the other is a generic proof on an operator attening a pNet structure.

This paper is organised as follows. Section 2 provides a formal denition of pNets, and of their operational semantics. Section 3 illustrates the expressiveness of pNets by providing examples expressing either classical constructs of process calculi, or more advanced coordination mechanisms. Section 4 proposes a strong bisimulation theory for pNets. Finally Section 5 gives an overview of related works and Section 6 concludes this paper.

2 Parameterised Networks (pNets): denition

In this rst section we dene pNets and the notations we will use in this paper; we conclude this section by providing an operational semantics for pNets.

Inria

Notations. We extensively use indexed structures over some countable indexed sets, which are equivalent to mapping over the countable set. a i∈I i , or equivalently (i →a i ) i∈I denotes a family of elements a i indexed over the set I. Consequently, a i∈I i denes both I the set over which the family is indexed (called range ), and a i the elements of the family. E.g., a i∈{3} is the mapping with a single entry a at index 3; it will also be denoted (3 →a) in the following. When this is not ambiguous, we shall use notations for sets, and typically write indexed set over I when formally we should speak of multisets, and write x ∈ a i∈I i to mean ∃i ∈ I. x = a i . An empty family is denoted ∅. is a disjoint union operator on indexed sets: it requires that the two sets are indexed over disjoint sets. The elements of the union are accessed by using an index of one of the two families. When convenient, we will use ā to abbreviate for a i∈I i , for some I.

Term algebra. Our models rely on the notion of parameterised actions. We leave unspecied the constructors of the algebra that will allow building actions and expressions. We denote ¶ the set of parameters (or variables) 2 . We denote by Σ the signature of those constructors and by T ¶ the term algebra of Σ over the set of variables ¶. We suppose that we are able to distinguish inside T ¶ a set of action terms denoted A ¶ (parameterised actions ), a set of expression terms denoted E ¶ , and, among expressions, a set of Boolean expressions (guards) denoted B ¶ (with:

E P ∩ A P = ∅ ∧ B ¶ ⊆ E ¶ ∧ A P ∪ E ¶ ⊆ T ¶ ).
For each term t ∈ T ¶ we dene fv(t) the set of free variables of t. For α ∈ A ¶ , iv(α) returns a subset of fv(α) which are the input variables of α, i.e., the variables newly dened by reception of their value during the action α.

pNets can be used with any term algebra. As a consequence our examples will show dierent notations for actions inspired from dierent litterature sources, like classical input-output interactions with parameters, à la value-passing CCS [START_REF] Milner | Communication and Concurrency[END_REF]. These will be written ?a(x 1 , ..., x n ) for inputs, !a(v 1 , .., v n ) for outputs, or a(v 1 , .., v n ) and τ for synchronised actions; in that case we have fv(?a(x)) = iv(?a(x)) = {x}, and for a value v iv(!a(v)) = ∅. In other cases we use Lotos-style oers, with specic δ and accept(x) action terms, or Meije-SCCS action monoids, like in a.b, a f (n) . Naturally the expressiveness of the synchronisation constructs will depend signicantly on the action algebra.

We allow countable indexed sets to depend upon variables, and denote I ¶ the set of indexed sets with a range depending on variables of ¶. For example, simple intervals of the form [1..n], for some n ∈ ¶, represents a set of parameterised and variable size; the instantiation of such a set, i.e., the value of the set when the value of n is known, will unsurprisingly give the expected result. The set of expressible parameterised sets and the decidability of some results depend on the term algebra. For simplicity and at rst, the reader can consider that all the parameterised sets are intervals where bounds are linear expression of the parameters, typically of the form [1..m + 2. n]. Those correspond to the parameterised intervals we used in our practical use cases; for these intervals the interpretation of the parameter valuation, including dynamic change of parameter value, raises no particular diculty. In that case, variables in ¶ will be given a value that is a natural number. We suppose the existence of an inclusion relationship ⊆ over I ¶ , with the natural guarantee that this operation ensures set inclusion when one replaces variables by 2 We will use bothequivalently the term variable, as usual in term algebras, and the word parameter that is more usual for parameterised systems, to denote elements of ¶ RR n°8579 their values.

The pNets Model

The rst comprehensive denition of pNets was published in [START_REF] Barros | Behavioural models for distributed fractal components[END_REF]. The denition of pNets provided here is a simplied 3 version that is convenient for providing a concise formal denition of pNets and to reason about them. pNets are networks of processes: they provide a hierarchical structure to organise processes. At the leaves of the structure we have pLTSs (parameterised labelled transition systems) described in Denition 2.1. Denition 2.2 describes the hierarchical composition. pNets are parameterised by a set ¶ of variables, used both in value-passing and in the processes topology. We suppose the set ¶ is dened globally, but it could also be dened locally in each pNet.

A pLTS is a labelled transition system with variables that can be wrote and read by the actions performed in the transitions; a pLTS can have guards and assignment of variables on transitions. Variables can be manipulated, dened, or accessed inside states, actions, guards, and assignments. Denition 2.1 (pLTS). A pLTS is a tuple pLT S S, s 0 , → where:

• S is a set of states.

• s 0 ∈ S is the initial state.

• →⊆ S × T × S is the transition relation. Where

T = { α, e b , (x j := e j ) j∈J |α ∈ A ¶ ∧ e b ∈ B ¶ ∧ x j ∈ ¶ ∧ e j ∈ E ¶ }
α are actions, e b are guards, and variables in iv(α) are assigned when the transition is performed (as the input variables in traditional value-passing calculi). There may be also side-eects on variables, these will be specied by the additional assignments.

Note that we make no assumption on niteness of S or of branching in →. A sort is a set of actions. It can be viewed as the signature of the pNet. In the case of a pLTS, it is the set of labels appearing on the transitions: Sort( S, s0, → ) = {α|∃s, s , e b , e j∈J j , t, x j∈J j .(s, t, s ) ∈→ ∧ t = α, e b , (xj := ej) j∈J } pNets are constructors for hierarchical behavioural structures: a pNet is formed of other pNets, or pLTSs at the bottom of the hierarchy tree. A composite pNet consists of a set of subnets, each exposing a set of actions according to its sort. The synchronisation between a global action of the pNet and actions of the subnets is given by synchronisation vectors of the form SV k = α l∈L k l → α k : a synchronisation vector synchronises one or several actions of subnets, and exposes a single resulting global action (α k ). A pNet can either compose sub-pNets given explicitly, or be used as an operator accepting other pNets as parameters. Placeholders for the pNets that will be provided later are called holes, that play a role similar to process variables in usual process algebras. Actions synchronised in synchronisation vectors are both actions performed by sub-pNets and by holes.

I ∩ H = ∅ • SV k∈K k is a set of synchronisation vectors (K ∈ I ¶ ). ∀k ∈ K, SV k = α l∈L k lk → α k where α k ∈ A ¶ , L k ∈ I ¶ , ∅ ⊂ L k ⊆ I H, ∀l ∈ L k ∩ I. α lk ∈ Sort(pNet l ), and ∀l ∈ L k ∩ H. α lk ∈ So l .
We denote Label(SV k ) = α k .

• The set of holes of the sub-pNets, and of local holes of the pNet are all disjoint:

∀i ∈ I. Holes(pNet i ) ∩ H = ∅ ∀i 1 , i 2 ∈ I. i 1 = i 2 ⇒ Holes(pNet i1 ) ∩ Holes(pNet i2 ) = ∅
The preceding denition relies on the two functions dened below. Denition 2.3 (Sorts). The sort of a pNet is the set of actions that a pNet can perform:

Sort( pNet, So, SV k∈K k ) = {Label(SV k )|k ∈ K}
Denition 2.4 (Holes). The set of holes of a pNet is dened inductively as follows:

Holes( S, s 0 , → ) = ∅ Holes( pNet i∈I i , So h∈H h , SV ) = H ∪ i∈I Holes(pNet i )
Vocabulary. A subnet is either a sub-pNet or a hole.

A pNet Q is closed if it has no hole: Holes(Q) = ∅; else it is said to be open.

When I ∪ H =[0.

.n] we denote synchronisation vectors: < α 1 , .., α n > → α, and elements not taking part in the synchronisation are denotedas in: < -, -, α, -, ->→ α.

Denition 2.5 (pNet composition

). An open pNet: pNet = pNet i∈I i , So h∈H h , SV can be (par- tially) lled by providing a family of pNets (pNet l ) l∈L of the right sort to ll its holes.

Suppose ∀l ∈ H ∩ L. Sort(pNet l ) ⊆ So h , then 4 :

pNet (pNet l ) l∈L = pNet i (pNet l ) l∈L i∈I (pNet l ) l∈J∩L , So h∈H\L h
, SV Note that L can be larger than H. In such a case, the elements of (pNet l ) l∈L\H can ll holes at an arbitrary depth inside the tree structure of pNet. Also, if pNet is closed, then pNet[pNet ] = pNet.

A trivial example. Let us rst dene a trivial open pNet that can encapsulate another pNet

and transmit its communications/synchronisation actions unchanged. We also use this rst example to dene a graphical format for the pNets presentation.

Example 2.6 (Identity pNet). For a sort S, an identity pNet, I S , is dened as:

I S := ∅, (0 →S), {(0 →a) → a|a ∈ S}
The corresponding graphical denition is:

4 else the composition is undened S 0 SV I S = {< a >→ a} a:S This I S pNet has a single hole, indexed by 0, of sort S. For any action of S, it transmits this action between the external interface of I S (to/from processes in its environment), and the pNet that lls the hole. Overall, the behaviour of this pNet is that, for any pNet Q, I S [Q] behaves as Q.

For the examples in this paper, we use a graphical representation of pNets, certainly easier to read in most cases than the full mathematical notation. A pNet is represented by a box with subnets represented as circles on the left of the box. When a subnet is a hole, the sort is given in the circle and there is a line leading to nothing, decorated with the index below the circle. If the subnet is given, the line is connected to a pNet (see e.g. example 3.2 in page 9). On the right part we put the synchronisation vectors, often as a reference to a term outside the box.

An operational semantics for pNets

This section provides an operational semantics for the pNet model; it is based on a valuation domain for the variables of the pNet, that can be nite or innite. The operational semantics is dened for closed pNets only; the semantics for a pNet with a hole is more complicated, it should be a function of the pNet put in the hole. We suppose the existence of a unique valuation domain D. This domain can be a countable instantiation domain for each variable. We require that for a boolean expression e, if all the variables of e are given a value in D it is possible to decide whether e is true or false. Similarly, it must be possible to decide whether two expressions have the same value (e.g., when two action labels are the same).

We let φ = {x j → V j |j ∈ J} be a valuation function, mapping x j , which range over all variables of the considered pNet, to V j ∈ D, values. For a term t ∈ T ¶ , tφ ∈ D is the value of the term obtained by replacing each variable by their values given by φ. A valuation can also be applied to indexed sets. In all cases, the variables are replaced by their value and the new expression is evaluated. We dene Φ as the set of all possible valuations. We choose Φ a subset of Φ the set of valuations that can be explored: only valuation functions such that φ ∈ Φ are considered. This allows us to restrict the valuation domain and, for example, consider only nite valuations or letting some variables range only on a small domain. While in Φ the valuation domain is the same for all variables, in Φ each variable can range over a dierent sub-domain. We dene an update operator + on valuations, where φ 1 + φ 2 replaces some of the values dened in φ 1 by the ones in φ 2 ; φ 2 might also dene new entries:

{x j → V j |j ∈ J} + {x j → V j |j ∈ J } = {x j → V j |j ∈ J } ∪ {x j → V j |j ∈ J \ J }
We suppose that variable names are unique but, as variables are used locally to each pNet/pLTS, it would also be possible to use qualied names to avoid collision. The semantics of a pNet is denoted -Φ , which is a LTS 5 . It relies on a set of states for closed pNets S Φ (-) that are hierarchical composition of states reecting the structure of the pNet. Then, -Φ denes a set of transitions between such states. Denition 2.7 (Operational semantics of closed pNets). Let φ 0 ∈ Φ be an initial valuation associating a value to each variable of ¶. The semantics of pNet is a LTS pNet Φ = S Φ (pNet), S 0 (pNet), → where:

The set of states of pNet Φ , denoted S Φ (pNet) is dened as follows 6 :

S Φ ( S, s 0 , → ) = {(s, φ)|s ∈ S ∧ φ ∈ Φ} S Φ ( pNet i∈I i , ∅, SV k∈K k ) = { s i∈Iφ i | φ ∈ Φ ∧ ∀i ∈ Iφ. s i ∈ S Φ (pNet i )}
The initial state S 0 (pNet) is the composition of initial states:

S 0 ( S, s 0 , → ) = (s 0 , φ 0 ) S 0 ( pNet i∈I i , ∅, SV k∈K k ) = S 0 (pNet i ) i∈Iφ0
labels are {αφ|α ∈ Sort(pNet) ∧ φ ∈ Φ}; and transitions are dened as pNet Φ , the smallest set of transitions satisfying the rules below.

φ, φ , φ ∈ Φ s α, e b , (xj:=ej ) j∈J -------------→ s ∈→ φ = φ+{x i → V i |x i ∈ iv(α) ∧ V i ∈ D} e b φ = True φ = φ + {x j → e j φ |j ∈ J} (s, φ) αφ --→ (s , φ ) ∈ S, s 0 , → Φ Tr1 φ, φ ∈ Φ α l∈L l → α ∈ SV ∀i ∈ Iφ \ Lφ. s i = s i ∀l ∈ Lφ. φ l ∈ Φ ∧ s l α l φ l ---→ s l ∈ pNet l Φ φ = φ + l∈Lφ φ l s i∈Iφ i αφ --→ s i i∈Iφ ∈ pNet i∈I i , ∅, SV Φ

Tr2

In these rules, any variable can be assigned any value in the corresponding data domain. Then the eects of transitions (reception of valeus, eects of assignments) will restrict the possible values in subsequent states of the pNet, while constraints introduced by the synchronisation vectors, in rule Tr2, will restrict the set of possible valuations.

Note that only states of pLTSs are associated with a valuation, but states of the pNets still use the valuation to decide (expand) the set of sub-pNets embedded in the pNet. Rule Tr1 deals with transitions between states of the pLTS; only input variables and assigned variables are allowed to change value in the valuation; the resulting valuation is obtained by the successive updates from the input variable assignments, and the explicit assignments from the transition.

Remark that the predicate in a transition is evaluated in a valuation that includes the values carried by the communication action, allowing for expressing non-local decisions as in Lotos gate negotiation. Note also that there is a priori no predened direction for the ow of data because it is dependent on the chosen term algebra.

Rule Tr2 deals with transitions between states of the pNet; A given synchronisation is picked, it involves the set L ⊆ I of sub-pNets. The resulting valuation is obtained by the combination of all updates happening in the sub-pNets involved in the synchronisation (φ {φ l } l∈Lφ in the rule); sub-pNets not involved in the transition keep the same state.

The fact that each variable has a (nite or innite) complete instantiation ensures that the semantics is a (possibly innite) fully instantiated LTS that has no more variable. This condition 6 We use the . . . notation to easily identify states of the operational semantics in the rest of the paper.

is crucial for the decidability of strong bisimilarity presented in Section 4. If we choose a nite domain for each variable and if each pLTS has a nite set of states, the semantics of the pNet will be a nite LTS that can be used in a nite-state model-checker. The semantics dened above is illustrated in Section 3.2, with an example of a closed pNet encoding a n-places buer. Giving a denotational semantics for open pNets is out of the scope of this paper, however, an open pNet can be seen as a function that accepts pNets to ll its hole. Once all the holes are lled, we can use the semantics of closed pNets dened above.

Examples and Expressiveness

This section illustrates the expressiveness of pNets by exhibiting pNets for several classical constructs of process calculi. These pNets behave similarly to the original construct: the reachable states and traces simulate faithfully the original construct. Proving richer equivalence between the modelled construct and the pNet or providing a general results on expressiveness of pNets with other existing models is out of the scope of this paper.

Constructions from classical (value-passing) algebras

We rst focus on value passing algebras. The rst example models the parallel operator of CCS, synchronising input and output actions, or transmitting those actions unchanged to the outside.

Example 3.1 (CCS-like Synchronisation). Let C be a set of channel names, V a set of values.

We denote S C the sort: There are two holes indexed l and r (synchronisation vectors are written taking l = 0 and r = 1). There are four families of synchronisation vectors: the rst two sets of vectors synchronise input and output actions from the process to the right (resp. left) to the one to the left (resp. right), it is visible as a τ action; the two last sets allow any action of a process to be visible at the level of the parallel operator, and potentially to be synchronised by another parallel operator.

S C = {τ } ∪ {?a(x)|a ∈ C, x ∈ ¶} ∪ {!a(v)|a ∈ C, v ∈ V }.
The two rst vectors necessitate two fresh variables for each channel name and for each occurrence of the parallel operator. Value passing is obtained by an adequate denition of the valuation domains of the free variables: for each fresh variable x introduced by the synchronisation vector for channel c, the valuation domain should include the set of values that can be transmitted over the channel c. This set can be any over-approximation, and can be rened by typing on channels.

Note that input and output actions have a symmetric role in the synchronisation vector, they will be distinguished in the way they can appear in pLTSs, and in the way they are handled by rule Tr1. Inria Example 3.2 (Choice, Disruption, and Sequence). Next we show how to encode various artefacts for combining 2 processes. These are a classical non-deterministic choice as in CCS (here denoted +), a disruption operator similar to the Lotos Disable ([>) , and a sequencing operator with value passing similar to the Lotos Enable (>>). For the Choice pNet, the rst action of one of the holes decides which branch of the LTS is activated; all subsequent actions will be from the same side. Concerning the Disable pNet, the left sub-process evolves alone for any number of steps; but at any time the right sub-process can interrupt it and from this point keep the control. Finally the Enable pNet is a sequencing operator with data transmission: the left sub-process emits a specic exit signal δ (we denote S1 δ = S1 ∪ {δ} its sort), transmitting data values to the right sub-process through an initial accept action.

Those examples rely on some pLTSs dedicated to control of the rest of the pNet: they encode the state of the assembly and enable dierent transitions depending on this state; we call these pLTSs controllers. Controllers are typical artefacts managing an assembly of processes, with dynamic evolution of the control part. A similar idea has been used for giving a compositional behaviour semantics to open process expressions in Lotos [START_REF] Lakas | Les Transformations Lotomaton : une contribution à la pré-implémentation des systèmes Lotos[END_REF].

3.2 A closed pNet system: the n-places Buer Now we give an example of a closed pNet representing a well-known toy example: an n-places buer. We also use this example to illustrate the operational semantics of closed pNets.

The standard way to build a n-places buer in CCS is to dene a 1-place buer as a 2 states process: B =?i(x).!o(x).B, and to compose n instances of B using parallel, renaming, and restriction operators: (B[a1/o]||B[a1/i, a2/o]||...)\ a1,a2,... . We could have used a direct encoding of each of the CCS operators using open pNets, and build a (rather complicated) pNet system to express the n-places buer. But we prefer to show the expressiveness of pNets by building the full (parameterised) system using a single pNet node, synchronising all one-place buers in one step.

SV Buf f er(n) i(x) S S < -, ..., -, !o(x) >→!o(x) >} < -, ..., -, !o(x), ?i(x), -, ..., ->→ τ >, SV Buf f er(n) = {<?i(x), -, ..., ->→?i(x) >, S = {?i(x), !o(x)} o(x)
Computing the operational semantics of the n-places Buer Computing the possible transitions of such a pNet involves using the rules of the operational semantics from Section 2.2, building all possible proof trees combining transitions of the pLTSs at the leaves of our system, with all adequate synchronisation vectors of the pNet node.

For simplicity of notations, consider a Buer of size 2:

Buffer(1)
Buffer( 1)

S SV Buf f er(2) < -, !o(x) >→!o(x) >} <!o(x), ?i(x) >→ τ >, SV Buf f er(2) = {<?i(x), ->→?i(x) >, S = {?i(x), !o(x)} S
We start with a (global) parameter set P = {x 1 , x 2 }, and an initial valuation φ 0 . Chose a valuation Φ containing φ 0 , and all possible valuations of the variables in P . The initial state of Buf f er(2) Φ is (s 0 , φ 0 ), (s 0 , φ 0 ) . The only way to build a transition from this state is to use rule Tr1 with the rst synchronisation vector <?i(x 1 ), ->→?i(x 1 ) in which only the rst sub-pNet of Buer( 2) is working, and to use Tr2 to prove the initial transition of this pLTS:

s0 ?i(x 1 )φ 1 -----→ s1 ∈→ Buf f er(1) iv(?i(x1)) = {x1} v1 ∈ D φ1 = x1 → v1 (s0, φ0) ?i(x 1 )φ 1 -----→ (s1, φ0 + φ1) ∈ Buf f er(1) Φ Tr2 (s0, φ0
) ?i(x 1 )φ 1 -----→ (s1, φ0 + φ1) φ ∈ Φ k = 1 SV1 =<?i(x1), ->→?i(x1) H = {1} φ1 = {x1 → v1}
(s0, φ0), (s0, φ0)

?i(x 1 )φ 1 -----→ (s1, φ0 + φ1), (s0, φ0) ∈ Buf f er(2) Φ

Tr1

A similar construction leads to the full transition relation of Buf f er(2) Φ :

(s 0 , φ 0 ), (s 0 , φ 0 )

?i(v1)

----→ (s 1 , φ 1 ), (s 0 , φ 1 )

φ 1 = φ 0 + {x 1 → v 1 } (s 1 , φ 1 ), (s 0 , φ 1 ) τ -→ (s 0 , φ 2 ), (s 1 , φ 2 ) φ 2 = φ 1 + {x 2 → v 1 } (s 0 , φ 2 ), (s 1 , φ 2 ) !o(v1)
----→ (s 0 , φ 3 ), (s 0 , φ 3 )

φ 3 = φ 2 (s 0 , φ 2 ), (s 1 , φ 2 ) ?i(v2) ----→ (s 1 , φ 4 ), (s 1 , φ 4 ) φ 4 = φ 2 + {x 1 → v 2 } (s 1 , φ 4 ), (s 1 , φ 4 ) !o(v2)
----→ (s 1 , φ 5 ), (s 0 , φ 5 ) φ 5 = φ 4 ...

Inria

If the domain of x is innite, then this transition relation will also innite, but all transitions are of the same form as one of the 5 above, with only the valuation values changing.

Naturally in our modeling platform we have specic syntax to express the parameterised structures and the instantiation. This is beyond the scope of this paper.

Richer action algebras

In this section we investigate action algebras with expressive constructs and their use in the synchronisation vectors of pNets, lifting the richness of these constructs at the level of processes.

The two following examples are borrowed from Meije-SCCS [START_REF] Simone | Higher-level synchronizing devices in Meije-SCCS[END_REF], where the action algebra includes a simultaneity product, and has globally the structure of a commutative monoid.

SV Ack = {< a m , a n >→ a Ack(n,m) } a:A,n,m:N at S A S A SV Ack
These two open pNets are examples of the richness of computations that can be expressed in synchronisation vectors, mixed with synchronisation capacities in the Ackermann case. Such mechanisms in the Meije-SCCS structure were proved decidable (though computationally expensive) using the theory of semi-linear sets. One could imagine further extensions using some satisability modulo theory (SMT), taking into account the properties of the data-types embedded in the action algebra; in that case decidability may have to be discussed.

Many-to-many Communications

pNets oer richer and higher-level synchronisation capacities than classical one-to-one communications. pNets are particularly convenient for expressing one-to-many and many-to-one communications that are frequently used in modern grid or cloud middleware. The examples of this section all have the same top-level structure, with a number of holes with identical sort S, but they dier in the way subnets are synchronised. We present here pNets modelling either one-to-many schemas (Unicast, Broadcast, and Scatter), or many-to-one synchronisation (Synchronisation Barrier).

We rst present one-to-many communications. For each of the 3 variants, we build a pNet assembling a group of processes (subnets). A process communicating with this group synchronises with some of the subnets, and the argument of the communication (the payload of the message) can be distributed in dierent ways. In the Unicast pNet the payload is delivered to a single element of the group, only one subnet synchronises. When broadcasting, each element receives its own copy of the payload, while in the Scattering pNet each subnet receives a dierent piece of the payload. Typically, the pNet representing the group will then be assembled with some data provider pNet as pNet||Group S,N in which Group can be a unicast, broadcast or scatter pNet. The provider would be a process sending messages of type !a(arg), in which arg is a value to be passed to each/all of the subnets in the group (for unicast and broadcast), or a vector of such values in the case of scatter, with the length of the vector equal to the length of the group.

In the 3 cases, elements of the groups (the holes) all have a sort containing reception events ?a ∈ S, that carry some value (iv(a) = {v}, v ∈ ¶).

Example 3.6 (Unicast). A unicast pNet dispatches actions to a set of pNets that ll its holes, all of sort S. The resulting unicast pNet is of sort {?a(n)| ?a ∈ S ∧ n ∈ N }:

Unicast S,N := ∅, (n →S) n∈N n , {(n →a) → a(n)| a ∈ S ∧ n ∈ N }
We provide below the graphical denition for this pNet when N = [1.

.n]. This way, it is possible to choose which subnet performs the action, or to allow any of them to perform the action, and to know which of them performed it.

Example 3.7 (Broadcast). A broadcast pNet dispatches actions to a set of pNets that ll its holes. The holes are indexed over a set N . Each hole of the pNet has sort S, where S only contains reception actions, ?a ∈ S, that intuitively carry some value (iv(a) = {v}, v ∈ ¶). We build a broadcasting pNet of sort S: n 1 ..... SV BrCast = {<?a, ..., ?a, ..., ?a >→?a} ?a:S SV BrCast S S Example 3.8 (Scatter). The Scattering pNet is similar to the Broadcast pNet, except that instead of duplicating the argument, it splits the argument in as many pieces as there are elements in the target group. The sort of the scattering pNet is S N , i.e., vectors of terms, each subnet, indexed j, will receive its own piece of the global action term ?a, denoted here ?a.j. SV Scatter = {<?a.1, ..., ?a.j, ..., ?a.n >→?a} ?a:S N SV Scatter S S Reversely, we dene a many-to-one communication acting as a synchronisation barrier. It is a synchronising pattern in an asynchronous system: it waits for events from a set of processes, and when all events have arrived it creates some sort of global data from data received, and sends it to an external process.

Strong Bisimulation for pNets

In this section, we dene a convenient notion of (strong) bisimulation for closed pNets, and prove that this equivalence is a congruence w.r.t. any kind of pNet context. We rst dene a context in the pNet formalism. Dening a context syntactically as one would do in usual process algebras is possible in our case. However, pNets already provide a way to dene expressions with holes.

A context pNet is a pNet C with a single hole, we index this hole by •. To alleviate proofs, we distinguish contexts featuring a single hole at the top-level of the pNet structure, and call them top1-contexts from contexts having a single hole at any depth.

Denition 4.2 (1-context). A 1-context of sort

So is either: a top1-context pNet of sort So: pNet, (• →So), SV , or a pNet pNet, ∅, SV , in which one (and only one) of the pNet i is a 1-context of sort So.

Recall that the operation pNet[{P i }] lls some holes of pNet, with {P i } a family of pNets indexed with the indexes of the holes. Then, provided Sort(Q) ⊆ So, C[(• →Q)] is the closed pNet where the hole is replaced by Q (e.g., C[(• →Q)] = pNet ∪ (• →Q), ∅, SV in the case of a top1-context).

Strong bisimulation

Strong bisimulation of pNets is relatively classical except that it relates instantiated states, and that the two bisimilar states of pNets can perform dierent transitions with dierent valuations provided the application of the two valuations on the two labels give the same result. Denition 4.3 (Strong Bisimulation). Let P and Q be two closed pNets. A relation R ⊆

S Φ (P ) × S Φ (Q) is a strong simulation if for each (s, t) ∈ R, for any valuation set φ ∈ Φ, whenever s αφ -→ s ∈ P Φ , then ∃φ ∈ Φ, β, t , such that t βφ -→ Φ t ∈ Q Φ and (s , t ) ∈ R and αφ = βφ .
A relation R is a strong bisimulation if R and R -1 are strong simulations. Consider two closed pNets P and Q, two states s ∈ S Φ (P ) and t ∈ S Φ (Q) are strongly bisimilar, denoted by s, P ∼ t, Q i (s, t) ∈ R, for some strong bisimulation R ⊆ S Φ (P ) × S Φ (Q).

Two closed pNets P and Q are strongly bisimilar, denoted by P ∼ Q, i their initial states are strongly bisimilar: S 0 (P ), P ∼ S 0 (Q), Q Observe that the bisimilarity between pNets only implies that their reachable states are equivalent.

Proposition 4.4 (Strong Bisimulation is a congruence for top1-contexts). Let P and Q be two closed pNets and s ∈ S Φ (P ), t ∈ S Φ (Q) two strongly bisimilar states s, P ∼ t, Q .

Then for any top1-context C of sort S, i.e., C = pNet i∈I i , (• →S), SV , such that Sort(P ) ∪ Sort(Q) ⊆ So, we can build two closed pNets C[(• →P )] and C[(• →Q)] ensuring that: For all s , t of the form s = s i∈Iφ i

(• →s) ∈ S Φ (C[• →P ]), t = s i∈Iφ i (• →t) ∈ S Φ (C[• →Q]
) with ∀i ∈ Iφ. s i ∈ S Φ (pNet i ); we have s , P ∼ t , Q . Consequently, provided Sort(P ) ∪ Sort(Q) ⊆ So, for any top1-context C of sort So:

P ∼ Q ⇒ C[(• →P )] ∼ C[(• →Q)].
The proof (in Appendix 7.1) is done using classical bisimulation techniques and distinguishing synchronisation vectors involving actions of the hole from the others. We use Property 4.4 to show that strong bisimulation is a congruence, for 1-contexts where the hole can occur at arbitrary depth.

Theorem 4.5 (Strong bisimulation is a congruence). Let P and Q be two bisimilar closed

pNets: P ∼ Q. Then for any 1-context C of sort So, such that Sort(P ) ∪ Sort(Q) ⊆ So, we have C[(• →P )] ∼ C[(• →Q)].
The proof follows from Proposition 4.4 by induction on the structure of contexts (see Appendix

7.2).

This result can be extended to n-ary contexts (by replacing one hole at a time), allowing to compose pNets in any possible way.

Example of properties. To illustrate the interplay between variable valuations, input variables in communication, and the strong bisimulation, we run here a small classical example,

Inria P0 P0 P0 P0 P0 P0 P0 P0 P0 P0 P0 P0 P0 P0 P0 P0 P0 P1 P1 P1 P1 P1 P1 P1 P1 P1 P1 P1 P1 P1 P1 P1 P1 P1 P11 P11 P11 P11 P11 P11 P11 P11 P11 P11 P11 P11 P11 P11 P11 P11 P11 P12 P12 P12 P12 P12 P12 P12 P12 P12 P12 P12 P12 P12 P12 P12 P12
[x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] [x=0] out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] [~ x=0] out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q0 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q1 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q11 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12 Q12
in?x in?x in?x in?x in?x in?x in?x in?x in?x in?x in?x in?x in?x in?x in?x in?x in?x tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau inspired from [START_REF] Ingólfsdóttir | A symbolic approach to value-passing processes[END_REF], where it was used to discuss about early, late, and symbolic equivalences in value-passing CCS. Let us prove that the two pLTSs P and Q in Figure 1 are strongly bisimilar, even if matching transitions in their semantics do not come from the same symbolic branch of the pLTS.

Computing the operational semantics of these two pLTS requires xing a valuation set Φ. It is enough to use only two possible values for variable x, distinguishing the possible evaluations of the guard [x=0]. We use {0, 1}, corresponding to the most abstract domain for x preserving the semantics. Then we compute P Φ and Q Φ by unfolding dierent possible valuations and transitions of the process.

Then checking the equivalence of the two LTSs classically involves the building of equivalence classes of states, where each state includes an explicit valuation. This requires exhibiting pairs of equivalent states as in any classical bisimulation algorithm, only here we have to exhibit explicitly the valuations of variables.

The most possible abstract domain for the variable x preserving the semantics is {0, 1}, so we x Φ = {φ 0 , φ 1 }, with two possible valuations φ 0 = (x → 0) and φ 1 = (x → 1). Running rule Tr1 on process P, choosing arbitrarily φ 0 as the initial valuation, unfolds the semantic LTS shown in Figure 2. P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P0,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P1,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P11,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P12,phi_0 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P1,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P11,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 P12,phi_1 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 in?0 tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau

out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0 out!0
tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau tau

out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!1 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2 out!2
in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1 in?1

Bisimilar states:

((P 0 , φ 0 ) (Q 0 , φ 0 )) ((P 1 , φ 0 ) (Q 1 , φ 0 )) ((P 1 , φ 1 ) (Q 1 , φ 1 )) ((P 11 , φ 0 ) (Q 11 , φ 0 )) ((P 12 , φ 0 ) (P 12 , φ 1 )) ((Q 12 , φ 0 ) (Q 11 , φ 1 )) ((P 11 , φ 1 ) (Q 12 , φ 1 ))
Figure 2: Behaviour unfolding of process P , and classes of bisimilar states of P and Q

We leave the semantics of Q as an exercise for the reader. The last step is to prove equivalence of P and Q. This is a simple exercise, we only have to exhibit a bisimulation relation between the states of the semantic LTSs, being careful of transitions that do not come from the same branches of the original pLTSs (see right part of Figure 2).

Application to Flattening Operator

Finally, this section presents a attening operation for pNet contexts and proves strong bisimilarity. The purpose of this section is to illustrate further the interaction between bisimulation and pNets structure on an example that is useful both from a practical and from a theoretical point of view. The attening operator can be used to atten a pNet hierarchy, it is used when building a model for a large system (to reduce the state-space) and can also be used to ease compositional formal reasoning. We suppose here that the action algebras limits the parameters of the actions to be only variables. This restriction avoids us to have to deal with unication between action terms here; it is possible to add a pNet in the attened structure dealing with the unication.

Flat(C, C ) = pNet pNet , (• →So ), SV where SV = {(α l ϕ) l∈L\{•} β l∈L l → α |α l∈L l → α ϕ ∈ SV ∧ β l∈L l → β ∈ SV ∧• ∈ L ∧ α•ϕ = β ∧ ϕ = (xn → yn) n∈N ∧ ∀n ∈ N. (xn ∈ fv(α•) ∧ yn ∈ fv(β))} ∪{(α l ) l∈L → α |(α l ) l∈L → α ∈ SV ∧ • / ∈ L}
This denition uses the fact that action parameters can only be variables, and thus an action β triggered by a subnet can only match the action α • in the synchronisation vector if there exist ϕ that assigns to each free variable of α • a variable of β such that the two actions are the same. ϕ is then applied to all the actions α i of the original synchronisation vector. Now we prove the most interesting property of the attening: it preserves strong bisimulation: Proposition 4.7 (Flattening and strong bisimulation).

∀P closed pNet, C[• →C [• →P ]]∼F lat(C, C )[• →P ]
The full proof is in Appendix 7.3. This property has several consequences, as it shows that it is sucient to prove congruence for the top-level contexts instead of checking holes occurring deeper in the pNet tree. We can then derive a Flatten operator that attens a closed pNet P hierarchy, it produces a pNet composing only pLTSs as explained below.

Observe that the hole in the context can be indexed by an index other than •. We dene a function F 0 as follows: Let P = pNet i∈I i , ∅, SV . Either P is at (i.e. ∀i ∈ I. pNet i is a pLTS then F 0 (P ) = P ); or ∃i 0 ∈ I. 7 The recursive application of F 0 on P reaches a xed-point if all the sub-pNets are indexed over nite set, in that case we call Flatten(P ) this xed-point and have Flatten(P ) ∼ P .

pNet i0 = pNet i∈I i , ∅, SV , then let C = pNet i∈I\{i0} i , (i 0 →S 0 ), SV . Take i 1 ∈ I and have C = pNet i∈I \{i1} i , (i 1 →S 1 ), SV . Then P = C[i 0 →C [i 1 →pNet i1 ]]∼F lat(C, C )[i 1 →pNet i1 ] = F 0 (P ).
On the practical side, Property 4.7 justies some strategies used to optimize the state-space generation for hierarchical pNet structures before model-checking. More precisely, we often use a hierarchical approach for state-space generation, starting bottom-up with state-space (= LTS) of pLTSs at the leaves, then computing products for each level of the pNet tree, reducing each intermediate LTS using bisimulation. But this brute force approach happen to be expensive (in term of the size of intermediate LTSs) when some subsystems explode because of the lack of information about their execution contexts. In such cases it can be very useful to apply rst attening (removing some of the hierarchical levels of the pNet) before applying the hierarchical stat-space generation.

Concerning generic proofs, this operator can help in proving various properties, like associativity of the CCS operators and +. Indeed, proving that Flatten(P (Q R)) is bisimilar to Flatten((P Q) R) becomes trivial because the two attened pNets are equal. The case of + is less trivial because the attened pNets are not the same for (P + Q) + R and P + (Q + R), proving their bisimilarity requires arguments similar to the direct study. On the contrary the enabling operator from Lotos (denoted >>) is not associative, and Flatten(P >> (Q >> R)) and Flatten((P >> Q) >> R) are not the same and cannot be proved to be bisimilar in the general case.

Finally, we expect this operator to help us in the denition of more complex semantic notions to reason on pNets, e.g., a symbolic semantics for pNets, or some notion of barbed congruence. Indeed, thanks to attening, it will be sucient to dene a semantics on a at pNet only synchronising LTSs.

Related Works

Synchronisation vectors. As mentioned in the introduction, this research naturally inherits from the seminal work by Arnold and Nivat on synchronisation vectors [START_REF] Arnold | Finite transition systems[END_REF][START_REF] Arnold | Nivat's processes and their synchronization[END_REF]. The theoretical expressiveness of (closed) pNets is the same, but their tree structure is essential to search for compositionality, and for the denition of open structures. Moreover, Arnold/Nivat synchronisation vectors did not include explicit data values; in our approach, this ability is very important for usability in verication tools.

Formats for SOS semantic rules. The closest work to this paper may be the eorts in the nineties [START_REF] Groote | Structured operational semantics and bisimulation as a congruence[END_REF] to dene the tyft/tyxt format and its extensions. The expressive power of synchronisation vectors is similar to that of SOS rules with positive hypothesis and structured transition labels. Close to the limits of what pNets (and tyft/tytx) can express, you would nd replication mechanisms: in pNets this is encoded as the dynamic activation of a new instance inside one (unbounded) parameterised hole. One signicant dierence is that pNets allow for synchronisation of an unbounded number of subnets, while in the tyft/tyxt format and its variants (to the best of our knowledge), this is not possible. We already had a similar distinction when comparing with the MEIJE-SCCS format in Section 1. Our approach with pNets is more constructive and pragmatic, as our main interests are for dening behavioural semantics for various programming languages in the parallel and distributed computation area, and we want our model, its expressiveness, and its limits to be compatible with an ecient implementation in a modeling and verication environment.

Other semantic-level frameworks. In the family of low-level formalisms for distributed systems, we must cite Lotos-NT and BIP.

Lotos NT [START_REF] Mateescu | Translating Pi-Calculus into LOTOS NT[END_REF] is a low-level language designed as an ecient execution language for Lotos or E-Lotos, but also as an intermediate formalism for the model-checking of these languages. It was originally designed to express easily the complex synchronisation mechanisms of E-Lotos, but later used successfully to encode the Pi-calculus. Still it relies strongly on specic parallel operators; the direct multi-way and parameterised synchronisation vectors of pNets allow for a much more exible and direct encoding of other mechanisms.

BIP [START_REF] Basu | Rigorous component-based system design using the bip framework[END_REF] is a formal framework that allows building and analysing complex component-based systems. It applies to both synchronous (reactive) and asynchronous (distributed) systems by coordinating the behaviour of a set of primitive and heterogeneous components. A component's behaviour is described as a Petri net extended with data and functions, whereas coordination is described as interactions between components and scheduling policies between interactions.

Even if the BIP framework allows powerful compositional reasoning on the system, it does not support the denition of parameterised components, nor does it allow (in its basic versions) explicit data transfer between components. On the other side, the priority functionality of BIP would require to use some kind of negative premisses, that we cannot do in the current version of pNets.

One aspect we have not tried yet, but that seems to t naturally with the pNet appraoch, is formalisms dedicated to the external coordination of components, as e.g. with the REO connectors language [START_REF] Arbab | A channel-based coordination model for component composition[END_REF]. This would certainly be an interesting basis for studying integration of component description formalisms with exogeneous coordination or choregraphy.

Conclusion and Discussion

pNets have been used to provide a general behavioural specication formalism in dierent contexts, in particular it proved to be particularly powerful for expressing the behaviour of distributed objects and of distributed components.

In this paper, we illustrate the expressiveness of pNets by showing how they can be used to express a wide range of classical synchronisation patterns, including constructs of value-passing algebras. We have also exhibited more complex interaction and synchronisation patterns used for many-to-many communication schemes in distributed component-based applications. In that case, pNet parameters are used both as data values and as topology indexes.

We propose a behavioural semantics and a bisimulation theory, starting with a strong bisimulation relation for closed pNets. Both the semantics and the equivalence are based on all possible valuations, and can be thought of early versions. We prove that the strong bisimulation indeed is a congruence for all pNets contexts, and we provide a more constructive approach for combining pNets using a attening operator.

Our next goal is to look for appropriate bisimulation relations for open pNets. Such equivalences should be considering hypotheses on the behaviour of holes, as was used in so-called Inria FH-bisimulations in [START_REF] Simone | Higher-level synchronizing devices in Meije-SCCS[END_REF], but a particular challenge will be to nd more constructive equivalences that will give us ecient approaches to build proofs in a compositional (congruent) manner. Such compositional theories and proof methods are of course essential in the analysis of hierarchical component systems. Another promising perspective is to investigate the proof of symbolic properties that are valid independently of the parameter valuations and to identify conditions on data and indexes in which one can prove such properties, such an approach could rely on previous works on symbolic reasoning for value passing processes [START_REF] Ingólfsdóttir | A symbolic approach to value-passing processes[END_REF]. The properties of congruence and of the attening operator are promising rst steps toward a bisimulation theory for open pNets. Strong Bisimulation is a congruence for top1-contexts Let P and Q be two closed pNets and s ∈ S Φ (P ), t ∈ S Φ (Q) two strongly bisimilar states s, P ∼ t, Q . Then for any top1-context C of sort So, i.e., C = pNet i∈I i , (• →So), SV , such that Sort(P ) ∪ Sort(Q) ⊆ So, we can build two closed pNets C[(• →P )] and C[(• →Q)] ensuring that: for all s , t of the form s = s

i∈Iφ i (• →s) ∈ S Φ (C[• →P ]), t = s i∈Iφ i (• →t) ∈ S Φ (C[• →Q])
with ∀i ∈ Iφ. s i ∈ S Φ (pNet i ); we have s , P ∼ t , Q . Proof. Because s, P ∼ t, Q , then there exists a strong bisimulation R ⊆ S Φ (P ) × S Φ (Q) such that (s, t) ∈ R. Finally, as (s , t ) ∈ R, by denition of R, ( (s i ) i∈Iφ (• →s , (s i ) i∈Iφ (• →t ) ) ∈ R.

The proof for R-1 is similar, so we have proved that R is a strong bisimulation.

7.2 Proof of theorem 4.5

Strong bisimulation is a congruence Let P and Q be two bisimilar closed pNets: P ∼ Q. or C is a 1-context of the form pNet i∈I i , ∅, SV , with pNet i0 a 1-context for a given i 0 ∈ I, with Sort(pNet i0 ) = So i0 , and all other pNet Consider the closed pNet P and an initial valuation φ 0 ∈ Φ associating a value to each variable of P . We will make a binary relation

R = s i∈Iφ i (• → (s i ) i∈I φ (• →s) , s i∈Iφ i s i i∈I φ • →s | ∀i ∈ Iφ. s i ∈ S Φ (pNet i ) ∧ ∀i ∈ I φ . s i ∈ S Φ (pNet i ) ∧ s ∈ S Φ (P )
It is easy to see that the initial states composed from an initial valuation φ 0 and initial states of the sub-pNets are related according to R. Conversely, when proving that R -1 is a simulation, the most representative case is when all the processes are involved.

  pNets: un modéle expressif pour les réseaux de processus paramétrés (Version étendue) Résumé : Cet article étudie les Réseaux Paramétrés d'Automates Synchronisés (pNets) d'un point de vue théorique. Nous illustrons l'expressivité du modèle pNets en montrant comment encoder un large éventail de constructions classiques des calculs de processus avec passage de donnés, mais aussi la façon dont nous pouvons facilement exprimer les schémas d'interaction complexes utilisés dans distribués systèmes modernes. Notre formalisme permet de modéliser des systèmes complets, utilisant une hiérarchie (fermée) de pNets; mais nous pouvons également construire des systèmes ouverts exprimant des opérateurs de composition. Concernant les aspects plus fondamentaux, nous dénissons une théorie de bisimulation forte spéciquement adpatée à notre modèle, prouvons ses propriétés, et l'illustrons sur certains exemples. Un des aspects originaux de la démarche est de relier la composition des pNets avec la notion de bisimulation; ceci est illustré par l'étude des propriétés d'un opérateur d'aplatissement. Mots-clés : Méthodes formelles, Systèmes distribués, Sémantique comportementale, Systèmes de transition structurés, Bisimulation 1 Introduction

  The pNet of the synchronisation operator, || C , is dened as: r l ∪{<?a(x), !a(x) >→ τ } a:C,x:P,xf resh SV ||c = {<!a(x), ?a(x) >→ τ } a:C,x:P,xf resh SV ||c S C S C ∪{< -, b >→ b} b:SC ∪{< b, ->→ b} b:SC

  -, b, r >→ b} b:S2 } + = {< a, -, l >→ a} a:S1 SV [> = {< a, -, l >→ a} a:S1 SV >> = {< a, -, l >→ a} a:S1 ∪{< -, b, r >→ b} b:S2 } ∪{< -, b, r >→ b} b:S2 } ∪{< δ(x), accept(x), δ >→ τ }} These three pNets have a similar structure with two holes. The left hole, indexed l, has sort S1, the right hole has sort S2. The third subnet, contains an LTS encoding their control part. These control parts, and the synchronisation vectors, are the elements dening their specic behaviour.

Example 3 . 3 .

 33 Using pNets, we express such a construct using a parameterised pNet with n subnets, and as many synchronisation vectors expressing binary synchronisation between the subnets:

Example 3 . 4 .

 34 Fibonacci. Here we have a single hole with sort S A = {a n |a ∈ A, n ∈ N} with A a set of action names. Then the open pNet F ib transforms any action of the subnet by increasing its intensity. 0 SV F ib = {< a n >→ a f ib(n) } a:A,n:N at S A SV F ib Example 3.5. Ackermann. The Ack pNet is similar, though it synthesises a signal of intensity Ack(m, n), synchronising inputs of the same base action from 2 subnets. r l

n 1 .

 1 .... SV Index = {< -, ..., a, ..., ->→ a(n)} a:S,n:N SV Index S S This pNet has card(N ) holes, each of sort S. For each action of S it allows the synchronisation of one hole with the external world. The index of the hole is matched with the exported action.

Inria Example 3 . 9 (

 39 Synchronisation Barrier). This pNet collects actions from a set of m pNets. Its holes, of sort S, are indexed over a set N = [1..m]. The pNet also contains a collecting process Coll that gathers individual 'a' messages from the holes, and stores them in an array (if any hole sends 'a' twice, the new value replaces the older one); when the array is full it transmits the resulting array as an argument of the 'synchro' global action. The sort of the SBarrier pNet is {?get(a, k)|a ∈ S ∧ k ∈ [1..m]} ∪ {!synchro(A)|A ∈ S }, where S is the set of arrays of length m containing elements in S. ..... !synchro(A); [full(A)] A:=empty(1..m) ?get(a,k); A[k]:=a 1 m ∪ {< -, ..., -, !synchro(A) >→!synchro(A)} A:S ′ SV Barrier S SV Barrier = {< -, ..., a, ..., -, ?get(a, k) >→?get(a, k)} k:[1..m],a:S S Coll This section has illustrated the expressiveness of pNets through examples. We have shown their capacity to express rich composition patterns mimicking both classical synchronisations, and modern many-to-many interactions.

Denition 4 . 1 (

 41 top1-context). A top1-context of sort So is a pNet C of the form pNet, (• →So), SV where pNet is a family of closed pNets.

Figure 1 :

 1 Figure 1: Process P and Process Q.

Denition 4 . 6 (

 46 Flattening). Let C = (pNet , (• →So ), SV , and C = pNet, (• →So), SV with Sort(C ) ⊆ So; we dene Flat(C, C ) as follows:

7 Appendix 7 . 1

 771 Proof of proposition 4.4:

Then for any 1 -

 1 context C of sort So, such that Sort(P ) ∪ Sort(Q) ⊆ So, we have C[(• →P )] ∼ C[(• →Q)].Proof. We prove theorem 4.5 by induction on the structure of C: either C is a top1-context, we can apply Proposition 4.4, and conclude C[(• →P )] ∼ C[(• →Q)].

  we have pNet i0 [(• →P )] ∼ pNet i0 [(• →Q)]. Now consider the top1-context C [(• →So i0 )] = pNet i∈I\i0 i , {(• →So i0 )}, SV .Then using Property 4.4 we have:C[(• →P )] = C [(• →(pNet i0 [(• →P ])) ∼ C [(• →(pNet i0 [(• →Q])) = C[(• →Q)] 7.3 Proof of Proposition 4.7Flattening and strong bisimulation∀P closed pNet, C[• →C [• →P ]]∼F lat(C, C )[• →P ]Proof. Let P be a closed pNet and C and C two contexts; C = pNet, (• →So), SV and C = pNet , (• →So ), SV with Sort(C ) ⊆ So. Then F lat(C, C ) = pNet pNet , (• →So ), SV with SV dened below:SV = {(α l ϕ) l∈L\{•} β l∈L l → α |α l∈L l → α ϕ ∈ SV ∧ β l∈L l → β ∈ SV ∧• ∈ L ∧ α•ϕ = β ∧ ϕ = (xn → yn) n∈N ∧ ∀n ∈ N. (xn ∈ fv(α•) ∧ yn ∈ fv(β))} ∪{(α l ) l∈L → α |(α l ) l∈L → α ∈ SV ∧ • / →C [• →P ]]∼F lat(C, C )[• →P ],we only need to prove their initial states are bisimilar.

  ) i∈I φ 2 (• →t) ∈ R. We focus on the case involving actions of C, C , and P at the same time; the other cases are either special case of this one or similar to the proof of Proposition 4.4. As the action αφ 1 can be performed in C[• →C [• →P ]] Φ , based on the denition of rule Tr2, there must be a synchronisation vector of the form α l∈L {•} l → α in the denition of C[• →C [• →P ]] with L ⊆ I (in the case involving C, C , and P ). Also, this implies that by rule Tr2, there is ψ such that βψ is a transition of C [• →P ] Φ , and thus there is a synchronisation vector in C of the form β l∈L {•} l → β with L ⊆ I (remember we consider that P is involved in the synchronisation), additionally βψ = α • φ 1 by applicability of Tr2. And there must exist ϕ such that β = α • ϕ because action parameters must be variables. Consequently, by denition of F lat(C, C ), α l ϕ l∈L β l∈L • l → αϕ is a synchronisation vector of F lat(C, C ). Thus the action αφ 1 can be performed in F lat(C, C )[• →P ] Φ ; it leads to the expected state by construction (the two Tr2 rules are replaced by a single one): s i∈Iφ i s i i∈I φ (• →s) αφ1 -→ t i∈Iφ2 i t i i∈I φ 2 (• →t) .

F

  lat(C, C )[• →P ] Φ then the rule Tr2 can be triggered and there must exist a synchronisation in F lat(C, C )[• →P ] of the form: α l∈L l β l∈L {•} l → α; then (by denition of the attening operator) there must exist a synchronisation vector in C of the form: (α l ϕ -1 ) l∈L • → αϕ -1 and in C of the form: β l∈L • l → β where ϕ is the assignment that was used to build the synchronisation vector(β = α • ϕ). Then it is easy to see that the action αφ 1 can be performed in C[• →C [• →P ]] Φ by two applications of the Tr2 rule.

  ¶ is the set over which holes are indexed, each hole h is of sort So h . I and H must be disjoint:

	Denition 2.2 (pNets). A pNet is a hierarchical structure where leaves are pLTSs:
	pNet	pLT S | pNet i∈I i , So j∈J j	, SV k∈K k	where
	• pNet i∈I i	is the family of sub-pNets where I ∈ I ¶ is the set over which sub-pNets are indexed.
	• H ∈ I

  The states of C[(• →P )] (resp. C[(• →Q)]) are tuples of the form s i∈Iφ (s i ) i∈Iφ (• →s ) , where φ = φ {φ l } l∈Lφ φ P ) and ∀i / ∈ L. s i = s i . Since (s, t) ∈ R,then there exists φ Q such that t βφ Q -→ t in Q Φ , (s , t ) ∈ R, and βφ Q = α P φ P . According to rule Tr2, s i∈Iφ (s i ) i∈Iφ (• →t ), where φ = φ {φ l } l∈Lφ φ Q .

i u , where the last element u is a state of P (resp. Q).

Dene R = {(

s i∈Iφ i (• →s) , s i∈Iφ i (• →t) )|(s, t) ∈ R, ∀i ∈ Iφ. s i ∈ S Φ (pN et i )}. We will prove that R is a strong bisimulation. Suppose ( s i∈Iφ i (• →s) , s i∈Iφ i (• →t) ) ∈ R; then (s, t) ∈ R.

For any valuation φ 1 , for any transition s i∈Iφ i (• →s) αφ1 -→ (s i ) i∈Iφ (• →s ) , let us prove (by case analysis on the form of the synchronisation vector used to generate the global action α) that there is a corresponding transition in C[(• →Q)] Φ , and that their target states are bisimilar: If the action α only involves some pN et i∈I i , then there is a synchronisation vector, α l∈L l → α, with L ⊆ I. We have ∀l ∈ Lφ. s l α l φ l → s l in pN et i∈I i Φ (for some of the sub-pNets, but not involving P ), and s i∈Iφ i (• →s) αφ -→ (s i ) i∈Iφ (• →s) , where φ = φ {φ l } l∈Lφ and ∀i / ∈ L. s i = s i . According to rule Tr2, similarly s i∈Iφ i (• →t) αφ -→ (s i ) i∈Iφ (• →t) , and by denition of R, ( (s i ) i∈Iφ (• →s) , (s i ) i∈Iφ (• →t) ) ∈ R. If the interaction α involves both pN et i∈I i and the hole, then rule Tr2 is applicable and there is a synchronisation vector, α l∈L l (• →α P ) → α, with L ⊆ I (potentially L = ∅). We have ∀l ∈ Lφ. s l α l φ l → s l in pN et i∈I i Φ and s α P φ P -→ s in P Φ , and s i∈Iφ i (• →s) αφ -→ i (• →t) αφ -→

  The proof is similar:• →s ∈ R, and a transition can betriggered in F lat(C, C )[• →P ] Φ , then:Similarly to the case above, the important point is to notice that, if a transition is triggered in

	if	s i∈Iφ i	(• → s i	i∈I φ ) (• →s) , s i∈Iφ i	s i	i∈I φ
				s i∈Iφ i	s i	i∈I φ	(• →s)	αφ1 -→ t i∈Iφ2 i	t i	i∈I φ 2	(• →t)
	then we prove that
			s i∈Iφ i	(• → s i	i∈I φ ) (• →s)	αφ1 -→ t i	i∈Iφ2	(• → t i	i∈I φ 2 ) (• →t)
	with, by denition of R: t i∈Iφ2 i	(• → t i	i∈I φ 2 ) (• →t) , t i∈Iφ2 i	t i	i∈I φ 2

(• →t) ∈ R

The complete pNet model includes elements that are convenient for behavioural specication and model- checking like request queues and the possibility to ll a single hole with a family of pNets. Those elements are not necessary for the formal study we present here, expressiveness is indeed the same.Inria

RR n°8579

A (classical) LTS is indeed a pLTS with no parameter Inria

To make F 0 a function, we need to choose i 0 and i 1 deterministically, which can be done by choosing an arbitrary order on the indexing sets without loss of generality.Inria

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399