A Calculus for Open Ensembles and Their Composition

Abstract

We consider specifications of dynamically evolving ensembles consisting of entities which collaborate through message exchange. Each ensemble specification defines a set of messages, a set of process type declarations and an initial ensemble state. An ensemble state is given by a set of process instances that can trigger the creation of further process instances during ensemble evolution. We distinguish between internal and external messages of an ensemble. Internal messages are exchanged between the participants of a single ensemble while the external messages can be considered as ensemble interfaces which give rise to a composition operator for open ensemble specifications. A structural operational semantics for open ensemble specifications is provided based on two levels: a process and an ensemble level. We define an equivalence relation for ensemble specifications which generalizes bisimulation to dynamic architectures. As a main result we prove that equivalence of ensemble specifications is preserved by ensemble composition. We also introduce a semantic composition operator on the level of labeled transition systems and show that it is compatible with the syntactic composition of ensemble specifications; i.e. our semantics is compositional.

This work has been partially sponsored by the European Union under the FP7-project ASCENS, 257414.

Appendix

Proof of Theorem 1 :

By assumption, $EnsSpec 1$ and $EnsSpec 2$ have the same signature. Hence,$EnsSpec 1 \otimes EnsSpec$ and $EnsSpec 2 \otimes EnsSpec$ have the same signature. In the following of the proof let $EnsSpec 1 = (\varSigma ', Decls 1,\sigma 1_0)$, $EnsSpec 2 = (\varSigma ', Decls 2,\sigma 2_0)$ and $EnsSpec = (\varSigma , Decls ,\sigma _0)$. Let $T1 = (S1, \sigma 1_0, L1, \xrightarrow {}_1)$ be the semantics of $EnsSpec 1$, $T2 = (S2, \sigma 2_0, L2, \xrightarrow {}_2)$ be the semantics of $EnsSpec 2$, and let $T = (S, \sigma _0, L, \xrightarrow {})$ be the semantics of $EnsSpec$. W.l.o.g. we assume (*): For all $\sigma _1 \in S1, \sigma _2 \in S2, \sigma \in S$ we have $dom (\sigma _1) \cap dom (\sigma ) = \emptyset$ and $dom (\sigma _2) \cap dom (\sigma ) = \emptyset$. Let $\varDelta = \{(\sigma 1,\sigma 2,\varphi ) \mid \sigma 1 \in S1 , \sigma 2 \in S2, \varphi : dom (\sigma 1) \rightarrow dom (\sigma 2)~ is~bijective \}$. By assumption, there exists a bijective function $\varphi _0: dom (\sigma 1_0) \rightarrow dom (\sigma 2_0)$ and a bisimulation $R \subseteq \varDelta$, such that $(\sigma 1_0,\sigma 2_0,\varphi _0) \in R$. By definition,

$$\begin{aligned}&EnsSpec 1 \otimes EnsSpec = (\varSigma ' \otimes \varSigma , Decls 1 \cup Decls , \sigma 1_0+\sigma _0), and\\&EnsSpec 2 \otimes EnsSpec = (\varSigma ' \otimes \varSigma , Decls 2 \cup Decls , \sigma 2_0+\sigma _0) \end{aligned}$$

Obviously, $\varphi _0$ can be extended to a bijective function $(\varphi _0+ id _{ dom (\sigma _0)}):$ $dom (\sigma 1_0+\sigma _0) \rightarrow dom (\sigma 2_0+\sigma _0)$ such that $(\varphi _0+ id _{ dom (\sigma _0)})(i) = \varphi _0(i)$ if $i \in dom (\sigma 1_0)$ and $(\varphi _0+ id _{ dom (\sigma _0)})(i) = i$ if $i \in dom (\sigma _0)$.

