Eduard Baranov
email: eduard.baranov@uclouvain.be

Simon Bliudze
email: simon.bliudze@inria.fr

Expressiveness of component-based frameworks A study of the expressiveness of BIP

Keywords: component-based frameworks, expressiveness, BIP, glue operators, SOS formats

Expressiveness of component-based frameworks: A study of the expressiveness of BIP

Introduction

In our previous work [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF], we have formalised some of the properties that are desirable for component-based design frameworks, namely: incrementality, flattening, compositionality and modularity [START_REF] Gössler | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Sifakis | A framework for component-based construction[END_REF]. The formalisation is based on a very simple, abstract algebraic definition of the notion of component-based framework. We have also discussed the full expressiveness property, although without providing a formal definition for it. Intuitively, strong (resp. weak) full expressiveness of one framework w.r.t. another requires that each operator of the first be expressible as an operator (resp. composition of operators) in the second.

In this paper, we provide a formal definition of the notion of full expressiveness. We then apply it to study the expressiveness of the BIP (Behaviour-Interaction-Priority) framework [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF]8] and their variations.

BIP is a component-based framework for the design of concurrent systems based on the separation of concerns between coordination and computation [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF]8]. It is among the few frameworks, such as SCADE [START_REF] Boulanger | SCADE: Language and Applications[END_REF] and Ptolemy II [START_REF] Eker | Taming heterogeneity: The Ptolemy approach[END_REF], which combine the use of formal methods for defining their operational semantics and for model verification, with code generation. Recently we have developed a theory of architectures [START_REF] Attie | A general framework for architecture composability[END_REF][START_REF] Attie | A general framework for architecture composability[END_REF], which allows the compositional design of correct-by-construction BIP models. This theory formalises BIP design patterns, called architectures. The application of an architecture to a BIP system enforces the corresponding characteristic property. We have shown that safety properties are preserved by composition of architectures and have provided an algorithm for verifying whether two architectures are non-interfering, which guarantees the preservation of their liveness properties. This approach provides a compositional method for the design of correct-by-construction systems from a set of formalised user and system requirements. We have applied this methodology for the design of satellite on-board software, in particular for CubETH-a university-built nanosatellite-and in a project financed by the European Space Agency [START_REF] Mavridou | Architecturebased design: A satellite on-board software case study[END_REF][START_REF] Stachtiari | Early validation of system requirements and design through correctness-by-construction[END_REF].

BIP systems consist of components modelled as Labelled Transition Systems (LTS). Transitions are labelled by ports, which are used for synchronisation with other components. Composition operators defining such synchronisations are obtained by combining interaction and priority models. The classical operational semantics of the BIP composition operators [START_REF] Bliudze | The algebra of connectors -Structuring interaction in BIP[END_REF] is defined by SOS rules in a format, which is a restriction of GSOS [START_REF] Bloom | Ready simulation, bisimulation, and the semantics of CCS-like languages[END_REF]; we call this format BIP-like SOS. In the previous works [START_REF] Bliudze | The algebra of connectors -Structuring interaction in BIP[END_REF][START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF][START_REF] Bliudze | Causal semantics for the algebra of connectors[END_REF][START_REF] Bliudze | Synthesizing glue operators from glue constraints for the construction of component-based systems[END_REF], we have conducted an extensive study of the semantics and algebraic representations of the BIP glue operators. While the semantics of interaction models is very straightforward and did not change throughout those papers, that of the priority models has proven to be much subtler. Thus, in order to make the correct decisions for the future versions and flavours of BIP, it is essential to understand the impact of the meaning given to priority models on the resulting design framework, in particular its expressiveness, which is the central question of this paper.

In [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF], we have provided a counter-example showing that the classical semantics of BIP does not possess flattening, which implies that it does not possess strong full expressiveness w.r.t. BIP-like SOS either. This shows that the often encountered informal statement: "BIP possesses the expressiveness of the universal glue" (or its equivalent in slightly different formulations) is based on an erroneous proposition in previous work [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]Proposition 4]. The fundamental reasons for this absence of strong full expressiveness lie in the definition of the priority models. A priority model is a strict partial order on the underlying interaction model (set of allowed interactions). In particular, this definition guarantees that applying a priority model does not introduce deadlocks in the otherwise deadlock-free system. This property turns out to be one of the key reasons underlying the expressiveness limitations, since deadlocks can be introduced by certain operators respecting the BIP-like SOS format.

In this paper, we consider five variations of BIP, including the classical BIP, alongside five variations of the SOS formats defining the composition operator semantics and study their relative expressiveness. In doing so, we extend and refine the results previously published in the proceedings of the EXPRESS/SOS 2016 workshop [START_REF] Baranov | A note on the expressiveness of BIP[END_REF].

The first part of the paper introduces the general theory of expressiveness, by defining the notion of component-based framework, -identifying six possible expressiveness relations between two frameworks based on the notions of strong and weak full expressiveness of one framework w.r.t. another, -presenting several properties of these relations.

The second part of the paper studies the expressiveness relations among five variations of BIP and five SOS formats:

-Classical BIP (CBIP) and BIP-like SOS (BSOS) -Witness BIP-like SOS (WBSOS): WBSOS extends BIP-like SOS with positive premises that do not contribute to the transition defined by the rule, i.e. the enabledness of a transition in one of the components is tested without the transition being fired. -Simple (SiBSOS) and acyclic (AcBSOS) BIP-like SOS: These two restrictions of BSOS apply to sets of rules defining an operator. For a set of rules in the BIP-like SOS format, the inhibiting relation identifies interactions, whereof the enabledness inhibits a given interaction. SiBSOS considers only sets of BIP-like SOS rules with simple inhibiting relations, where the enabledness of one interaction is always sufficient to inhibit another one. AcBSOS requires in addition that the inhibiting relation be acyclic. -Relaxed BIP (RBIP): RBIP extends classical BIP by taking priority models to be arbitrary relations on sets of ports, i.e. without requiring that these be strong partial orders and limited to interactions provided by the components. -Complex BIP (XBIP): XBIP is a further extension of RBIP, which allows sets of interactions-as opposed to single interactions in CBIP and RBIP-to be used as inhibitors in the priority model. -Offer BIP (OBIP) and Firing-Negative-Activation SOS (FNASOS): These two frameworks are based on an alternative, offer semantics initially introduced in [START_REF] Bliudze | Synthesizing glue operators from glue constraints for the construction of component-based systems[END_REF], using the offer predicate, which allows testing whether a port is part of an enabled transition in an atomic component. -Activation BIP (ABIP): ABIP is a hybrid framework introduced for the sake of comparison, which mixes the classical and offer semantics by relying on the usual transition relation to define the semantics of priority models, but using the offer predicate for that of non-firing positive premises.

Figure 1 shows the comparison of expressiveness among the these frameworks. The figure is complete in the sense that all relations that are not shown explicitly can be deduced from those shown by application of the results presented in Section 2.

The rest of the paper is structured as follows. Section 2 presents the algebraic formalisation of component-based frameworks, strong and weak full expressiveness, and presents their properties. Section 3 provides the definitions and the formal semantics of all the variations of BIP and the SOS formats presented above. Section 4 analyses the expressiveness relations among these frameworks. Section 5 briefly discusses some related work. Finally, Section 6 concludes the paper. 2 Algebraic formalisation of component-based frameworks

Basic definitions

Every component-based design framework can be viewed as an algebra of components equipped with a semantic mapping. The algebra of components syntactically defines the composite components that can be assembled from a given set of the atomic ones. The semantic mapping associates to each component its corresponding behaviour. The codomain of the semantic mapping, which we call the semantic domain consists of a behaviour type-defined in terms of Labelled Transition Systems or a similar formalism-and an associated equivalence relation. This can be formalised as follows:

Definition 1 A component-based framework is a tuple (G, C, B, ≃, σ), where -G is a set of composition (glue) operators, we denote by G n ⊆ G, with n ∈ N, the subset of n-ary operators, -C is a set of atomic components, -(B, ≃) is a semantic domain, consisting of a behaviour type B and an equivalence relation ≃ ⊆ B × B, σ ∶ A ⇀ B is a partial semantic mapping from the algebraic structure

A ∶∶= C | o⟨C 1 , . . . , C n ⟩, C ∈ C, n ∈ N, C 1 , . . . , C n ∈ A and o ∈ G n ,
generated by G from C, which we call the algebra of components of the framework. (Notice that A does not appear explicitly in the tuple, since it is fully defined by G and C.)

We call the elements of A components and the elements of B behaviours. The algebraic structure A represents the set of all systems constructible within the framework.

The behaviour type B defines the semantic nature of the components manipulated by the framework. The equivalence relation ≃ ⊆ B × B allows comparing components in terms, for example, of their functionality, observable behaviour or capability of interaction with the environment. It is canonically lifted to A by putting,

C 1 ≃ C 2 iff σ(C 1 ) ≃ σ(C 2 ), for any C 1 , C 2 ∈ A.
The semantic mapping σ ∶ A ⇀ B assigns to each component its meaning in terms of the behaviour type B: for any C ∈ A, we say that σ(C) is the behaviour of C.

Example 1 A number of examples representing variations of the BIP framework will be provided in the subsequent sections. For an alternative example, consider the framework CCS -= (G -, C, B, ≃, σ -), taking both C and B to be the subset of purely sequential processes in CCS [START_REF] Milner | Communication and Concurrency[END_REF]:

C = B ∶∶= l | l.P | P 1 + P 2 , l ∈ L, P, P 1 , P 2 ∈ B,
where L = {τ } ∪ {a, a | a ∈ A}, for some given set of actions A. Take ≃ be the branching bisimilarity relation [6]. Take G = {∥, \A}, where ∥ is the classical binary CCS parallel composition (synchronising a and a, for any a ∈ A) and \A is the unary restriction operator, which hides all actions in the set A ⊆ A by replacing them with τ . The semantic mapping σ is defined trivially for \A and through the expansion lemma [START_REF] Milner | Communication and Concurrency[END_REF], for ∥.

σ o⟨C 1 , . . . , C n ⟩ = õ σ(C 1 ), . . . , σ(C n ) , for all n ∈ N, C 1 , . . . , C n ∈ A and o ∈ G n .
We call {õ | o ∈ G} the set of defining mappings of σ.

Example 2 Clearly, the semantic mapping in Example 1 is structural. Alternatively, any semantic mapping defined using Structural Operational Semantics rules [START_REF] Plotkin | A structural approach to operational semantics[END_REF] is, indeed, structural.

Before moving on to the notions necessary for comparing the expressiveness of component-based frameworks, we introduce the following technical definition.

Definition 3 Given a framework F = (G, C, B, ≃, σ) and a set of variables Z, we will denote by G[Z] the set of expressions on variables in Z, defined by the following grammar:

G[Z] ∶∶= Z | o⟨E 1 , . . . , E n ⟩, Z ∈ Z, n ∈ N, E 1 , . . . , E n ∈ G[Z] and o ∈ G n .
Comparing the expressiveness of two component-based frameworks is only possible when their semantic domains coincide.

1 1 Two component-based frameworks with distinct semantic domains can be compared by mapping to a common behaviour type and taking an appropriate equivalence relation consistent with those of the frameworks. However, this essentially boils down to a substitution of the semantic domains, i.e. considering a different pair of frameworks.

Definition 4 Given two frameworks

F i = (G i , C i , B, ≃, σ i ) i∈{1,2}
with the same semantic domain, we say that F 1 has strong full expressiveness w.r.t. F 2 , denoted

F 2 ◂ F 1 iff ∀n ∈ N, ∀o ∈ G n 2 , ∃õ ∈ G n 1 ∶ ∀C i 1 , . . . , C i n ∈ A i , n ⋀ k=1 σ 1 (C 1 k ) ≃ σ 2 (C 2 k ) ⟹ σ 1 (õ⟨C 1 1 , . . . , C 1 n ⟩) ≃ σ 2 (o⟨C 2 1 , . . . , C 2 n ⟩) . (1)
We say that F 1 has weak full expressiveness w.r.t. F 2 , denoted

F 2 ◃ F 1 iff, ∀n ∈ N, ∀o ∈ G n 2 , ∃õ ∈ G 1 [Z 1 , . . . , Z n ] ∶ ∀C i 1 , . . . , C i n ∈ A i , n ⋀ k=1 σ 1 (C 1 k ) ≃ σ 2 (C 2 k ) ⟹ σ 1 õ[C 1 1 /Z 1 , . . . , C 1 n /Z n ] ≃ σ 2 o⟨C 2 1 , . . . , C 2 n ⟩ , ( 2
)
where õ[C with the extension from σ -to σ being trivial:

1 1 /Z 1 , . . . , C 1 n /Z n ] ∈ A 1 is the component obtained by substituting in õ the variables Z k by components C 1 k , for all k ∈ [1, n].
σ(C 1 + C 2 ) def = σ(C 1 ) + σ(C 2 )
. We trivially have CCS -◂ CCS . It is easy to show that the + operator cannot be encoded by any combination of parallel composition and restriction, essentially since the choice represented by + has to be maintained throughout the subsequent execution of the process, whereas both parallel composition and restriction are "memoryless". Hence, CCS / ◃ CCS -.

Notice that both strong and weak full expressiveness are preorders, i.e. they are reflexive and transitive. Strong full expressiveness trivially implies the weak one. Notice that the six comparison relations are mutually disjoint. The intuitive meanings of the three relations in the first row of Table 1 are the following: given two frameworks

F i = (G i , C i , B, ≃, σ i ), if for
any operator in G 2 we can find a corresponding operator in G 1 such that its application to an equivalent set of components would result in equivalent components, then F 1 has at least equivalent expressiveness or is more expressive than F 2 . There are three options for the converse. If there is a corresponding operator in G 2 for any operator in G 1 , then their expressiveness are equivalent. If every operator in G 1 , which does not have a corresponding one in G 2 , can be represented by a hierarchy of operators in Table 1 Expressiveness comparison relations (three "less expressive" relations indicated in grey are symmetric to the "more expressive" ones; the two relations in the second row are not used in the subsequent sections of this paper-they are only presented for the sake of completeness)

F 2 ?F 1 F 1 ?F 2 ◂ ◃ ∧ / ◂ / ◃ ◂ F 1 and F 2 have strongly equivalent expressiveness F 1 is weakly more expressive than F 2 F 1 is strongly more expressive than F 2 F 1 ⇔ F 2 F 2 → F 1 F 2 ⇒ F 1 ◃ ∧ / ◂ F 1 is weakly less expressive than F 2
F 1 and F 2 have weakly equivalent expressiveness Notice that the relations shown in Table 1 are mutually exclusive. For instance, contrary to the usual intuition behind the use of the symbols '⇔' and '⇒' in predicate logics,

