Associative composition of components with double-sided interfaces

Abstract

Distributed systems are often organized in chains of components (e.g. business process chains), where each component naturally has a double-sided (left and right) interface. We suggest a corresponding, highly abstract and general framework (in mathematical terms: a monoid) of components and their composition, with minimal assumptions on the underlying global infrastructure (in fact, just a global set of symbols). As a fundamental property, decisive for the composition of more than two components, composition of such properties turns out to be associative. We discuss a number of instantiations of this framework (mainly classes of Petri nets), some of which preserve important properties (such as soundness of workflows) under composition. We glance at a number of generalizations and specializations.

Appendix: Proof of the theorem

For component models X,Y, in the sequel we write

$$\begin{aligned} XY \text { for } Y \cdot Y \end{aligned}$$

(11)

Let G, H and K be component models. To prove the Theorem, with Definition 2 we have to show:

$$\begin{aligned}&\text {The nodes of } (GH)K \text { and of } G(HK) \text { coincide}.\end{aligned}$$

(12)

$$\begin{aligned}&\text {The arcs of } (GH)K \text { and of } G(HK) \text { coincide,}\end{aligned}$$

(13)

$$\begin{aligned}&^{*}{}{((GH)K)} = ^{*}{}{(G(HK))}\end{aligned}$$

(14)

$$\begin{aligned}&((GH)K)^{*} = (G(HK))^{*}\end{aligned}$$

(15)

$$\begin{aligned}&\lambda _{^{*}{}{((GH)K)}} = \lambda _{^{*}{}{(G(HK))}}\end{aligned}$$

(16)

$$\begin{aligned}&\lambda _{((GH)K)^{*}} = \lambda _{(G(HK))^{*}}\end{aligned}$$

(17)

$$\begin{aligned}&\delta _{^{*}{}{((GH)K)}} = \delta _{^{*}{}{(G(HK))}}\end{aligned}$$

(18)

$$\begin{aligned}&\delta _{((GH)K)^{*}} = \delta _{(G(HK))^{*}} \end{aligned}$$

(19)

Proof of (12)

Definitions 2 and 4 immediately imply for component models X, Y and $f \in {{\mathrm{inner}}}(X)$:

$$\begin{aligned} f \in {{\mathrm{inner}}}(XY) \text { and } f \in {{\mathrm{inner}}}(YX). \end{aligned}$$

This in turn implies for all $f \in {{\mathrm{inner}}}(G) \, \cup \, {{\mathrm{inner}}}(H) \, \cup \, {{\mathrm{inner}}}(K)$: $f \in {{\mathrm{inner}}}((GH)K)$ and $f \in {{\mathrm{inner}}}(G(HK))$. The proposition then follows with forthcoming properties (23) and (24), and Definition 2. $\square$

Proof of (13)

Property (12) implies that the matching pairs of (GH)K and of G(HK) coincide. Hence, the replacements of arcs in the arc sets of (GH)K and of G(HK), as in Definition 4, coincide. $\square$

Proof of (16)

For component models X and Y, the $\lambda$-label of an element e in $^{*}{}{X}$ or $^{*}{}{Y}$ remains when e moves to $^{*}{}{(XY)}$, according to Definition 4. Likewise, the $\lambda$-label of an element e in $X^*$ or $Y^*$ remains when e moves to $(XY)^*$. The proposition the follows with (14) and (15). $\square$

Proof of (17)

Analog to Proof of (16). $\square$

(14) and (18) are proven in the sequel. (15) and (19) follow analogously to (14) and (18) and are left to the reader.

Proof of (14) and (18)

In the sequel, a portP is the left or right interface $^{*}{}{X }$ or $X^*$ of one of the component models

$$\begin{aligned} X = G, H, K, GH, HK, (GH)K \text{ or } G(HK) {.} \end{aligned}$$

(20)

With respect to a port P and $f \in P$ we write

$$\begin{aligned}&\max (P) \text{ for } |\{p \in P \; | \; \lambda _P(p) = \lambda _P(f)\}|, \text{ and } \end{aligned}$$