Now, let $T1^\otimes = (S1^\otimes , \sigma 1_0+\sigma _0, L1^\otimes , \xrightarrow {}_1^\otimes )$ be the semantics of $EnsSpec 1 \otimes EnsSpec$ and $T2^\otimes = (S2^\otimes , \sigma 2_0+\sigma _0, L2^\otimes , \xrightarrow {}_2^\otimes )$ be the semantics of $EnsSpec 2 \otimes EnsSpec$. Let $\varDelta ^\otimes = \{(\sigma 1^\otimes ,\sigma 2^\otimes ,\varphi ^\otimes ) \mid \sigma 1^\otimes \in S1^\otimes , \sigma 2^\otimes \in S2^\otimes , \varphi ^\otimes : dom (\sigma 1^\otimes ) \rightarrow dom (\sigma 2^\otimes )~ is~bijective \}$. We have to construct a bisimulation $R^\otimes \subseteq \varDelta ^\otimes$, such that $(\sigma 1_0+\sigma _0,\sigma 2_0+\sigma _0,\varphi _0+ id _{ dom (\sigma _0)}) \in R^\otimes$. For this purpose, we define

Clearly, $(\sigma 1_0+\sigma _0, \sigma 2_0+\sigma _0, \varphi _0+ id _{ dom (\sigma _0)}) \in R^\otimes$. It remains to prove that $R^\otimes$ is a bisimulation between $T1^\otimes$ and $T2^\otimes$. We will prove the first four cases (1.1)–(1.4) of Definition 9. The other cases are symmetric. Assume $(\sigma 1^\otimes ,\sigma 2^\otimes ,\varphi ^\otimes ) \in R^\otimes$, i.e. $\sigma 1^\otimes$ is of the form $\sigma 1+\sigma , \sigma 2^\otimes = \sigma 2+\sigma$ and $\varphi ^\otimes = \varphi + id _{ dom (\sigma )}$ such that $(\sigma 1,\sigma 2,\varphi ) \in R$.