F 1 is slightly more expressive than F 2 F 2 ← F 1 F 1 ↔ F 2 F 2 ⇢ F 1 / ◃ F 1 is strongly less expressive than F 2 F 1 is slightly less expressive than F 2 F 1 and F 2 are incomparable F 2 ⇐ F 1 F 2 ⇠ F 1 F 1 F 2 G 2 ,
F 1 ⇔ F 2 implies F 1 / ⇒ F 2 .
In particular, a framework is never more expressive than itself, i.e. F / ⇒ F and F / → F .

Properties of the comparison relations

We now provide some key properties of the relations defined in the previous section. The relations ⇒, → and ⇔ are transitive.

Proposition 1 For any frameworks F 1 , F 2 , F 3 and any R ∈ {⇒, →, ⇔ }, we have

F 1 RF 2 and F 2 RF 3 implies F 1 RF 3 .
Proof. We provide the proof for R = →. Those for ⇔ and ⇒ are even more straightforward.

Since F 1 → F 2 and F 2 → F 3 , by definition of →, hold the relations shown in the following diagram:

F 1 ◂ F 2 ◂ F 3 ∥ ∥ ∥ F 1 ▹ F 2 ▹ F 3 ∥ ∥ ∥ F 1 / ▸ F 2 / ▸ F 3 From the transitivity of ◂ and ◃, we conclude that F 1 ◂ F 3 and F 3 ◃ F 1 . Suppose that F 3 ◂ F 1 . Then, from the above diagram, we deduce F 2 ◂ F 3 ◂ F 1 , i.e. F 2 ◂ F 1 , which contradicts the assumption F 1 → F 2 . We conclude that F 3 / ◂ F 1 and, therefore, F 1 → F 3 .
In particular, transitivity of ⇔ implies that this relation is, indeed, an equivalence. We will now show that all the relations introduced above are preserved by ⇔. First, consider the following lemma.

Lemma 1 For any frameworks F 1 , F 2 , F 3 , such that F 1 ⇔ F 2 and any R ∈ {◂, ▸, ◃, ▹}, we have

F 1 RF 3 iff F 2 RF 3 .
Proof. Follows from the transitivity of ◂ and ◃ and the fact that ◂ implies ◃.

Corollary 1 For any frameworks F 1 , F 2 , F 3 , such that F 1 ⇔ F 2 and any R ∈ {⇔, →, ⇒, ↔, ⇢, }, we have F 1 RF 3 iff F 2 RF 3 .
Lemma 2 For any frameworks F 1 , F 2 , F 3 , hold the following implications:

1. F 1 ◂ F 2 ∧ F 1 / ◂ F 3 implies F 2 / ◂ F 3 , 2. F 1 ◂ F 2 ∧ F 1 / ◃ F 3 implies F 2 / ◃ F 3 , 3. F 1 ◂ F 2 ∧ F 3 / ◂ F 2 implies F 3 / ◂ F 1 , 4. F 1 ◂ F 2 ∧ F 3 / ◃ F 2 implies F 3 / ◃ F 1 .
Proof. Similarly to Lemma 1, all these implications follow from the transitivity of ◂ and ◃ and, for implications 2 and 4, from the fact that ◂ implies ◃.

From Lemma 2 and the transitivity of ◂ and ◃ we deduce the following corollary.

Corollary 2 For any frameworks F 1 , F 2 , F 3 , hold the following implications:

1. F 1 ⇒ F 2 → F 3 implies F 1 ⇒ F 3 , 2. F 1 → F 2 ⇒ F 3 implies F 1 ⇒ F 3 .
Proof. In both items, we have

F 1 ◂ F 2 ◂ F 3 . From the transitivity of ◂ we deduce F 1 ◂ F 3 .
In 1, we have

F 2 / ◃ F 1 ∧ F 2 ◂ F 3 which, by Lemma 2 (2), implies F 3 / ◃ F 1 . Similarly, in 2, we have F 1 ◂ F 2 ∧ F 3 /
◃ F 2 which, by Lemma 2 (4), implies

F 3 / ◃ F 1 .
Thus, in both cases, we, indeed, have

F 1 ⇒ F 3
Notice that relation combinations other than those in Proposition 1 and the two corollaries above do not provide immediate "shortcut" relations. This is mostly due to the fact that the complement relations / ◂ and / ◃ are not transitive. For instance, given F 1 , F 2 and F 3 , such that

F 1 ◃ F 2 ◃ F 3 but F 1 / ◂ F 2 /
◂ F 3 , we can proceed as follows:

1. Take all composition operators from F 1 that do not have corresponding ones in F 2 and add them to F 3 as "syntactic sugar" for the corresponding hierarchical expressions. 2. Add two completely new operators two F 3 and another completely new operator to F 2 with the semantics defined as the composition of those for the two new operators in F 3 .

Denoting the extended frameworks by

F ′ 2 and F ′ 3 , we have F 1 ◃F ′ 2 ◃F ′ 3 , F 1 / ◂ F ′ 2 / ◂ F ′ 3 but F 1 ◂ F ′ 3 .
Without constituting a formal proof, this manipulation does provide an intuition for the reason why other relation combinations do not have generic shortcuts.

Definition 6 The framework is said to possess uniform flattening 2 if the set of composition operators G is closed under composition:

∀n ∈ N, ∀i, j ∈ [1, n] (i ≤ j), ∀o 1 ∈ G n-j+i , ∀o 2 ∈ G j-i+1 , ∃o 3 ∈ G n , ∀C 1 , C 2 , . . . , C n ∈ A ∶ o 1 ⟨C 1 , . . . , C i-1 , o 2 ⟨C i , . . . , C j ⟩, C j+1 , . . . , C n ⟩ ≃ o 3 ⟨C 1 , . . . , C n ⟩ .
As mentioned above, strong full expressiveness trivially implies weak full expressiveness. The converse holds in presence of uniform flattening.

Proposition 2 For two frameworks F 1 and F 2 , such that F 1 has uniform flattening,

F 2 ◃ F 1 implies F 2 ◂ F 1 .
Sketch of the proof. Weak full expressiveness guaranties that any operator o from G 2 is expressible as a hierarchy of operators in G 1 . Uniform flattening applied several times to this hierarchy can "flatten" it to a single glue corresponding to o. Thus, the requirement for strong full expressiveness is satisfied.

According to Definition 4, in order to establish that one framework has strong (resp. weak) full expressiveness w.r.t. another, we have to prove the existence of the corresponding operator (resp. hierarchical construction) that preserves the semantic equivalence (see [START_REF] Boulanger | SCADE: Language and Applications[END_REF] or ( 2)). Below, we show that, under additional assumptions, it is sufficient to only check the preservation of the behaviour equality.

Definition 7 A framework (G, C, B, ≃, σ) is compositional iff ∀n ∈ N, ∀o ∈ G n , ∀C i 1 , . . . , C i n ∈ A i (i ∈ {1, 2}), n ⋀ k=1 C 1 k ≃ C 2 k ⟹ o⟨C 1 1 , . . . , C 1 n ⟩ ≃ o⟨C 2 1 , . . . , C 2 n ⟩ . ( 3
)
Lemma 3 ([4]) If the semantic mapping of a framework is structural and the defining mappings (see Definition 2) preserve the equivalence of the operands, then the framework is compositional.

Proof. By the assumptions of the lemma, we have:

σ o⟨C 1 1 , . . . , C 1 n ⟩ = õ σ(C 1 1 ), . . . , σ(C 1 n ) ≃ õ σ(C 2 1 ), . . . , σ(C 2 n ) = σ o⟨C 2 1 , . . . , C 2 n ⟩ .
All composition operators that we will consider in this paper satisfy the assumptions of the above lemma.

Proposition 3 For two frameworks

F i = (G i , C, B, ≃, σ i ) i∈{1,2} , whereof F 1 is com-
positional, with the same atomic components, the same semantic domain, and such that, for any C ∈ C, holds σ 1 (C) = σ 2 (C), we have 2 The notion of uniform flattening is stronger than that of flattening introduced in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF] in that it requires the operator o 3 to be the same, independently of the choice of C 1 , . . . , C n .

1. F 2 ◂ F 1 if ∀n ∈ N, ∀o ∈ G n 2 , ∃õ ∈ G n 1 ∶ ∀C i 1 , . . . , C i n ∈ A i , n ⋀ k=1 σ 1 (C 1 k ) = σ 2 (C 2 k ) ⟹ σ 1 (õ⟨C 1 1 , . . . , C 1 n ⟩) = σ 2 (o⟨C 2 1 , . . . , C 2 n ⟩) , (4) 2. F 2 ◃ F 1 if ∀n ∈ N, ∀o ∈ G n 2 , ∃õ ∈ G 1 [Z 1 , . . . , Z n ] ∶ ∀C i 1 , . . . , C i n ∈ A i , n ⋀ k=1 σ 1 (C 1 k ) = σ 2 (C 2 k ) ⟹ σ 1 õ[C 1 1 /Z 1 , . . . , C 1 n /Z n ] = σ 2 o⟨C 2 1 , . . . , C 2 n ⟩ , (5)
where all notations are as in Definition 4.

Proof. We prove the proposition for

F 2 ◂ F 1 -the proof for F 2 ◃ F 1 is similar.
Let us denote A m i the set of components C ∈ A i , such that the maximal chain of applications of composition operators in the construction of C has the length m. In particular,

A 0 i = C.
The proof is by induction of the structural depth of the components involved. The induction hypothesis is the following: with the restriction of the last quantification to ∀C

i 1 , . . . , C i n ∈ A m i , (4) implies (1) and ∀C ∈ A m 2 , ∃C ′ ∈ A m 1 ∶ σ 1 (C ′ ) = σ 2 (C). (6)
The induction step will consist in proving that if this statement holds for all m ′ < m, then it also holds for m. The base case is m = 0, i.e. the quantification is over atomic components only.

Consider a pair of operators o and õ, which satisfy (4) with the last quantification being replaced by ∀C

σ 1 õ⟨C 2 1 , . . . , C 2 n ⟩ = σ 2 o⟨C 2 1 , . . . , C 2 n ⟩ . Since σ 1 (C 1 k ) ≃ σ 2 (C 2 k ) = σ 1 (C 2 k ), by compositionality of F 1 , we have σ 1 õ⟨C 1 1 , . . . , C 1 n ⟩ ≃ σ 1 õ⟨C 2 1 , . . . , C 2 n ⟩
and, combining the two,

σ 1 õ⟨C 1 1 , . . . , C 1 n ⟩ ≃ σ 2 o⟨C 2 1 , . . . , C 2 n ⟩ .
Notice that, for m = 0, (6) holds trivially by the assumption of the proposition with

C 2 = C 1 .
Let us now prove the induction step. First of all, consider a component

C ∈ A m 2 . Since m > 0, we have C = o⟨C 1 , . . . , C l ⟩, for some o ∈ G 2 and C 1 , . . . , C l ∈ A m-1 2 .
Hence, by the induction hypothesis, there exist

C ′ 1 , . . . , C ′ l ∈ A m-1 1 , such that σ 1 (C ′ k ) = σ 2 (C k ), for all k ∈ [1, l]. By (4), there exists õ ∈ G 1 , such that σ 1 õ⟨C ′ 1 , . . . , C ′ l ⟩ = σ 2 o⟨C 1 , . . . , C l ⟩ = σ 2 (C). Denoting C ′ = õ⟨C ′ 1 , . . . , C ′ l ⟩ ∈ A m 1
, we obtain the proof of the induction step for (6).

Consider now a pair of operators o and õ, which satisfy (4) with the last quantification replaced by ∀C

i 1 , . . . , C i n ∈ A m i . Consider, furthermore, two sets of components C i 1 , . . . , C i n ∈ A m i , such that σ 1 (C 1 k ) ≃ σ 2 (C 2 k ), for all k ∈ [1, n]
. By (6) (as proven above), there exist

C 2 1 ′ , . . . , C 2 n ′ ∈ A m 1 , such that σ 1 (C 2 k ′ ) = σ 2 (C 2 k ), for all k ∈ [1, n]
. By (4), we have

σ 1 õ⟨C 2 1 ′ , . . . , C 2 n ′ ⟩ = σ 2 o⟨C 2 1 , . . . , C 2 n ⟩ . Since σ 1 (C 1 k ) ≃ σ 2 (C 2 k ) = σ 1 (C 2 k ′ ), by compositionality of F 1 , we have σ 1 õ⟨C 1 1 , . . . , C 1 n ⟩ ≃ σ 1 õ⟨C 2 1 ′ , . . . , C 2 n ′ ⟩
and, combining the two,

σ 1 õ⟨C 1 1 , . . . , C 1 n ⟩ ≃ σ 2 o⟨C 2 1 , . . . , C 2 n ⟩ ,
which proves the induction step for (1) and thereby concludes the proof of the proposition.

All the frameworks considered in the subsequent sections have structural semantics and follow SOS formats that preserve bisimilarity. Since we consider a bisimilarity-based equivalence relation on the behaviour type, all these frameworks are compositional by Lemma 3. Furthermore, all these frameworks have the same set of atomic components and, up to a canonical extension (see Section 3.3.3), the same semantic domain. They satisfy all the assumptions of Proposition 3, which means that we can prove the positive results about their relative expressiveness by studying the defining mappings of the matching composition operators and showing that their application preserves the equality of behaviours. (Negative results are proven by counterexamples.)

3 The BIP component-based framework

Classical BIP

In this section, we briefly recall BIP and its classical operational semantics, as initially published in [START_REF] Bliudze | The algebra of connectors -Structuring interaction in BIP[END_REF].

Semantic domain

The behaviour type in BIP is the set of Labelled Transition Systems (LTS).

Definition 8 A labelled transition system (LTS) is a triple (Q, P, -→), where Q is a set of states, P is a set of ports, and -→ ⊆ Q×2 P ×Q is a set of transitions labelled by sets of ports, such that only self-loops can be labelled by the empty set of ports, i.e. (q, ∅, q ′ ) ∈ -→ implies q = q ′ . For q, q ′ ∈ Q and a ∈ 2 P , we write

q a -→ q ′ iff (q, a, q ′ ) ∈ - →. A label a ∈ 2 P is active in a state q ∈ Q (denoted q a -→), iff there exists q ′ ∈ Q such that q a -→ q ′ . We abbreviate q / a -→ def = ¬(q a -→).
Note 1 In the rest of the paper, whenever we speak of a set of LTSs

B i = (Q i , P i , - → i ), for i ∈ [1, n],
we assume that all P i are pairwise disjoint, i.e. i ≠ j implies P i ∩ P j = ∅. We denote

P def = ⋃ n i=1 P i .
When the indices are clear from the context, we drop them on transition relations and simply write -→.

The equivalence of LTS is defined through a bisimulation relation [START_REF] Park | Concurrency and automata on infinite sequences[END_REF].

