From Event-Oriented Models to Transition Systems

Abstract

Two structurally different methods of associating transition system semantics to event-oriented models of distributed systems are distinguished in the literature. One of them is based on configurations (event sets), the other on residuals (model fragments). In this paper, a variety of models is investigated, ranging from extended prime event structures to configuration structures, and it is shown that the two semantics lead to isomorphic results. This strengthens prior work where bisimilarity (but not necessarily isomorphism) is achieved for a smaller range of models. Thanks to the isomorphisms obtained here, a wide range of facts known from the literature on configuration-based transition systems can be extended to residual-based ones.

E. Best, N. Gribovskaya and I. Virbitskaite—Supported by German Research Foundation through grant Be 1267/14-1.

A Proofs

This appendix contains the proofs of the results obtained for $\mathcal {E}\in {\mathbb {E}^{g}_L}$ and $\star =mset$. All the proofs can be found at http://www.iis.nsk.su/virb/BGV-proofsketches-2018.pdf.

Proof of Lemma 4

• (i) Take an arbitrary $A\in Con$. This implies that $A\subseteq E$ and $\lnot (x \ \sharp \ x')$, for all $x,x'\in A$. Check that $A\cap E'\in Con'$. Suppose a contrary, i.e. there is $a,a'\in A\cap E'$ such that $a\ \sharp '\ a'$. By the definition of $\sharp '$, this means that $a, a'\in A$ and $a\ \sharp \ a'$, contradicting $A\in Con$. So, $A\cap E'\in Con'$. Next, take an arbitrary $A'\in Con'$. We shall show that $A'\in Con$. Assume a contrary, i.e. there is $a,a'\in A'$ such that $a\ \sharp \ a'$. Since $A'\in Con'$, it holds that $A'\subseteq E'$. By the definition of $\sharp '$, we get $a\ \sharp '\ a'$, contradicting $A'\in Con'$. Hence, $A'\in Con$.

• (ii) Follows from the definitions of the components of $\mathcal {E}\setminus X$.

• (iii) Next, we show that $X\cup X'\in Con$. As $X\in \textit{Conf}(\mathcal{E})$ ($X'\in \textit{Conf}(\mathcal{E}')$), we get $X\in Con$ ($X'\in Con'$). By item (i), it holds that $X'\in Con$. Suppose a contrary, i.e. $X\cup X'\not \in Con$. Then, we can find $e'\in X'$ and $e\in X$ such that $e'\ \sharp \ e$. Since $X'\in \textit{Conf}(\mathcal{E}')$, there are $e'_1, \ldots , e'_m$ ($m\ge 0$) such that $X' = \{e'_1, \ldots , e'_m\}$ and $\{e'_1, \ldots , e'_i\} \vdash ' e'_{i+1}$, for all $i<m$. W.l.o.g., assume $e'=e'_j$ for some $1\le j\le m$. By the definition of $\vdash '$, there is $W'\subseteq \{e'_1, \ldots , e'_{j-1}\}$ such that $(W',e'_j)\in \ \vdash '_{min}$. Then, due to the definition of $\vdash '_{min}$, there is $(W,e'_j)\in \ \vdash _{min}$ such that $W' = W\cap E'$ and $\{e'_j\}\cup X \in Con$, contradicting $e'\ \sharp \ e\in X$.

Check that ${W}\cup X\cup X'\in Con$ iff $(W\setminus X)\cup X'\in Con'$ and $W\cup X\in Con$. Assume ${W}\cup X\cup X'\in Con$. Clearly, it holds that $W\cup X\in Con$. Next, it easy to see that $(W\cup X\cup X')\cap E'\in Con'$, due to item (i). This means $({W\setminus X})\cup X'\in Con'$. Conversely, suppose $(W\setminus X)\cup X'\in Con'$ and $W\cup X\in Con$. By item (i), we have $(W\setminus X)\cup X'\in Con$. Moreover, we know that $X\cup X'\in Con$. Hence, it holds that ${W}\cup X\cup X'\in Con$.    $\Box$

Proof of Proposition 1

• (i) Let $\mathcal{E}'=\mathcal{E}\setminus X$ with $X\in Conf_\star (\mathcal{E})$ and $\mathcal{E}''=\mathcal{E}'\setminus X'$ with $X'\in Conf_\star (\mathcal{E}')$.

Since $X\in Conf_\star (\mathcal{E})$ ($X'\in Conf_\star (\mathcal{E}')$), X ($X'$) is a finite, conflict-free, and secured subset of E ($E'$) and $\emptyset \rightarrow _\star ^*X$ in $\mathcal{E}$ ($\emptyset \rightarrow _\star ^*X'$ in $\mathcal{E}'$). Obviously, $X\cup X'$ is a finite subset of E, by the definition of $E'$. Next, due to Lemma 4(iii), we have that $X\cup X'\in Con$. Further, we check that $X\cup X'$ is secured. As X is secured, there is a sequence $e_1 \ldots e_n\ (n\ge 0)$ such that $X=\{e_1, \ldots , e_n\}$, and $\{e_1, \ldots , e_i\}\vdash e_{i+1}$, for all $i<n$. Moreover, there exists a sequence $e'_1 \ldots e'_m\ (m\ge 0)$ such that $X'=\{e'_1, \ldots , e'_m\}$, and $\{e'_1, \ldots , e'_j\}\vdash ' e'_{j+1}$, for all $j<m$, because $X'$ is secured in $\mathcal{E}'$. Consider a sequence $e_1 \ldots e_n\,e_{n+1}=e'_1 \ldots e_{n+m}=e'_m$. Clearly, $\{e_1, \ldots , e_n,\,e_{n+1}, \ldots , e_{n+m}\}=X\cup X'$. Check that $\{e_1, \ldots , e_l\}\vdash e_{l+1}$, for all $l<n+m$. We know that $\{e_1, \ldots , e_l\}\vdash e_{l+1}$, for all $l<n$. Consider the case when $l=n$. Obviously, $\emptyset \vdash ' e_{n+1}=e'_1$, i.e. $\emptyset \vdash '_{min} e_{n+1}=e'_1$. This means that there is $(W,e'_1)\in \ \vdash _{min}$ such that $\emptyset = W\cap E'$ and $\{e'_1\}\cup X \in Con$. Since $W\subseteq E'\cup X$ and $W\cap E'=\emptyset$, we get $W\subseteq X\in Con$. Then, $X\vdash e_{n+1}$, i.e. $\{e_1, \ldots , e_n\}\vdash e_{n+1}$. Finally, we verify the case when $n+1\le l<n+m$. We know that $\{e'_1, \ldots , e'_{l-n}\}\vdash ' e'_{l-n+1}$. Then, $W'\vdash '_{min} e'_{l-n+1}$, for some $W'\subseteq \{e'_1, \ldots , e'_{l-n}\}$. This means that there is $(W,e'_{l-n+1})\in \ \vdash _{min}$ such that $W' = W\cap E', \{e'_{l-n+1}\}\cup X \in Con$, and $W'\cup X \in Con$. So, $W'\cup X\vdash e'_{l-n+1}$. Since $X\cup X'\in Con$ and $W'\subseteq \{e'_1, \ldots , e'_{l-n}\} \subseteq X'$, $X\cup \{e'_1, \ldots , e'_{l-n}\}\in Con$. Then, $\{e_1, \ldots , e_n,\,e_{n+1}, \ldots , e_{l}\}\vdash e_{l+1}$. Hence, $X\cup X'$ is a configuration of $\mathcal{E}$. Since $\emptyset \subseteq X\cup X'$ we get $\emptyset \rightarrow _\star X\cup X'$ in $\mathcal{E}$. Thus, $X\cup X'\in Conf_\star (\mathcal{E})$.

Set $\widetilde{\mathcal{E}} = \mathcal{E} \setminus (X \cup X')$. Check that $\mathcal{E}'' = \widetilde{\mathcal{E}}$. By definition, $\widetilde{E} = E\setminus (X\cup X')=(E\setminus X)\setminus X'=E'\setminus X'=E''$. Then, again by definition, $\sharp ''=\sharp ' \cap (E'' \times E'') = (\sharp \cap (E' \times E')) \cap (E''\times E'') = \sharp \cap (E'' \times E'') = \sharp \bigcap \widetilde{E} \times \widetilde{E}=\widetilde{\sharp }$, and $l''=l \mid _{E''}=l\mid _{\widetilde{E}}=\widetilde{l}$. Using that $\widetilde{E} = E''$ and $\widetilde{\sharp } = \sharp ''$, it is straightforward to verify that $\widetilde{Con}=Con''$. It remains to show that $\widetilde{\vdash }=\ \vdash ''$. We know that $\widetilde{\vdash }_{min}=\{(\widetilde{W},e)\}\mid$ $\exists (W,e)\in \ \vdash _{min}$ s.t. $e\in \widetilde{E}, \widetilde{W}=W\cap \widetilde{E}$, $\{e\}\cup (X\cup X')\in Con$, $\widetilde{W}\cup (X\cup X')\in Con\}$. On the other hand, we have that $\vdash ''_{min}=\{(W'',e)\mid$ $\exists (W',e)\in \ \vdash '_{min}$ s.t. $e\in E'', W''=W'\cap E'', \{e\}\cup X'\in Con', W''\cup X'\in Con'\}$. Due to the definition of $\vdash '_{min}$, $\vdash ''_{min}=\{(W'',e)\mid$ $\exists (W,e)\in \ \vdash _{min}$ s.t. $e\in E'\cap E'', W''=(W'=W\cap E')\cap E'', \{e\}\cup X\in Con$, $\{e\}\cup X'\in Con'$, $W''\cup X'\in Con'$, $W'\cup X\in Con\}=\{(W'',e)\mid$ $\exists (W,e)\in \ \vdash _{min}$ s.t. $e\in E'', W''=W\cap E'', \{e\}\cup X\in Con, \{e\}\cup X'\in Con'$, $W''\cup X'\in Con'$, $W'\cup X\in Con\}$. As $\widetilde{W} = W\setminus (X\cup X'), \widetilde{W}\cup X\cup X' = W\cup X \cup X'$, as $W' = W\setminus X, W'\cup X = W\cup X$, and as $W''=W'\setminus X', W''\cup X'=W'\cup X'=(W\setminus X)\cup X'$. Hence, $\widetilde{W}\cup X\cup X'\in Con$ iff $W''\cup X'\in Con'$ and $W'\cup X\in Con$, due to Lemma 4(iii). Notice that $e\not \in X \cup X'$, because $e\in E''$. We also have that $\{e\}\cup X\cup X'\in Con$ iff $\{e\}\cup X'\in Con'$ and $\{e\}\cup X\in Con$, again by Lemma 4(iii). Due to $\widetilde{E} = E''$, we get that $\widetilde{\vdash }_{min}=\ \vdash ''_{min}$. Moreover, it holds that $\widetilde{\vdash }=\{(\widetilde{W},e)\}\mid \widetilde{W}\in \widetilde{Con}$, $\exists (W,e)\in \ \widetilde{\vdash }_{min}$ s.t. $W\subseteq \widetilde{W}\}=\{(W'',e)\}\mid W''\in Con''$, $\exists (W,e)\in \ \vdash ''_{min}$ s.t. $W\subseteq W''\}=\ \vdash ''$, because $\widetilde{Con}=Con''$ and $\widetilde{\vdash }_{min}=\ \vdash ''_{min}$.

• (ii) Assume $X,X''\in \textit{Conf}_\star (\mathcal{E})$ and $X{\mathop {\rightarrow }\limits ^{}}_\star X''$. Since $X''\in Conf_\star (\mathcal{E})$, we have $X''\in \textit{Conf}(\mathcal{E})$, i.e. $X''$ is finite, conflict-free (i.e., $X''\in Con$), and secured (i.e., there exists a sequence $t=e''_1\ldots e''_n$ of events from $E\ (n\ge 0)$ such that $X''=\{e''_1, \ldots , e''_n\}$, and $\{e''_1, \ldots , e''_i\}\vdash e''_{i+1}$, for all $i<n$. Using the sequence t and the fact that $X{\mathop {\rightarrow }\limits ^{}}_\star X''$, i.e. $X\subseteq X''$, construct a sequence $t'$ as follows: $t'_0 = \epsilon$, $t'_{i+1} = t'_i\,e''_{i+1}$, if $e''_{i+1}\not \in X$, and $t'_{i+1} = t'_i$, otherwise. W.l.o.g. assume $t'= e'_1\ldots e'_k\ (k\ge 0)$ and $X'=\{e'_1,\ldots ,e'_k\}$. Clearly, $X'$ is a finite subset of $E'$. As $X''\in Con$, then $X''\setminus X=X'=X''\cap E'\in Con'$, by Lemma 4(i). We shall show that $\{e'_1, \ldots , e'_{j}\}\vdash ' e'_{j+1}$, for all $j<k$. Take an arbitrary $j<k$. Clearly, $e'_1, \ldots , e'_{j},e'_{j+1}\in X'\subseteq E'$ and $\{e'_1,\ \ldots ,\ e'_{j}\}\in Con'$. W.l.o.g., assume $e'_{j+1} = e''_{i+1}$, for some $e''_{i+1}\in X''$. As $X''\in \textit{Conf}(\mathcal{E})$, we get that $W''=\{e''_1, \ldots , e''_i\}\vdash e''_{i+1}$. Then, $W\vdash _{min}e''_{i+1}$, for some $W\subseteq W''$. Obviously, $W''\cap E'= \{e'_1,\ \ldots ,\ e'_{j}\}$. Set $W'=W\cap E'$. Clearly, $W'\cup \{e''_{i+1}\}\cup X \subseteq X''$. As $X''\in Con$, we get that $W'\cup X \in Con$ and $\{e''_{i+1}\}\cup X \in Con$. So, $W'\vdash '_{min} e'_{j+1}$. Since $W'\subseteq \{e'_1, \ldots , e'_{j}\}\in Con'$, $\{e'_1, \ldots , e'_{j}\}\vdash ' e'_{j+1}$. This implies, $X'$ is a configuration of $\mathcal{E}\setminus X$. Since $\emptyset \subseteq X'$, we have $\emptyset \rightarrow _\star X' = X''\setminus X$ in $\mathcal{E}\setminus X$. Hence, $X'\in Conf_\star (\mathcal{E}\setminus X)$.    $\Box$

Proof of Proposition 2

• (i) Take an arbitrary $X\in Conf_\star (\mathcal {E})$. This means that $X_0=\emptyset \rightarrow _\star X_1\ldots X_{n-1}\rightarrow _\star X_n = X$ ($n\ge )$) in ${\mathcal {E}}$. Then, we get that $X_i\in Conf_\star (\mathcal {E})\ (0\le i\le n)$ and $X_{i-1} \subseteq X_i\ (1\le i\le n)$. We shall proceed by induction on n.

• $n=0$. $\mathcal {E}\setminus X_0=\mathcal {E}\in Reach_\star (\mathcal {E})$.

• $n=1$. By the induction hypothesis, $\mathcal {E}\setminus X_0\in Reach_\star (\mathcal {E})$. Check that $\mathcal {E}\setminus X_{0}{\mathop {\rightharpoonup }\limits ^{p_1}}_\star \mathcal {E}\setminus X_1$. Since $X_{0}\rightarrow _\star X_1$ in $\mathcal {E}$, it holds $X_{1}\setminus X_{0}\in Conf_\star (\mathcal {E}\setminus X_{0})$ and $\emptyset \rightarrow _\star X_1\setminus X_{0} = A_1$ in $\mathcal {E}\setminus X_{0}$, by Proposition 1(ii). Next, due to Proposition 1(i), we have $(\mathcal {E}\setminus X_{0}) \setminus A_1=\mathcal {E}\setminus (X_{0}\cup (X_1\setminus X_{0}))= \mathcal {E}\setminus X_{1}$. This implies that $\mathcal {E}\setminus X_{0}\ {\mathop {\rightharpoonup }\limits ^{p_1}}_\star$ $\mathcal {E}\setminus X_{1}$, where $p_1=l_\star (A_1)$. So, $\mathcal {E}\setminus X_{1}\in Reach_\star (\mathcal {E})$.

• $n>1$. By the induction hypothesis, $\mathcal {E}\setminus X_{n-2}\ {\mathop {\rightharpoonup }\limits ^{p_{n-1}}}_\star$ $\mathcal {E}\setminus X_{n-1}$. Reasoning as in the previous item, we get that $\mathcal {E}\setminus X_{n-1}$ ${\mathop {\rightharpoonup }\limits ^{p_n}}_\star$ $\mathcal {E}\setminus X_{n}$, where $p_n=l_\star (A_n)$. Thus, $\mathcal {E}\setminus (X_{n}=X)\in Reach_\star (\mathcal {E})$.

• (ii) Take an arbitrary $\mathcal {E}'\in Reach_\star (\mathcal {E})$. This means that $\mathcal {E}=\mathcal {E}_0$ ${\mathop {\rightharpoonup }\limits ^{p_1}}_\star$ $\mathcal {E}_1 \ldots \mathcal {E}_{n-1}$ ${\mathop {\rightharpoonup }\limits ^{p_n}}_\star \ \mathcal {E}_n=\mathcal {E}'$ ($n\ge 0$). By the definition of ${\mathop {\rightharpoonup }\limits ^{p_{i+1}}}_\star$, it holds that $\mathcal {E}_{i+1}=\mathcal {E}_{i}\setminus X_{i+1}$, for some $X_{i+1}\in Conf_\star (\mathcal {E}_{i})$ such that $\emptyset \rightarrow _\star X_{i+1}$ in $\mathcal {E}_i$ and $p_{i+1}=l_\star (X_{i+1})$ ($i<n$). Verify that $Y_{i+1} = \mathop {\bigcup }\limits _{j=1}^{i+1} X_{j}\in Conf_\star (\mathcal {E})$ and $\mathcal {E}_{i+1}=\mathcal {E}\setminus Y_{i+1}$, for all $i<n$.

We shall proceed by induction on n.

• $n=0$. Obvious.

• $n=1$. Then, $Y_1=X_1\in Conf_\star (\mathcal {E})$ and $\mathcal {E}_1=\mathcal {E}_0\setminus X_{1}=\mathcal {E}\setminus Y_{1}$.

• $n>1$. By the induction hypothesis, $Y_{n-1} = \mathop {\bigcup }\limits _{j=1}^{n-1} X_{j}\in Conf_\star (\mathcal {E})$ and $\mathcal {E}_{n-1}=\mathcal {E}\setminus Y_{n-1}$. Check that $Y_{n}=\mathop {\bigcup }\limits _{j=1}^{n} X_{j}\in Conf_\star (\mathcal {E})$ and $\mathcal {E}_{n}=\mathcal {E}\setminus Y_{n}$. As $\mathcal {E}_{n}=\mathcal {E}_{n-1}\setminus X_{n}$, it holds that $\mathcal {E}_{n}=(\mathcal {E}\setminus Y_{n-1})\setminus X_{n}$. According to Proposition 1(i), we have that $Y_{n-1}\cup X_{n}\in Conf_\star ({\mathcal E})$ and $\mathcal {E}_{n}=\mathcal {E}\setminus (Y_{n-1}\cup X_{n})=\mathcal {E}\setminus Y_{n}$.

Thus, $\mathcal {E}'=\mathcal {E}\setminus Y_{n}$.

• (iii) It follows from the definitions of the transition relations and Proposition 1(i),(ii).

• (iv) Due to item (ii), there is $X'\in Conf_\star (\mathcal {E})$ such that $\mathcal {E}'=\mathcal {E}\setminus X'$. According to the definition of ${\mathop {\rightharpoonup }\limits ^{p}}_\star$, there is $\widetilde{X}'\in Conf_\star (\mathcal {E}')$ such that $\mathcal {E}''=\mathcal {E}'\setminus \widetilde{X}'$, $\emptyset \rightarrow _\star \widetilde{X}'$ in $\mathcal {E}'$, and $p=l_\star (\widetilde{X}')$. Then, $X''=X'\cup \widetilde{X}'\in Conf_\star (\mathcal {E})$ and $\mathcal {E}''=\mathcal {E}\setminus X''$, by Proposition 1(i). Clearly, $X',X''\in Conf(\mathcal {E})$ and $X'\subseteq X'\cup \widetilde{X}' = X''$. Hence, $X'\rightarrow _\star X''$ in $\mathcal {E}$. Obviously, $l_\star (X''\setminus X')=p$. Thus, $X'{\mathop {\rightharpoondown }\limits ^{p}}_\star X''$ in $\mathcal {E}$.    $\Box$

Proof of Theorem 1

Define a mapping $g : Conf_\star ({\mathcal E})\rightarrow Reach_\star ({\mathcal E})$ as follows: $g(X) = \mathcal{E}\setminus X$, for all $X\in Conf_\star {\mathcal E})$. Clearly, $g(\emptyset )=\mathcal{E}$. By the definition of $\mathcal{E}\setminus X$ and Proposition 2(i), g is well-defined. Check that g is a bijective mapping.

Suppose that $g(X)=g(X')$, for some $X,X'\in Conf_\star ({\mathcal E})$. This means that ${\mathcal E}\setminus X = {\mathcal E}\setminus X'$. By the definition of ${\mathcal E}\setminus X$ and ${\mathcal E}\setminus X'$, we get that $E\setminus X = E\setminus X'$. Since $X,X'\subseteq E$, we have that $X=X'$. Thus, g is an injective mapping.

Take an arbitrary $\mathcal{E}'\in Reach_\star ({\mathcal E})$. Due to Proposition 2(ii), we get that $\mathcal{E}' = \mathcal{E}\setminus X$, for some $X\in Conf_\star ({\mathcal E})$. So, g is a surjective mapping.

We finally show that $X {\mathop {\rightharpoondown }\limits ^{p}}_\star X'$ in $\textit{TC}_\star (\mathcal{E})$ iff $g(X) {\mathop {\rightharpoonup }\limits ^{p}}_\star g(X')$ in $\textit{TR}_\star (\mathcal{E})$. It follows from Proposition 2(iii) and (iv) and the fact that g is a bijective mapping.

Thus, g is indeed an isomorphism.    $\Box$