(21)

$$\begin{aligned}&P(f) \text{ for } \delta _P(f) . \end{aligned}$$

(22)

In (21), $\text {max}(P)$ refers to an element f of P that is clear in each context, and is not noted for the sake of readability. Intuitively formulated, $\max (P)$ is the number of nodes in P with labels coinciding with the label of f. These nodes are numbered by $\delta _P$, and P(f) is the corresponding number of f. Obviously holds $\square$

Lemma 1

Let P be a port, let $f \in P$. Then $P(f) \le \max (P)$.

In order to show (14) and (18) we observe (by Definition 4) that, $^{*}{}{((GH)K)}$ and $^{*}{}{(G(HK))}$ contain only nodes of $^{*}{}{G}, ^{*}{}{H}$ and $^{*}{}{K}$. Therefore it suffices to show for each $f \in \, ^{*}{}{G} \, \cup \; ^*\negthickspace \, H \, \cup \, ^*\negthickspace \, K$:

$$\begin{aligned} f \in ^{*}{}{((GH)K)} \text{ and } f \in ^{*}{}{(G(HK))}, \text{ with } ^{*}{}{((GH)K)}(f) = ^{*}{}{(G(HK))}(f) \end{aligned}$$

(23)

or for some node g,

$$\begin{aligned} (g,f) \in {{\mathrm{inner}}}((GH)K) \text{ and } (g,f) \in {{\mathrm{inner}}}(G(HK)). \end{aligned}$$

(24)

We start with some obvious properties that are later on used to justify deduction steps:

Fig. 10

Structure of the proof of (14)

Fig. 11

Case 1

Lemma 2

Let X, Y be component models.

• (i) Let $x \in ^{*}{}{X}$. Then $x \in ^{*}{}{(XY)}$ and $^{*}{}{(XY)}(x)= ^{*}{}{X}(x)$.

• (ii) Let $y \in Y^{*}$. Then $y \in (XY)^{*}$ and $(XY)^{*}(y)= Y^{*}(y)$.

• (iii) Let $y \in ^{*}{}{Y}$ and $\max (X^{*}) \ge ^{*}{}{Y}(y)$. Then there exists a unique $x\in X^{*}$ with $\lambda _{^{*}{}{Y}}(y) = \lambda _{X^*}(x)$, $X^{*}(x) = ^{*}{}{Y}(y)$ and $(x,y) \in {{\mathrm{inner}}}(XY)$.

• (iv) Let $y \in ^{*}{}{Y}$ and let $\max (X^{*}) < ^{*}{}{Y}(y)$. Then $y \in ^{*}{}{(XY)}$ and $^{*}{}{(XY)}(y) = \max (^{*}{}{X}) + ^{*}{}{Y}(y)-\max (X^{*})$

• (v) Let $x \in X^{*}$ and $X^{*}(x) > \max (Y^{*})$. Then $x \in (XY)^{*}$ and $(XY)^{*}(x)=X^{*}(x)+\max (Y^{*}) - \max (^{*}{}{X})$.

• (vi) Let $\max (X^{*}) > \max (^{*}{}{Y})$. Then $\max (^{*}{}{(XY)}) = \max (^{*}{}{X})$.

• (vii) Let $\max (X^{*}) \ge \max (^{*}{}{Y})$. Then $\max ((XY)^{*}) = \max (Y^{*}) + \max (X^{*}) - \max (^{*}{}{X})$.

• (viii) Let $\max (X^{*}) < \max (^{*}{}{Y})$. Then $\max (^{*}{}{(XY)}) = \max (^{*}{}{X}) + \max (^{*}{}{Y}) - \max (X^{*})$.

• (ix) Let $\max (X^{*})< \max (^{*}{}{Y})$. Then $\max ((XY)^{*})= \max (Y^{*})$

• (x) $\max (^{*}{}{X}) \le \max (^{*}{}{(XY)})$.

• (xi) Let $f \in X^*$. Then $\max (X^*) \ge X^*(f)$.