Definition 9 Let B 1 = (Q 1 , P, - → 1 ) and B 2 = (Q 2 , P, - → 2 ) be two LTS, and let R ⊆ Q 1 × Q 2 be a binary relation. -R is a simulation iff, for all q 1 Rq 2 , q 1 a -→ 1 q ′ 1 implies q 2 a -→ 2 q ′ 2 for some q ′ 2 ∈ Q 2 such that q ′ 1 Rq ′ 2 .
-R is a bisimulation iff both R and R -1 are simulations.

We say that B 1 and B 2 are bisimilar if there exists a bisimulation relation total on both Q 1 and Q 2 .

Definition 10 Two behaviours B i = (Q i , P i , - →), for i = 1, 2 are equivalent if P 1 = P 2 ,
and the two LTS are bisimilar.

Glue operators

BIP glues consist of two layers. Interaction models define the sets of allowed interactions, i.e. synchronisations between the transitions of their operand components. Priority models define the scheduling-or conflict resolution-policies, reducing non-determinism when several synchronisations allowed by the interaction model are enabled simultaneously.

Interaction models For given disjoint sets of ports

P i , for i ∈ [1, n], we denote P = ⋃ n i=1 P i . An interaction model is a set of interactions γ ⊆ 2
P . The semantics of the application of an interaction model γ is defined for any set of components

C 1 , . . . , C n such that σ(C i ) = (Q i , P i , - → i ), for i ∈ [1, n], by putting σ γ⟨C 1 , . . . , C n ⟩ def = (Q, P, - → γ ), with Q = ∏ n i=1 Q i and the minimal transition relation - → γ satisfying the rule a ∈ γ q i a∩P i ----→ q ′ i i ∈ I q i = q ′ i i ∉ I q 1 . . . q n a -→ γ q ′ 1 . . . q ′ n , (7)
where

I = {i ∈ [1, n] | a ∩ P i ≠ ∅}.
Intuitively, this means that an interaction a allowed by the interaction model γ can be fired when all the components involved in a are ready to fire the corresponding transitions. All the components that are not involved in a remain in their current states.

Priority models For a component C, such that σ(C) = (Q, P, - →), a priority model is a strict 3 partial order π ⊆ 2 P × (2 P \ {∅}) (we write a ≺ b as a shorthand for (a, b) ∈ π).
The semantics of the application of a priority model π is defined by putting σ(π⟨C⟩

1 2 3 p q p q (a) C 1
) def = (Q, P, - → π ), with the minimal transition relation - → π satisfying the rule q a -→ q ′ q / b - → a ≺ b q a -→ π q ′ . (8)
Intuitively, this means that an interaction can be fired only if no higher-priority interaction is enabled. In this context, it is important to notice that only interactions belonging to the interaction model of a BIP glue operator can be used in the priority model.

Definition 11 An n-ary BIP glue operator is a triple

(P i ) n i=1 , γ, π , where (P i ) n i=1
are disjoint sets of ports and, denoting P def = ⋃ n i=1 P i , the remaining two elements γ ⊆ 2 P and π ⊆ γ × (γ \ {∅}) are, respectively, interaction and priority models on

P .
In the remainder of the paper, we omit the sets of ports (P i ) n i=1 when they are clear from the context.

We will denote by CBIP the framework combining the above defined elements, with LTS being both the behaviour type and the set of atomic components, bisimilarity used as the semantic equivalence and composition operators and the semantic mapping defined as in Definition 11 and rules [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF] and (8).

To simplify the notation, we denote the component obtained by applying the glue operator (P i ) n i=1 , γ, π to sub-components B 1 , . . . , B n , by πγ⟨B 1 , . . . , B n ⟩ instead of (P i ) n i=1 , γ, π ⟨B 1 , . . . , B n ⟩. Furthermore, when π = ∅, we write directly γ⟨B 1 , . . . , B n ⟩, omitting π.

Example 5 Consider the two components C 1 and C 2 shown in Figures 2(a) and 2(b), respectively. We have P 1 = {p, q} and P 2 = {r}, and put γ = {p, q, r, qr} and π = {q ≺ r}. 4 The semantics of the glue operator defined by the combination of the interaction model γ and the priority model π is given by the following four rules, obtained by composing rules of forms ( 7) and (8) and removing premises whereof satisfaction does not depend on the state of the operand behaviours (e.g. the premise a ∈ γ is satisfied in all states):

q 1 p -→ q ′ 1 q 1 q 2 p -→ q ′ 1 q 2 , q 2 r -→ q ′ 2 q 1 q 2 r -→ q 1 q ′ 2 , q 1 q -→ q ′ 1 q 2 r -→ q ′ 2 q 1 q 2 qr --→ q ′ 1 q ′ 2 , q 1 q -→ q ′ 1 q 2 / r -→ q 1 q 2 q -→ q ′ 1 q 2 . ( 9
)
4 To simplify the notation we use the juxtaposition γ = {p, q, r, qr} instead of the set notation γ = {p}, {q}, {r}, {q, r} for interactions. Similarly, we directly write π = {q ≺ r} instead of π = {(q, r)}

The behaviour of the composed component πγ⟨B 1 , B 2 ⟩ is shown in Figure 2(c). The dashed arrow 21 q -→ 31 shows the transition present only in σ(γ⟨B 1 , B 2 ⟩), but not in σ(πγ⟨B 1 , B 2 ⟩). Solid arrows show the transitions of σ(πγ⟨B 1 , B 2 ⟩).

Among the transitions labelled by q, only the transition 22 q -→ 32 is enabled and not 21 q -→ 31 (Figure 2(c)). Indeed, the negative premise in the fourth rule of (9), generated by the priority q ≺ r, suppresses the interaction q when a transition labelled r is possible in the second component.

Let us now recall an important property of the BIP glue operators with the above semantics, which was originally shown in [START_REF] Gößler | Priority systems[END_REF]: application of a priority model does not introduce deadlocks.

Definition 12 Let B = (Q, P, - →) be a behaviour. A state q ∈ Q is a deadlock iff holds the statement ∀a ⊆ P, q / a -→. Lemma 4 ([24]) Let C i , such that σ(C i ) = (Q i , P i , - →), for i ∈ [1, n]
, be a set of components, γ and π be respectively interaction and priority models on

P = ⋃ n i=1 P i . A state q ∈ ∏ n i=1 Q i is a deadlock in σ(πγ⟨C 1 , . . . , C n ⟩) if and only if it is a deadlock in σ(γ⟨C 1 , . . . , C n ⟩).
Proof. The "if" implication is trivial. To prove the "only if" implication, assume that, for some a ∈ γ, we have q a -→ γ . Let b ⊆ P be an interaction, maximal w.r.t.

π, such that b ∈ γ, a ≺ b and q b - → γ . If such b exists, holds q b - → π . Otherwise holds q a -→ π . In both cases, q is not a deadlock in σ(πγ⟨C 1 , . . . , C n ⟩).
Notice that this proof does not rely on π being a strict partial order. The lemma can be generalised to any acyclic relation π ⊆ γ × γ.

BIP-like SOS format

Observe that the rules in [START_REF] Bliudze | Exogenous coordination of concurrent software components with JavaBIP[END_REF] are obtained by composing rules of forms ( 7) and (8). In particular, the fourth rule is obtained by the following derivation:

q ∈ γ q 1 q -→ q ′ 1 q 2 = q ′ 2 q 1 q 2 q -→ γ q ′ 1 q ′ 2 r ∉ γ ∨ q 2 / r -→ q 1 q 2 / r -→ γ (*) q 1 q 2 q -→ π q ′ 1 q ′ 2 . ( 10
)
The sub-derivation (*) in ( 10) is obtained by negating the premises of the instance of ( 7) with a = r. This is possible because the transition relation in σ(γ⟨B 1 , B 2 ⟩) is defined by ( 7) inductively, i.e. it is the minimal transition relation satisfying [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF]. In ( 9), we have simplified [START_REF] Bliudze | The algebra of connectors -Structuring interaction in BIP[END_REF] by removing premises, whereof satisfaction does not depend on the state of the operand behaviours: q ∈ γ (satisfied in all states) and r ∉ γ (dissatisfied in all states), and by replacing q ′ 2 with q 2 . Notice that the priority q ≺ r affects the behaviour of the composed system only because r ∈ γ. Indeed, if r did not belong to γ, the premise r ∉ γ would always be satisfied independently of the state of the system.

Every BIP glue operator is a combination of a (possibly trivial) interaction model with a (possibly trivial) priority model. By merging a rule of form (8) with a layer consisting of one or several rules of form ( 7)-as in the example [START_REF] Bliudze | The algebra of connectors -Structuring interaction in BIP[END_REF] above-and simplifying by removing the constant premises, we always obtain a rule in the format

q i a∩P i ----→ q ′ i i ∈ I q i = q ′ i i ∉ I q j / b j -→ (j, b j ) ∈ H q 1 . . . q n a -→ q ′ 1 . . . q ′ n , (11)
where

I = {i ∈ [1, n] | a ∩ P i ≠ ∅}, whereas H ⊆ [1, n] × 2 P and b j ∈ 2 P j \ {∅},
for each (j, b j ) ∈ H. Below we call this format BIP-like SOS. Thus, the semantics of every BIP glue operator can be defined by a set of rules in the BIP-like SOS format.

Note 2 Notice that for two rules in any given format, if their conclusions coincide but the set of all the premises of one of the rules is contained in that of the other rule, then the latter rule is redundant. Indeed, whenever the rule with more premises can be applied, so can be the rule with less premises. Similarly, if a rule has contradictory premises, as for example q a -→ q ′ and q / a -→, it is redundant, since it can never be applied.

Below, we will consider only sets of rules that do not contain such redundant ones and will sometimes emphasize this fact by explicitly calling such sets nonredundant.

Definition 13 A BIP-like SOS operator is the composition operator defined as (P i ) n i=1 , R , where (P i ) n i=1 are disjoint sets of ports and R is a non-redundant set of BIP-like SOS rules [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF].

We will denote by BSOS the framework with the same atomic components and the same semantic domain as CBIP (i.e. LTS and bisimilarity) and with BIP-like SOS glue operators with their semantics defined inductively by the corresponding sets of rules.

The following example shows that BSOS does not possess flattening. Although, in Section 2.2, we have only defined uniform flattening, this example shows that BSOS does not possess even a weaker form defined in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF], where different operators are admitted for different sets of operand components.

Example 6 Consider two composition operators defined by sets of rules in the BIPlike SOS format:

o 1 ∶ q 1 p -→ q ′ 1 q 1 q 2 q 3 p -→ q ′ 1 q 2 q 3 , q 2 r -→ q ′ 2 q 3 / s -→ q 1 q 2 q 3 r -→ q 1 q ′ 2 q 3 , q 3 s -→ q ′ 3 q 1 q 2 q 3 s -→ q 1 q 2 q ′ 3 . ( 12
)
o 2 ∶ q p -→ q ′ q / r -→ q p -→ q ′ , q r -→ q ′ q r -→ q ′ , q s -→ q ′ q s -→ q ′ . (13)
Consider three components C 1 , C 2 and C 3 shown in Figure 3 However, the BIP-like SOS rule format [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] only allows the use of the negative premise q 3 / s -→, which would induce the opposite behaviour, i.e. blocking p in 135 instead of 136. Thus, it is impossible to represent the behaviour of o 2 ⟨o 1 ⟨C 1 , C 2 , C 3 ⟩⟩ with a single BIP-like SOS composition operator.

In Section 4.1, we will show that CBIP does not have even weak full expressiveness w.r.t. BSOS. In the following subsections, we first introduce two useful variations of the BSOS format (Section 3.2), then we present some BIP modifications that we use in our study (Section 3.3).

Variations of the BIP-like SOS format

Witness BIP-like SOS

In Example 6 above, a transition labelled by p is available in all states of the composed component, where r is not enabled. The enabledness of r is controlled by the operator o 1 as follows: r is disabled in all states of σ(o 1 ⟨C 1 , C 2 , C 3 ⟩), where at least one premise of the corresponding rule in o 1 is not satisfied. Thus, in order to flatten the composition o 2 • o 1 , the rule for the transition p should be split into two: one with the premise q 2 / r -→ that allows p in all states where r is not enabled in the behaviour B 2 ; and another with the premise ¬q 3 / s -→ or, equivalently, q 3 s -→. This latter rule would allow p in all states, where s is enabled; in such states r is blocked by the operator o 1 . We call premises of the form q 3 s -→ witness.

Definition 14 A Witness BIP-like SOS operator is a composition operator defined as (P i ) n i=1 , R , where (P i ) n i=1 are disjoint sets of ports and R is a non-redundant set of SOS rules in the following format:

q i a∩P i ----→ q ′ i i ∈ I q i = q ′ i | i ∉ I q j / b j -→ (j, b j ) ∈ H q k c k --→ | (k, c k ) ∈ L q 1 . . . q n a -→ q ′ 1 . . . q ′ n , (14)
with

I = i ∈ [1, n] | a ∩ P i ≠ ∅ and H, L ⊆ [1, n]×2 P , such that, for each (j, b j ) ∈ H, holds b j ∈ 2 P j and, for each (k, c k ) ∈ L, holds c k ∈ 2 P k .
We call the premises of the form q i a∩P i ----→ q ′ i firing; the premises of the form q j / b j -→ negative; and the premises of the form q k c k --→ witness.

We will denote by WBSOS the framework, which has the same semantic domain and atomic components as above, but uses witness BIP-like SOS operators with the semantic mapping defined by (14). Sketch of the proof. The proof follows by taking the classical composition of SOS rules. We only have to prove that this composition preserves the format (14). This is straightforward for the firing premises. For the witness premises, the only difference is that the target state is irrelevant, so the top-level firing premises in the composition of two rules become witness premises by dropping the target state. For negative premises, top-level firing and witness premises become negative in the composed rule, while top-level negative rules become witness. Thus the format is, indeed, preserved.

Example 7 To illustrate the above proof, consider the following three rules:

q 1 a -→ q ′ 1 q 234 / bc -→ q 56 d -→ q 1 q 234 q 56 a -→ q ′ 1 q 234 q 56 , q 2 b - → q ′ 2 q 3 / e -→ q 4 c - → q ′ 4 q 2 q 3 q 4 bc -→ q ′ 2 q 3 q ′ 4 , q 5 d -→ q ′ 5 q 6 f -→ q 5 q 6 d -→ q ′ 5 q 6 .
Substituting the second and third rules for the corresponding premises of the first rule, we obtain the following three rules, differing only in their second premises:

q 1 a -→ q ′ 1 q 2 / b - → q 5 d -→ q 6 f -→ q 1 q 2 q 3 q 4 q 5 q 6 a -→ q ′ 1 q 2 q 3 q 4 q 5 q 6 , q 1 a -→ q ′ 1 q 3 e -→ q 5 d -→ q 6 f -→ q 1 q 2 q 3 q 4 q 5 q 6 a -→ q ′ 1 q 2 q 3 q 4 q 5 q 6 , q 1 a -→ q ′ 1 q 4 / c - → q 5 d -→ q 6 f -→
q 1 q 2 q 3 q 4 q 5 q 6 a -→ q ′ 1 q 2 q 3 q 4 q 5 q 6 . Indeed, all these rules respect the format (14).

Inhibiting relation

In this section, we provide a technical definition that will be instrumental in the rest of the paper.

Definition 15 We call a function f ∶ X → Y a choice function and write f ∶ X ⇉ Y ∶ (x).Φ(x, f ), where Φ(x, y) is a predicate over X × Y , if, for each x ∈ X, holds Φ x, f (x) .
For example, for a set R of rules in the format [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] above, the choice function

h ∶ R ⇉ ⋃ r∈R H r ∶ (r).h ∈ H r (15)
selects, for each rule r ∈ R, one of its negative premises. (It is well defined for a set of rules R, where each rule has at least one negative premise, i.e. H r ≠ ∅.)

Consider a family of disjoint sets of ports (P i ) n i=1 and a non-redundant set R of rules in format [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]:

r ∈ R ∶ q i a r ∩P i ----→ q ′ i i ∈ I r q i = q ′ i i ∉ I r q j / b r j -→ (j, b r j ) ∈ H r q 1 . . . q n a r --→ q ′ 1 . . . q ′ n .
Given an interaction a, we denote

R a = r ∈ R | a r = a ∧ H r ≠ ∅ , the set of rules
with the conclusion labelled by a, which have negative premises. Notice that, since R is non-redundant, there are two possibilities: either 1) there is exactly one rule in R with conclusion a and no negative premises, in which case R a = ∅; or 2) all rules with conclusion a have negative premises, in which case

R a = {r ∈ R | a r = a}.
Clearly, for the interaction a to be inhibited by the negative premises, one negative premise must be involved for each rule in R a .

We will now define the inhibiting relation π ⊆ 2 P × 2

2 P \{∅} \ ∅ by defining π(a)
for each interaction a among the conclusions of the rules in R, such that R a ≠ ∅. Intuitively, the set π(a) comprises all possible sets of interactions, formed by combining negative premises from all the rules with conclusion a, that would block a if enabled simultaneously. We need π(a) to be a set of sets of interactions, rather than a set of interactions, in order to distinguish, for example, two transitions

q j b r1 j --→ and q j b r2 j
--→ (with the same j) from a single one q j b r1 j b r2 j

-----→. Fix an interaction a as above and consider the choice function h in (15

) over R a , i.e. h ∶ R a ⇉ ⋃ r∈R a H r ∶ (r).h ∈ H r . We denote J h def = j ∈ [1, n] | ∃r ∈ R a ∶ h(r) = (j, ) (16)
the set of indices involved in the premises chosen by h. Notice that different premises can be associated to the same index in J h . Therefore, for a given choice h, we consider another choice function that selects, for each index in J h , the label of one premise among those chosen by h (recall [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]

that H r ⊆ [1, n] × 2 P , for each r ∈ R): b h ∶ J h ⇉ 2 P ∶ (j).(j, b h ) ∈ h(R a ) . (17)
Consider now the interaction b = ⋃ j∈J h b h (j). By construction of h, J h and b h , we have b ∩

P j = b h (j) (recall (11) that, for each (j, b j ) ∈ H r , we have b j ∈ 2 P j \ {∅}).
Hence, whenever b is enabled, we have q j b h (j)

----→, i.e. all the premises involved in the construction of b are dissatisfied. Thus, by combining all possible choices of b h we obtain a set of interactions that, if all are enabled, guarantees that each of the rules with the conclusion labelled by a has a dissatisfied premise, thereby effectively blocking a. In order to define π(a), we consider all possible choices of h to form a set of sets of interactions (in (18) below, we reproduce the definitions from ( 15), ( 16) and ( 17)):

π(a) def = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ ⋃ j∈J h b h (j) b h ∶ J h ⇉ 2 P ∶ (j).(j, b h ) ∈ h(R a ) h ∶ R ⇉ ⋃ r∈R H r ∶ (r).h ∈ H r , J h = j ∈ [1, n] | ∃r ∈ R a ∶ h(r) = (j, ) ⎫ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎭ . ( 18
)
To illustrate the need for π(a) to be a set of sets of ports, compare the following four sets of rules:

5 P 1 = {p}, P 2 = {r, s} q 1 p -→ q ′ 1 q 2 / rs -→ q 1 q 2 p -→ q ′ 1 q 2 π = (p, rs) P 1 = {p}, P 2 = {r}, P 3 = {s} q 1 p -→ q ′ 1 q 2 / r -→ q 1 q 2 q 3 p -→ q ′ 1 q 2 q 3 , q 1 p -→ q ′ 1 q 3 / s -→ q 1 q 2 q 3 p -→ q ′ 1 q 2 q 3 π = (p, rs) P 1 = {p}, P 2 = {r, s} q 1 p -→ q ′ 1 q 2 / r -→ q 1 q 2 p -→ q ′ 1 q 2 , q 1 p -→ q ′ 1 q 2 / s -→ q 1 q 2 p -→ q ′ 1 q 2 π = (p, r ⋅ s) P 1 = {p}, P 2 = {r}, P 3 = {s} q 1 p -→ q ′ 1 q 2 / r -→ q 3 / s -→ q 1 q 2 q 3 p -→ q ′ 1 q 2 q 3 π = (p, r), (p, s)
Definition 16 Given a family of disjoint sets of ports (P i ) n i=1 and a non-redundant set R of rules in format [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF], the corresponding inhibiting relation π is defined by [START_REF] Dezani-Ciancaglini | Sessions and session types: An overview[END_REF]. If, for each a in the domain of π, all sets in π(a) are singleton, we say that the inhibiting relation π is simple. We call complex inhibiting relations that are not simple.

Among the four examples above, only the third one is not simple. In the first and second examples, the set π(p) = {rs} contains one singleton set comprising the interaction rs. In the third example, π(p) = {r, s} contains one set comprising two singleton interactions r and s. Finally, in the fourth example, π(p) = {r}, {s} contains two singleton sets comprising singleton interactions r and s, respectively.

Simple and acyclic restrictions of BIP-like SOS

For the sake of rendering the expressiveness hierarchy more explicit, we consider the two restrictions of BSOS below.

First consider the operator defined by the rules

q 1 p -→ q ′ 1 q 2 / r -→ q 3 / s -→ q 1 q 2 q 3 p -→ q ′ 1 q 2 q 3 , q 2 r -→ q ′ 2 q 3 / s -→ q 1 q 2 q 3 r -→ q 1 q ′ 2 q 3 , q 2 r -→ q ′ 2 q 1 / p -→ q 1 q 2 q 3 r -→ q 1 q ′ 2 q 3 , q 3 s -→ q ′ 3 q 1 / p -→ q 1 q 2 q 3 s -→ q 1 q 2 q ′ 3 . ( 19
)
5 We denote by r ⋅ s the set of two singleton interactions r and s, as opposed to rs, which denotes one interaction consisting of the two ports. [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] with a simple and acyclic inhibiting relation.

We will denote by SiBSOS and AcBSOS the frameworks, which have the same semantic domain and atomic components as above, but use, respectively, simple and acyclic BIP-like SOS operators with the semantic mapping defined by the corresponding sets of rules in format [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF].

Note 3 Notice that, for any classical BIP operator (P i ) n i=1 , γ, π , the inhibiting relation of the set of BIP-like SOS rules defining its semantics coincides with π and, therefore, is simple and acyclic.

Modifications of BIP

Relaxation of priority models

The first option proposed in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF] is the relaxation of the priority model. The key point that distinguishes relaxed priority models from the classical ones is that π can be an arbitrary relation. Notice that we do not require the relation π to be acyclic or transitive. If all interactions involved in a cyclic dependency in π are enabled simultaneously, they block each other, potentially introducing a deadlock. We have also removed the restriction π ⊆ γ × γ, which requires a slight modification of semantics. Clearly, the behaviour of γ⟨C 1 , . . . , C n ⟩ does not have transitions, whereof labels are not in γ. Hence, the rules defining the semantics of a priority model will have no effect for all priorities outside γ × γ. Thus, we need to apply interaction and priority models simultaneously.

Given components

(C i ) n i=1 , such that σ(C i ) = (Q i , P i , - → i )
, the semantics of the simultaneous application of an interaction model γ and a priority model π is defined by putting

σ(πγ(C 1 , . . . , C n )) def = (Q, P, - → πγ ), with Q = ∏ n i=1 Q i and the minimal transition relation - → πγ inductively defined by the set of rules ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ q i a∩P i ----→ q ′ i i ∈ I {q i = q ′ i | i ∉ I} q j(b) / b∩P j(b) -----→ b ∈ π(a) q 1 . . . q n a -→ πγ q ′ 1 . . . q ′ n a ∈ γ, j ∶ π(a) ⇉ [1, n] ∶ (b).b ∩ P j ≠ ∅ ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ , ( 20
) where I = {i ∈ [1, n] | a ∩ P i ≠ ∅}.
The negative premises of each rule in [START_REF] Eker | Taming heterogeneity: The Ptolemy approach[END_REF] are determined by the choice function

j ∶ π(a) ⇉ [1, n] ∶ (b).b ∩ P j ≠ ∅.
Intuitively, for an interaction a to be blocked by a higher-priority interaction b, every rule with the conclusion labelled by a must have at least one of its premises violated. Here, for every such rule and for every higher-priority interaction b, we choose one component, i.e. that indexed by j(b), involved in b and test that the corresponding sub-interaction is disabled:

q j(b) / b∩P j(b)
-----→. Thus, whenever b is enabled, every rule authorising a has at least one of its premises violated.

We will denote by RBIP the framework that extends CBIP with relaxed operators using the semantic mapping defined by [START_REF] Eker | Taming heterogeneity: The Ptolemy approach[END_REF]. Notice that for the operators with classical priority models the classical and the modified semantics coincide.

BIP with complex priority relations

A further modification of BIP consists in extending priority models to rely on sets of interactions to inhibit another one, instead of a single interaction. This extension will allow us to recover the full expressiveness of BIP-like SOS through complex inhibiting relations.

Given components

(C i ) n i=1 , such that σ(C i ) = (Q i , P i , - → i )
, the semantics of the simultaneous application of an interaction model γ and a complex priority model π is defined by putting

σ(πγ(C 1 , . . . , C n )) def = (Q, P, - → πγ ), with Q = ∏ n i=1 Q i and the minimal transition relation - → πγ inductively defined by the set of rules ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ q i a∩P i ----→ q ′ i i ∈ I {q i = q ′ i | i ∉ I} q j(α) / b(α)∩P j(α) --------→ α ∈ π(a) q 1 . . . q n a -→ πγ q ′ 1 . . . q ′ n a ∈ γ, b ∶ π(a) ⇉ ⋃ π(a) ∶ (α).b ∈ α, j ∶ π(a) ⇉ [1, n] ∶ (α).b(α) ∩ P j ≠ ∅ ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ , (21)
where

I = {i ∈ [1, n] | a ∩ P i ≠ ∅}.
The negative premises of each rule in [START_REF] Felleisen | On the expressive power of programming languages[END_REF] are determined by two choice func-

tions b ∶ π(a) ⇉ ⋃ π(a) ∶ (α).b ∈ α and j ∶ π(a) ⇉ [1, n] ∶ (α).b(α) ∩ P j ≠ ∅.
Intuitively, for an interaction a to be blocked by a higher-priority set of interactions α, every rule with the conclusion labelled by a must have at least one of its premises violated. Here, for every such rule and for every higher-priority set of interactions α, the choice function b selects the interaction b(α) ∈ α, while the choice function j selects one of the components involved in b(α), i.e. such that b(α) ∩ P j(α) ≠ ∅. The corresponding premise q j(α)

/ b(α)∩P j(α)
--------→ tests whether b(α) is disabled. Thus, whenever all interactions in α are enabled, every rule authorising a has at least one of its premises violated.

We will denote by XBIP the framework which has the same semantic domain and atomic components as above, but uses complex BIP operators with the semantic mapping defined by [START_REF] Felleisen | On the expressive power of programming languages[END_REF].

Notice that by taking, for a relaxed priority model π ∈ 2 P × (2 P \ ∅), the complex priority model π def = (a, {b}) | (a, b) ∈ π , relaxed BIP operators can be canonically transformed into complex ones. The relaxed and the complex semantics for these operators coincide, since there is only one possible choice function b in the semantics (21) of π.

Extension of behaviour with the offer predicate

In the previous sections, we have observed that with the classical semantics information about transitions enabled in the components was lost after the application of the interaction model, preventing relaxed priority from taking effect. We have addressed this to some extent by modifying the way the semantics mapping is defined through combining the SOS rules for interaction and for priority models into one.

An alternative approach, consists in extending the definition of the component behaviour to integrate part of this information about the active transitions of its subcomponents. In order to do this we extend the notion of behaviour with an additional offer predicate [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF][START_REF] Bliudze | Synthesizing glue operators from glue constraints for the construction of component-based systems[END_REF]. The notable difference with the approach of the previous section is that information is made available about the active transitions of the atomic subcomponents at the lowest levels of the hierarchy instead of the one immediately underneath the considered one.

Definition 24 An extended behaviour is a quadruple B = (Q, P, -→, ↑), where (Q, P, -→) is an LTS and ↑ is an offer predicate on Q × P , such that q↑p holds (the port p ∈ P is offered in the state q ∈ Q) whenever there is a transition from q containing p, that is (∃a ∈ 2 P ∶ p ∈ a ∧ q a -→) ⇒ q↑p. The offer predicate extends to sets of ports: for a ∈ 2 P , q↑a def = ⋀ p∈a q↑p. Notice that q↑∅ ≡ true. We denote q a def = ¬(q↑a) = ⋁ p∈a q p. Definition 25 Two extended behaviours

B i = (Q i , P i , - → i , ↑ i ), with i = 1, 2, are equivalent if P 1 = P 2 and there exists a bisimulation relation R ⊆ Q 1 × Q 2 , total on both Q 1 and Q 2 ,
such that the offer predicates coincide on bisimilar states, i.e. for all (q 1 , q 2 ) ∈ R and p ∈ P 1 , holds q 1 ↑ 1 p ⇔ q 2 ↑ 2 p.

Note 4

In the rest of the paper we assume that all behaviours are extended. The classical and relaxed BIP as well as various formats of SOS rules require a simple modification of the corresponding semantic mapping in order to work with extended behaviours. Given a framework F = (G, C, B, ≃, σ), where the semantic domain (B, ≃) is the LTS with bisimilarity-based equivalence from Definition 10, we define the corresponding extended version

