Distribution of Behaviour into Parallel Communicating Subsystems

TL;DR

This paper investigates how complex systems can be decomposed into communicating subsystems while preserving behavioral equivalence, focusing on automata learning and bisimilarity, and proving limitations of such decompositions.

Contribution

It introduces methods for decomposing systems into communicating subsystems that preserve branching bisimilarity and establishes fundamental limitations of divergence-preserving decompositions.

Findings

Synchronous and asynchronous decompositions maintain branching bisimilarity.

No universal decomposition operator preserves divergence-preserving branching bisimilarity.

The study advances understanding of system decomposition in distributed automata learning.

Abstract

The process of decomposing a complex system into simpler subsystems has been of interest to computer scientists over many decades, for instance, for the field of distributed computing. In this paper, motivated by the desire to distribute the process of active automata learning onto multiple subsystems, we study the equivalence between a system and the total behaviour of its decomposition which comprises subsystems with communication between them. We show synchronously- and asynchronously-communicating decompositions that maintain branching bisimilarity, and we prove that there is no decomposition operator that maintains divergence-preserving branching bisimilarity over all LTSs.

Equations

$$\{\begin{array}{ll}(s,t)\stackrel{a}{\to }(s^{\prime },t)& \text{iff }a\in {\Sigma }_1\wedge \overline{a}\notin {\Sigma }_2\wedge s{\stackrel{a}{\to }}_1{s}^{\prime },\\ (s,t)\stackrel{a}{\to }(s,t^{\prime })& \text{iff }a\in {\Sigma }_2\wedge \overline{a}\notin {\Sigma }_1\wedge t{\stackrel{a}{\to }}_2{t}^{\prime },\text{ and}\\ (s,t)\stackrel{\tau }{\to }(s^{\prime },t^{\prime })& \text{iff }a\in {\Sigma }_1\wedge \overline{a}\in {\Sigma }_2\wedge s{\stackrel{a}{\to }}_1{s}^{\prime }\wedge t{\stackrel{\overline{a}}{\to }}_2{t}^{\prime },\end{array}$$

$$S_{C_1}=\{(s,1)\mid s\in S\}{S}_{C_2}=\{(s,2)\mid s\in S\}{S}_C=S_{C_1}\cup S_{C_2}$$

$${\Sigma }_C=\{c_{s_1,s_2},\overline{c_{s_2,s_1}}\mid s_1\in S_{C_1},s_2\in S_{C_2}\}$$

$${\Sigma }_{T_1}=\{t_{s_1}\mid s_1\in S_C\}$$

$$S_{T_1}=\{t_{a,s_1}\mid a\in {\Sigma }_1,s_1\in S_{C_1}\}$$

$${\Sigma }_{S_1}={\Sigma }_{T_1}\cup {\Sigma }_C\cup \overline{{\Sigma }_{T_2}}{\Sigma }_{S_2}={\Sigma }_{T_2}\cup \overline{{\Sigma }_C}\cup \overline{{\Sigma }_{T_1}}$$

$$\begin{gathered} s_i{\stackrel{c_{s_i,s_j}}{\to }}_i{s}_j \\ {s}_i{\stackrel{\overline{c_{s_i,s_j}}}{\to }}_j{s}_j \end{gathered}$$

$$s_i{\stackrel{a}{\to }}_i{t}_{a,s_i^{\prime }}{\stackrel{t_{s_i^{\prime }}}{\to }}_i{s}_i^{\prime }$$

$$s_i{\stackrel{\overline{t_{s_i^{\prime }}}}{\to }}_j{s}_i^{\prime }$$

$$S_x=S_1\times S_2$$

$$=(S_C\times S_C)\cup (S_{T_1}\times S_{T_2})$$

$$\cup (S_{T_1}\times S_C)\cup (S_C\times S_{T_2})$$

$$(s_i,s_i){\stackrel{a}{\to }}_x{s}_a{\stackrel{\tau }{\to }}_x(s_i^{\prime },s_i^{\prime }),$$

$$\text{where }{s}_a=\{\begin{array}{ll}(t_{a,s_i^{\prime }},s_i)& \text{if }i=1,\\ (s_i,t_{a,s_i^{\prime }})& \text{if }i=2.\end{array}$$

$$(s_i,s_i){\stackrel{\tau }{\to }}_x(s_j,s_j)$$

$$S_{C_i}=\{s_i\mid s\in S\}{S}_C=S_{C_1}\cup S_{C_2}$$

$${\Sigma }_{C_{i,j}}=\{c_{s_{i,j}}\mid s\in S\}{\Sigma }_{T_i}=\{t_{s_i}\mid s\in S\}$$

$$S_{T_i}=\{t_{a,s_i}\mid a\in {\Sigma }_i,s_i\in S_{C_i}\}$$

$${\Sigma }_{S_i}={\Sigma }_{T_i}\cup \overline{{\Sigma }_{T_j}}\cup {\Sigma }_{C_{i,j}}\cup \overline{{\Sigma }_{C_{j,i}}}$$

$$\begin{gathered} \text{Lbag}{s}_i,Q_i\text{Rbag}{\stackrel{c_{s_{i,j}}}{\to }}_i\text{Lbag}{s}_j,Q_i\text{Rbag} \\ \text{Lbag}{s}_i,Q_i\text{Rbag}{\stackrel{\overline{c_{s_{i,j}}}}{\to }}_j\text{Lbag}{s}_i,t_{s_j}\cdot Q_i\text{Rbag} \end{gathered}$$

$$\text{Lbag}{s}_i,Q_i\text{Rbag}{\stackrel{a}{\to }}_i\text{Lbag}{t}_{a,s_i^{\prime }},Q_i\text{Rbag}{\stackrel{t_{s_i^{\prime }}}{\to }}_i\text{Lbag}{s}_i^{\prime },Q_i\text{Rbag}$$

$$\text{Lbag}{s}_i,Q_i\text{Rbag}{\stackrel{\overline{t_{s_i^{\prime }}}}{\to }}_j\text{Lbag}{s}_i,t_{s_i^{\prime }}\cdot Q_i\text{Rbag}$$

$$\text{Lbag}s,Q\cdot t_{s^{\prime }}\text{Rbag}\stackrel{\tau }{\to }\text{Lbag}{s}^{\prime },Q\text{Rbag}$$

$$\begin{array}[]{l@{}}\{\langle s,(\Lbag s_{i},\epsilon\Rbag,\Lbag s_{i},\epsilon\Rbag)\rangle,\\ \langle s,(\Lbag s_{i},t_{s_{j}}\Rbag,\Lbag s_{j},\epsilon\Rbag)\rangle,\langle s,(\Lbag s_{j},\epsilon\Rbag,\Lbag s_{i},t_{s_{j}}\Rbag)\rangle,\\ \langle s,(t_{a,s_{i}},\Lbag r_{i},\epsilon\Rbag)\rangle,\langle s,(\Lbag r_{i},\epsilon\Rbag,t_{a,s_{i}})\rangle,\\ \langle s,(\Lbag s_{i},\epsilon\Rbag,\Lbag r_{i},t_{s_{i}}\Rbag)\rangle,\langle s,(\Lbag r_{i},t_{s_{i}}\Rbag,\Lbag s_{i},\epsilon\Rbag)\rangle,\\ \langle u,(t_{b,s^{\prime}_{i}},\Lbag r_{i},t_{s_{i}}\Rbag)\rangle,\langle u,(\Lbag r_{i},t_{s_{i}}\Rbag,t_{b,s^{\prime}_{i}})\rangle\mid\\ r,s,u\in S\text{ and }i,j\in\{1,2\}\text{ where }i\neq j\text{ and }a,b\in\Sigma_{i}\text{ and }r\xrightarrow{a}s\xrightarrow{b}u\}.\\ \end{array}$$

Full text

1 Introduction

The process of decomposing a complex system into simpler subsystems is the cornerstone of behavioural analysis regardless of where it is applied, to the atom or to the human psyche. Studying the relationship between a complex system and the total behaviour of its decomposition is the subject matter of this paper. However, instead of atoms or human brains, in the field of formal methods, we simply dissect automata. This paper studies how the behaviour of a Labelled Transition System (LTS) can be distributed into a parallel (de)composition of communicating subsystems while maintaining behavioural equivalence.

Motivation

This work was motivated by a case study in the industry [5] based on which we pursued the possibility of deducing the internal components of a system based on the model inferred by the active model learning technique [2]. If it were possible at all, then the learned system must be equivalent to the parallel decomposition deduced.

Our goal is to examine the possibility of such deduction and we do that by devising a decompositioning scheme with certain assumptions, then examine its equivalence with the original system.

Related Work

Previous work done on the topic of decomposition focuses on uniqueness properties and on producing simpler components. For example the primary decomposition theorem by Krohn and Rhodes states that any automaton can be decomposed into a cascaded product of simpler automata such that the automaton is homomorphic to its decomposition [11]. And in 1998, Milner and Moller introduced a semantics of parallel decompositions comprising non-communicating subsystems [13], and they proved that any finite system of behaviour can be decomposed into a unique set of prime parallel non-communicating subsystems. While Milner and Moller’s theorem was in strong bisimulation set in the Calculus of Communicating Systems (CCS), Luttik [12] later introduced a more general framework of commutative monoids that can be used to establish unique decomposition in weak and branching bisimulation semantics.

In contrast to those works, we consider decomposing a system based on partitioning its alphabet into disjoint sets and we require that the subsystems communicate. In that sense, this work is more similar to Brinksma et al. [4] and Hultström [10] who made a decomposition based on a given partition of actions. Another similarity is the need for synchronisation between subsystems as defined in Section 4.1.

Contribution

We define two decompositions of parallel communicating subsystems, one synchronous and the other asynchronous, and we prove that both decompositions maintain branching bisimilarity [7] with the source automaton. We also prove that there is no way of decomposing an automaton (under certain conditions) such that it is divergent-preserving branching-bisimilar [6] to the resulting decomposition. We consider branching bisimilarity, but the results of this paper easily carry over to other equivalences such as weak bisimilarity.

Outline

The outline of this paper is as follows. Section 2 introduces the preliminaries. Section 3 defines and discussed the general decomposition operator on which we base our arguments. Section 4 defines two decompositions of communicating subsystems, one for synchronous communication and the other for asynchronous communication, and proves that each maintains a branching bisimulation relation with the source automaton. Section 5 contains the proof that there is no way of decomposing an automaton, through our general decomposition operator, such that it maintains divergence preserving branching bisimulation with its decomposition. Finally, Section 6 discusses the results and interprets them in light of our initial motivation.

Acknowledgement

We wish to thank Rick Erkens, Bas Luttik, Thomas Neele, Joshua Moerman, Pieter Cuijpers, Bharat Garhewal, Hans van Wezep, Arjan Mooij and the referees of the EXPRESS/SOS 2019 workshop for their thorough feedback, for sharing their knowledge, and for their motivation and support.

2 Preliminaries

In this section, we present the preliminaries of labelled transition systems, the synchronous product and bisimulation relations, aided by [8]. We start with the definition of a labelled transition system (LTS).

Definition 2.1** (LTS).**

We define our LTS as a four-tuple $(S,\Sigma,\rightarrow,s_{0})$ where:

• •

$S$ is a non-empty finite set of states.

• •

$\Sigma$ is the alphabet, also referred to as the action set.

• •

${\rightarrow}\subseteq S\times\Sigma\times S$ is a transition relation.

• •

$s_{0}$ is the initial state.

We use the notation $x\xrightarrow{a}y$ to express a transition with action $a$ from state $x$ to state $y$. This and variations of it are formally defined as follows.

Definition 2.2** (Transition Relation).**

Let $(S,\Sigma,\rightarrow,s_{0})$ be an LTS with $s,s^{\prime}\in S$ and $a\in\Sigma\cup\{\tau\}$, where $\tau$ is the internal/unobservable action. We use the following notations:

[TABLE]

Next, we define complementary actions, i.e., actions on which communicating systems synchronise. Then we define the synchronous product of two automata, and show what role complementary actions play in computing it.

Definition 2.3** (Co-actions).**

For an arbitrary action $a$ that is not $\tau$, the action $\overline{a}$ (read as a bar) is called its co-action. Also, $\overline{(\overline{a})}=a$. We say that actions $a$ and $\overline{a}$ are complementary to each other and we call them a pair of complementary actions.

We lift this operator to sets of actions such that $\overline{\Sigma}=\{\overline{a}\mid a\in\Sigma\}$.

Definition 2.4** (Synchronous Product).**

The synchronous product of two LTSs

$(S_{1},\Sigma_{1},\rightarrow_{1},q_{0})\times$ $(S_{2},\Sigma_{2},\rightarrow_{2},r_{0})$ is the tuple $(S_{1}\times S_{2},\Sigma_{x},\rightarrow_{x},$ $(q_{0},r_{0}))$

where $\Sigma_{x}=(\Sigma_{1}\cup\Sigma_{2})\setminus\{a,\overline{a}\mid a\in\Sigma_{1}\land\overline{a}\in\Sigma_{2}\}$.

The transition relation ${\rightarrow_{x}}\subseteq(S_{1}\times S_{2})\times\Sigma_{x}\times(S_{1}\times S_{2})$ is defined as follows:

[TABLE]

where $\tau$ is the unobservable action.

Next, we define two notions of behavioural equivalence.

Definition 2.5** (Branching bisimulation).**

Given an LTS $(S,\Sigma,\rightarrow,s_{0})$ and a relation $\mathcal{R}\subseteq S\times S$. We call $\mathcal{R}$ a branching bisimulation relation iff for all states $s,t\in S$ such that $\langle s,t\rangle\in\mathcal{R}$, it holds that:

if $s\xrightarrow{a}s^{\prime}$, then:

• •

$a=\tau$ and $\langle s^{\prime},t\rangle\in\mathcal{R}$; or

• •

$t\xrightarrow{\tau}^{*}t^{\prime}\xrightarrow{a}t^{\prime\prime}$, $\langle s,t^{\prime}\rangle\in\mathcal{R}$ and $\langle s^{\prime},t^{\prime\prime}\rangle\in\mathcal{R}$. 2. 2.

Symmetrically, if $t\xrightarrow{a}t^{\prime}$, then:

• •

$a=\tau$ and $\langle s,t^{\prime}\rangle\in\mathcal{R}$; or

• •

$s\xrightarrow{\tau}^{*}s^{\prime}\xrightarrow{a}s^{\prime\prime}$, $\langle s^{\prime},t\rangle\in\mathcal{R}$ and $\langle s^{\prime\prime},t^{\prime}\rangle\in\mathcal{R}$.

Two states $s$ and $t$ are branching bisimilar, denoted $s\leftrightarroweq_{b}t$ iff there is a branching bisimulation relation $\mathcal{R}$ such that $\langle s,t\rangle\in\mathcal{R}$. Two LTSs $P$ and $Q$ are branching bisimilar, denoted $P\leftrightarroweq_{b}Q$, iff their initial states are.

A state $s$ with $s\xrightarrow{\tau}^{\omega}$ is called divergent. Hence, a state with a $\tau$ loop is also called divergent. Branching bisimulation does not preserve divergence, i.e., a divergent state can be branching bisimilar to a non-divergent one. Therefore, a stronger equivalence relation, namely divergence-preserving branching bisimulation, is defined below.

Definition 2.6** (Divergence-preserving branching bisimulation).**

Given an LTS $(S,\Sigma,\rightarrow,s_{0})$ and a relation $\mathcal{R}\subseteq S\times S$. We call $\mathcal{R}$ a divergence-preserving branching bisimulation relation iff it is a branching bisimulation relation and for all states $s,t\in S$ with $\langle s,t\rangle\in\mathcal{R}$, there is an infinite sequence $s\xrightarrow{\tau}s_{1}\xrightarrow{\tau}s_{2}\xrightarrow{\tau}$ with $\langle s_{i},t\rangle\in\mathcal{R}$ for all $i>0$ iff there is an infinite sequence $t\xrightarrow{\tau}t_{1}\xrightarrow{\tau}t_{2}\xrightarrow{\tau}$ and $\langle s,t_{i}\rangle\in\mathcal{R}$ for all $i>0$.

Two states $s$ and $t$ are divergence-preserving branching bisimilar, denoted $s\leftrightarroweq_{db}t$ iff there is a divergence-preserving branching bisimulation relation $\mathcal{R}$ such that $\langle s,t\rangle\in\mathcal{R}$. Two LTSs $P$ and $Q$ are divergence-preserving branching bisimilar, denoted $P\leftrightarroweq_{db}Q$, iff their initial states are.

3 The Decomposition Operation

In this section, we establish a decompositioning scheme that is based on action partitioning in order to refer to it as the general decomposition operation on which our theorems apply. Our general decomposition operation is a function transforming a single LTS, given two disjoint actions sets, into two LTSs. It is formally defined as follows.

Definition 3.1** (General Decomposition Operation).**

Given an LTS $M$ with alphabet $\Sigma$ and given two alphabets $\Sigma_{1},\Sigma_{2}$ such that $\Sigma=\Sigma_{1}\cup\Sigma_{2}$ and $\Sigma_{1}\leavevmode\nobreak\ \cap\leavevmode\nobreak\ \Sigma_{2}=\emptyset$, we call $G$ a general decomposition operator iff $G(M,\Sigma_{1},\Sigma_{2})=(M_{1},M_{2})$ such that $M_{1}$ has alphabet $\Sigma_{M_{1}}$ with ${\Sigma_{1}\subseteq\Sigma_{M_{1}}}$ and ${\Sigma_{M_{1}}\cap\Sigma_{2}=\emptyset}$, and likewise, $M_{2}$ has alphabet $\Sigma_{M_{2}}$ with $\Sigma_{2}\subseteq\Sigma_{M_{2}}$ and $\Sigma_{M_{2}}\cap\Sigma_{1}=\emptyset$.

We refer to a method of decomposing automata as a decomposition operation whereas the result of such transformation is called a decomposition. A decomposition comprises two or more automata. This transformation is depicted in Figure 2. Throughout the paper, we compare LTSs to the synchronous product of the decomposition, and if a a certain bisimulation relation holds between these two, then we say that the operation maintains that relation.

The idea behind this transformation is, given a partition of actions of a system, to generate two subsystems, each using exclusively one of the two parts.

Recursive decomposition.

Note that Definition 3.1 can easily be applied recursively allowing to decompose behaviour into multiple components. As the alphabets over which an automaton can be decomposed can be empty, the number of components over which behaviour can be split can even be arbitrarily large.

4 Branching Bisimilar Decompositions

In this section, we define two decomposition operations that are designed to maintain branching bisimilarity, and we actually prove that they do. The first one ($decomp_{s}$) decomposes into synchronously communicating subsystems while the second ($decomp_{a}$) decomposes into asynchronously communicating ones. In both of these operations, we build two automata that pass control between one another using $c$ messages. Only if an automaton seizes control can it perform one of its actions, otherwise it has to wait for the other to hand control over. Formal definitions and more detail follow.

4.1 Decomposing into Synchronous Subsystems

We define the decomposition of synchronous subsystems, summarised in Figure 1 in two patterns; the top dictates the decomposition of every state in the source LTS while the bottom dictates the decomposition of every transition. An omitted third pattern is symmetric to the second such that the transition’s label simply belongs to the second subsystem rather than the first.

Definition 4.1** (Synchronous Decomposition Operation).**

Given an LTS $M=(S,\Sigma,\rightarrow,q)$ and two alphabets $\Sigma_{1},\Sigma_{2}$ such that $\Sigma=\Sigma_{1}\cup\Sigma_{2}$ and $\Sigma_{1}\cap\Sigma_{2}=\emptyset$, then we can decompose $M$ over $\Sigma_{1}$ and $\Sigma_{2}$ by applying the following operation:

$decomp_{s}(M,\Sigma_{1},\Sigma_{2})=(M_{1},M_{2})$ where:

$M_{1}=(S_{C}\cup S_{T_{1}},\Sigma_{1}\cup\Sigma_{S_{1}},\rightarrow_{1},(q,1))$

$M_{2}=(S_{C}\cup S_{T_{2}},\Sigma_{2}\cup\Sigma_{S_{2}},\rightarrow_{2},(q,1))$. 2. 2.

For every state $s$ in $S$, we introduce two states $(s,1),(s,2)\in S_{C}$:

[TABLE]

Notation.

Tuple-states of the form $(s,i)$ such as $(s,1)$ and $(s,2)$ are shortened to $s_{i}$. Therefore, it is to be held throughout the paper that $s_{i}$ is derived from $s$ rather than it being a completely unrelated symbol to $s$. 3. 3.

The set of $c$-actions is defined as follows:

[TABLE] 4. 4.

The sets of $t$ actions and $t$ states are defined as follows:

[TABLE] 5. 5.

The complete sets of actions of $M_{1}$ and $M_{2}$ are respectively defined as:

[TABLE] 6. 6.

The transition relations ${\rightarrow_{i}}\subseteq(S_{C}\cup S_{T_{i}})\times(\Sigma_{i}\cup\Sigma_{S_{i}})\times(S_{C}\cup S_{T_{i}})$ are defined as follows. For $i,j\in\{1,2\}$ and $i\neq j$, $\rightarrow_{i}$ is the minimal relation satisfying the following:

1. (a)

For all $s\in S$ and for all $c_{s_{i},s_{j}}\in\Sigma_{C}$:

[TABLE] 2. (b)

For all $s,s^{\prime}\in S$, and all $a\in\Sigma_{i}$, if $s\xrightarrow{a}s^{\prime}$, then:

[TABLE]

Two classes of actions are introduced, $c$-actions and $t$-actions. The $c$-actions come in pairs, and they resemble passing a control token between $M_{1}$ and $M_{2}$. For instance, looking at Figure 2, when, at some state $r\in S$ for which a pair of states $r_{1},r_{2}\in S_{C}$ exists in both $M_{1}$ and $M_{2}$, and control is to be passed from $M_{1}$ to $M_{2}$, then a pair of complementary $c$ actions synchronises, namely, actions $c_{r_{1},r_{2}}$ and $\overline{c_{r_{1},r_{2}}}$, to produce a synchronous transition in both machines from $r_{1}$ to $r_{2}$. Likewise, actions $c_{r_{2},r_{1}}$ and $\overline{c_{r_{2},r_{1}}}$ synchronise to pass control in the opposite direction from $M_{2}$ to $M_{1}$.

The $t$-actions are introduced to synchronise transitions occurring in one machine with the other. In addition, they require the introduction of $t$-states. Observe Figure 2 where an $a_{1}$ transition occurs in $M_{1}$. The aim is the transition $r_{1}\xrightarrow{a_{1}}s_{1}$, but in order to synchronise this with $M_{2}$, we introduce a middle state $t_{a_{1},s_{1}}\in S_{T_{1}}$ from which the only possible transition is $t_{a_{1},s_{1}}\xrightarrow{t_{s_{1}}}s_{1}$ which synchronises with the transition $r_{1}\xrightarrow{\overline{t_{s_{1}}}}s_{1}$ in $M_{2}$.

The operation ($decomp_{s}$) can be summarised by two patterns shown in Figure 1; the top pattern applies to each state and the bottom one applies to each transition.

Is the Decomposition a Simplification?

The decomposition is obviously larger than the original system. That is due to the nature of an alphabet-partitioning-based decomposition where subsystems must hand control over between one another. Thus, every subsystem must have, for each state in the original, multiple ones expressing where control lies. In special cases, a smaller component may suffice; for example, in Figure 2, because state $r$ enables no $b$ actions, a state $r_{2}$ is not needed and all transitions going to $r_{2}$ can instead go to $r_{1}$. However, we believe that our definition the way it is is more understandable because of its generality and symmetry. The element of simplification lies not in reducing the size of a system but rather in partitioning its alphabet.

Computing the Synchronous Product.

For a decomposition $(M_{1},M_{2})$ by Definition 4.1, the synchronous product $M_{x}=M_{1}\times M_{2}$ is the LTS $(S_{x},\Sigma_{1}\cup\Sigma_{2},\rightarrow_{x},(q_{1},q_{1}))$, where:

[TABLE]

with $\Sigma_{S_{1}},\Sigma_{S_{2}},S_{T_{1}},S_{T_{2}}$ being sets introduced by $decomp_{s}$. The transition relation $\rightarrow_{x}$ is defined as follows for $i,j\in\{1,2\}$ and $i\neq j$:

if $s\xrightarrow{a}s^{\prime}$ and $a\in\Sigma_{i}$ then by (LABEL:eq1) there is a state $t_{a,s^{\prime}_{i}}\in S_{T_{i}}$ and a pair of complementary actions $t_{s^{\prime}_{i}},\overline{t_{s^{\prime}_{i}}}\in\Sigma_{S_{i}}$ such that:

[TABLE]

[TABLE] 2. 2.

For all $s\in S$, there exist $c_{s_{i},s_{j}},c_{s_{j},s_{i}}\in\Sigma_{C}$ such that, by (5), $s_{i}\xrightarrow{c_{s_{i},s_{j}}}_{i}s_{j}$ and $s_{i}\xrightarrow{\overline{c_{s_{i},s_{j}}}}_{j}s_{j}$, and thus:

[TABLE]

4.2 Proof that the synchronous decomposition operation maintains branching bisimulation

In this subsection, we show an application of $decomp_{s}$ (Definition 4.1) to a sample LTS, we demonstrate that $decomp_{s}$ maintains branching bisimilarity, and then we prove that branching bisimilarity is maintained through any and all applications of $decomp_{s}$.

Figure 2 shows the LTS at the left side and its decomposition at the right side. The two patterns shown in Figure 1 can be applied directly to this LTS. The top pattern applies twice, once per state, and the bottom pattern applies three times, once per transition.

Next, we compute the synchronous product and form one LTS shown at the right of Figure 3. The nodes are divided into two equivalence classes, top and bottom. The states in the top class are branching bisimilar to state $r$ whereas the states in the bottom one are branching bisimilar to state $s$.

The following proves the branching bisimilarity and thus proves that there is a way of decomposing an LTS such that branching bisimilarity is maintained.

Theorem 4.2**.**

Given an LTS $M=(S,\Sigma,\rightarrow,s_{0})$ and two alphabets $\Sigma_{1},\Sigma_{2}$ such that $\Sigma=\Sigma_{1}\cup\Sigma_{2}$ and $\Sigma_{1}\cap\Sigma_{2}=\emptyset$, and given an LTS $M_{x}=M_{1}\times M_{2}$ where $(M_{1},M_{2})=decomp_{s}(M)$ by Definition 4.1, then $M\leftrightarroweq_{b}M_{x}$.

Proof.

Let $M_{1}=(S_{C}\cup S_{T_{1}},\Sigma_{1}\cup\Sigma_{S_{1}},\rightarrow_{1},q_{1})$ and $M_{2}=(S_{C}\cup S_{T_{2}},\Sigma_{2}\cup\Sigma_{S_{2}},\rightarrow_{2},q_{2})$.

Define a relation $\mathcal{R}\subseteq S\times((S_{C}\cup S_{T_{1}})\times(S_{C}\cup S_{T_{2}}))$ with $\mathcal{R}=\{\langle s,(s_{n},s_{n})\rangle$, $\langle r^{\prime},(t_{a,r^{\prime}_{n}},r_{n})\rangle$, $\langle r^{\prime},(r_{n},t_{a,r^{\prime}_{n}})\rangle$ $\mid s,r,r^{\prime}\in S,n\in\{1,2\}$, $a\in\Sigma$, $r\xrightarrow{a}r^{\prime}\}$. We prove that $\mathcal{R}$ is a branching bisimulation relation through the following cases:

Consider a pair $\langle s,s_{x}\rangle=\langle s,(s_{n},s_{n})\rangle$ where $n\in\{1,2\}$.

1. (a)

Assume $s\xrightarrow{a}s^{\prime}$. Then we have two cases:

1. i.

$a\in\Sigma_{1}$. Then, by (8), $s_{x}\xrightarrow{a}_{x}(t_{a,s^{\prime}_{n}},s_{n})$. We see that $\langle s^{\prime},(t_{a,s^{\prime}_{n}},s_{n})\rangle\in\mathcal{R}$. 2. ii.

$a\in\Sigma_{2}$. Then, by (8), $s_{x}\xrightarrow{a}_{x}(s_{n},t_{a,s^{\prime}_{n}})$. We see that $\langle s^{\prime},(s_{n},t_{a,s^{\prime}_{n}})\rangle\in\mathcal{R}$. 2. (b)

Assume $s_{x}\xrightarrow{a}_{x}s_{x}^{\prime}$. Then we have the following three cases:

1. i.

$a\in\Sigma_{1}\land\overline{a}\not\in\Sigma_{2}$, then this transition is only possible, by definition, through the transition $s\xrightarrow{a}s^{\prime}$ for some $s^{\prime}$ such that $s_{x}^{\prime}\overset{\mathrm{(\ref{eq3})}}{=}(t_{a,s^{\prime}},s_{1})$. We see that $\langle s^{\prime},s_{x}^{\prime}\rangle\in\mathcal{R}$. 2. ii.

$a\in\Sigma_{2}\land\overline{a}\not\in\Sigma_{1}$. This is a symmetric case where $s\xrightarrow{a}s^{\prime}$ and $s_{x}^{\prime}\overset{\mathrm{(\ref{eq3})}}{=}(s_{2},t_{a,s^{\prime}})$. We see that $\langle s^{\prime},s_{x}^{\prime}\rangle\in\mathcal{R}$. 3. iii.

$a\in\Sigma_{1}\land\overline{a}\in\Sigma_{2}$, then the only transition possible is the $\tau$ transition of (LABEL:eq5). Then $s_{x}^{\prime}=(s_{m},s_{m})$ where $m\in\{1,2\}$ and $m\neq n$. We see that $\langle s,s_{x}^{\prime}\rangle\in\mathcal{R}$. 2. 2.

Consider a pair $\langle r,r_{x}\rangle=\langle s^{\prime},(t_{a,s^{\prime}_{n}},s_{n})\rangle$ where $n\in\{1,2\}$, $a\in\Sigma$ and $s\xrightarrow{a}s^{\prime}$.

1. (a)

Assume $r\xrightarrow{a}r^{\prime}$. Then we show that $r_{x}\xrightarrow{\tau}_{x}r_{x}^{\prime}$ and $r_{x}^{\prime}\xrightarrow{a}_{x}r_{x}^{\prime\prime}$ and $\langle r,r_{x}^{\prime}\rangle\in\mathcal{R}$ and $\langle r^{\prime},r_{x}^{\prime\prime}\rangle\in\mathcal{R}$. We do this for $a\in\Sigma_{1}$. The case for $a\in\Sigma_{2}$ is symmetric.

1. i.

$r_{x}^{\prime}\overset{\mathrm{(\ref{eq3})}}{=}(s^{\prime}_{2},s^{\prime}_{2})$. We see that $\langle r,r_{x}^{\prime}\rangle\in\mathcal{R}$. 2. ii.

Since $r=s^{\prime}$ and $r\xrightarrow{a}r^{\prime}$, then by (8), there exists a state $r_{x}^{\prime\prime}$ such that $r_{x}^{\prime}\xrightarrow{a}_{x}r_{x}^{\prime\prime}$, and $r_{x}^{\prime\prime}=(t_{a,s^{\prime\prime}_{2}},s^{\prime}_{2})$, where $s^{\prime\prime}=r^{\prime}$. We see that $\langle r^{\prime},r_{x}^{\prime\prime}\rangle\in\mathcal{R}$. 2. (b)

Assume $r_{x}\xrightarrow{a}_{x}r_{x}^{\prime}$. By the definition of $\rightarrow_{x}$, it is only possible that $a$ is a $\tau$ action and that $n=1$. Thus, $r_{x}^{\prime}\overset{\mathrm{(\ref{eq3})}}{=}(s^{\prime}_{2},s^{\prime}_{2})$. We see that $\langle r^{\prime},r_{x}^{\prime\prime}\rangle\in\mathcal{R}$. 3. 3.

Consider a pair $\langle r,r_{x}\rangle=\langle s^{\prime},(s_{n},t_{a,s^{\prime}_{n}})\rangle$ where $n\in\{1,2\}$, $a\in\Sigma$ and $s\xrightarrow{a}s^{\prime}$. This case is symmetric to Case 2.

∎

Corollary 4.3**.**

It follows from Theorem 4.2 that there is a universal way of decomposing an LTS $M$ using a general synchronous decomposition operator (Definition 3.1) such that $M$ is branching-bisimilar to the synchronous product of its decomposition.

4.3 Decomposing into Asynchronous Subsystems

We consider asynchronous communication between subsystems simply because many practical systems use asynchronous communication and the aim is to extend our proof towards that. So, we define a new decomposition operation ($decomp_{a}$) such that the communication between subsystems is asynchronous. We assign each subsystem a queue that stores received messages until they are consumed. An action of sending such a message does synchronise, however, with the queue of the opposite side receiving it. The operation $decomp_{a}$ is summarised in Figure 4.

Definition 4.4** (LTS with Queue).**

A queue is an ordered-list of actions. An LTS with a queue is a transition system of the shape $(S\times Q,\Sigma,\rightarrow,s_{0})$. A state in $S\times Q$ holds the contents of the queue $Q$ and is written as $\Lbag s,Q\Rbag$.

Elements in a queue are concatenated using the $\cdot$ operator. Appending an element $m$ to the back of a queue $Q$ produces the queue $m\cdot Q$, while $Q\cdot m$ represents the queue with $m$ in the front. The symbol $\epsilon$ represents the empty queue.

Definition 4.5** (Decomposing into asynchronous subsystems).**

Given an LTS $M=(S,\Sigma,\rightarrow,r_{0})$ and two alphabets $\Sigma_{1},\Sigma_{2}$ such that $\Sigma=\Sigma_{1}\cup\Sigma_{2}$ and $\Sigma_{1}\cap\Sigma_{2}=\emptyset$, then we can decompose $M$ over $\Sigma_{1}$ and $\Sigma_{2}$ by applying the following operation:

$decomp_{a}(M,\Sigma_{1},\Sigma_{2})=(M_{1},M_{2})$ where, for $i,j\in\{1,2\}$ and $i\neq j$, $M_{i}$ is an LTS with a queue (Definition 4.4) defined as follows:

$M_{i}=((S_{C}\cup S_{T_{i}},Q_{i}),\Sigma_{i}\cup\Sigma_{S_{i}},\rightarrow_{i},r_{1})$ 2. 2.

For every state in $S$, we introduce a pair of states $s_{1},s_{2}\in S_{C}$, a pair of $c$-actions, and a pair of $t$-actions:

[TABLE] 3. 3.

Sets of $t$-states are defined as follows:

[TABLE] 4. 4.

Sets of synchronous actions are defined as follows:

[TABLE] 5. 5.

The transition relation ${\rightarrow_{i}}\subseteq(S_{C}\cup S_{T_{i}})\times Q_{i}\times(\Sigma_{i}\cup\Sigma_{S_{i}})\times(S_{C}\cup S_{T_{i}})\times Q_{i}$ is the minimal relation satisfying the following:

1. (a)

For all $s\in S$:

[TABLE] 2. (b)

For all $s,s^{\prime}\in S$, and all $a\in\Sigma_{i}$, if $s\xrightarrow{a}s^{\prime}$, then:

[TABLE] 3. (c)

Consuming an element from the front of a queue is an internal transition of the form:

[TABLE]

We see in (13) that the two automata synchronise on action $c_{s_{i,j}}$. The effect is a message sent from $M_{i}$ and received in the queue of $M_{j}$. The same occurs in (LABEL:eq:a-transition-2). Moreover, this makes sending messages only possible when both machines are in sync, i.e., on the same state $s_{i}$. This model is inspired by asynchronous communication in practice and we found it necessary that a sent message is received before any other actions are performed by either side.

The question may arise “why do we still see synchronisation? Is this still considered asynchronous communication?”; and the answer is that it is asynchronous in the sense that the sending party does not know whether and when the receiving party is willing to receive the communication. This is different from synchronous communication where the sender knows that the receiver is willing to participate.

For this construction, a queue of size 1 is enough as it never contains more than one message. If the size of the queue was more than 1, then the transition in (LABEL:eq:a-transition-2) can apply recursively until the queue is full. However, any transition beyond the first one does not translate into a transition in the product because action $c_{s_{i,j}}$ needs to synchronise with its co-action. In other words, in the product automaton, the queue cannot contain more than one message. Therefore, the upperbound of size 1 of the queue is not a requirement, but rather follows from the construction.

4.4 Proof that the Asynchronous Decomposition Operation Maintains Branching Bisimulation

In this subsection, similar to Section 4.2, we prove that the asynchronous decomposition operation ($decomp_{a}$) also maintains branching bisimilarity. Figure 5 shows the result of applying $decomp_{a}$ to the same example behaviour as in Figure 2. In Figure 6, we compute the synchronous product of the decomposition of Figure 5 and then divide the nodes of the product into two equivalence classes, top and bottom. The states in the top class are branching bisimilar to state $r$ whereas the states in the bottom on are branching bisimilar to state $s$.

Next, we prove that any LTS decomposed using Definition 4.5 maintains branching bisimulation with its decomposition, thus by proving that there is at least one universal method of decomposing LTSs into asynchronous ones while maintaining branching bisimulation.

Theorem 4.6**.**

Given an LTS $M=(S,\Sigma,\rightarrow,s_{0})$ and two alphabets $\Sigma_{1},\Sigma_{2}$ such that $\Sigma=\Sigma_{1}\cup\Sigma_{2}$ and $\Sigma_{1}\cap\Sigma_{2}=\emptyset$, and given an LTS $M_{x}=M_{1}\times M_{2}$ where $(M_{1},M_{2})=decomp_{a}(M)$ by Definition 4.5, then $M\leftrightarroweq_{b}M_{x}$.

Proof.

Let $M_{1}=((S_{C}\cup S_{T_{1}},Q_{1}),\Sigma_{1}\cup\Sigma_{S_{1}},\rightarrow_{1},r_{1})$ and $M_{2}=((S_{C}\cup S_{T_{2}},Q_{2}),\Sigma_{2}\cup\Sigma_{S_{2}},\rightarrow_{2},r_{1})$.

Define a relation $\mathcal{R}\subseteq S\times((S_{C}\cup S_{T_{1}},Q_{1})\times(S_{C}\cup S_{T_{2}},Q_{2}))$ with $\mathcal{R}=$

[TABLE]

We prove that $\mathcal{R}$ is a branching bisimulation relation through the following cases:

Consider a pair $\langle s,s_{x}\rangle=\langle s,(\Lbag s_{i},\epsilon\Rbag,\Lbag s_{i},\epsilon\Rbag)\rangle$ where $i\in\{1,2\}$.

1. (a)

Assume $s\xrightarrow{a}s^{\prime}$. Then if $a\in\Sigma_{1}$, then $s_{x}\xrightarrow{a}_{1}s^{\prime}_{x}$ where $s^{\prime}_{x}\overset{(\ref{eq:a-transition-2})}{=}(t_{a,s^{\prime}_{i}},\Lbag s_{i},\epsilon\Rbag)$ with $i=1$. Else if $a\in\Sigma_{2}$ then $s_{x}\xrightarrow{a}_{2}s^{\prime\prime}_{x}$ where $s^{\prime\prime}_{x}\overset{(\ref{eq:a-transition-2})}{=}(\Lbag s_{i},\epsilon\Rbag,t_{a,s^{\prime}_{i}})$ with $i=2$. We see that both pairs $\langle s,s^{\prime}_{x}\rangle$ and $\langle s,s^{\prime\prime}_{x}\rangle$ are in $\mathcal{R}$. 2. (b)

Assume $s_{x}\xrightarrow{a}_{x}s^{\prime}_{x}$. Then we have the following three cases:

1. i.

$a\in\Sigma_{1}\land\overline{a}\not\in\Sigma_{2}$, then this transition is only possible, by definition, through the transition $s\xrightarrow{a}s^{\prime}$ for some $s^{\prime}$ such that $s_{x}^{\prime}\overset{\mathrm{(\ref{eq:a-transition-2})}}{=}(t_{a,s^{\prime}},s_{1})$. We see that the pair $\langle s^{\prime},s_{x}^{\prime}\rangle\in\mathcal{R}$ and is covered in case 4. 2. ii.

$a\in\Sigma_{2}\land\overline{a}\not\in\Sigma_{1}$. This is a symmetric case where $s\xrightarrow{a}s^{\prime}$ and $s_{x}^{\prime}\overset{\mathrm{(\ref{eq:a-transition-2})}}{=}(s_{2},t_{a,s^{\prime}})$. We see that the pair $\langle s^{\prime},s_{x}^{\prime}\rangle\in\mathcal{R}$ and is covered in case 5. 3. iii.

$a\in\Sigma_{1}\land\overline{a}\in\Sigma_{2}$, then the only transition possible is the $\tau$ transition of (13). Then either $s_{x}^{\prime}=(\Lbag s_{j},\epsilon\Rbag,\Lbag s_{i},t_{s_{j}}\Rbag)$ or $s^{\prime}_{x}=(\Lbag s_{i},t_{s_{j}}\Rbag,\Lbag s_{j},\epsilon\Rbag)$ where $j\in\{1,2\}$ and $j\neq i$. We see that in both possible values of $s^{\prime}_{x}$, the pair $\langle s,s_{x}^{\prime}\rangle\in\mathcal{R}$ and is covered in cases 2 and 3. 2. 2.

Consider a pair $\langle s,s_{x}\rangle=\langle s,(\Lbag s_{i},t_{s_{j}}\Rbag,\Lbag s_{j},\epsilon\Rbag)\rangle$.

1. (a)

Assume $s\xrightarrow{a}s^{\prime}$. Then $s_{x}\xrightarrow{\tau}_{x}(\Lbag s_{j},\epsilon\Rbag,\Lbag s_{j},\epsilon\Rbag)$, and we covered the pair $\langle s,(\Lbag s_{j},\epsilon\Rbag,\Lbag s_{j},\epsilon\Rbag)\rangle$ in case 1. 2. (b)

Assume $s_{x}\xrightarrow{a}_{x}s^{\prime}_{x}$. The only possible transition in $\rightarrow_{x}$ is if $a$ is a $\tau$ action consuming the queue message $t_{s_{j}}$ then $s^{\prime}_{x}=(\Lbag s_{j},\epsilon\Rbag,\Lbag s_{j},\epsilon\Rbag)$ and we covered the pair $\langle s,(\Lbag s_{j},\epsilon\Rbag,\Lbag s_{j},\epsilon\Rbag)\rangle$ in case 1. 3. 3.

Consider a pair $\langle s,s_{x}\rangle=\langle s,(\Lbag s_{j},\epsilon\Rbag,\Lbag s_{i},t_{s_{j}}\Rbag)\rangle$. Symmetric to case 2. 4. 4.

Consider a pair $\langle s,s_{x}\rangle=\langle s,(t_{a,s_{i}},\Lbag r_{i},\epsilon\Rbag)\rangle$ such that $r\xrightarrow{a}s$.

1. (a)

Assume $s\xrightarrow{b}s^{\prime}$. Then $s_{x}\xrightarrow{\tau}_{x}(\Lbag s_{i},\epsilon\Rbag,\Lbag r_{i},t_{s_{i}}\Rbag)$. 2. (b)

Assume $s_{x}\xrightarrow{b}_{x}s^{\prime}_{x}$. The only possible transition in $\rightarrow_{x}$ is if $b$ is a $\tau$ action resulting from the synchronisation of the two transitions $t_{a,s_{i}}\xrightarrow{t_{s_{i}}}_{i}\Lbag s_{i},\epsilon\Rbag$ and $\Lbag r_{i},\epsilon\Rbag\xrightarrow{\overline{t_{s_{i}}}}_{j}\Lbag r_{i},t_{s_{i}}\Rbag$. Then, in the product, $s_{x}\xrightarrow{\tau}_{x}(\Lbag s_{i},\epsilon\Rbag,\Lbag r_{i},t_{s_{i}}\Rbag)$; and the pair $\langle s,(\Lbag s_{i},\epsilon\Rbag,\Lbag r_{i},t_{s_{i}}\Rbag)\rangle\in\mathcal{R}$ and is covered in case 6. 5. 5.

Consider a pair $\langle s,s_{x}\rangle=\langle s,(\Lbag r_{i},\epsilon\Rbag,t_{a,s_{i}})\rangle$. Symmetric to case Case 4. 6. 6.

Consider a pair $\langle s,s_{x}\rangle=\langle s,(\Lbag s_{i},\epsilon\Rbag,\Lbag r_{i},t_{s_{i}}\Rbag)\rangle$ such that $r\xrightarrow{a}s$.

1. (a)

Assume $s\xrightarrow{b}s^{\prime}$. Then because of the queue-consuming transition $\Lbag r_{i},t_{s_{i}}\Rbag\xrightarrow{\tau}_{j}\Lbag s_{i},\epsilon\Rbag$, then $s_{x}\xrightarrow{\tau}_{x}(\Lbag s_{i},\epsilon\Rbag,\Lbag s_{i},\epsilon\Rbag)$.

The pair $\langle s,(\Lbag s_{i},\epsilon\Rbag,\Lbag s_{i},\epsilon\Rbag)\rangle$ is covered in case 1. 2. (b)

Assume $s_{x}\xrightarrow{b}_{x}s_{x}^{\prime}$, then there are two possible values for $b$:

1. i.

Action $b$ is a queue-consuming $\tau$, then $s_{x}\xrightarrow{\tau}_{x}(\Lbag s_{i},\epsilon\Rbag,\Lbag s_{i},\epsilon\Rbag)$; and the pair

$\langle s,(\Lbag s_{i},\epsilon\Rbag,\Lbag s_{i},\epsilon\Rbag)\rangle$ is covered in case 1. 2. ii.

$b\in\Sigma_{i}$, then $s_{x}\xrightarrow{b}_{x}(t_{b,s^{\prime}_{i}},\Lbag r_{i},t_{s_{i}}\Rbag)$ such that $s\xrightarrow{b}s^{\prime}$; and the pair $\langle s^{\prime},(t_{b,s^{\prime}_{i}},\Lbag r_{i},t_{s_{i}}\Rbag)\rangle\in\mathcal{R}$. 7. 7.

Consider a pair $\langle s,s_{x}\rangle=\langle s,\Lbag r_{i},t_{s_{i}}\Rbag,\Lbag s_{i},\epsilon\Rbag)\rangle$. Symmetric to case 6. 8. 8.

Consider a pair $\langle s,s_{x}\rangle=\langle s,(t_{a,s_{i}},\Lbag\Lbag p_{i},\epsilon\Rbag,t_{r_{i}}\Rbag)\rangle$ such that $p\xrightarrow{b}r\xrightarrow{a}s$. Then $s_{x}\xrightarrow{\tau}(t_{a,s_{i}},\Lbag r_{i},\epsilon\Rbag)$; and the pair $\langle s,(t_{a,s_{i}},\Lbag r_{i},\epsilon\Rbag)\rangle$ is covered in case 4. 9. 9.

Consider a pair $\langle s,s_{x}\rangle=\langle s,(\Lbag p_{i},t_{r_{i}}\Rbag,t_{a,s_{i}})\rangle$ such that $p\xrightarrow{b}r\xrightarrow{a}s$. This is symmetric to case 8.

∎

Corollary 4.7**.**

It follows from Theorem 4.6 that there is a universal way of decomposing an LTS $M$ using a general asynchronous decomposition operator (Definition 3.1) such that $M$ is branching-bisimilar to the synchronous product of its decomposition.

5 Proof that no decomposition operation maintains $\leftrightarroweq_{db}$

In this section, we prove that there is no way of decomposing an LTS such that it is divergence-preserving branching-bisimilar to the synchronous product of its decomposition.

We define confluence based on [9].

Definition 5.1** (Confluence).**

An LTS $(S,\Sigma_{1}\cup\Sigma_{2},\rightarrow,s_{0})$ is called confluent over $\Sigma_{1}$ and $\Sigma_{2}$ iff for all states $s,s_{a},s_{b}\in S$ and for all $a\in\Sigma_{1}$ and $b\in\Sigma_{2}$, if $s\xrightarrow{a}s_{a}$ and $s\xrightarrow{b}s_{b}$, then there is a state $s_{c}$ such that $s_{b}\xrightarrow{a}s_{c}$ and $s_{a}\xrightarrow{b}s_{c}$.

Lemma 5.2**.**

Any LTS $M$ that is the synchronous product (Definition 2.4) of two LTSs $M_{1}$ and $M_{2}$ whose action sets are $\Sigma_{1}$ and $\Sigma_{2}$ respectively, is confluent over two sets $\Sigma_{1}\setminus\overline{\Sigma_{2}}$ and $\Sigma_{2}\setminus\overline{\Sigma_{1}}$.

Proof.

Consider the synchronous product $(S_{1}\times S_{2},\Sigma_{x},\rightarrow_{x},(q_{0},r_{0}))$ from Definition 2.4 and some actions $a\in\Sigma_{1}\setminus\overline{\Sigma_{2}}$ and $b\in\Sigma_{2}\setminus\overline{\Sigma_{1}}$. Then $a\neq\overline{b}$. Consider some states $s,s^{\prime}\in S_{1}$, $t,t^{\prime}\in S_{2}$, and $s_{a}\in S_{1}\times S_{2}$. We know that if $(s,t)\xrightarrow{a}s_{a}$ then that is due to a transition $s\xrightarrow{a}s^{\prime}$ and that makes $s_{a}=(s^{\prime},t)$, and that given a transition $t\xrightarrow{b}t^{\prime}$, then a transition $(s^{\prime},t)\xrightarrow{b}(s^{\prime},t^{\prime})$ is possible. Similarly, if $(s,t)\xrightarrow{b}(s,t^{\prime})$ then $(s,t^{\prime})\xrightarrow{a}(s^{\prime},t^{\prime})$. Therefore, the defined synchronous product is confluent. ∎

Figure 7 (centre) shows a simple LTS $P$. Concretely, it is defined as $(\{p,r,s\},\Sigma_{1}\cup\Sigma_{2},{\rightarrow},p)$ with alphabets $\Sigma_{1}=\{a\}$ and $\Sigma_{2}=\{b\}$ and transitions $p\xrightarrow{a}r$ and $p\xrightarrow{b}s$. In the following lemma and theorem, we prove that no way of decomposing $P$ maintains divergence-preserving branching bisimulation.

Lemma 5.3**.**

Given the LTS $P$ (Figure 7, centre) with action set $\Sigma_{1}\cup\Sigma_{2}$, let $P_{1}$ and $P_{2}$ be two LTSs with action sets $\Sigma_{P_{1}}$ and $\Sigma_{P_{2}}$ respectively, and with $\Sigma_{1}\subseteq\Sigma_{P_{1}}$ and $\Sigma_{2}\subseteq\Sigma_{P_{2}}$ and $\Sigma_{1}\cap\Sigma_{2}=\emptyset=\Sigma_{1}\cap\Sigma_{P_{2}}=\Sigma_{P_{1}}\cap\Sigma_{2}$. Let $P_{x}$ be the synchronous product $P_{1}\times P_{2}$ by Definition 2.4. Then $P\not\leftrightarroweq_{db}P_{x}$.

Proof.

We prove this lemma by contradiction. Assume that $P\leftrightarroweq_{db}P_{x}$, and let $p_{x}$ be the initial state of $P_{x}$, then $p\leftrightarroweq_{db}p_{x}$. As $p$ is not divergent and cannot do a $\tau$-transition, it holds that only finite sequences of $\tau$’s are possible from $p_{x}$. This can be seen as follows. If $p_{x}\xrightarrow{\tau}p_{1}\xrightarrow{\tau}p_{2}\xrightarrow{\tau}\cdots$, then $p\leftrightarroweq_{b}p_{i}$ for all $i>0$. Hence, $p_{x}$ is divergent. But this is not possible because $p$ is not divergent. So, $p_{x}$ takes a finite number of $\tau$ steps to reach some state $p^{\prime}_{x}$ where $p^{\prime}_{x}\not\xrightarrow{\tau}$.

Since it must be that $p\leftrightarroweq_{db}p^{\prime}_{x}$, and since $p\xrightarrow{a}r$ and $p\xrightarrow{b}s$ where $a\in\Sigma_{1}$ and $b\in\Sigma_{2}$, then there are two states $r_{x}$ and $s_{x}$ such that $p^{\prime}_{x}\xrightarrow{a}r_{x}$ and $p^{\prime}_{x}\xrightarrow{b}s_{x}$, and $r\leftrightarroweq_{db}r_{x}$ and $s\leftrightarroweq_{db}s_{x}$.

Now because $a\in\Sigma_{1}\setminus\overline{\Sigma_{2}}$ and $b\in\Sigma_{2}\setminus\overline{\Sigma_{1}}$, then $P_{x}$ is confluent over these two sets, then there must exist a state $p^{\prime\prime}_{x}$ such that $r_{x}\xrightarrow{b}p^{\prime\prime}_{x}$. However, $r\not\xrightarrow{b}$. Therefore, $r\not\leftrightarroweq_{db}r_{x}$. Contradiction. Therefore $P\not\leftrightarroweq_{db}P_{x}$. ∎

The proof is illustrated in Figure 7 showing that divergence-preserving branching bisimulation ($\leftrightarroweq_{db}$) does not hold when decomposing the LTS $P$ due to the confluence property of decompositions. On the other hand (literally the other hand of the same figure), branching bisimulation holds when decomposing LTS $P$. The reason it holds under $\leftrightarroweq_{b}$, but not under $\leftrightarroweq_{db}$ is that the former admits infinite $\tau$ cycles, i.e. divergence, which, as demonstrated here in right side of the figure, avoids the premise of confluence altogether. [3] provides a similar insight into how divergence maintains branching bisimilarity but breaks divergence-preserving branching bisimilarity.

Theorem 5.4**.**

There is no decomposition operation that maintains divergence-preserving branching bisimulation ($\leftrightarroweq_{db}$) for all LTSs.

Proof.

We prove this theorem by contradiction. Assume that there is a decomposition operation that maintains $\leftrightarroweq_{db}$ for all LTSs. Then it must do so for any arbitrary LTS $P$. But since Lemma 5.3 proves that no LTS maintains $\leftrightarroweq_{db}$ for one such LTS $P$, i.e the one in Figure 7, then there is no decomposition operation that maintains $\leftrightarroweq_{db}$ for all LTSs. ∎

6 Interpretation

One way to understand this fundamental result is that if the subsystems of the decomposition must communicate, then there is no escape from introducing divergence in order to maintain equivalence over any and all decompositions of LTSs.

With respect to automata learning, this result implies that, unless one values divergency, it is not possible to make any assumption about the distribution of components based on the information that is learned. If one can observe divergencies while learning behaviour, it might be possible to say something about the internal structure of a system though this will be highly non trivial to accomplish.

And with respect to software, our result says that it is always possible to distribute a piece of software over different components if one allows divergent behaviour. Otherwise, such a distribution is not possible and based on our proof. One can see that this already applies to very simple behaviours.

Furthermore, divergence, in an industrial context, is undesired due to the requirement of fairness, i.e., one subsystem seizing unfair control over the total behaviour of the system through infinite looping. This means that if some decomposition is found to maintain fairness, then that is guaranteed not to be the case universally over all contexts and all LTSs.