For the proof of (14) and (18) we distinguish seven cases, structured as shown in Fig. 10. Property (24) applies to cases 2.1, 3.1 and 3.2.2.1. For all other cases we show property (23). Figures outline the (increasingly more involved) proof steps of the seven cases.

• Case 1$f \in ^{*}{}{G}$ (Fig. 11). We prove (23):

  • a) $f \in ^{*}{}{(G(HK))}$ and $^{*}{}{(G(HK))}(f)=^{*}{}{G}(f)$, by Case 1 and Lemma 2(ii).

  • b) $f \in ^{*}{}{(GH)}$ and $^{*}{}{(GH)}(f) = ^{*}{}{G}(f)$, by Case 1 and Lemma 2(ii). Then $f \in ^{*}{}{((GH)K)}$ and $^{*}{}{((GH)K)}(f)=^{*}{}{G}(f)$, by Lemma 2(i).

• Case 2$f \in ^{*}{}{H}$.

  • Case 2.1$\max (G^{*}) \ge ^{*}{}{H}(f)$ (Fig.12). We prove (24).

    • There exists a unique $g \in G^{*}$ with $\lambda _{G^*}(g) = \lambda _{^*\negthickspace \, H}(f)$ and $G^{*}(g) = ^{*}{}{H}(f)$, by Case 2.1 and Lemma 2(iii).

      • a) $f \in ^{*}{}{(HK)}$ and $^{*}{}{(HK)}(f) = ^{*}{}{H}(f)$, by Case 2 and Lemma 2(i).

        Then $\max (G^{*}) \ge ^{*}{}{(HK)}(f)$, by Case 2.1. Then $(g,f) \in {{\mathrm{inner}}}(G(HK))$, by Case 2 and Lemma 2(iii).

      • b) $(g,f) \in {{\mathrm{inner}}}(GH)$, by Case 2, Case 2.1 and Lemma 2(iii).

        Then $(g,f) \in {{\mathrm{inner}}}((GH)K)$, by Definition 4.

  Fig. 12

  

  Case 2.1

  Fig. 13

  

  Case 2.2

  • Case 2.2$\max (G^{*}) < ^{*}{}{H}(f)$ (Fig. 13). We prove (23).

    • As a shorthand, let

      $$\begin{aligned} n =_\textit{def} \max (^{*}{}{G}) + ^{*}{}{H}(f)- \max (G^{*}). \end{aligned}$$

      (25)
      • a)
        $$\begin{aligned} f \in ^{*}{}{(HK)} \text { and } ^{*}{}{(HK)}(f) = ^{*}{}{H}(f) \end{aligned}$$

        (26)

        by Case 2 and Lemma 2(i).

        Then $\max (G^{*}) < ^{*}{}{(HK)}(f)$, by Case 2.2. Then by Lemma 2(iv) $f \in ^{*}{}{(G(HK))}$ and

        $$\begin{aligned}&^{*}{}{(G(HK))}(f)\\&\quad =\max (^{*}{}{G}) + ^{*}{}{(HK)}(f) - \max (G^{*}) \text {, by Lemma}~2(iv)\\&\quad =\max (^{*}{}{G}) + ^{*}{}{H}(f)-\max (G^{*}) \text {, by } (26)\\&\quad =n \text {, by } (25) \end{aligned}$$

      • b) $f \in ^{*}{}{(GH)}$ and

        $$\begin{aligned} ^{*}{}{(GH)}(f) = \max (^{*}{}{G})+^{*}{}{H}(f) - \max (G^{*}) \end{aligned}$$

        (27)

        by Case 2 and Lemma 2(iv).

        Then $f \in ^{*}{}{((GH)K)}$ and

        $$\begin{aligned}&^{*}{}{((GH)K)}(f)\\&\quad =^{*}{}{(GH)}(f) \text {, by Lemma}~2{} \textit{(i)}\\&\quad =\max (^{*}{}{G}) + ^{*}{}{H}(f) - \max (G^{*}) \text {, by } (27)\\&\quad =n \text {, by } (25). \end{aligned}$$