F ′ = (G, C, B ′ , ≃ ′ , σ ′ )
, where B ′ is the set of extended behaviours as in Definition 24, ≃ ′ is the equivalence from Definition 25 and the semantic mapping σ ′ is defined by putting σ

′ (C) def = (Q, P, - →, ↑), with (Q, P, - →) = σ(C) and q↑p def ⇔ ∃a ∈ 2 P ∶ p ∈ a ∧ q a -→, if C ∈ C, ∃i ∈ [1, n] ∶ q i ↑p, if C = o⟨C 1 , .
. . , C n ⟩ and q = (q 1 , . . . , q n ).

Notice that the predicate ↑ is defined by the same rule, for all composition operators.

In [START_REF] Bliudze | Synthesizing glue operators from glue constraints for the construction of component-based systems[END_REF], a set of composition operators has been proposed that utilise the information about offered ports. They are defined by the rules in the following format:

q i a∩P i ----→ q ′ i | i ∈ I q i = q ′ i | i ∉ I q k b k | (k, b k ) ∈ H q j ↑c j | j ∈ J q 1 . . . q n a -→ q ′ 1 . . . q ′ n , (22)
where

I = {i ∈ [1, n] | a ∩ P i ≠ ∅}, J ⊆ [1, n], c j ∈ 2 P j , for all j ∈ J, H ∈ [1, n]×2 P and for each (k, b k ) ∈ H holds b k ∈ 2 P k \ {∅}.
In [START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF], there are three types of premises respectively called firing, negative and activation premises. Firing and activation premises are collectively called positive. Notice that, while the firing premises are the same as in BSOS, the negative ones are based on a different predicate. Notice, furthermore, that q↑c 1 ∧q↑c 2 = q↑(c 1 ∪ c 2 ). Hence one activation premise per component is sufficient to define any inference rule.

Definition 26 An FNASOS operator is the composition operator defined as

(P i ) n i=1 ,
R , where (P i ) n i=1 are disjoint sets of ports and, denoting P def = ⋃ n i=1 P i , R is a nonredundant set of SOS rules in the format [START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF].

We denote by FNASOS the framework with the same atomic components as in CBIP, the semantic domain consisting of the set of extended behaviours and their equivalence as per Definition 24 and Definition 25, and the set of FNASOS composition operators with the semantic mapping defined by the corresponding sets of rules [START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF]. Sketch of the proof. The proof follows by taking the classical composition of SOS rules. Notice that, for any n-ary composition operator, the definition of the offer predicate can also be written as a set of SOS rules:

q i ↑p q 1 . . . q n ↑p i ∈ [1, n] . (23)
Thus, we only have to notice that this composition trivially preserves the format [START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF]. Indeed, for firing premises, the rules in the same format are substituted directly. For, negative and activation premises, substituted rules are in format [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF] and, therefore, negative premises are substituted by negative premises, witness premises-by witness premises.

Offer BIP

The offer predicate can be used instead of the transition relation for the definition of priorities. This offer semantics has been extensively studied in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF], where we have shown, among others, that instead of separating interaction and priority models, the same composition operators can be equivalently defined by including negative and activation port typings into interactions. Thus priorities are incorporated into extended interaction models, which can be encoded as Boolean formulas. In this paper we use this equivalent definition, since the Boolean encoding facilitates some of the proofs of expressiveness relations below. Notice, however, that this choice is purely a matter of convenience, since priority models can be defined explicitly in a straightforward manner, based on the inhibiting relation as in Section 3.2.3.

For a set of ports P , we denote Ṗ def = { ṗ | p ∈ P } and P def = {p | p ∈ P }. We call the elements of P , Ṗ and P activation, firing and negative port typings respectively.

Definition 27 For a given set of ports P , an extended interaction is a subset a ⊆ P ∪ Ṗ ∪ P . An extended interaction model is a set of extended interactions γ ⊆ 2 P ∪ Ṗ ∪P .

For a given extended interaction a, we define the following sets of ports:

-act(a) are disjoint sets of ports and, denoting

P def = ⋃ n i=1 P i , γ ⊆ 2 P ∪ Ṗ ∪P is an extended interaction model.
The semantics is defined for a set of components

C i such that σ(C i ) = (Q i , P i , - →, ↑) 6 , with i ∈ [1, n] by putting σ(γ⟨C 1 , . . . , C n ⟩) def = Q, P, - → γ , ↑ γ with Q = ∏ n i=1 Q i , the offer predicate ↑ γ defined by q 1 . . . q n ↑ γ p def ⟺ ∃i ∈ [1, n] ∶ q i ↑p
and the transition relation -→ γ inductively defined by the rule

a ∈ γ q i fire(a)∩P i -------→ q ′ i i ∈ I q i = q ′ i | i ∉ I q i ↑ act(a) ∩ P i | i ∈ [1, n] q i p | i ∈ [1, n], p ∈ neg(a) ∩ P i q 1 . . . q n fire(a) -----→ γ q ′ 1 . . . q ′ n , (24)
where

I = {i ∈ [1, n] | fire(a) ∩ P i ≠ ∅}.
We will denote by OBIP the framework, which has the same semantic domain and atomic components as FNASOS, but uses the set of offer BIP glue operators with the semantic mapping defined by (24).

Activation BIP

Finally, for the sake of comparison, we consider another framework, which mixes the classical and offer semantics by relying on the usual transition relation to define the semantics of priority models, but using the offer predicate for that of non-firing positive premises.

Definition 29 For given sets of ports P , an interaction with activation is a subset a ⊆ P ∪ Ṗ . An interaction model with activation is a set γ ⊆ 2 P ∪ Ṗ of interactions with activation.

Definition 30 An activation BIP glue operator is defined by (P i ) n i=1 , γ, π , where

(P i ) n i=1 are disjoint sets of ports, γ ⊆ 2 P ∪
Ṗ is an interaction model with activation and π ⊆ 2

P ∪ Ṗ × 2 2 P \{∅} \ {∅} is a priority model.
The semantics of the application of an operator

(P i ) n i=1 , γ, π is defined for any set of components C 1 , . . . , C n such that σ(C i ) = (Q i , P i , - → i , ↑ i ), for i ∈ [1, n], by putting σ(πγ⟨C 1 , . . . , C n ⟩) def = (Q, P, - → πγ , ↑ πγ ), with Q = ∏ n i=1 Q i and the minimal transition relation - → πγ satisfying the rule ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ q i fire(a)∩P i -------→ q ′ i | i ∈ I q i = q ′ i | i ∉ I q j(α) / b(α)∩P j(α) --------→ α ∈ π(a) q k ↑(a ∩ P k ) | k ∈ K q 1 . . . q n a -→ πγ q ′ 1 . . . q ′ n a ∈ γ, b ∶ π(a) ⇉ ⋃ π(a) ∶ (α).b ∈ α, j ∶ π(a) ⇉ [1, n] ∶ (α).b(α) ∩ P j ≠ ∅ ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ , (25)
where

I = {i ∈ [1, n] | a ∩ Ṗi ≠ ∅} and K = {k ∈ [1, n] | a ∩ P k ≠ ∅}.
The offer predicate ↑ πγ is defined as above by q 1 . . . q n ↑ πγ p def ⟺ ∃i ∈ [1, n] ∶ q i ↑ i p. We will denote by ABIP the framework, which has the same semantic domain and atomic components as FNASOS, but uses the set of activation BIP glue operators with the semantic mapping defined by [START_REF] Gössler | Language primitives and type discipline for structured communication-based programming[END_REF].

Proofs of the expressiveness relations

In this section we prove the relations depicted in Figure 1. First, in Section 4.1, we show in-depth comparison of classical BIP and simple BIP-like SOS explaining the limitations of CBIP and how one could circumvent them. Then, in Section 4.2, we prove the rest of relations between the different frameworks.

Note 5 Since the first element of all composition operators is the disjoint sets of ports (P i ) n i=1 , we will omit mentioning it explicitly in most of the following proofs. Indeed, if we want to apply two composition operators to the same sets of behaviours, their disjoint sets of ports have to be equal. Instead, we will speak of composition operators over P , where P = ⋃ n i=1 P i , with (P i ) n i=1 being mostly implicit.

By Lemma 3, all the frameworks considered in the paper are compositional. Furthermore, they all share the same set of atomic components and-the extension of behaviours with the offer predicate being canonical-the same semantic domain. Therefore, to prove strong/weak full expressiveness relations we will rely on Proposition 3. Thus we only have to exhibit operators that, given pairs of sets of components where corresponding pairs of components have the same behaviour, produce components with the same behaviour. In this context, the sets of states and ports, as well as offer predicates of the composed behaviours coincide trivially. Thus, in the proofs we will only check the equality of transition relations. The following lemma shows that it is not necessary to consider target states of transitions and it is sufficient to compare labels of outgoing transitions for each state of composed systems.

(o 1 ⟨C 1 , . . . , C n ⟩) = (Q, P, - → o 1 , ↑) and σ(o 2 ⟨C 1 , . . . , C n ⟩) = (Q, P, - → o 2 , ↑):
for any state q ∈ Q and for any transition label a ∈ 2

P , if q a -→ o 1 ⇔ q a -→ o 2 then q ′ | (q, a, q ′ ) ∈ - → o 1 = q ′ | (q, a, q ′ ) ∈ - → o 2 . Proof. If q / a -→ o 1 then q / a
-→ o 2 and both sets are empty. Suppose now that (q, a, q

′ ) ∈ - → o 1 , for some q ′ ∈ Q. Then q a -→ o 1 q
′ and, by the assumption of the lemma q a -→ o 2 . Furthermore, there exists a corresponding interaction a, interaction with activation or extended interaction b with fire(b) = a, or a rule r with the conclusion q

a -→ o 1 q ′ . Let q = (q i ) n i=1 and q ′ = (q ′ i ) n i=1
and notice that, for all BIP glues and all considered SOS rule formats, (q, a, q

′ ) ∈ - → o 1 if, for all i ∈ [1, n], q i a∩P i ----→ q ′ i , if a ∩ P i ≠ ∅, and q i = q ′ i otherwise. Since q a -→ o 2 ,
there exists an enabled rule in the semantics of o 2 with the conclusion a. Since the enabledness of the rule does not depend on the target states of the firing premises, we can consider the same firing premises as for o 1 , i.e.

q i a∩P i ----→ q ′ i , if a ∩ P i ≠ ∅. Hence, q a -→ o 2 q
′ and, therefore, {q ′ | (q, a, q

′ ) ∈ - → o 1 } = {q ′ | (q, a, q ′ ) ∈ - → o 2 }.

Expressiveness of the classical BIP

In [4, Example 2.9 and its discussion] we have shown an AcBSOS operator7 that cannot be expressed as a CBIP operator. In the following example we provide a simplified version of the one in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF] and an intuitive justification.

Example 8 Consider the BSOS operator defined by the following two rules:

q 1 p -→ q ′ 1 q 2 / r -→ q 1 q 2 q 3 p -→ q ′ 1 q 2 q 3 , q 2 r -→ q ′ 2 q 3 s -→ q ′ 3 q 1 q 2 q 3 rs -→ q 1 q ′ 2 q ′ 3 (26)
with the port partition P = {p}, {r}, {s} . Figure 4(b) shows the behaviour resulting from the application of this operator to the components in Figure 4(a). If this operator were to be realised by a single CBIP operator, then necessarily its interaction model would be γ = {p, rs}. Since rs is only enabled in the state 124, there is no way to define the priority model so as to suppress p in the states 124 and 125, but not in 134 and 135. Since operator ( 26) is simple and acyclic, we conclude that CBIP does not have strong full expressiveness w.r.t. SiBSOS and AcBSOS.

The example below shows that CBIP does not have even weak full expressiveness w.r.t. SiBSOS, whereas the subsequent proposition shows that it does have it w.r.t. AcBSOS.

Example 9 Consider a composition operator defined by the following two rules:

q 1 p -→ q ′ 1 q 1 / r -→ q 1 p -→ q ′ 1 , q 1 r -→ q ′ 1 q 1 / p -→ q 1 r -→ q ′ 1 , (27)
applied to the component shown in Figure 5(a). The behaviour of the composed component is shown in Figure 5(b). Assume that there exists a hierarchy of BIP glues, such that applying them to the same component results in an equivalent composed component. States 1 and 2 of the composed component behaviour have outgoing transitions p and r, respectively, thus all interaction models in the glues have to contain both interactions p and r. State 3 is a deadlock. Interaction models do not forbid any transition from this state and priority models cannot introduce deadlock by Lemma 4. This contradicts the assumption and, consequently, the set of rules ( 27) is not expressible in CBIP.

The two fundamental reasons for this lack of expressiveness are related to the definition of the priority model:

the information used by the priority model refers only to interactions authorised by the underlying interaction model-all the information about transitions enabled in sub-components is lost [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF]; -the priority model π must be a strict partial order.

As we explain below, among these two reasons, the first one is easily addressed to achieve weak, rather than strong, full expressiveness, whereas the second one presents the main difficulty.

What can be done without changing the BIP glue? As in Section 3.2.3, consider an n-ary BIP-like SOS operator o = (P i ) n i=1 , R with R a non-redundant set of rules

q i a r ∩P i ----→ q ′ i i ∈ I r q i = q ′ i | i ∉ I r q j / b r j -→ (j, b r j ) ∈ H r q 1 . . . q n a r --→ q ′ 1 . . . q ′ n , ( 28
)
for each r ∈ R, where, as before,

I r = i ∈ [1, n] | a r ∩ P i ≠ ∅ , H r ⊆ [1, n] × 2 P and, for each (j, b r j ) ∈ H r , holds b r j ∈ 2 P j . For an interaction a ∈ {a r | r ∈ R}, de- note R a def = {r ∈ R | a r = a ∧ H r ≠
∅} the set of rules with negative premises that have the conclusion labelled by a. Let π be the inhibiting relation of o (Definition 16).

Note 6 As for the transition relations and offer predicates, we will henceforth omit the indices on the semantic mappings σ, since they will be clear from the context. For instance, in the proof of the proposition below, σ will refer to both the semantic mapping of CBIP and that of AcBSOS.

Proposition 6 If π is simple and acyclic, then the operator o can be realised by a hierarchical composition of BIP glue operators.

Proof. Since π is acyclic, we can associate a depth d(a) to each interaction a involved in π as the length of the longest path leading to a in the directed acyclic graph defined by π. Denote

d def = max a d(a). Furthermore, for i ∈ [1, d], denote π i def = {(a, b) ∈ π | d(a) = i -1}.
Clearly all π i are strict partial orders. Furthermore

π i ⊆ π ⊆ γ 1 × γ 1 , for all i ∈ [1, d] and γ 1 = γ 2 ∪ b | a ∈ γ 2 , (a, b) ∈ π , where γ 2 = a r | r ∈ R .