• (1.1) Let $\sigma 1^\otimes \xrightarrow { pi :m!}^\otimes _1 \sigma 1'^\otimes$ be a transition in $T1^\otimes$ with an external message m! of $\varSigma ' \otimes \varSigma$. According to the semantics of ensemble specifications, the transition is induced by a transition on the process level of the form such that $pi \in dom (\sigma 1^\otimes )$ and $\sigma 1^\otimes ( pi ) = P$ and $\sigma 1'^\otimes = \sigma 1^\otimes {\scriptstyle [ pi \mapsto P']}$. Since m! is an external message of $\varSigma ' \otimes \varSigma$, it is an external message of $\varSigma '$ or of $\varSigma$.

  If m! is an external message of $\varSigma '$, the transition induces a transition $\sigma 1 \xrightarrow { pi :m!}_1 \sigma 1'$ in T1 with $pi \in dom (\sigma 1)$ and $\sigma 1( pi ) = P$ and $\sigma 1' = \sigma 1{\scriptstyle [ pi \mapsto P']}$. Since R is a bisimulation between T1 and T2, there exists $\sigma 2 \xrightarrow {\varphi ( pi ):m!}_2 \sigma 2'$, such that $(\sigma 1',\sigma 2',\varphi ) \in R$. This transition is induced by a transition on the process level of the form such that $\varphi ( pi ) \in dom (\sigma 2)$ and $\sigma 2(\varphi ( pi )) = Q$ and $\sigma 2' = \sigma 2{\scriptstyle [\varphi ( pi ) \mapsto Q']}$. Taking into account that $\sigma 2^\otimes = \sigma 2+\sigma$, the transition induces also a transition $\sigma 2^\otimes \xrightarrow {\varphi ( pi ):m!}_2^\otimes \sigma 2'^\otimes$ in $T2^\otimes$ with $\sigma 2'^\otimes = \sigma 2'+\sigma$. Since $(\sigma 1,\sigma 2,\varphi ) \in R$, $\sigma 1'^\otimes = \sigma 1'+\sigma$, $\sigma 2'^\otimes = \sigma 2'+\sigma$, we have $(\sigma 1'^\otimes ,\sigma 2'^\otimes ,\varphi ^\otimes ) \in R^\otimes$.

  If m! is an external message of $\varSigma$, the transition induces a transition $\sigma \xrightarrow { pi :m!} \sigma '$ in T with $pi \in dom (\sigma )$ and $\sigma ( pi ) = P$ and $\sigma ' = \sigma {\scriptstyle [ pi \mapsto P']}$. Then $\sigma 1'^\otimes = \sigma 1+\sigma '$. But the transition induces also a transition $\sigma 2^\otimes \xrightarrow { pi :m!}_2^\otimes \sigma 2'^\otimes$ in $T2^\otimes$ such that $\sigma 2'^\otimes = \sigma 2+\sigma '$. Since $(\sigma 1,\sigma 2,\varphi ) \in R$ we then have also $(\sigma 1'^\otimes ,\sigma 2'^\otimes ,\varphi ^\otimes ) \in R^\otimes$.

• (1.2) This case is proved analogously to (1.1).

• (1.3) Let $\sigma 1^\otimes \xrightarrow { pi :\mathbf{create }( fresh (\sigma 1^\otimes ))}^\otimes _1 \sigma 1'^\otimes$ be a transition in $T1^\otimes$. The transition is induced by a transition on the process level of the form such that $pi \in dom (\sigma 1^\otimes )$ and $\sigma 1^\otimes ( pi ) = P1$ and $\sigma 1'^\otimes =$ $\sigma 1^\otimes {\scriptstyle [ pi \mapsto P1']+[ fresh (\sigma 1^\otimes ) \mapsto Q1]}$. Since $\sigma 1^\otimes$ is of the form $\sigma 1+\sigma$ with $\sigma 1 \in S1$ and $\sigma \in S$, we consider two cases (a) and (b).

  (a) $pi \in dom (\sigma 1)$: Then induces a transition$\sigma 1 \xrightarrow { pi :\mathbf{create }( fresh (\sigma 1))}_1 \sigma 1'$ in T1 such that $\sigma 1' = \sigma 1{\scriptstyle [ pi \mapsto P1']+[ fresh (\sigma 1) \mapsto Q1]}$. Since R is a bisimulation between T1 and T2, there exists$\sigma 2 \xrightarrow {\varphi ( pi ):\mathbf{create }( fresh (\sigma 2))}_2 \sigma 2'$ in T2 such that $(\sigma 1',\sigma 2',\varphi ') \in R$ with $\varphi ' = \varphi {\scriptstyle +[ fresh (\sigma 1) \mapsto fresh (\sigma 2)]}$. This transition is induced by a transition on the process level of the form such that $\varphi ( pi ) \in dom (\sigma 2)$ and $\sigma 2(\varphi ( pi )) = P2$ and $\sigma 2' = \sigma 2{\scriptstyle [\varphi ( pi ) \mapsto P2']+[ fresh (\sigma 2) \mapsto Q2]}$.

  The transition induces also a transition$\sigma 2^\otimes \xrightarrow {\varphi ( pi ):\mathbf{create }( fresh (\sigma 2^\otimes ))}^\otimes _2 \sigma 2'^\otimes$ in $T2^\otimes$ with $\varphi ( pi ) \in dom (\sigma 2^\otimes )$ and $\sigma 2^\otimes (\varphi ( pi )) = P2$ and $\sigma 2'^\otimes = \sigma 2^\otimes {\scriptstyle [\varphi ( pi ) \mapsto P2']+[ fresh (\sigma 2^\otimes ) \mapsto Q2]}$. Taking into account the assumption (*) from above on disjointness of definition domains, we have $fresh (\sigma 1) \notin dom (\sigma )$ and $fresh (\sigma 2) \notin dom (\sigma )$. Since $\sigma 1^\otimes = \sigma 1+\sigma$ and $\sigma 2^\otimes = \sigma 2+\sigma$, we can assume $fresh (\sigma 1^\otimes ) = fresh (\sigma 1)$ and $fresh (\sigma 2^\otimes ) = fresh (\sigma 2)$. Hence, $\sigma 1'^\otimes = \sigma 1'+\sigma$ and $\sigma 2'^\otimes = \sigma 2'+\sigma$. Since $(\sigma 1',\sigma 2',\varphi ') \in R$, we get $(\sigma 1'^\otimes ,\sigma 2'^\otimes ,\varphi '^\otimes ) \in R^\otimes$ with $\varphi '^\otimes$ defined as $\varphi ^\otimes {\scriptstyle +[ fresh (\sigma 1^\otimes ) \mapsto fresh (\sigma 2^\otimes )]}$ which is the same as $\varphi '+ id _{ dom (\sigma )}$ since $\varphi ^\otimes {\scriptstyle +[ fresh (\sigma 1^\otimes ) \mapsto fresh (\sigma 2^\otimes )]} =$ $\varphi ^\otimes {\scriptstyle +[ fresh (\sigma 1) \mapsto fresh (\sigma 2)]} = \varphi {\scriptstyle +[ fresh (\sigma 1) \mapsto fresh (\sigma 2)]}+ id _{ dom (\sigma )} = \varphi '+ id _{ dom (\sigma )}$.⁹

  (b) $pi \in dom (\sigma )$: Then induces a transition$\sigma \xrightarrow { pi :\mathbf{create }( fresh (\sigma ))} \sigma '$ in T such that $\sigma ' = \sigma {\scriptstyle [ pi \mapsto P1']+[ fresh (\sigma ) \mapsto Q1]}$.

  induces also a transition $\sigma 2^\otimes \xrightarrow { pi :\mathbf{create }( fresh (\sigma 2^\otimes ))}^\otimes _2 \sigma 2'^\otimes$ in $T2^\otimes$. Since $pi \in dom (\sigma ), \sigma 1^\otimes = \sigma 1+\sigma$ and $\sigma 2^\otimes = \sigma 2+\sigma$, we assume, similarly as in case (a), $fresh (\sigma 1^\otimes ) = fresh (\sigma ) = fresh (\sigma 2^\otimes )$. Hence, $\sigma 1'^\otimes = \sigma 1+\sigma '$ and $\sigma 2'^\otimes = \sigma 2+\sigma '$. Since $(\sigma 1,\sigma 2,\varphi ) \in R$, we get $(\sigma 1'^\otimes ,\sigma 2'^\otimes ,\varphi '^\otimes ) \in R^\otimes$ with $\varphi '^\otimes$ defined as $\varphi + id _{ dom (\sigma ')}$.

• (1.4) Let $\sigma 1^\otimes \xrightarrow {( pi \rightarrow qi ):m}_1^\otimes \sigma 1'^\otimes$ be a transition in $T1^\otimes$. This transition is induced by two transitions on the process level of the form such that $pi , qi \in dom (\sigma 1^\otimes )$, $\sigma 1^\otimes ( pi ) = P1, \sigma 1^\otimes ( qi ) = Q1$ and $\sigma 1'^\otimes = \sigma 1^\otimes {\scriptstyle [ pi \mapsto P1', qi \mapsto Q1']}$. Since $\sigma 1^\otimes$ is of the form $\sigma 1+\sigma$ with $\sigma 1 \in S1$ and $\sigma \in S$, we consider four cases (a), (b), (c) and (d) with (c) ((d) resp.) being the most interesting ones.

  (a) $pi , qi \in dom (\sigma 1)$: Then induce a transition$\sigma 1 \xrightarrow {( pi \rightarrow qi ):m}_1 \sigma 1'$ in T1 such that $\sigma 1' = \sigma 1{\scriptstyle [ pi \mapsto P1', qi \mapsto Q1']}$. Hence, $\sigma 1'^\otimes = \sigma 1'+\sigma$. Since R is a bisimulation between T1 and T2, there exists$\sigma 2 \xrightarrow {(\varphi ( pi ) \rightarrow \varphi ( qi )):m}_1 \sigma 2'$ in T2 such that $(\sigma 1',\sigma 2',\varphi ) \in R$. This transition is induced by transitions on the process level of the form such that $\sigma 2' = \sigma 2{\scriptstyle [\varphi ( pi ) \mapsto P2', \varphi ( qi ) \mapsto Q2']}$. The transitions induce also a transition $\sigma 2^\otimes \xrightarrow {(\varphi ( pi ) \rightarrow \varphi ( qi )):m}_2^\otimes \sigma 2'^\otimes$ in $T2^\otimes$ such that $\sigma 2'^\otimes = \sigma 2'+\sigma$. Since $\sigma 1'^\otimes = \sigma 1+\sigma '$ and $(\sigma 1',\sigma 2',\varphi ) \in R$, we get $(\sigma 1'^\otimes ,\sigma 2'^\otimes ,\varphi ^\otimes ) \in R^\otimes$.

  (b) $pi , qi \in dom (\sigma )$: Then induce a transition$\sigma \xrightarrow {( pi \rightarrow qi ):m} \sigma '$ in T such that $\sigma ' = \sigma {\scriptstyle [ pi \mapsto P1', qi \mapsto Q1']}$. Hence, $\sigma 1'^\otimes = \sigma 1+\sigma '$. The transitions induce also a transition $\sigma 2^\otimes \xrightarrow {( pi \rightarrow qi ):m}_2^\otimes \sigma 2'^\otimes$ in $T2^\otimes$ such that $\sigma 2'^\otimes = \sigma 2+\sigma '$. Since $\sigma 1'^\otimes = \sigma 1+\sigma '$ and $(\sigma 1,\sigma 2,\varphi ) \in R$, we get $(\sigma 1'^\otimes ,\sigma 2'^\otimes ,\varphi ^\otimes ) \in R^\otimes$.

  (c) $pi \in dom (\sigma 1)$ and $qi \in dom (\sigma )$: Then m! is an external message of $\varSigma '$ and induces a transition $\sigma 1 \xrightarrow { pi :m!}_1 \sigma 1'$ in T1 with $pi \in dom (\sigma 1)$, $\sigma 1( pi ) = P1$ and $\sigma 1' = \sigma 1{\scriptstyle [ pi \mapsto P1']}$. Moreover, m? is an external message of $\varSigma$ and induces a transition $\sigma \xrightarrow { qi :m?} \sigma '$ in T with $qi \in dom (\sigma )$, $\sigma ( qi ) = Q1$ and $\sigma ' = \sigma {\scriptstyle [ pi \mapsto Q1']}$. Hence, $\sigma 1'^\otimes = \sigma 1'+\sigma '$.

  Since R is a bisimulation between T1 and T2, there exists $\sigma 2 \xrightarrow {\varphi ( pi ):m!}_2 \sigma 2'$ in T2, such that $(\sigma 1',\sigma 2',\varphi ) \in R$. This transition is induced by a transition on the process level of the form such that $\varphi ( pi ) \in dom (\sigma 2)$, $\sigma 2(\varphi ( pi )) = P2$ and $\sigma 2' = \sigma 2{\scriptstyle [\varphi ( pi ) \mapsto P2']}$.

  Then, the transitions and induce also a transition $\sigma 2^\otimes \xrightarrow {(\varphi ( pi ) \rightarrow qi ):m}_2^\otimes \sigma 2'^\otimes$ in $T2^\otimes$ such that $\sigma 2'^\otimes = \sigma 2'+\sigma '$. Since $\sigma 1'^\otimes = \sigma 1'+\sigma '$ and $(\sigma 1',\sigma 2',\varphi ) \in R$, we get $(\sigma 1'^\otimes ,\sigma 2'^\otimes ,\varphi ^\otimes ) \in R^\otimes$.

  (d) $pi \in dom (\sigma )$ and $qi \in dom (\sigma 1)$: The proof is analogous to case (c).       $\square$

Proof of Theorem 2 :

Let $T1 = (S1, \sigma 1_0, L1, \xrightarrow {}_1)$, $T2 = (S2, \sigma 2_0, L2, \xrightarrow {}_2)$, $T1 \otimes T2 = (S1 \otimes S2,$ $(\sigma 1_,\sigma 2_0), L1 \otimes L2, \xrightarrow {}_\otimes )$, and $T^\otimes = (S^\otimes , \sigma 1_0+\sigma 2_0, L^\otimes , \xrightarrow {}^\otimes )$. Since for the construction of $T1 \otimes T2$ we have assumed that the states in S1 and S2 have disjoint definition domains, we can define a bijection $\beta : S1 \otimes S2 \rightarrow S^\otimes$ such that $\beta ((\sigma 1,\sigma 2)) = \sigma 1+\sigma 2$. To show that $\beta ((\sigma 1,\sigma 2))$ is indeed in $S^\otimes$ and that $\beta$ preserves and reflects transitions we perform an induction on the length of the derivation to reach states in $S1 \otimes S2$ and in $S^\otimes$. The base case holds, since $\beta ((\sigma 1_0,\sigma 2_0)) = \sigma 1_0+\sigma 2_0 \in S^\otimes$. For each direction we show as an example one induction step.The other cases are similar.

(open output left): Let $m! \in \varSigma 1_{ ext }, m? \notin \varSigma 2_{ ext }$ and $(\sigma 1,\sigma 2) \xrightarrow { pi :m!}_\otimes (\sigma 1',\sigma 2)$ because of $\sigma 1 \xrightarrow { pi :m!}_1 \sigma 1'$. Then $\sigma 1 \xrightarrow { pi :m!}_1 \sigma 1'$ is induced by by a transition on the process level of the form such that $pi \in dom (\sigma 1)$, $\sigma 1( pi ) = P$ and $\sigma 1' = \sigma 1{\scriptstyle [ pi \mapsto P']}$. By induction hypothesis, $\beta ((\sigma 1,\sigma 2)) = \sigma 1+\sigma 2 \in S^\otimes$. Then, the transition induces also a transition $\sigma 1+\sigma 2 \xrightarrow { pi :m!}^\otimes \sigma 1'+\sigma 2$ in $T^\otimes$. Hence $\beta ((\sigma 1',\sigma 2)) \in S^\otimes$.

Conversely, let $\sigma ^\otimes \xrightarrow { pi :m!}^\otimes \sigma '^\otimes$ be a transition in $T^\otimes$ with an external message m! of $\varSigma 1 \otimes \varSigma 2$. The transition is induced by a transition on the process level of the form such that $pi \in dom (\sigma ^\otimes )$, $\sigma ^\otimes ( pi ) = P$ and $\sigma '^\otimes = \sigma ^\otimes {\scriptstyle [ pi \mapsto P']}$. By induction hypothesis, $\sigma ^\otimes = \beta ((\sigma 1,\sigma 2)) = \sigma 1+\sigma 2$ such that $\sigma 1 \in T1, \sigma 2 \in T2$ with $dom (\sigma 1) \cap dom (\sigma 2) = \emptyset$. W.l.o.g. we consider the case $m! \in \varSigma 1_{ ext }$. Then, $pi \in dom (\sigma 1)$. Hence, the transition induces also a transition $\sigma 1 \xrightarrow { pi :m!}_1 \sigma 1'$ in T1 such that $\sigma 1' = \sigma 1{\scriptstyle [ pi \mapsto P']}$. Therefore, $\sigma '^\otimes = \sigma 1'+\sigma 2 = \beta ((\sigma 1',\sigma 2))$. Since m! is external in $\varSigma 1 \otimes \varSigma 2$, we have $m? \notin \varSigma 2_{ ext }$. Thus we can apply the rule (open output left) and get $(\sigma 1,\sigma 2) \xrightarrow { pi :m!}_\otimes (\sigma 1',\sigma 2)$.       $\square$