• Case 3$f \in ^{*}{}{K}$.

  • Case 3.1$\max (H^{*})\ge ^{*}{}{K}(f)$ (Fig. 14). We prove (24).

    • There exists a unique $h \in H^{*}$ with

      $$\begin{aligned} H^{*}(h) = ^{*}{}{K}(f) \end{aligned}$$

      (28)

    • and $(h,f) \in {{\mathrm{inner}}}(HK)$, by case 3, case 3.1 and Lemma 2(iii).

      • a) Then $(h,f) \in {{\mathrm{inner}}}(G(HK))$ by Definition 4.

      • b) $f \in ^{*}{}{K}$ and $\max (H^*) \ge ^{*}{}{K}(f)$, by case 3 and case 3.1.

        Then $f \in ^{*}{}{K}$ and $\max ((GH)^{*}) \ge ^{*}{}{K}(f)$, by (21), and, obviously, $H^* \subseteq (GH)^*$.

        Then there exists a unique $g \in (GH)^{*}$ with $\lambda _{^{*}{}{K}}(f) = \lambda _{(HK)^*}(g)$ and $(GH)^{*}(g) = ^{*}{}{K}(f)$ and $(g,f) \in {{\mathrm{inner}}}((GH)K)$, by Lemma 2(iii).

        Furthermore, $g=h$, because $\delta _{(GH)^*}$ is injective.

        Then $(h,f) \in {{\mathrm{inner}}}((GH)K)$.

  • Case 3.2$\max (H^{*}) < ^{*}{}{K}(f)$.

    • In the rest of this proof, let

      $$\begin{aligned} n=_{\text {def}} \max (^{*}{}{G}) + \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (G^{*})-\max (H^{*}) \end{aligned}$$

      (29)

    • Furthermore it holds:

      $$\begin{aligned} f \in ^{*}{}{(HK)} \text {and} ^{*}{}{(HK)}(f) = \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (H^{*}) \end{aligned}$$

      (30)

    • by 3.2 and Lemma 2(iv).

  Fig. 14

  

  Case 3.1

  Fig. 15

  

  Case 3.2.1 (a)

  • Case 3.2.1$\max (G^{*}) < \max (^{*}{}{H})$ (Figs. 15, 16). We prove (23).

    • a) $f \in ^{*}{}{(HK)}$ and $\max (G^*) < ^{*}{}{(HK)}(f)$, by (29) and (30).

      Then $f \in ^{*}{}{(G(HK))}$ and

      $$\begin{aligned}&^{*}{}{(G(HK))}(f)\\&\quad = \max (^{*}{}{G}) + ^{*}{}{(HK)}(f) - \max (G^{*}) \text { , by }(30) \text { and Lemma}~2\text {(iv)}&\\&\quad = \max (^{*}{}{G}) + \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (H^{*}) - \max (G^{*}) \text { , by } (30)\\&\quad = n \text { , by } (29) \end{aligned}$$

    • b) $\max ((GH)^{*}) = \max (H^{*})$, by 3.2.1 and Lemma 2(ix). Then $\max ((GH)^{*}) < ^{*}{}{K}(f)$ by 3.2. Then $f \in ^{*}{}{((GH)K)}$ and

      $$\begin{aligned}&^{*}{}{((GH)K)}(f)\\&\quad =\,\max (^{*}{}{(GH)}) + ^{*}{}{K}(f) - \max ((GH)^{*}) \text {, by case 3 and Lemma}~2\text {(iv)}\\&\quad =\, \max (^{*}{}{G}) + \max (^{*}{}{H})- \max (G^*) + ^{*}{}{K}(f) - \max ((GH)^*)\text {,}\\&\qquad \text { by Lemma}~2\text {(viii)}\\&\quad =\, \max (^{*}{}{G}) + \max (^{*}{}{H})- \max (G^*) + ^{*}{}{K}(f) - \max (H^*) \text {, by Lemma}~2\text {(ix)}\\&\quad =\, n \text {, by } (29). \end{aligned}$$

  • Case 3.2.2$\max {G^*} \ge \max (^{*}{}{H})$.

  • Case 3.2.2.1$\max (G^{*}) \ge \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (H^{*})$ (Figs. 17, 18). We prove (24).

    • There exists a unique $g \in G^{*}$ with

      $$\begin{aligned} G^{*}(g) = \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (H^{*}) \text {,} \end{aligned}$$

      (31)

    • by 3.2.2 and Lemma 2(v).

      • a) $f \in ^{*}{}{K}$ and $\max (H^*) \ge ^{*}{}{K}(f)$, by case 3 and case 3.2.

        Then $f \in ^{*}{}{(HK)}$ and $^{*}{}{(HK)}(f) = \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (H^*)$, by Lemma 2(iv) and (31).

        Then $(g,f) \in {{\mathrm{inner}}}(G(HK))$, by Lemma 2(iii).

      • b) $G^{*}(g) > \max (^{*}{}{H})$ by (31) and case 3.2.

        Then $g \in (GH)^{*}$, and $(GH)^{*}(g) = \max (H^{*}) + G^{*}(g) - \max (^{*}{}{H})$ by (31) and Lemma 2(v).

        Then $g \in (GH)^{*}$ and $(GH)^{*}(g) = ^{*}{}{K}(f)$, by (31).

        Then $\max ((GH)^{*}) \ge ^{*}{}{K}(f)$ and $(GH)^{*}(g) = ^{*}{}{K}(f)$ by Lemma 1.

        Then $(g,f) \in {{\mathrm{inner}}}((GH)K)$ by Lemma 2(iii).

      Fig. 16

      

      Case 3.2.1 (b)

      Fig. 17

      

      Case 3.2.2.1 (a)

      Fig. 18

      

      Case 3.2.2.1 (b)

  • Case 3.2.2.2$\max (G^{*}) < \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (H^{*})$ (Figs. 19, 20). We prove (23).

    • a) $f \in ^{*}{}{(HK)}$ and $^{*}{}{(HK)}(f)$

      $$\begin{aligned} = \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (H^{*}) \end{aligned}$$

      (32)

      by case 3.2 and Lemma 2(iv).

      Then $f \in ^{*}{}{(HK)}$ and $\max (G^{*}) < ^{*}{}{(HK)}(f)$, by case 3.2.2 and case 3.2.2.2. Then $f \in ^{*}{}{(G(HK))}$ and

      $$\begin{aligned}&^{*}{}{((GH)K)}(f)\\&\quad = \max (^{*}{}{G}) + ^{*}{}{(HK)}(f) - \max (G^{*}) \text { , by Lemma}~2\text {(iv)}\\&\quad = \max (^{*}{}{G}) + \max (^{*}{}{H}) + ^{*}{}{K}(f) - \max (H^{*}) - \max (G^{*}) \text { , by } (32)\\&\quad = n \text { , by } (29). \end{aligned}$$

    • b) $\max (G^{*}) + \max (H^{*}) -\max (^{*}{}{H}) < ^{*}{}{K}(f)$, by 3.2.2.2.

      Then $\max ((GH)^{*}) < ^{*}{}{K}(f)$ by Lemma 2(vii). Then $f \in ^{*}{}{((GH)K)}$ and

      $$\begin{aligned}&^{*}{}{((GH)K)}(f)\\&\quad = \max (^{*}{}{(GH)}) + ^{*}{}{K}(f) - \max ((GH)^{*}) \text { , by case 3. and Lemma}~2\text {(iv)}\\&\quad = \max (^{*}{}{G}) + ^{*}{}{K}(f) - \max ((GH)^{*}) \text { , by case 3.2.2 and Lemma}~2\text {(vi)}\\&\quad = \max (^{*}{}{G}) + ^{*}{}{K}(f) - (\max (G^{*}) + \max (H^{*}) - \max (^{*}{}{H})) \text { , by case}\\&\qquad \text { 3.2.2 and Lemma}~2\text {(vii)}\\&\quad = n \text { , by } (29). \end{aligned}$$

Fig. 19

Case 3.2.2.2 (a)

Fig. 20

Case 3.2.2.2 (b)