Hence, for all

i ∈ [1, d], (γ 1 , π i ) is a BIP glue operator. The operator o is equivalent to the composition (γ 2 , ∅) • (γ 1 , π d ) • ⋅ ⋅ ⋅ • (γ 1 , π 1
). We show that for any set of components

C i with σ(C i ) = (Q i , P i , - →), for i ∈ [1, n], holds σ γ 2 ⟨π d γ 1 ⟨. . . π 1 γ 1 ⟨C 1 , . . . , C n ⟩ . . .⟩⟩ = σ(o⟨C 1 , . . . , C n ⟩). We denote B o = σ(o⟨C 1 , . . . , C n ⟩) , B πγ = σ γ 2 ⟨π d γ 1 ⟨. . . π 1 γ 1 ⟨C 1 , . . . , C n ⟩ . . .⟩⟩ .
The sets of states and ports of these behaviours are the same, thus we need to check only that their transition relations coincide.

Let q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B o .
This means that, among the rules defining o, i.e. for some r ∈ R, there is a rule

q i a∩P i ----→ q ′ i i ∈ I r q i = q ′ i i ∉ I r q j / b r j -→ (j, b r j ) ∈ H r q 1 . . . q n a -→ q ′ 1 . . . q ′ n , (29)
such that q i a∩P i ----→, for all i ∈ I, and q j / b r j -→ for all (j, b r j ) ∈ H r . By construction both γ 1 and γ 2 contain a. Hence, a is enabled in the state q 1 . . . q n of σ(γ 1 ⟨C 1 , . . . , C n ⟩) and in the same state of B πγ , provided that it is not disabled by any of priorities π 1 , . . . , π d . Thus, we have to show that no interaction available from this state has higher priority. By construction, priority rules that contain a in the left-hand side can appear only in π d(a)-1 , thus other priority models cannot block a. Priority rules of the form

a ≺ b have b = ⋃ s∈R a b s j(s) , for some j ∶ R a ⇉ [1, n] ∶ (s).(j, b s j ) ∈ H s .
Since all the premises of ( 29) are satisfied in q

1 . . . q n , interaction b r j(r) is disabled. Hence, b is also disabled. Thus q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B πγ . Let q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B πγ .
This means that both γ 1 and γ 2 contain the interaction a. Therefore, by the construction of γ 2 , there is at least one rule

q i a∩P i ----→ q ′ i i ∈ I q i = q ′ i i ∉ I q j / b j -→ (j, b j ) ∈ H q 1 . . . q n a -→ q ′ 1 . . . q ′ n , (30)
with conclusion labelled by a among the rules defining o. Furthermore, the priority model

π d(a)-1 contains priorities of the form a ≺ b, with b = ⋃ s∈R a b s j(s) , for all j ∶ R a ⇉ [1, n] ∶ (s).(j, b s j ) ∈ H s . Notice that a priority rule b ≺ c such that a ≺ b cannot appear in priorities π 1 , . . . , π d(a)-1 since d(b) ≥ d(a)+1.
Assume that none of rules defining o, with the conclusion labelled by a, applies in q 1 . . . q n a -→ q ′ 1 . . . q ′ n . This necessarily means that each of these rules has a negative premise that is not satisfied. Let b = ⋃ s∈R a b s j(s) with b s j(s) , for all s ∈ R a , being the labels of dissatisfied premises. Then b is an enabled interaction in σ(γ 1 ⟨C 1 , . . . , C n ⟩) such that a ≺ b and b cannot be blocked by priorities π 1 , . . . , π d(a)-1 . Consequently, b is enabled in σ(π d(a)-1 γ 1 ⟨. . . π 1 γ 1 ⟨C 1 , . . . , C n ⟩ . . .⟩) and blocks a, which contradicts the assumption q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B πγ . Hence, there is at least one rule of the form [START_REF] Mousavi | Semantics and expressiveness of ordered SOS[END_REF] in the definition of o with all premises satisfied in q 1 . . . q n and, therefore,

q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B o .
Thus, CBIP has weak full expressiveness w.r.t. AcBSOS.

What can be achieved by relaxing constraints on priority models? Instead of imposing additional constraints on the set of BIP-like SOS operators we can relax the priority model of BIP.

Definition 31 A semi-relaxed BIP operator is a triple (P i ) n i=1 , γ, π , where (P i ) n i=1
are disjoint sets of ports and, denoting P = ⋃ n i=1 P i , γ is an interaction model on P and π is a relaxed priority model on γ, π ⊆ γ × γ.

Notice that the priority model is not required to be a partial order but, contrary to the relaxed BIP (Definition 21), it can involve only interactions from the interaction model. Its semantics is defined exactly as that of classical priority models, by (8).

Given a simple BIP-like SOS operator o = (P i ) n i=1 , R , we consider its inhibiting relation π and the interaction models γ 1 , γ 2 as in the proof of Proposition 6. Since π ⊆ γ 1 ×γ 1 , the operator (γ 1 , π) is a semi-relaxed BIP operator. The operator o is then equivalent to the composition (γ 2 , ∅) • (γ 1 , π), where π is considered as a relaxed priority model.

Proposition 7 For any set of components (C i ) n i=1 with σ(C i ) = (Q i , P i , - →), for i ∈ [1, n], holds σ γ 2 ⟨πγ 1 ⟨C 1 , . . . , C n ⟩⟩ = σ(o⟨C 1 , . . . , C n ⟩) . Proof. Denote B o = σ(o⟨C 1 , . . . , C n ⟩) and B πγ = σ γ 2 ⟨πγ 1 ⟨C 1 , . . . , C n ⟩⟩ .
The sets of states and ports of these behaviours are the same. Thus, we need to check only that their transitions coincide.

Let q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B o .
This means that, among the rules defining o, i.e. for some r ∈ R, there is a rule

q i a∩P i ----→ q ′ i i ∈ I r q i = q ′ i i ∉ I r q j / b r j -→ (j, b r j ) ∈ H r q 1 . . . q n a -→ q ′ 1 . . . q ′ n , (31)
with all its premises satisfied for the respective behaviours σ(C i ). By construction both γ 1 and γ 2 contain a. Hence, a is enabled in the state q 1 . . . q n of σ(γ 1 ⟨C 1 , . . . , C n ⟩) and in the same state of σ(γ 2 ⟨πγ 1 ⟨C 1 , . . . , C n ⟩⟩), provided that it is not disabled by the priority π. Thus, we have to show that no interaction available from this state has higher priority.

Priority rules in π that contain a are of the form a ≺ b,

with b = ⋃ s∈R a b s j(s) , for some j ∶ R a ⇉ [1, n] ∶ (s).(j, b s j ) ∈ H s .
Since all the premises of (31) are satisfied in q 1 . . . q n , interaction b r j(r) is disabled. Hence, b is also disabled. Thus

q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B πγ . Let q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B πγ .
This means that both γ 1 and γ 2 contain the interaction a. Therefore, by the construction of γ 2 , there is at least one rule

q i a∩P i ----→ q ′ i i ∈ I q i = q ′ i i ∉ I q j / b j -→ (j, b j ) ∈ H q 1 . . . q n a -→ q ′ 1 . . . q ′ n , (32)
among the rules defining o. Furthermore, the priority model π has to contain priorities of the form a ≺ b,

with b = ⋃ s∈R a b s j(s) , for some j ∶ R a ⇉ [1, n] ∶ (s).(j, b s j ) ∈ H s .
Assume now that none of the rules defining o, with the conclusion labelled by a, applies in q 1 . . . q n . Since q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B πγ , this necessarily means that each of these rules has a negative premise that is not satisfied. Let b = ⋃ s∈R a b s j(s) with b s j(s) , for all s ∈ R a , being the labels of dissatisfied premises. Then b is an enabled interaction such that a ≺ b, which contradicts the assumption

q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B πγ .
Hence, there is at least one rule of the form [START_REF] Park | Concurrency and automata on infinite sequences[END_REF] in the definition of o with all premises satisfied in q 1 . . . q n and, therefore,

q 1 . . . q n a -→ q ′ 1 . . . q ′ n in B o .
Thus, we conclude that semi-relaxed BIP (same as RBIP, but with semi-relaxed glue operators instead of relaxed ones) has weak full expressiveness w.r.t. SiBSOS.

Notice that the relaxed priority model defined over the interaction model does not allow recovering strong full expressiveness. For instance, consider the operator defined by the single rule (2 P \∅) is a strict partial order, without requiring that it refers only to interactions (i.e. we do not impose π ⊆ γ × γ). This relaxation does not recover even weak full expressiveness w.r.t. simple BIP-like SOS operators. Indeed, Example 9 is still not expressible.

q 1 p -→ q ′ 1 q 1 / r -→ q 1 p -→ q ′ 1 , (33)

Comparison of the modifications of BIP and SOS formats

In this section, we provide the proofs for the expressiveness comparison between various BIP glues and SOS rules formats shown in Figure 1.

CBIP → AcBSOS and CBIP ⇒ SiBSOS: As shown in Section 4. Example 11 Consider two components in Figure 7(a) and the activation BIP glue operator {p}, {r, s} , { ṗr, ṙ, ṡ}, ∅ . The semantics of this operator is given by the rules

q 1 p -→ q ′ 1 q 2 ↑r q 1 q 2 p -→ q ′ 1 q 2 , q 2 r -→ q ′ 2 q 1 q 2 r -→ q 1 q ′ 2 , q 2 s -→ q ′ 2 q 1 q 2 s -→ q 1 q ′ 2 . ( 34
)
The composed component behaviour (shown in Figure 7(b) without the offer predicate) has a transition p only in the state 12. Suppose that there exists a hierarchy of BIP-like SOS operators with the equivalent semantics. All of them must contain rules allowing transitions r and s. However it is not possible to allow transition p from state 12 but not from state 13, since the only negative premise that can be used to block it is q 2 / s -→ and it would block p in both states.

ABIP WBSOS: Activation BIP does not have weak full expressiveness w.r.t. WBSOS as shown in the following example.

Example 12 Consider two components shown in Figure 8(a) and the WBSOS operator defined by the following set of rules:

q 1 p -→ q ′ 1 q 2 rs -→ q 1 q 2 p -→ q ′ 1 q 2 , q 2 r -→ q ′ 2 q 1 q 2 r -→ q 1 q ′ 2 , q 2 s -→ q ′ 2 q 1 q 2 s -→ q 1 q ′ 2 , q 2 rs -→ q ′ 2 q 1 q 2 rs -→ q 1 q ′ 2
.

Consider the states 12 and 13 of the composed component behaviour (shown in Figure 8(b) with ports offered in each state shown in parentheses): the former does not have an outgoing transition p while the latter does. In ABIP any interaction with the firing support p would allow the transition p from both states, since the two states are indistinguishable in terms of the offer predicate. Thus the transition p from the state 12 has to be blocked by a relaxed priority model. However, any priority rule blocking this transition in the state 12 also blocks it in the state 13 since the set of enabled transitions in the state 12 is a subset of the set of transitions enabled in the state 13. Thus, this system is inexpressible in ABIP.

The converse is shown by another example. Consider an activation BIP operator o 2 = {p, r}, γ 2 , π 2 , with γ 2 = { ṗr} and π = ∅ applied to the composed component o 1 ⟨C⟩. Both ports p and r are offered in the state 1 of σ o 1 ⟨C⟩ , thus the interaction ṗr is enabled in this state despite the fact that the state does not have any outgoing transition involving r. In the state 2, r is not offered and the interaction is not enabled.

Consider now the (witness) BIP-like SOS operator o ′ 1 defined by the rules

q p -→ q ′ q p -→ o ′ 1 q ′ , q r -→ q ′ q / p -→ q r -→ o ′ 1 q ′ .
Clearly, σ(o

′ 1 ⟨C⟩) = σ(o 1 ⟨C⟩
). However, it is not possible to construct a witness BIP-like SOS operator that applied to o ′ 1 ⟨C⟩ would result in a component with behaviour equivalent to σ(o 2 ⟨o 1 ⟨C⟩⟩). Indeed, it is not possible to distinguish states 1 and 2, since they have the same sets of outgoing transitions in σ(o 1 ⟨C⟩). Thus, WBSOS does not have strong full expressiveness w.r.t. AcBSOS and, since WBSOS possesses uniform flattening, it does not have weak full expressiveness either.

BSOS ⇒ WBSOS: Witness BSOS is an extension of BSOS, thus, trivially, it has strong full expressiveness w.r.t. BSOS. Example 12 presents a system with a WBSOS operator inexpressible in ABIP and, consequently, in BSOS.

OBIP ⇔ FNASOS: It is clear by comparing [START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF] and ( 24) that any offer BIP operator can be encoded in FNASOS. The inverse also holds: for any SOS rule in the FNASOS format [START_REF] Gößler | Priority systems[END_REF], we can provide a corresponding extended interaction, where firing, activation and negation supports are obtained from firing, activation and negative premises respectively. Since FNASOS possesses uniform flattening we can conclude the same for OBIP. The incomparability of CBIP and OBIP was shown in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF]. The same reasoning as in Example 9 proves that the offer BIP composition operator ({p, r}, γ) with γ = { ṗr, ṙp}, whereof the semantics is given by the rules

q 1 p -→ q ′ 1 q 1 r q 1 p -→ q ′ 1 , q 1 r -→ q ′ 1 q 1 p q 1 r -→ q ′ 1 ,
is inexpressible in CBIP. The following example from [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF] presents a system inexpressible in OBIP.

Example 14 Consider the atomic components shown in Figure 10 and the classical BIP composition operator {p, r}, {s} , γ, π with the interaction model γ = {p, r, pr, s} and priority model π = {s ≺ pr}. Since, classical priority semantics refers to the enabledness of an interaction, in the behaviour of the composed system the interaction s is available in the state 14, but not in the state 24. In the offer semantics, all three ports are offered in both states 14 and 24 of this system. Therefore, these two states are indistinguishable and s cannot be inhibited in only one of them by any hierarchical composition of OBIP operators. 9.

Consider the offer BIP glue operator o 3 = {p, r}, γ 3 , with γ 3 = { ṗr} applied to the composed component o 1 ⟨C⟩. Both ports p and r are offered in the state 1, thus the interaction ṗr is enabled in this state despite the fact that the state does not have any outgoing transition involving r. In the state 2, r is not offered and the interaction is not enabled.

As in Example 13, it is not possible to construct a hierarchy of witness BIP-like SOS operators corresponding to o 3 , since the states 1 and 2 have the same sets of outgoing transitions in σ(o 1 ⟨C⟩) and are, therefore, indistinguishable by witness BIP-like SOS operators.

Additional results for flat systems

In the previous section, we have analysed the expressiveness relations among the introduced frameworks. In particular, we have shown that WBSOS, ABIP and OBIP are pairwise incomparable. It is interesting to observe that, when restricted to flat systems, i.e. those consisting of one operator applied to sets of atomic components, a comparison can be established: every OBIP operator can be expressed as an ABIP operator and every ABIP operator can be expressed as a WBSOS one.

The restriction to atomic components is crucial here: indeed, the equivalence q↑p ⇔ ∃a ∶ q a -→ ∧ p ∈ a holds only on atomic components.

For any set of atomic components

C 1 , . . . , C n ∈ C with σ(γ⟨C 1 , . . . , C n ⟩) = Q, P, -
→, ↑ , and for any state q ∈ Q, the valuation v q = (p = q↑p) p∈P satisfies φ a (denoted v q ⊧ φ a ) if and only if some extended interaction from I a is enabled in the state q.

For a given valuation v ⊧ φ a , we build an interaction with activation b

v a = ṗ | p ∈ fire(a) ∪ p | v(p) = true ∧ p ∉ fire(a)
and an associated set of priorities

π v a = b v a ≺ {c} | c ∈ 2 P ∧ ∃p ∈ c ∶ v(p) = false .
The activation BIP glue operator equivalent to γ is õ =

(P i ) n i=1 , γ ′ , π ′ , with -an interaction model with activation γ ′ = b v a | a ∈ γ, v ⊧ φ a , -a complex priority model π ′ = ⋃ a∈γ ⋃ v∈Part a π v a .
Consider a set of atomic components C 1 , . . . , C n ∈ C and suppose that q fire(a)

-----→ in σ(γ⟨C 1 , . . . , C n ⟩) for some a ∈ γ. Let v q = (p = q↑p) p∈P be the valuation induced by the offer predicate in the state q. We have v q ⊧ φ a . By construction of γ ′ , we

have b = { ṗ | p ∈ fire(a)}∪{p | v q (p) = true ∧ p ∉ fire(a)} ∈ γ ′ .
Notice that all ports of b are offered in the state q and fire(b) = fire(a). Thus, q fire(b)

-----→ in σ(γ ′ ⟨C 1 , . . . , C n ⟩). By construction of π ′ , all interactions with higher priority contain a port p, such that v q (p) = false, i.e. p is not offered in the state q and, consequently, none of these interactions is enabled in q. Thus, q fire(a)

-----→ in σ(π ′ γ ′ ⟨C 1 , . . . , C n ⟩). Suppose now that q fire(b) -----→ in σ(π ′ γ ′ ⟨C 1 , . . . , C n ⟩) for some b ∈ γ ′ and take v = (p = p ∈ fire(b) ∪ act(b)) p∈P . Since b is enabled, we have v(p) ⇒ q↑p.
Suppose that, for some p ∈ P , we have q↑p ∧ ¬v(p). Since all the components are atomic, there is an interaction c enabled in q such that p ∈ c. By construction of π ′ , there is a priority rule b ≺ {c} that would block b in the state q, contradicting the assumption q fire(b) -----→. Hence, we have v(p) ⇔ q↑p, for all p ∈ P . Let I b = {a ∈ γ | fire(a) = fire(b)} and a Boolean formula φ b built as above. By construction, v ⊧ φ b . Since v(p) ⇔ q↑p, this means that some interaction from I b is enabled in the state q of σ(γ⟨C 1 , . . . , C n ⟩) and, therefore,

q fire(b) -----→ in σ(γ⟨C 1 , . . . , C n ⟩).
Despite the fact that ABIP does not have strong full expressiveness w.r.t. OBIP, for any system obtainable in OBIP from a given set of atomic components, we can build an equivalent one in ABIP from the same set of atomic components. Indeed, since FNASOS (hence, also OBIP) possesses uniform flattening, any hierarchy of OBIP operators can be replaced by a single operator. By Proposition 8, there exists a corresponding one in ABIP. These operators applied to the same set of atomic components would result in equivalent systems.

A WBSOS composition operator equivalent to a given ABIP operator (P i ) n i=1 , γ, π on atomic components can be constructed as follows. Given an interaction with activation a ∈ γ, we consider a set of witness BIP-like SOS rules S a obtained by removing all redundant rules from the set

⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ q i fire(a)∩P i -------→ q ′ i i ∈ I q i = q ′ i | i ∉ I q j(α) / b(α)∩P j(α) --------→ α ∈ π(a) q k c∩P k ----→ c ∈ J, k ∈ K c q 1 . . . q n fire(a) -----→ q ′ 1 . . . q ′ n J ⊆ 2 P , s.t. act(a) ⊆ ⋃ c∈J c ; b ∶ π(a) ⇉ ⋃ π(a) ∶ (α).b ∈ α, j ∶ π(a) ⇉ [1, n] ∶ (α).b(α) ∩ P j ≠ ∅ ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ , (36)
where

I = {i ∈ [1, n] | fire(a) ∩ P i ≠ ∅} and K c = {k ∈ [1, n] | c ∩ P k ≠ ∅}.
In the positive premises we require a set of transitions J that has to be enabled in the state of the composed component such that each port from the activation support of a is involved in at least one transition and, consequently, offered (since we only consider atomic components here). In the negative premises, we require all higher-priority sets of interactions to be disabled. , ⋃ a∈γ S a , with S a the set of rules [START_REF] Sobocinski | A non-interleaving process calculus for multi-party synchronisation[END_REF], for each a ∈ γ. Then, for any set of atomic components C 1 , . . . , C n , we have σ(πγ⟨C 1 , . . . , C n ⟩) = σ(o⟨C 1 , . . . , C n ⟩).

Proof. Let q d -→ in σ(πγ⟨C 1 , . . . , C n ⟩). There exists an interaction with activation a ∈ γ such that fire(a) = d, q↑p holds for all p ∈ act(a), and none of the higher-priority sets of interactions α ≻ a are enabled. Consider the set of interactions J that are enabled in the state q of the unrestricted parallel composition of

C 1 , . . . , C n , i.e. J = c ⊆ P | (c ∩ P i = ∅) ∨ q i c∩P i ---→ in σ(C i ) , i ∈ [1, n] .
Notice that act(a) ⊆ ⋃ c∈J c, since all ports in act(a) are offered. By construction of the operator o, there is a subset of rules in S a with the activation premises defined by J. Since all interactions in J are enabled, these activations premises are satisfied in q. Since none of the sets α ≻ a is enabled, we can choose, for each α, the cor- [START_REF] Sobocinski | A non-interleaving process calculus for multi-party synchronisation[END_REF], the choice function realisations b ∶ α ↦ b α and j ∶ α ↦ j α , we obtain a rule in S a8 , whereof the negative premises are also satisfied and we have q

responding b α ∈ α and j α ∈ [1, n], such that q j α / b α ∩P jα ------→. By taking, in
d -→ in σ(o⟨C 1 , . . . , C n ⟩). Let q d -→ in σ(o⟨C 1 , . . . , C n ⟩).
There is a rule r ∈ S a , for some a ∈ γ, that allows this transition in the composed component behaviour. Let J be the set of interactions defining the activation premises in r. Notice that all interactions c ∈ J are enabled in the state q. By construction of r, fire(a) = d. For all ports p ∈ act(a), there is an interaction c ∈ J, such that p ∈ c. Hence, q↑p. For each set of interactions α ≻ a, there is one negative premise in r. Since this premise is satisfied, α is disabled. Thus, the interaction a is enabled in the state q and q d -→ in σ(πγ⟨C 1 , . . . , C n ⟩).

Related Work

The results in this paper build mainly on our own previous work. However, the following related work should also be mentioned.

Usually, formalisms are compared by flattening structure and reducing to a behaviourally equivalent model, e.g. automata and Turing machines. In this manner, all finite state formalisms turn out to be expressively equivalent independently of the features used for the composition of behaviours. Many models and languages are Turing-expressive, while their coordination capabilities are tremendously different. [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] A first framework formally capturing meanings of expressiveness for sequential programming languages and taking into account not only the semantics but also the primitives of languages was provided in [START_REF] Felleisen | On the expressive power of programming languages[END_REF]. It allows formal reasoning about and distinguishing between core elements of a language and syntactic sugar. Although a number of studies have taken a similar approach in the context of concurrency, we will point only to [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF] and the references therein. The key difference of our approach lies in the strong separation between the computation and coordination aspects of the behaviour of concurrent systems. Indeed, we consider that all sequential computation resides within the components of the system that are not subject to any kind of modification. Thus, we focus on the following question:

what system behaviour can be obtained by coordination of a given set of concurrent components?

An extensive overview of SOS formats is provided in [START_REF] Mousavi | SOS formats and meta-theory: 20 years after[END_REF], including some results comparing their expressiveness. More results comparing different formats of SOS can be found in [START_REF] Mousavi | Semantics and expressiveness of ordered SOS[END_REF]. The expressiveness property is closely related to the translation between languages. One of the definitions of encoding compared with other approaches can be found in [START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF]. It should be noted, however, that the above mentioned separation of concerns principle also leads to a very simple rule format. Indeed, the format that we consider is essentially a small subset of GSOS. Our focus in this paper, is more on the expressiveness of the coordination mechanism provided by BIP than on that of the various SOS rule features.

There exist several works comparing BIP with various connector frameworks. A comparative study of three connector frameworks-tile model [16], wire calculus [START_REF] Sobocinski | A non-interleaving process calculus for multi-party synchronisation[END_REF] and BIP [8]-was presented in [START_REF] Bruni | Connector algebras, petri nets, and bip[END_REF]. An attempt to relate BIP and Reo has been made recently [START_REF] Dokter | Relating BIP and reo[END_REF]. From the operational semantics perspective, these comparisons only take in account operators with positive premises. In particular, priority in BIP is not considered, whereas it is central for the present paper.

Finally, in our formalisation of component-based frameworks, we rely on the notion of "behaviour type". This can cover a very large spectrum, ranging from programs and labelled transition systems, through OSGi bundles and browser plug-ins, to systems of differential equations etc. Behaviour types can be organised in type systems and studied separately, as, for example, in the co-algebra theory [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF]. However, this notion should be distinguished, for instance, from classes in object-oriented programming or session [START_REF] Dezani-Ciancaglini | Sessions and session types: An overview[END_REF]26] and behavioural [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF] types for communication protocols. For instance, the notion of a class could be compared to that of a behaviour type in our sense as follows: a program would typically comprise a multitude of classes, whereas a component framework has only one underlying behaviour type. Although, in principle, component-based frameworks can be heterogeneous, e.g. Ptolemy II [START_REF] Eker | Taming heterogeneity: The Ptolemy approach[END_REF], that is rely on several distinct behaviour types for the design process, those aimed at the design of executable systems must have an underlying unifying behaviour type allowing the study and manipulation of a system as a whole.

Conclusion

Our previous investigations [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF] of several properties that we consider fundamental for component-based design frameworks have revealed that the often encountered informal statement: "BIP possesses the expressiveness of the universal glue" (or its equivalent in slightly different formulations) is based on an erroneous proposition in previous work [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]Proposition 4]. We have, therefore, undertook an additional study of BIP expressiveness, whereof the results have been presented in this paper.

To achieve this goal, we rely on the algebraic formalisation of the notion of component-based design framework introduced in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF] and refined in this paper. We have defined two new comparison relations among component-based frameworks, weak and strong full expressiveness, which characterise whether systems that can be constructed in one framework can also be constructed in the other. Although these properties are stronger than the corresponding expressiveness preorders introduced in [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF], they provide a simpler setup for the comparison of the expressiveness of component-based frameworks. The notion of weak full expressiveness is different from the weak expressiveness preorder in [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]: the former relaxes the strong form of the property by allowing hierarchical composition of glue operators, whereas the latter considers only flat operators, but allows a limited use of additional coordinating behaviour. Studying the combination of the two relaxations could be an interesting direction for future work.

We have studied the weak and full expressiveness of BIP w.r.t. operators defined by SOS rules in a particular format, which we call BIP-like SOS, and some of its restrictions. The set of all the operators that can be defined using BIP-like SOS rules is the "universal glue", w.r.t. which full expressiveness has been erroneously claimed in [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]. The two restrictions that we consider are characterised by the so-called inhibiting relation, which identifies the interactions, enabledness whereof inhibits that of another given one. The first restriction, SiBSOS, considers only sets of BIP-like SOS rules with simple inhibiting relations, where the enabledness of one interaction is always sufficient to inhibit another one. To the contrary, operators defined by sets of rules with complex inhibiting relations might require a combination of interactions to be enabled simultaneously to inhibit one given interaction.

Semantics of BIP operators is defined in terms of rules with only simple inhibiting relations. We observe, however, that there are two obstacles to achieving strong full expressiveness w.r.t. SiBSOS: 1) a BIP priority model is required to be a strict partial order on interactions and 2) by the definition of the BIP operational semantics, priorities can only be applied to interactions that appear in the interaction model. The combination of these two requirements ensures that priorities cannot introduce new deadlocks. However, negative premises in BIP-like SOS rules-which correspond to priorities in BIP glue operators-can do so. In order to introduce deadlocks, the inhibiting relation must have cycles. We show that BIP glue operators have weak full expressiveness w.r.t. BIP-like SOS operators that have acyclic inhibiting relations, with at most d + 1 layers of glue necessary to encode a BIP-like SOS operator, whereof the depth of the inhibiting relation is A relaxation of both of the above requirements together recovers strong full expressiveness w.r.t. SiBSOS. However, it calls for a definition of the operational semantics of BIP glue operators, which combines the interaction and the priority models, as opposed to the classical definition, where the interaction model is applied first, then the priority model is applied to the resulting component.

A relaxation of only the first requirement, which does not require any other modifications of the BIP semantics, leads to weak full expressiveness w.r.t. SiBSOS. Moreover, we have shown that at most two layers of glue are necessary to encode any operator.

In order to achieve the expressive power of the full BIP-like SOS format, we have defined an extension of BIP, called XBIP, which allows priorities to use combinations of interactions.

In order to put the above results into a broader perspective, we have also analysed the expressiveness relations among several variations of BIP semantics and SOS formats used to define these. In particular, we have considered two new types of premises that can be used to define glue operators. The offer predicate q↑p (and its negative form q p) is used to access information about the activation of the port p in the current state of the corresponding atomic component. Another variation, witness BIP-like SOS, using premises of the form q a -→, allows testing the enabledness of an interaction in the current global state without firing it.

The offer predicate is used to define the homonymous, offer semantics of BIP, introduced in [START_REF] Bliudze | Synthesizing glue operators from glue constraints for the construction of component-based systems[END_REF] and studied extensively in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF]. The Offer BIP turns out to be largely incomparable to other variations of BIP considered in the paper. The advantages of offer BIP, as outlined in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF], are that it possesses a number of nice properties, in particular strong full expressiveness w.r.t. the rule format used to define its semantics and flattening. More importantly, contrary to classical BIP and the variations obtained by adding positive premises, offer BIP lends itself nicely to a Boolean encoding and, therefore, efficient implementations using, for instance, Binary Decision Diagrams as in JavaBIP [START_REF] Bliudze | Exogenous coordination of concurrent software components with JavaBIP[END_REF].

As mentioned above, studying the combination of the two weak forms of full expressiveness-allowing both hierarchical glue and limited use of additional coordinating behaviour-could be an interesting direction for future work. Another direction for future work would consist in exploring the expressiveness of the full BIP framework, including the data manipulation and transfer as formalised in [14].

Fig. 1

 1 Fig. 1 Expressiveness relations among the considered frameworks.

Example 3

 3 In addition to CCS -from Example 1, consider the framework CCS = (G, C, B, ≃, σ), where C, B and ≃ are the same as in CCS -, whereas G = G -∪{+},

i 1 , 1 k ) ≃ σ 2 (C 2 k 2 k ) = σ 2 (C 2 k

 11222 . . . , C i n ∈ C, and two sets of atomic componentsC i 1 , . . . , C i n ∈ C (for i = 1, 2), such that σ 1 (C ), for all k ∈ [1, n].Since, by the assumption of the proposition, σ 1 (C ), we have by[START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF]

σ πγ⟨C 1 , C 2 ⟩Fig. 2

 122 Fig. 2 Components and behaviour for Example 5

Fig. 3

 3 Fig. 3 Components for Example 6

Proposition 4

 4 WBSOS possesses uniform flattening.

Definition 20

 20 Let P be a set of ports. A relaxed priority model on P is a relation π ⊆ 2 P × (2 P \ {∅}).

Proposition 5 FNASOS

 5 possesses uniform flattening.

def=

  a ∩ P , the activation support of a, -fire(a) def = {p ∈ P | ṗ ∈ a}, the firing support of a, -neg(a) def = {p ∈ P | p ∈ a}, the negative support of a. Definition 28 An offer BIP glue operator is defined by (P i ) n i=1 , γ , where (P i ) n i=1

Lemma 5

 5 Let (C i ) n i=1 be a set of components, with σ(C i ) = (Q i , P i , -→, ↑), and let P = ⋃ n i=1 P i . Let o 1 and o 2 be composition operators over P . Then, the following statement holds for behaviours of composed systems σ

Fig. 4 Fig. 5

 45 Fig. 4 Component and behaviour for Example 8

1 p-→ 3 . 3 p-

 133 applied to a component with the behaviour in Figure5. The composed component behaviour has a single transition The interaction model of BIP cannot contain r, as it is not possible to exclude transition 2 r -→ 3 with a priority model. The transition → 3 has to be excluded by the priority model, however it cannot use r in the priority model. Further relaxation of the definition of BIP operators by removing the restriction π ⊆ γ × γ results exactly in the relaxed BIP (Definition 21). With this relaxation we obtain strong full expressiveness w.r.t. SiBSOS, since any simple BIP-like SOS operator o is then clearly equivalent to (γ 2 , π) with γ 2 containing interactions that label conclusions of the rules defining o (as in the proof of Proposition 6), while π is the inhibiting relation of o. Thus, RBIP has strong full expressiveness w.r.t. SiBSOS. Consider another relaxation of the definition of BIP glue operators, by taking operators (P i ) n i=1 , γ, π , with P = ⋃ n i=1 P i , such that the priority model π ⊆ 2 P ×

Fig. 7 Fig. 8

 78 Fig. 7 Components and behaviour for Example 11

Fig. 9

 9 Fig. 9 An atomic component (a) and the behaviour after application of the first glue operator (b) in Examples 13, 15 and 16 (ports offered in each state are shown in parentheses)

Example 13

 13 Consider the atomic component C shown in Figure 9(a) and an activation BIP glue operator o 1 = {p, r}, γ, π , with γ = { ṗ, ṙ} and π = {r ≺ {p}}. The behaviour of o 1 ⟨C⟩ is shown in Figure 9(b).

Corollary 3

 3 OBIP possesses uniform flattening.

Fig. 10

 10 Fig. 10 Atomic components for Example 14

Proposition 8

 8 When restricted to flat systems, every OBIP operator can be expressed as an ABIP one:∀n ∈ N, ∀o ∈ OBIP n , ∃õ ∈ ABIP n ∶ ∀C 1 , . . . , C n ∈ C, σ(õ⟨C 1 , . . . , C n ⟩) ≃ σ(o⟨C 1 , . . . , C n ⟩) . (35)Proof. Consider an OBIP glue operator o = (P i ) n i=1 , γ , with γ an extended interaction model on P = ⋃ n i=1 P i . For a given extended interaction a ∈ γ we denote I a = {b ∈ γ | fire(b) = fire(a)} the set of all interactions in γ with the same firing support as a. Consider the following Boolean formula on P :φ a = ⋀ p∈fire(a)

Proposition 9

 9 Let (P i ) n i=1 , γ, π be an ABIP operator and take a WBSOS operator o = (P i ) n i=1

Definition 5

 5 Based on the full expressiveness relations, we introduce six comparison relations, presented in Table1. For instance (second cell of the first row), if F 1 has strong full expressiveness w.r.t. F 2 , whereas F 2 has only weak-but not strong-full expressiveness w.r.t. F 1 , we say that F 1 is weakly more expressive than F 2 (alternatively, F 2 is weakly less expressive than F 1 ) and denote this by F 2 → F 1 . The full expressiveness relations from Example 3 mean that CCS is strongly more expressive than CCS

	Example 4

-, i.e. CCS -⇒ CCS .

  then F 1 is weakly more expressive than F 2 . Finally, if there exists an operator in G 1 that cannot be represented by any combination of operators in G 2 , then F 1 is strongly more expressive than F 2 . If such inexpressible operators exists in both G 1 and G 2 then F 1 and F 2 are incomparable (third row of Table

  and a composed component o 2 ⟨o 1 ⟨C 1 , C 2 , C 3 ⟩⟩. Transition p in σ(o 2 ⟨o 1 ⟨C 1 , C 2 , C 3 ⟩⟩) is available only in states where r was not enabled inσ(o 1 ⟨C 1 , C 2 , C 3 ⟩).In particular, in the state 135, p is available, since r is blocked by s in the second rule defining o 1 . To the contrary, in the state 136, p is blocked by r in the first rule defining o 2 . The only difference between the active actions in the global states 135 and 136 is that s is active in 135, but not in 136. Thus, to obtain the same behaviour as in o 2 ⟨o 1 ⟨C 1 , C 2 , C 3 ⟩⟩ using a single BIP-like SOS operator, we have to test the activity of s.

  It has the simple inhibiting relation π = (p, r), (p, s), (r, ps), (s, p) . Notice that the (singleton) interactions p and s form a cycle in the inhibiting relation and they would block each other if enabled simultaneously.Since all sets in the codomain of a simple inhibiting relation are singleton, they can be systematically opened, e.g. replacing (a, {b}) by (a, b), without loss of information. This implies that a simple inhibiting relation on 2Definition 17 We say that a simple inhibiting relation is acyclic if it does not have any cycles when considered as a relation on 2 i=1 are disjoint sets of ports and R is a non-redundant set of BIP-like SOS rules[START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] with a simple inhibiting relation.[START_REF] Dokter | Relating BIP and reo[END_REF] An acyclic BIP-like SOS operator is a composition operator defined as (P i )

		P × 2 2	P \{∅} \ ∅
	can be equivalently considered as a relation on 2
	Definition 18 A simple BIP-like SOS operator is a composition operator defined as (P i ) n i=1 , R , where (P i )
	Definition n i=1 , R , where (P i )	n i=1 are disjoint sets of ports and R is a non-redundant
	set of BIP-like SOS rules

P × (2 P \ {∅}). P × (2 P \ {∅}).

n

  Definition 21 A relaxed BIP operator is a triple (P i )

	n i=1 , γ, π), where (P i )	n i=1 are
	disjoint sets of ports and, denoting P

def = ⋃ n i=1 P i , γ ⊆ 2

P is an interaction model and π ⊆ 2 P × (2 P \ {∅}) is a relaxed priority model.

  Definition 22 Let P be a set of ports. A complex priority model on P is a relation

	n i=1 are
	disjoint sets of ports,

π ⊆ 2 P × 2 2 P \{∅} \ {∅} . Definition 23 A complex BIP operator is a triple (P i ) n i=1 , γ, π , where (P i ) γ ⊆ 2 P is an interaction model and π ⊆ 2 P × 2 2 P \{∅} \ {∅} is a complex priority model.

  1, CBIP has weak full expressiveness w.r.t. AcBSOS and does not have even weak full expressiveness w.r.t. SiBSOS. Example 8 shows that CBIP does not have strong full expressiveness w.r.t. AcBSOS. Since the semantic mapping of CBIP is defined through acyclic BIP-like SOS (see Note 3), both AcBSOS and SiBSOS have strong full expressiveness w.r.t. CBIP. SiBSOS: As observed in Section 4.1, RBIP has strong full expressiveness w.r.t. SiBSOS. On the other hand, the semantic mapping of RBIP is defined through sets of rules in the BIP-like SOS format with simple inhibiting relations. Thus SiBSOS also has strong full expressiveness w.r.t. RBIP. RBIP: Follows from CBIP ⇒ SiBSOS and RBIP ⇔ SiBSOS by Corollary 1. Component and behaviour for Example 10 RBIP ⇒ XBIP: XBIP is an extension of RBIP, thus it has strong full expressiveness w.r.t. RBIP. The following example shows that RBIP does not have weak full expressiveness w.r.t. XBIP. Example 10 Consider an XBIP operator {p}, {r, s} , γ = {p, r, s}, π = (p, {r, s}) applied to components shown in Figure6(a). The behaviour of the composed component is shown in Figure6(b). Assume there exists a hierarchy of RBIP operators such that applying them to the same components results in an equivalent composed one. Clearly, all interaction models have to involve p, thus transition p from the state 12 must be blocked by a relaxed priority model. If this priority model contains p ≺ r or p ≺ pr, then the transition p would also be blocked in the state 13. Similarly, for p ≺ s or p ≺ ps and the state 14. Priority rules p ≺ rs and p ≺ prs cannot be applied in any state, since they require that transition rs be available (see[START_REF] Eker | Taming heterogeneity: The Ptolemy approach[END_REF] and notice that r and s belong to the interface of the same component). Thus, no priority rule can block p only in the state 12. BSOS: The semantic mapping of XBIP is defined in terms of the BIPlike SOS format, implying that BSOS has strong full expressiveness w.r.t. XBIP. On the other hand, given any BIP-like SOS composition operator o = (P i ) , where γ is the set of interactions labelling the conclusions of the rules in R and π is the inhibiting relation, is clearly equivalent to o. Hence, XBIP also has strong full expressiveness w.r.t. BSOS. SiBSOS: Since AcBSOS is a restriction of SiBSOS, the latter has strong full expressiveness w.r.t. the former. On the other hand, AcBSOS does not have weak full expressiveness w.r.t. SiBSOS. Indeed, that would imply that so does CBIP, which is not the case, since we have already established CBIP ⇒ SiBSOS. BSOS: Follows from SiBSOS ⇔ RBIP, RBIP ⇒ XBIP and XBIP ⇔ BSOS by Corollary 1. ABIP: Clearly, ABIP is an extension of XBIP. Thus, it has strong full expressiveness w.r.t. XBIP. The following example shows that BSOS does not have weak full expressiveness w.r.t. ABIP. By Lemma 1, since XBIP ⇔ BSOS, this implies that XBIP does not have weak full expressiveness w.r.t. ABIP either.

			r		s
				2					12
	p	p	r	r	s	s		r	r	s	s
	1		3		4	p	13			14	p
		(a) Atomic components			(b) Composed behaviour
	Fig. 6 n i=1 , R , the XBIP operator (P i ) n i=1 , γ, π

RBIP ⇔ CBIP ⇒ XBIP ⇔ AcBSOS ⇒ SiBSOS ⇒ XBIP ⇒

  Example 14 shows that OBIP does not have weak full expressiveness w.r.t. CBIP. Since we have CBIP ⇒ RBIP ⇒ XBIP ⇒ ABIP, this means that OBIP does not have weak full expressiveness w.r.t. ABIP either. The following example shows that ABIP does not have weak full expressiveness w.r.t. OBIP, i.e. OBIP and ABIP are incomparable. 15 Consider an atomic component C shown in Figure 9(a). Both ports p and r are offered in the state 1, while only p is offered in the state 2. Consider the offer BIP glue operator o 1 = {p, r}, γ , with γ = { ṗ, ṙp}. The behaviour of the composed component is shown in Figure 9(b). Notice that the offer predicates of σ(C) and σ(o 1 ⟨C⟩) coincide. Consider the offer BIP glue operator o 2 = {p, r}, γ 2 , with γ 2 = { ṗr} applied to the composed component o 1 ⟨C⟩. Both ports p and r are offered in the state 1, thus the interaction ṗr is not enabled in this state despite the fact that the state does not have any outgoing transition involving r. Consider now the activation BIP operator o ′ 1 = {p, r}, γ, π , with γ = { ṗ, ṙ} and π = {r ≺ {p}}. Clearly σ(o ′ 1 ⟨C⟩) = σ(o 1 ⟨C⟩). However, there is no activation BIP glue operator or a hierarchy of operators that, applied to o ′ 1 ⟨C⟩ would produce a component equivalent to o 2 ⟨o 1 ⟨C⟩⟩. Indeed, this would require forbidding the transition p from the state 1 without forbidding it from the state 2, as is the case in σ(o 2 ⟨o 1 ⟨C⟩⟩). Indeed, we have to keep ṗ in the interaction model, since 2 By the same argument as above, Example 14 shows that OBIP does not have weak full expressiveness w.r.t. WBSOS. The following example proves that they are incomparable. 16 Consider the same atomic component C and the same o 1 as in Example 15. Component C and the behaviour of o 1 ⟨C⟩ are shown in Figure

	Example
	Example p -→ 1,
	but there are no transitions from state 1 that could be used to inhibit p through
	a complex priority model.

OBIP ABIP:

OBIP WBSOS:

As opposed to a (non-strict) partial order, which is a reflexive, antisymmetric and transitive relation, a strict partial order is an irreflexive and transitive (hence also antisymmetric) one.

As in Note 1, we omit the indices on ↑, whenever they are clear from the context.

We have only introduced the term "AcBSOS" in the present paper. In[START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF], we speak of composition operators defined by sets of SOS rules.

The rule S a might be removed from the operator o as redundant, however this would imply the existence of another rule with the same conclusion and whereof premises would also be satisfied in the state q.

Acknowledgments

The contribution of Simon Bliudze to the work presented in this paper has been partially funded by Hauts-de-France regional STaRS programme under the grant agreement № 2019.00170.