1 Introduction↩︎

Asynchronous automata (AA) are a foundational model for concurrent systems, where independent processes synchronise on a predefined set of shared actions. The property of connectedly communicating processes was introduced in [1] as a subclass of AAs where the monadic second order logic theory is decidable in the branching time setting. An AA is said to be connectedly communicating if there is a bound \(d\) such that, when some process executes \(d\) steps without hearing from some other process, then these two processes will not communicate any more in the future, even indirectly. In the context of distributed algorithms, this property can model a permanent crash of a communication link, which is a realistic assumption in large networks. Some algorithms like consensus or election are designed to be (sometimes partially) resilient with respect to such failures [2], [3]. In the asynchronous communication setting, when there is no uniform bound on communication delays, a process which does not receive messages from another process may also assume that a failure occurred and stop communicating with this process. This would be the case for instance in a client-server architecture, where the client stops sending requests if it does not receive any answer from the server for some time.

Zielonka’s theorem provides a method for synthesising a deterministic AA from a given deterministic finite-state automaton (DFA) satisfying a certain commutativity property, and an alphabet distribution among processes [4]. This construction is known to be extremely complex and has been the subject of numerous refinements and optimisations (e.g. [5]–[7]), leading to an optimal Zielonka-type construction [8]. In all these constructions, each process keeps track of what it believes to be the latest “information” available to every other process. When there is a shared action, the processes share their local information, reconcile them and update their local states. This underlying idea is implemented using a gossip automaton in [6], [9], and so-called zones in [7], [8]. This yields a number of local states that is exponential in the number of processes, whereas the construction can be kept polynomial in the number of states of the DFA.

Several solutions have been considered to avoid the resolution of this gossip problem, e.g. compositional methods [10]–[12] that still require a number of states exponential in the number of processes. Other solutions are based on restricting the topology of communications [13], [14] and a recent work [15] has proposed a logic-based construction going through a local, past-oriented fragment of propositional dynamic logic. The AA is obtained by a cascade product of localised AAs, which essentially operate on a single process.

Finally, a recent proposal [16] considered so-called fair specifications: a DFA is \(d\)-fair whenever every word of length \(d\) that can be read in the DFA makes every process participate at least once. In this case, a synthesis procedure is presented where the resulting AA is linear in the size of the DFA, polynomial in the size of the alphabet, and the only exponential explosion is related to the parameter \(d\). The complexity is independent of the number of processes. The synthesis procedure has been implemented in a tool FAAST [17] and has also been used to synthesise AAs recognising all \(d\)-fair traces of a (potentially non-fair) DFA specification. Other orthogonal restrictions on the DFA specification leading to implementations include safe AAs [18] and realistic AAs [19].

Our goal in this paper is to present an AA synthesis procedure for specifications corresponding to connectedly communicating processes. The condition of connected communication that we study in this article can be seen as a relaxation of the fairness constraint: we first show that in DFA specifications modelling connectedly communicating processes, the strongly connected components are fair for the subset of processes that are still potentially communicating with each other. Then, we adapt the construction proposed in [16], wherein each process maintains a finite suffix of its view. Thanks to the fairness hypothesis, the prefix of its view that it has cut is known by every other process. We cannot do this any more for our case of connected communication, since processes may separate after having communicated to a certain point. To handle this aspect, we need a mechanism to cut parts of the view in the middle (and not necessarily a prefix). Hence, our modified construction splits the view into phases and cuts a prefix within each phase. The phase splits happen when some processes stop communicating, and thus do not occur too often. Therefore, we obtain a construction that is polynomial in the number of states of the DFA, and where the only exponential explosion is related to the parameter \(d\), and the separation depth of processes.

After presenting preliminary notions in Section 2, we recall the construction for fair systems [16] in Section 3. In Section 4, we provide a characterization of DFAs corresponding to connectedly communicating processes and go on to the full construction in Section 5. Additional examples are presented in Appendix 7. Missing proofs and technical details can be found in other clearly marked appendices.

2 Preliminaries↩︎

We build upon the work in [16], and thus reuse some of the preliminary definitions as in [16]. Let \(\Sigma\) be a finite alphabet. A concurrent alphabet is a pair \((\Sigma, I)\) with \(I\subseteq \Sigma\times \Sigma\) a symmetric and irreflexive relation called the independence relation. The corresponding dependence relation is the set \(D = (\Sigma\times \Sigma) \setminus I\). A concrete independence relation can be obtained by distributing the letters into a finite set \(P\) of processes, formally defined by a function \(\mathrm{loc}\colon \Sigma \to 2^P\) where \(\mathrm{loc}(a)\) is the set of processes that can read the letter \(a \in \Sigma\). We further define \(\Sigma_p = \{a \in \Sigma \mid p \in \mathrm{loc}(a)\}\) as the alphabet of process \(p\in P\). We call \((\Sigma, \mathrm{loc})\) a distributed alphabet. Such a distribution naturally leads to an independence relation \(I_\mathrm{loc}= \{(a, b) \in \Sigma\times \Sigma \mid \mathrm{loc}(a) \cap \mathrm{loc}(b) = \emptyset\}\). We extend the function \(\mathrm{loc}\) to words by letting \(\mathrm{loc}(\varepsilon) = \emptyset\), and \(\mathrm{loc}(ua) = \mathrm{loc}(u) \cup \mathrm{loc}(a)\) for all \(u \in \Sigma^*\) and \(a \in \Sigma\).

Traces

A trace over a concurrent alphabet \((\Sigma, I)\) is a labelled partial order \(t = (\mathcal{E}, \leq, \lambda)\) where \(\mathcal{E}\) is a set of events, \(\lambda\colon \mathcal{E}\to \Sigma\) labels each event by a letter, and \(\leq\) is a partial order of \(\mathcal{E}\) such that for all \(e, f \in \mathcal{E}\), \((\lambda(e), \lambda(f)) \notin I\) implies \(e\leq f\) or \(f\leq e\); and secondly, \(e \lessdot f\) implies \((\lambda(e), \lambda(f)) \notin I\) where \({\lessdot} = {\le} \setminus {\le^2}\) is the immediate successor relation induced by the partial order. The number of events in the trace \(t\) is denoted as \(|t|\), and is called its length. If we have a distributed alphabet \((\Sigma, \mathrm{loc})\), we also let \(|t|_p\) be the number of events in which a process \(p\) participated, i.e. \(|t|_p = |\{e\in \mathcal{E}\mid \lambda(e)\in \mathrm{loc}(p)\}|\). A word \(w=a_0\cdots a_{n-1}\in \Sigma^*\) gives rise to a unique trace by putting one event per position in the word, and defining the successor relation \(\lessdot\) as all the pairs \((i, j)\) of positions such that \(i<j\), \((a_i, a_j)\notin I\) and there are no positions \(k\) such that \(i<k<j\) and \((a_i, a_k), (a_k, a_j)\notin I\). We call this word a linearisation of the trace. Two words \(w\) and \(w'\) mapped to the same trace are said to be equivalent. The lengths \(|w|\) and \(|w|_p\) are defined similarly as for traces.

Minimal (respectively, maximal) elements of a trace \(t\) are all the events that have no smaller (respectively, larger) events. The set of minimal (respectively, maximal) events of \(t\) is denoted by \(\min(t)\) (respectively, \(\max(t)\)). Given two traces \(t_1 = (\mathcal{E}_1, \leq_1, \lambda_1)\) and \(t_2 = (\mathcal{E}_2, \leq_2, \lambda_2)\), the concatenation \(t_1 t_2\) is the trace \((\mathcal{E}', \leq', \lambda')\) where \(\mathcal{E}'= \mathcal{E}_1 \cup \mathcal{E}_2\), \(\lambda'(e) = \lambda_1(e)\) if \(e \in \mathcal{E}_1\), and \(\lambda'(e) = \lambda_2(e)\) otherwise, and \(\leq'\) is the transitive closure of \({\leq_1} \cup {\leq_2} \cup \{ (x, y) \mid x \in \mathcal{E}_1, y \in \mathcal{E}_2, \text{ and } (\lambda'(x), \lambda'(y)) \notin I\}\).

Views

For a trace \(t = (\mathcal{E}, {\leq}, \lambda)\), a subset \(J\subseteq \mathcal{E}\) is called an ideal of \(t\) if for all \(e\in J\), and \(f\in \mathcal{E}\) such that \(f\leq e\), we have \(f\in J\). An ideal can also be seen as a trace \(u\) which is a prefix of the trace \(t\), i.e., there exists a trace \(v\) such that \(t = uv\). For a subset \(S\subseteq \mathcal{E}\) of events, we let \(S{\downarrow}\) be the ideal \(\{f\in \mathcal{E} \mid \exists e\in S \; f\leq e\}\). We identify special ideals called views: the view of a process \(p\) in a trace \(t\) is the ideal of \(t\) consisting of all events currently known by the process \(p\). Formally, we let \(\max_p(t)\) be the largest event of \(t\) that is labelled in \(\Sigma_p\). Then, the view of process \(p\) in a trace \(t\), denoted as \(\mathrm{view}_p(t)\), is the ideal \(\{\max_p(t)\}{\downarrow}\). The view of a set of processes \(X \subseteq P\) in a trace \(t\) is the ideal \(\{\max_p(t) \mid p\in X\}{\downarrow}\), obtained as the union of the views of the processes in \(X\).

Foata normal form

The Foata normal form (FNF) of a trace encodes a maximal parallel execution of the trace [20]. To define this notion formally, we use the concept of steps from [21]. A step is a non-empty subset \(S \subseteq\Sigma\) of pairwise independent letters: it is sometimes called a clique, from the point of view of the graph of the independence relation. In a step, all letters can be executed in parallel. Observe that the set of labels of the minimal elements of a trace \(t\) provides a maximal step for \(t\). Then, the FNF \(\mathsf F(t)\) of a trace \(t\) is a sequence of steps \(\varphi = S_1 S_2 \cdots S_m\) where \(S_1\) is the set of minimal elements of \(t\), and \(S_2 \cdots S_m = \mathsf F(t')\) where \(t'\) is the trace obtained by removing all minimal elements from \(t\). The FNF is a unique decomposition of the trace into maximal steps. We let \(|\varphi|\) be the total number of letters across all the steps of \(\varphi\). We write \(\mathsf F(t)_i\) for the \(i\)-th step of \(\mathsf F(t)\).

We denote by \(\varphi_i\) the \(i\)-th step of the FNF \(\varphi\). We shall also denote by \(|t|_{\mathsf F}\), the number of steps in the FNF decomposition of the trace \(t\), and we call it the Foata length of \(t\). In order to simplify further explanations, we suppose that a step \(\varphi_i\) exists as the empty set, for all \(i\) greater than the length of \(\varphi\): we do not depict this infinite sequence of empty sets when we give examples of FNF.

A crucial feature for our construction is the fact that FNF are increasing with respect to ideals: if a trace \(s\) is an ideal of \(t\), there is an injective correspondence from steps of \(s\) to the first \(|s|_{\mathsf F}\) steps of \(t\). Furthermore, if we know the FNF of the views of two (or more) processes \(p_1\) and \(p_2\), it is possible to deduce the FNF of the view of \(\{p_1, p_2\}\): they can accumulate their knowledge simply by taking pairwise unions of the steps. This gives us an algorithm to compute \(\mathrm{view}_X(t)\) for some \(X \subseteq P\), given \(\mathrm{view}_p(t)\) for all \(p \in X\). In the following, given two FNF \(\varphi=S_1\cdots S_m\) and \(\varphi'=S'_1\cdots S'_{m'}\), we write \(\varphi \cup \varphi'\) for the sequence of steps \((S_1 \cup S'_1) \cdots (S_n \cup S'_n)\) where \(n=\max(m,m')\) (remember that we have added empty steps at the end of the FNF so that \(S_k\) has a meaning, even for \(k\) greater than \(|\varphi|_{\mathsf F}\)).

Regular trace-closed languages and asynchronous automata

A language \(L \subseteq \Sigma^*\) is said to be trace-closed (for the independence relation \(I\)) if for all equivalent \(w, w' \in \Sigma^*\), \(w \in L\) iff \(w' \in L\). A trace-closed language is regular if it is accepted by a deterministic finite state automaton (DFA) \(\mathcal{A}= (Q, \Sigma, q_0, \delta, Q_f)\), where \(Q\) is the set of states, \(q_0\) is the unique initial state, \(Q_f\) the accepting states and \(\delta\colon Q\times \Sigma \to Q\) the partial function of transitions. We denote by \(q\xrightarrow a q'\) if \(\delta(q, a)=q'\), and we generalise the notation for a word \(w\) by letting \(q\xrightarrow{w}q'\) if there is a sequence of transitions \(q=q_0\xrightarrow {a_0} q_1 \xrightarrow {a_1} \cdots \xrightarrow{a_{n-1}} q_{n} = q'\) such that \(w=a_0 a_1 \ldots a_{n-1}\). As usual, the language recognised by \(\mathcal{A}\) is the set of words \(w\) such that there exists a run \(q_0 \xrightarrow{w}q'\) with \(q'\in Q_f\). Trace-closed regular languages are recognised by automata having a special syntactic property, called the diamond property.

For example, the DFA shown in Figure 1 satisfies the diamond property: \(q_0 \xrightarrow{12} q_1 \xrightarrow{34} q_2\) and \(q_0 \xrightarrow{34} q_3 \xrightarrow{12} q_2\). Similarly, the DFA shown in Figure 2 satisfies the diamond property. The diamond property is a sufficient condition for an automaton to recognise a trace-closed language. Indeed, if \(\mathcal{A}\) is a DFA satisfying the diamond property then for all \(q, q'\in Q\) and equivalent \(w, w' \in \Sigma^*\), \(q\xrightarrow w q'\) iff \(q\xrightarrow{w'} q'\). In particular, we extend this notation to traces \(t\) and Foata normal forms \(\varphi\), writing \(q\xrightarrow t q'\), and \(q\xrightarrow{\varphi} q'\). For instance, in the DFA of Figure 2, starting from \(q_0\), both the words \(12~34~13~24\) and \(34~12~24~13\) lead to the same state \(q_7\).

We will need a function already used in previous work to reconcile the views of several processes that have read independent letters after a point where they last synchronised:

As an example of the \(\mathrm{diam}\) function, notice that for the DFA in Figure 2, we have \(\mathrm{diam}(q_3, q_6, q_4, \{2, 4\}) = q_7\). Thus, if \(t_1 = 12~34\), \(t_2 = 24\), \(t_3 = 13\), we have \(\delta(q_0, t_1 t_2 t_3) = q_7\). An algorithm for computing the \(\mathrm{diam}\) function for a DFA satisfying the diamond property is sketched in Appendix 8. For the rest of the document, when we consider DFA specifications satisfying the diamond property, we will assume that \(\mathrm{diam}\) has been precomputed.

Zielonka’s theorem aims at distributing a trace-closed regular language to the individual processes by using asynchronous automata.

Figure 6 in Appendix 7 gives an example of an AA. The semantics of an AA is given by a DFA whose set of states is the product \(\Pi_{p\in P} Q_p\). We call these states the global states of \(\mathcal{B}\). Its initial global state is \(q^0\), and its final global states are given by \(F\). Moreover, for each letter \(a\in \Sigma\), we let \((q_p)_{p\in P} \xrightarrow a (q'_p)_{p\in P}\) if for all \(p'\notin\mathrm{loc}(a)\), \(q'_p = q_p\), and \(\delta_a((q_p)_{p\in \mathrm{loc}(a)}) = (q'_p)_{p\in \mathrm{loc}(a)}\). We can show that this DFA satisfies the diamond property, and thus, we let \(L_{\mathsf{tr}}(\mathcal{B})\) be its trace language, and say that the AA \(\mathcal{B}\) recognises \(L_{\mathsf{tr}}(\mathcal{B})\).

We now state Zielonka’s fundamental theorem. An illustration of the theorem is presented in Example 9 in Appendix 7.

3 Construction for fair systems↩︎

We briefly recall the AA construction of [16] when the DFA we start with is fair: a DFA \(\mathcal{A}\) is fair if each process participates at least once in every cycle of \(\mathcal{A}\). For example, the DFA of Figure 1 is fair. We define \(d\) to be the least integer such that in every path of length \(d\) all processes necessarily participate: observe that \(d\) is at most \(1\) plus the length of the longest acyclic path in the DFA. Such a DFA is called \(d\)-fair. Accordingly, a trace \(t\) is said to be \(d\)-fair if for every factor \(u\) of any linearisation \(w\) of \(t\), whenever \(|u|\geq d\), we have \(\mathrm{loc}(u) = P\), the set of all processes. The language of a \(d\)-fair DFA consists of only \(d\)-fair traces.

An AA maintaining local views

A first naïve construction gives an infinite-state AA, which is correct even for unfair DFAs. On a trace \(t\), the construction maintains \(\mathrm{view}_p(t)\) as the local state of a process \(p\). The main idea is to store the view in Foata normal form, i.e., \(\mathsf F(\mathrm{view}_p(t))\). The advantage of maintaining views in Foata normal form stems from Lemma 1 which explains how to obtain the combined view \(\mathsf F(\mathrm{view}_X(t))\) from the views of each process of \(X\). Therefore, when a new letter \(a\) appears, all processes in \(\mathrm{loc}(a)\) synchronise by taking a stepwise union of their local views, and then adding \(a\) as a new step, resulting in their new local state \(\mathsf F(\mathrm{view}_{\mathrm{loc}(a)} (t)) \{a\}\). Clearly, there are infinitely many states for each process. An example of such an AA maintaining views is depicted in Figure 1. For fair systems, it turns out that maintaining a bounded suffix of the view suffices.

Fair systems: cutting view prefixes

For a \(d\)-fair trace \(t\), when the local view of a process is sufficiently long, it can infer that a prefix of its view is identical to a prefix of the full trace \(t\), and moreover, this prefix is present in the view of all the other processes too:

We introduce some terminology: an event \(e\) of a trace \(t\) is said to be Second-Order Common Knowledge (\(\mathsf{SOCK}\)) for process \(p\) if \(p\) knows that \(e\) is present in the current view of every other process; formally, \(e\) is present in \(\mathrm{view}_{p'}(\mathrm{view}_p(t))\) for all processes \(p'\). Therefore, a process can remove from its view every Foata step in which all events are \(\mathsf{SOCK}\) for it: Lemma 3 ensures that the remaining suffix is bounded linearly w.r.t. \(d\). When processes synchronise, they need to be aware of which of them has cut the most, and then cut their prefixes up to this point, and then finally do the Foata union of the rest of the view. To implement this, local states of a process \(p\) in the AA are of the form \((c, q, \varphi)\) where

• \(c \in \mathbb{N}\) is a counter representing the number of letters in the view that have been cut,

• \(q\) is a state of the DFA reached after the prefix of the view that has been cut, and

• \(\varphi = S_1 S_2 \cdots S_m\) is a suffix of the view that remains, maintained in Foata normal form. Moreover, there is at least one letter \(a\in S_1\) which is not \(\mathsf{SOCK}\) for \(p\): in other words, \(p\) does not know whether \(a\) is present in the current view of some other process \(p'\).¹

To maintain this invariant, a cut operation \(\mathsf{cut}(c, q, \varphi)\) is defined on local states, as follows: if \(\varphi = S_1S_2 \cdots S_m\), we compute if all the events of \(S_1\) are \(\mathsf{SOCK}\) for \(p\); if it is the case we compute \(\mathsf{cut}(c+|S_1|, q', S_2 \cdots S_m)\) with \(q'\) the state such that \(q\xrightarrow {S_1} q'\); otherwise we let \(\mathsf{cut}(c, q, \varphi) = (c, q, \varphi)\). Notice that the only infinite component now is the counter \(c\). In fair systems the views of two processes diverge by at most \(d\), which can be used to do a modulo counting with \(2d\) values for the counter (see [16]):

Fair systems: synchronizing and expanding views

When a new letter appears, the processes participating in this letter reconcile their views by cutting their prefixes up to the process which has cut the most, and then performing a Foata union. More formally, for a letter \(a\) with \(\mathrm{loc}(a) = X\) and \((c_p, q_p, \varphi_p)\) being the local states of processes \(p \in X\), we define \(\mathsf{synchronise}((c_p, q_p, \varphi_p)_{p \in X}) = (c', q', \varphi')\) as follows:

• \(c' = \max_{p \in X} (c_p)\); choose a process \(p_{\max} \in X\) which maintains the largest counter value \(c'\) and let \(q' = q_{p_{\max}}\);

• for each process \(p \in X\), if \(\varphi_p = S_1 S_2 \dots S_m\), let \(j\) be the index such that \(S_1 \dots S_{j-1}\) contains exactly \(c' - c_p\) letters (existence of such an index is ensured by the construction, and these letters were the ones that were previously cut by \(p_{max}\)). We let \(\varphi'_p\) to be \(S_{j} \dots S_m\). Now, define \(\varphi' = \bigcup_{p \in X} \varphi'_p\).

Then, we define \(\mathsf{expand}((c', q', \varphi'), a) = \varphi' \cdot \{a\}\). Finally, we perform a cut operation on the resulting state: \(\mathsf{cut}(c', q', \varphi' \cdot \{a\} )\). This is the final local state of each process \(p \in X\) after reading the new letter \(a\). In summary, the new state of each \(p \in X\) after reading \(a\) is: \[\begin{align} \mathsf{cut}(\mathsf{expand}(\mathsf{synchronise}((c_p, q_p, \varphi_p)_{p \in X}), a)) \end{align}\]

Fair systems: determining the accepting states

From the local states reached on a trace \(t\), by applying Lemma 1, it is possible to determine the state of \(\mathcal{A}\) on reading the global trace \(t\). This way, one can determine which combination of local states is accepting.

4 Connectedly Communicating Processes↩︎

We now extend the algorithm of Section 3, to allow more DFAs. Consider the DFA in Figure 2. This DFA is not fair: in the cycle \(q_4 \xrightarrow{35} q_5 \xrightarrow{13} q_4\), processes \(2\) and \(4\) do not participate. However, in all the paths starting from \(q_4\) or \(q_5\), processes \(2\) and \(4\) do not communicate with \(1, 3, 5\), neither directly nor indirectly through a sequence of intermediate synchronisations. Such systems have been called connectedly communicating processes in [1]. This notion was originally defined on an asynchronous automaton. Here, we adapt it to the case of DFAs.

Processes \(p\) and \(p'\) are said to be separated in a trace \(t\) over \((\Sigma, \mathrm{loc})\) if there exists a linearisation \(uu'\) of \(t\) such that (1) \(\mathrm{loc}(u) \cap\mathrm{loc}(u')=\emptyset\) (\(u\) and \(u'\) are independent) and (2) \(|u|_{p'} = |u'|_p = 0\) (\(p'\) does not occur in \(u\), and \(p\) does not occur in \(u'\)). If such a linearisation does not exist for \(t\), we say that \(p\) and \(p'\) are potentially communicating in \(t\). For a word \(w \in \Sigma^*\), we say \(p\) and \(p'\) are separated in \(w\) if they are separated in the trace corresponding to \(w\). This definition of separation allows one to semantically define the notion of languages over connectedly communicating processes: intuitively, two processes that are potentially communicating (i.e., not separated yet) must learn about each other often enough.

In [1], a system is called a \(k\)-CCP if it satisfies the above definition with the value taken to be \(k\). In our work, we consider an alternate characterization and a different parameter which we will describe next.

Testing connected communication

We formalize the potential communication between processes as an equivalence relation at each state of the DFA. This relation turns out to be identical for all states within a strongly connected component (SCC): an SCC is a subset of states such that there is a path between every pair of states, and moreover it is maximal in the sense that no strict superset of states satisfies this property. This gives a notion of communicating partners for a process at each SCC.

Notice that if \(s \xrightarrow{a} s'\) is a transition of \(\mathcal{A}\), then \(\equiv_{s'}\) is a refinement of \(\equiv_s\): if \(p\) and \(p'\) are potentially communicating in \(s'\), then they potentially communicate from \(s\) as well. This observation helps to prove the following lemma about states within the same SCC:

Thanks to the above lemma, for each SCC \(\Gamma\) of \(\mathcal{A}\), we can define \(\equiv_\Gamma\) to be equal to \(\equiv_s\) for some \(s \in \Gamma\). The relation \(\equiv_\Gamma\) will be called the potential communication relation for \(\Gamma\). Figure 2 shows this relation for the depicted DFA. Let us reconsider the separation depth of Definition 4. Since the potential communication relation is the same within an SCC, the number of times it can get refined is at most the height of a topological ordering of the SCCs (this is an ordering where \(\Gamma\) is less than \(\Gamma'\) if there is a path from a state in \(\Gamma\) to a state in \(\Gamma'\)). It can be smaller, since the relation may stay the same in several SCCs. If \(\mathcal{A}\) is fair, then the separation depth is equal to \(0\). Moreover, we can compute these equivalence relations in polynomial time by visiting the SCCs in reverse topological order. The next lemma provides an alternate characterization for a DFA to be connectedly communicating, by making use of the potential communication relation. This characterization allows one to test whether a given DFA is connectedly communicating.

We are now in a position to define a counterpart of the fairness parameter in the context of connectedly communicating DFAs. Consider a DFA which is connectedly communicating. For an SCC \(\Gamma\) of \(\mathcal{A}\), and an equivalence class \(X\) of \(\equiv_\Gamma\), the fairness parameter \(d_{\Gamma, X}\) is the minimum number such that in every path \(\sigma\) of length \(\ge d_{\Gamma, X}\) inside \(\Gamma\) that consists only of \(X\) actions (i.e. actions of \(\bigcup_{p\in X} \Sigma_p\)), we have \(\mathrm{loc}(\sigma) = X\). The maximum fairness parameter \(d\) is then defined to be the maximum over \(d_{\Gamma, X}\) for all \(\Gamma\) and all equivalence classes \(X\) of \(\Gamma\).

5 Construction for connectedly communicating specifications↩︎

We are now ready to formally state our main contribution:

A lower bound on the size of an AA equivalent to \(\mathcal{A}\) is provided in [16] in the case of a fair system, i.e. in which the separation depth is \(s=0\): this shows that the \(d\) component in the exponent is unavoidable. We first provide an overview of our construction.

Overview

As in the case of fair systems, each process maintains its local view of the trace read so far, in Foata normal form. For fair systems, all Foata steps which are \(\mathsf{SOCK}\) for the process could be deleted. This is no longer possible. Consider the trace of Example 2. Here is the view of process \(p_1\) in Foata normal form (ignore the dashed line in between for now): \[\begin{align} \left[ \begin{tabular}{c} 12 \\ 34\end{tabular} \right] \left[ \begin{tabular}{c} 235 \\\end{tabular} \right] \left[ \begin{tabular}{c} 12 \\ 34\end{tabular} \right] \left[ \begin{tabular}{c} 235 \\\end{tabular} \right] \left[ \begin{tabular}{c} 12 \\ 34\end{tabular} \right] ~ \tikz[baseline={(0,-0.5ex)}] \draw[dashed] (0,-0.5) -- (0,0.5);~ \left[ \begin{tabular}{c} 13 \\\end{tabular} \right] \left[ \begin{tabular}{c} 35 \\\end{tabular} \right] \left[ \begin{tabular}{c} 13 \\\end{tabular} \right] \end{align}\] Notice that the events in the first four Foata steps are \(\mathsf{SOCK}\) for \(p_1\). The fifth step \(\{12, 34\}\) (just before the dashed line) is not \(\mathsf{SOCK}\) since \(p_1\) does not know whether \(p_2\) is aware of event \(34\). Similarly, the events \(13~35~13\) are not \(\mathsf{SOCK}\). More importantly, \(13~35~13\) can never be \(\mathsf{SOCK}\) in any extension of the view consistent with \(\mathcal{A}'\). This is because in the state \(q_4\) reached after this trace, \(p_2\) and \(p_4\) have already separated from \(p_1\) (see right of Figure 2) and hence the events where they participate would no longer appear in the view of \(p_1\). Therefore, the construction cutting \(\mathsf{SOCK}\) events does not work anymore.

A natural thought is to focus simply on the potentially communicating partners of \(p_1\) at the end of the view, namely \([p_1]_{q_4} = \{p_1, p_3, p_5\}\). In the current view, \(p_1\) can deduce that all Foata steps, except for the last \(\{13\}\) are present in the views of \(p_3\) and \(p_5\) too: we call these events to be \(\mathsf{SOCK}[\{p_1, p_3, p_5\}]\) – \(\mathsf{SOCK}\) restricted to \(\{p_1, p_3, p_5\}\). In any extension, \(p_1\) will synchronise only with \(p_3\) or \(p_5\). Does this mean we can cut this entire prefix? Unfortunately, not. Even though in any extension, \(p_1\) can synchronise only with \(p_3\) or \(p_5\), there is a final step to determine whether the global state reached on a trace is accepting or not. In the construction of Section 3, the reconciliation happens by computing the joint view of all the processes, taking one at a time: \(\mathrm{view}_{\{p_1,p_2\}}\) is computed from \(\mathrm{view}_{p_1}\) and \(\mathrm{view}_{p_2}\) by cutting appropriate number of steps and then taking Foata union; then \(\mathrm{view}_{\{p_1,p_2,p_3\}}\) is computed from \(\mathrm{view}_{\{p_1, p_2\}}\) and \(\mathrm{view}_{p_3}\) and so on. Therefore, in the example above, the view of \(p_1\) would be synchronised with views of \(p_2\) and \(p_4\) as well, in the final step, to determine acceptance.

This brings us to the question: when can we safely cut an event? Here is our proposal. Assume the view is a sequence of Foata steps \(S_1 \dots S_m\), and the run of the DFA is \(q_0 \xrightarrow{S_1} q_1 \xrightarrow{S_2} \cdots \xrightarrow{S_m} q_m\). We show that \(S_i\) can be safely cut as long as every event in prefix \(S_1 \dots S_i\) lies in \(\mathsf{SOCK}[[p]_{q_i}]\), the second-order common knowledge of \(p\) restricted to partners of \(p\) at the next state \(q_i\) (and not the state \(q_m\) reached at the end of the view). For the above example, the state reached before the dashed line is \(q_3\), after which we have \(q_3 \xrightarrow{\{13\}} q_4 \xrightarrow{\{35\}} q_5 \xrightarrow{\{13\}} q_4\). At state \(q_3\), partners of \(p_1\) are all processes, i.e., \([p_1]_{q_3} = \{p_1, \dots, p_5\}\). Observe that \(34\) is not \(\mathsf{SOCK}[[p_1]_{q_3}]\). Therefore, we do not cut the last \(\{12, 34\}\) step. But, we can cut the following \(13~35\) since all steps up to \(13\) are \(\mathsf{SOCK}[[p_1]_{q_4}]\) and all steps up to \(35\) are \(\mathsf{SOCK}[[p_1]_{q_5}]\). The idea is that when we cut a Foata step in the view of a process, it knows that all events in its view up to this step are visible to each of its communicating partners.

In this mechanism to cut steps, we may encounter cuts in the middle of the view, unlike in the fair case where the cuts happened only at a prefix of the view. To book-keep the cuts, we mark the places where the cuts start (denoted by the dashed line). This amounts to splitting the view into phases. For the view above, the first phase is the part to the left of the dashed line, and the second phase is to its right. Within each phase, a prefix of Foata steps can be cut. In the first phase above, the prefix consisting of the first four Foata steps can be cut by applying our rule. For each phase, we will maintain a triple \((c, q, \varphi)\) as in the fair construction of Section 3. For the above view of \(p_1\), the state reached would be \((6, q_0, \{12, 34\})(2, q_5, \{13\})\).

Once we have local states in this form, the next challenge is to be able to compute the joint states when multiple processes synchronise. For instance, assume a letter \(a\) is being read, with \(\mathrm{loc}(a) = \{p, p'\}\). We need to reconcile the current views of \(p\) and \(p'\). Due to our cutting strategy, any new information that \(p\) can learn from \(p'\) would be after the last cut made in \(p\). However there could be an event which is cut in one process, but not cut yet in the other. The key observation is that \(p\) and \(p'\) can be at most one phase apart, and only the last phase of the lagging process needs to be synchronised with the last two phases of the leading process. All these ideas are concisely captured in Invariants (A), (B), (C) and (D) of Definition 5.

The final difficulty is to determine which global states are accepting. To do so, we need to be able to determine the state of \(\mathcal{A}'\) reached at the end of the global trace, simply by looking at the above maintained abstraction of the local views. Here is where we make use of Invariant (E) (Definition 5) and the \(\mathrm{diam}\) function (Section 2). We explain the determination of final states later in the section, after formalizing the local states and transitions of the AA \(\mathcal{B}\).

States of \(\mathcal{B}\)

We start by explaining how to produce an AA with infinitely many local states, due to the counters that will be unbounded. Later, we explain how to make this part finite by using the same modulo counting technique as in [16]. The local states of a process \(p\) in the (infinite) AA we are building have the shape: \(\sigma_p := (c_{p,i}, q_{p,i}, \varphi_{p,i})_{1 \leq i \leq \ell_p}\), where each triple is called a phase, that contains a counter value \(c_{p,i} \in \mathbb{N}\) to track the number of cut letters in this phase, a state \(q_{p,i}\) of \(\mathcal{A}\), and the Foata normal form \(\varphi_{p,i}\) of a trace. In the fair case discussed in Section 3, only a single phase is maintained along the computation. The local initial state of a process \(p\) is given by \((0, q_0, \varepsilon)\), with \(q_0\) being the initial state of \(\mathcal{A}\). Along our construction, we will maintain an invariant on the global states we reach in the AA, that is trivially fulfilled for the empty trace.

Cut and split operation

One of the more subtle operations that we have to perform along the computation is the splitting into phases in order to be able to perform more cuts. To do so, we introduce an operation \(\mathsf{cut\textsf{-}split}_{p,q}\) with \(p\) a process and \(q\) a state of \(\mathcal{A}\). This operation takes the Foata normal form \(\varphi\) of a trace \(t\) as parameter, and returns a sequence of phases. Moreover, for a set of processes \(X\), we say an event \(e\) is second-order common knowledge among \(X\) or \(\mathsf{SOCK}[X]\) for a process \(p\) if for all processes \(p' \in X\), \(\mathrm{view}_{p'}(\mathrm{view}_p(t))\) contains \(e\), i.e. \(p\) knows that every other process in \(X\) knows the event \(e\).

Let \(\varphi = S_1 S_2 \cdots S_m\) be the Foata steps, and let \(q=q_0 \xrightarrow{S_1} q_1 \xrightarrow{S_2} q_2 \cdots \xrightarrow{S_m} q_m\) be the run reading \(\varphi\) from \(q\). Here, \(\varphi\) is part of the view of process \(p\). If for all \(i\), every event in \(S_1 \dots S_i\) is \(\mathsf{SOCK}[[p]_{q_i}]\) for \(p\), then every letter can safely be cut and we let \(\mathsf{cut\textsf{-}split}_{p,q}(\varphi) = (|\varphi|, q_m, \varepsilon)\). Otherwise, let \(i\) be the minimal index such that some letter of \(S_1 \dots S_i\) is not \(\mathsf{SOCK}[[p]_{q_i}]\) for \(p\). Due to minimality of \(i\), the steps \(S_1\cdots S_{i-1}\) can safely be cut, but not \(S_i\). There are two further cases depending on whether we should split the last phase or not:

• If for all \(j>i\), at least a letter of \(S_i, S_{i+1}, \dots, S_j\) is not \(\mathsf{SOCK}[[p]_{q_j}]\) for \(p\), nothing else can be cut, and we thus let \(\mathsf{cut\textsf{-}split}_{p,q}(\varphi) = (|S_1\cdots S_{i-1}|, q_{i-1}, S_i\cdots S_m)\).

• Otherwise, there exists a minimal \(j>i\) such that all events in \(S_i, S_{i+1}, \dots, S_j\) are \(\mathsf{SOCK}[[p]_{q_j}]\). By minimality, \(S_{j-1}\) cannot be cut: there must exist a process in \([p]_{q_{j-1}}\) that, according to \(p\), does not know about a letter of \(S_i, S_{i+1}, \dots, S_{j-1}\), and this process cannot be among \([p]_{q_j}\), thus we have \([p]_{q_j} \subsetneq [p]_{q_{j-1}}\) (which will help us get invariant (B)). We split to build a first phase \((|S_1\cdots S_{i-1}|, q_{i-1}, S_i\cdots S_{j-1})\). We then continue this procedure with the steps \(S_j\cdots S_m\), and we thus define inductively \[\mathsf{cut\textsf{-}split}_{p,q}(\varphi) = (|S_1\cdots S_{i-1}|, q_{i-1}, S_i\cdots S_{j-1}) \; \mathsf{cut\textsf{-}split}_{p,q_{j-1}}(S_j\cdots S_m)\]

Transitions of \(\mathcal{B}\)

Before reading a letter \(a\), all processes in \(\mathrm{loc}(a)\) must synchronise their local states \((\sigma_p)_{p\in \mathrm{loc}(a)}\). We let \(\mathsf{synchronise}\big((\sigma_p)_{p\in \mathrm{loc}(a)}\big)\) be the local state obtained after synchronisation, as follows. We describe only this synchronisation between two processes \(p\) and \(p'\) participating in \(a\). The general case follows by induction. During our explanations, we use the invariant of Definition 5 that we want to maintain.

Let \(\sigma_p = (c_{i}, q_{i}, \varphi_{i})_{1\leq i\leq \ell}\) be the local state of process \(p\), and \(\sigma_{p'} = (c'_{i}, q'_{i}, \varphi'_{i})_{1\leq i\leq \ell'}\) be the local state of process \(p'\). Without loss of generality, we suppose that \(\ell'\leq \ell\) and if \(\ell = \ell'\), then \(c_{\ell'} \leq c_{\ell}\). Since \(p\) and \(p'\) are potentially communicating, by invariant (D), \(\ell'\in\{\ell,\ell-1\}\). By invariant (E), we know that for all \(1 \le i \le \ell'-1\), \((c_i, q_i, \varphi_i) = (c'_i, q'_i, \varphi'_i)\). We keep those phases unchanged during the synchronisation.

If \(\ell' = \ell-1\), we make \(p'\) catch up as follows. By invariant (D), we know that \(c'_{\ell'} \leq c_{\ell'}\): process \(p\) has cut more than \(p'\) in the \(\ell'\)-th phase. We thus cut the first \(c_{\ell'}-c'_{\ell'}\) letters from \(\varphi'_{\ell'}\) (as in [16], these letters are ensured to represent whole steps in the Foata normal form). The remaining Foata steps are then of the form \(\varphi_{\ell'}\psi\). In the state after synchronisation, we add the phase \((c_{\ell'}, q_{\ell'}, \varphi_{\ell'})\). We temporarily add a phase \((0, q_{\ell'}, \psi)\) to process \(p'\).

For the last phase (either \(p'\) had a phase of index \(\ell'=\ell\), or we have created one just above), we must synchronise the view of \(p\) that is \((c_\ell, q_\ell, \varphi_\ell)\), and the view of \(p'\) that is \((c'_\ell,q'_\ell, \varphi'_\ell)\). We still have \(c'_\ell \leq c_\ell\) (either it is by hypothesis, or we have \(c'_\ell=0\) by the case just above). We can thus still cut \(c_\ell-c'_\ell\) letters in the phase of \(p'\), to obtain some Foata steps \(\psi'\). Guided by Lemma 1, we then perform a componentwise union of the steps of \(\varphi_\ell\) and \(\psi'\) to obtain Foata steps \(\psi''\). We thus obtain \(\mathsf{synchronise}\big(\sigma_p, \sigma_{p'}\big) = (c_1, q_1, \varphi_1)\ldots (c_{\ell-1}, q_{\ell-1}, \varphi_{\ell-1})(c_{\ell}, q_\ell, \psi'')\).

Once all participating processes of \(\mathrm{loc}(a)\) have synchronised, the updated last phase \((c_\ell, q_\ell, \psi'')\) can then be expanded with a new step \(\{a\}\). To finish, we apply a phase split and replace the last phase \((c_{\ell}, q_\ell, \psi'')\) by the phases \(\mathsf{cut\textsf{-}split}_{p, q_\ell}(\psi''\{a\})\). We can show that if a trace \(t\) satisfies the invariant of Definition 5, then the trace \(ta\), obtained by adding a letter \(a\) also satisfies this invariant, which proves the correctness of the construction. A detailed example illustrating an entire run for each process is provided in Example 10 in Appendix 7.

Determining the accepting states of \(\mathcal{B}\)

At this point, the invariant of Definition 5 ensures that after reading a trace \(t\), each process \(p\) reaches a local state from which the state reached in \(\mathcal{A}\) on reading \(\mathrm{view}_p(t)\) can be computed. However, we need to be able to compute the state reached in \(\mathcal{A}\) after reading the whole trace \(t\), in order to declare if the global state of the AA is accepting or not. Our construction proceeds in two steps: (1) compute a tree depicting how two processes separate at each phase, (2) a bottom-up computation over this tree computing the states reached by \(\mathrm{view}_X(t)\) for a subset \(X\) of processes at each stage, until \(X\) equals the whole set of processes, which will then give us the required state. We first exemplify our construction, before formalising it.

We present some of the technical details here, and the rest in 10. For each process \(p\), let \(\sigma_p = (c_{p,i}, q_{p,i}, \varphi_{p,i})_{1 \le i \le \ell_p}\) be the local state that \(p\) reaches after trace \(t\). From the previous section, we know that \(t\) satisfies the invariant of Definition 5: in particular, we can use the states \(s_{p,0}, s_{p,1}, \dots, s_{p, \ell_p}\) of \(\mathcal{A}\) that are given by this invariant, so that \(s_{p,0}\) is the initial state of \(\mathcal{A}\), and \(q_{p,i} \xrightarrow{\varphi_{p,i}} s_{p,i}\) for all \(i\).

To compute the tree of separation, we consider an equivalence relation \(\equiv_j\) on processes defined as: \(p \equiv_j p'\) if \(p \equiv_{s_{r,j}} p'\) for all processes \(r\). Intuitively, \(p\) is made equivalent to \(p'\) if they are both potentially communicating at the end of Phase \(j\), according to all the processes. If a process \(r\) has fewer phases, we first normalise its local state by padding empty phases \((0, s_{r, \ell_r}, \varepsilon)\) so that in the end all processes have the same number \(m\) of phases. We then proceed to the bottom-up computation, starting from the leaves. For each leaf \(Y\), we synchronise the states of processes in \(Y\) by applying \(\mathsf{synchronise}\big((\sigma_{p'})_{p'\in Y}\big)\) and thus can compute an updated local state \(\sigma_Y = (c_{Y,i}, q_{Y,i}, \varphi_{Y,i})_{1 \le i \le m}\), as well as a state \(s_Y\) reached in \(\mathcal{A}\) after reading \(\mathrm{view}_Y(t)\). For the bottom-up computation, pick a node labelled with processes \(X\) and phase \(j\), with children over processes \(Y_1, \dots, Y_n\) at phase \(j+1\) such that \(X = Y_1 \cup \cdots \cup Y_n\). Assume we have computed the joint states for each \(Y_1, \dots, Y_n\), and in particular the states \(s_{Y_1}, \dots, s_{Y_n}\). Consider Invariant (E) of Definition 5. For each pair of processes \(p, p' \in X\), we have \(\ell_{p, p'} = j\). Therefore, for all processes in \(X\), all the phases up to \(j-1\) will be identical. Phase \(j\) may however differ which we will reconcile as follows.

Let \((c_i, q_i, \varphi_i)_{1\leq j\leq n}\) be the \(j\)-th phase of processes in \(Y_1, \ldots, Y_n\) respectively (each process of \(Y_i\) share the same \(i\)-th phase by the synchronisation that we have first performed). Let \(c = \max_{1\leq i\leq n} c_{i}\) be the maximal counter value. For all \(i\), we cut \(c-c_{i}\) letters to make a global synchronisation of the phase prefix (in particular the state part): thus, each local state now looks like \((c, q, \varphi'_{i})_{1 \le i \le n}\). We then reconcile \(Y_1\) and \(Y_2\) (continuing two by two, to reconcile all classes afterwards) as follows. First, we consider the pointwise intersection of Foata steps \(\varphi'_{Y_1}\) and \(\varphi'_{Y_2}\): what we have removed is necessarily independent of the other processes. Let \(\varphi''\) be the result, and \(s''=\delta(q, \varphi'')\). By Lemma 2, the state reached on \(\mathrm{view}_{Y_1 \cup Y_2}(t)\) is then \(s_{Y_1\cup Y_2} = \mathrm{diam}(s'', s_{Y_1}, s_{Y_2}, Y_1)\).

Modulo counters

The unbounded counters make the local state space infinite. However, we can use the crucial ingredient of Lemma 4, already used in the construction proposed in [16] for fair DFAs, where the views of processes cannot be more that \(d\) letters apart, if \(d\) is the fairness parameter. Thus, for a set of processes \(X\) communicating in an SCC of \(\mathcal{A}\) (that needs to be fair for \(X\), by Lemma [lem:CC-fair]), the number of letters cut by each process in \(X\) lies in a contiguous range of \(d\) values where \(d\) is the fairness parameter of this SCC. Thus, modulo \(2d\), these values lie in a cyclic interval of length \(d\) and when synchronising on an action, the processes can determine the process which has cut the largest number of letters (even if the value is lower than that of other processes) and the number of letters to be cut to match that process. We apply this modulo counting on an example in Appendix 11.

6 Conclusion and perspectives↩︎

In this article, we have proposed the construction of an AA given a regular trace language that is connectedly communicating: it is inspired by the one on fair languages [16] where only a suffix of the view is maintained by each process, but this approach requires splitting the local states into phases to be able to cut letters from the views of each process even in the middle. As perspectives, we plan on implementing the algorithm similarly as the tool FAAST [17] proposed for the fair case. In this tool, the construction of the AA is on-the-fly (the states and transitions are only computed when necessary at the execution) and can even be applied on non-fair languages, then providing a fair under-approximation: an AA is built, whose language is the set of \(d\)-fair traces of the specification language. We would like to study a similar strategy for connectedly communicating languages. This enables a synthesis procedure even for specifications that do not fulfil the connected communication property, thus allowing for synthesising resilient distributed algorithms, even without fairness properties handwritten in the formal specification.

7 Additional examples↩︎

Example 9. Let \(\Sigma = \{a, b, c\}\) be an alphabet distributed to two processes \(P_1\) and \(P_2\) as follows: \(\Sigma_{P_1} = \{a, c\}\) and \(\Sigma_{P_2} = \{b, c\}\). So the only synchronizing action is \(c\). Consider the language \(L = ((a + b)(a + b))^*c\). A DFA recognizing \(L\) is shown in Figure 5. An AA recognizing \(L\) is shown in Figure 6. Two blue \(c\) or two red \(c\) transitions can synchronise together. A blue \(c\) and a red \(c\) cannot be taken together. The transition syntax of AA allows for such coupled transitions: formally, \(\delta_c((0,0)) = (2,2)\) and \(\delta_c((1,1)) = (2,2)\).

8 Computing the \(\mathrm{diam}\) function↩︎

Assuming the existence and uniqueness of the \(\mathrm{diam}\) function, one can compute it for each set of process \(X \subseteq P\) and triple of states \((q_1, q_2, q_3)\) by finding words \(u, v\) such that \(\mathrm{loc}(u) \subseteq X\), \(\mathrm{loc}(v) \cap X = \emptyset\), \(\delta(q_1, u) = q_2\), and \(\delta(q_1, v) = q_3\). If these words \(u, v\) exist, then these can be found in time linear in the number of states by a simple graph search using transitions labelled by only \(\Sigma_X\) letters for \(u\) and only \(\Sigma \setminus \Sigma_X\) letters for \(v\). By the uniqueness of the \(\mathrm{diam}\) function, we set \(\mathrm{diam}(q_1, q_2, q_3, X) := \delta(q_1, uv)\).

9 Proofs of 4↩︎

10 Proofs of 5↩︎

Formalizing the accepting state computation

Assume we are given a global state \(\sigma = (\sigma_p)_{p \in P}\). Each \(\sigma_p\) is of this form: \[\begin{align} \sigma_p = (c_{p,i}, q_{p,i}, \varphi_{p,i})_{1 \le i \le \ell_p} \end{align}\] Process \(p\) has \(\ell_p\) phases. As done before, let \(s_{p, i}\) be the state reached by \(\mathcal{A}\) on reading \(\varphi_{p,i}\) starting from \(q_{p,i}\).

First we do a normalization so that all the processes have the same number of phases. Let \(m_{\sigma} = \max_{p \in P} \ell_p\). If for some process \(p'\), we have \(\ell_{p'} < m_\sigma\), then we add \(m_\sigma - \ell_{p'}\) extra phases \((0, s_{p', \ell_{p'}}, \varepsilon)\). For these extra phases, that is, for \(\ell_{p'} + 1 \le j \le m_\sigma\), we also have \(s_{p', j} = s_{p', \ell_{p'}}\). Therefore, we now have a global state of the form: \[\begin{align} \sigma_p = (c_{p,i}, q_{p,i}, \varphi_{p,i})_{1 \le i \le m_{\sigma}} \end{align}\]

Define a bunch of \(m_{\sigma}\) equivalence relations on the set of processes as follows: for \(1 \le j \le m_{\sigma}\), we say \(p \equiv^j p'\) if for all processes \(r \in P\), we have \(p \equiv_{s_{r, j}} p'\).

The following lemma is a consequence of the fact that for every process \(r\), the equivalence relation \(\equiv_{s_{r, j+1}}\) is a refinement of \(\equiv_{s_{r, j}}\).

This gives the partitions of processes communicating with each other in each “global” phase. The division of the processes looks like this:

We can now define a sequence of enhanced states \(\eta_{m_\sigma + 1}, \eta_{m_\sigma}\), \(\eta_{m_\sigma - 1}, \dots, \eta_1\) which we will define inductively.

We start with \(\eta_{m_\sigma + 1}\). Assume \(\equiv^{m_\sigma + 1}\) is the trivial relation where each process is the only one its equivalence class. Define \(\eta_{m_\sigma + 1}\) to be \((\sigma_p ~\mid~ s_{p, m_\sigma})_{p \in P}\).

Suppose we have \(\eta_{j+1}\): to each equivalence class \(Y\) of \(\equiv^{j+1}\), we have associated: \[\begin{align} (c_{Y,1}, q_{Y,1}, \varphi_{Y,1}) \cdots (c_{Y, j} q_{Y, j}, \varphi_{Y, j}) ~\mid~ s_Y \end{align}\] where \((c_{Y,1}, q_{Y,1}, \varphi_{Y,1}) \cdots (c_{Y, j}, q_{Y, j}, \varphi_{Y,j})\) equals \((c_{p,1}, q_{p,1}, \varphi_{p,1}) \cdots (c_{p,j}, q_{p,j}, \varphi_{p,j})\) for some \(p \in Y\). No matter which \(p\in Y\) we pick, this part will be the same.

Consider an equivalence class \(X\) of \(\equiv^j\). By 5, there is a collection of equivalence classes \(\mathcal{Y} = \{Y_i\}_{1 \le i \le n}\) of \(\equiv^{j+1}\) such that \(X = \bigcup \mathcal{Y}\).

By invariant \(\mathrm{(E)}\) of 5, we have that for all \(Y, Y' \in \mathcal{Y}\) and \(0 \le \ell \le j - 1\), \((c_{Y, \ell}, q_{Y, \ell}, \varphi_{Y, \ell}) = (c_{Y', \ell}, q_{Y', \ell}, \varphi_{Y', \ell})\) since processes in \(X\) communicate with each other in phase \(j\). We synchronise the enhanced states of \(\{Y_i\}_{1 \le i \le n}\) as follows.

1. Let \(c_j := \max_{y \in \mathcal{Y}} c_{Y, j}\). For each \(1 \le i \le n\) cut \(c_{Y, j} - c_{Y_i, j}\) letters of \(\varphi_{Y_i, j-1}\) to get the phase \((c_{Y, j}. q_{Y, j}, \varphi'_{Y_i, j})\).

2. Let \(\sigma_Z = (c_{X, \ell}, q_{X, \ell}, \varphi_{X, \ell})_{1 \le \ell \le j} := \sigma_{Y_1}\) and \(s_Z := s_{Y_1}\).

3. For \(i := 2\) to \(n\),

   1. Let \(\varphi_{ZY_i}\) be the Foata step-wise intersection of \(\varphi_{Z, j}\) and \(\varphi'_{Y_i, j}\), and \(q_{ZY_i} = \delta(q_{Y,j}, \varphi_{XY_i})\) be the state reached on reading the intersection. The remainder of the views of \(Z\) and \(Y_i\) starting from \(q_{ZY_i}\) are independent.

   2. Let \(s_Z := \mathrm{diam}(q_{ZY_i}, s_Z, s_{Y_i}, \cup_{1 \le \ell < i} Y_\ell)\), and \(\varphi_{Z, j}\) be the Foata step-wise union of \(\varphi_{Z, j}\) and \(\varphi'_{Y_i, j}\).

4. Finally define \(\eta_{j, X} := (c_{Z, \ell}, q_{Z, \ell}, \varphi_{Z, \ell})_{1 \le \ell < j} ~\mid~ s_Z\)

11 The example of the main body with modulo counters↩︎

We reconsider the DFA of Figure 2, but reading a longer trace than in Example 10 to demonstrate what happens when we use modulo counters, in the finite AA that we are constructing. We first read the five same first letters:

\[\begin{array}{c|l|l|l|l|l} & 12 & 34 & 235 & 34 & 12 \\ \hline p_1 & (0, q_0, \{\textcolor{blue}{12}\}) & (0, q_0, \{12\}) & (0, q_0, \{12\}) & (0, q_0, \{12\}) & (0, q_0, \{12, \textcolor{blue}{34}\} \{\textcolor{blue}{235}\} \{\textcolor{blue}{12}\})\\ \hline p_2 & (0, q_0, \{\textcolor{blue}{12}\}) & (0, q_0, \{12\}) & (0, q_0, \{ 12, \textcolor{blue}{34}\}\{\textcolor{blue}{235}\}) & (0, q_0, \{12, 34\} \{235\}) & (0, q_0, \{12, 34\} \{235\} \{\textcolor{blue}{12}\}) \\ \hline p_3 & (0, q_0, \varepsilon) & (0, q_0, \{\textcolor{blue}{34}\}) & (0, q_0, \{\textcolor{blue}{12}, 34\}\{\textcolor{blue}{235}\}) & (0, q_0, \{12, 34\} \{235\} \{\textcolor{blue}{34}\}) & (0, q_0, \{12, 34\} \{235\} \{34\})\\ \hline p_4 & (0, q_0, \varepsilon) & (0, q_0, \{\textcolor{blue}{34}\}) & (0, q_0, \{34\}) & (0, q_0, \{\textcolor{blue}{12}, 34\} \{\textcolor{blue}{235}\} \{\textcolor{blue}{34}\}) & (0, q_0, \{12, 34\} \{235\} \{34\}) \\ \hline p_5 & (0, q_0, \varepsilon) & (0, q_0, \varepsilon) & (0, q_0, \{\textcolor{blue}{12,34}\} \{\textcolor{blue}{235}\}) & (0, q_0, \{12,34\} \{235\}) & (0, q_0, \{12, 34\} \{235\}) \end{array}\]

We continue as before by reading \(235\; 12\; 34\) where we start cutting steps, and thus incrementing the counters:

\[\begin{array}{c|l|l|l} & 235 & 12 & 34 \\\hline p_1 & (0, q_0, \{12, 34\} \{235\} \{12\}) & (\textcolor{blue}{3}, \textcolor{blue}{q_0}, \{12, \textcolor{blue}{34}\} \{\textcolor{blue}{235}\} \{\textcolor{blue}{12}\}) & (3, q_0, \{12, 34\} \{235\} \{12\}) \\ \hline p_2 & (\textcolor{blue}{3}, \textcolor{blue}{q_0}, \{12, 34\} \{235\}) & (3, q_0, \{12, 34\} \{235\} \{\textcolor{blue}{12}\}) & (3, q_0, \{12, 34\} \{235\} \{12\}) \\ \hline p_3 & (\textcolor{blue}{3}, \textcolor{blue}{q_0}, \{12, 34\} \{235\}) & (3, q_0, \{12, 34\} \{235\}) & (3, q_0, \{12, 34\} \{235\} \{ \textcolor{blue}{34} \}) \\ \hline p_4 & (0, q_0, \{12, 34\} \{235\} \{34\}) & (0, q_0, \{12, 34\} \{235\} \{34\}) & (\textcolor{blue}{3}, \textcolor{blue}{q_0}, \{\textcolor{blue}{12}, 34\} \{\textcolor{blue}{235}\} \{ \textcolor{blue}{34} \}) \\ \hline p_5 & (\textcolor{blue}{3}, \textcolor{blue}{q_0}, \{12, 34\} \{235\}) & (3, q_0, \{12, 34\} \{235\}) & (3, q_0, \{12, 34\} \{235\}) \end{array}\]

We continue by reading new letters: \(235\; 34\; 12\; 235\). On the last one, the counter should be increased to \(9\), but since we count modulo \(2d=8\) (since the SCC \(\Gamma_1\) is fair with a fairness parameter \(d=4\)), the counter becomes \(1\):

\[\begin{array}{c|l|l|l|l} & 235 & 34 & 12 & 235\\\hline p_1 & (3, q_0, \{12, 34\} \{235\} \{12\}) & (3, q_0, \{12, 34\} \{235\} \{12\}) & (\textcolor{blue}{6}, \textcolor{blue}{q_0}, \{12, 34\} \{235\}\{\textcolor{blue}{12}\}) & (6, q_0, \{12, 34\} \{235\}\{12\}) \\\hline p_2 & (\textcolor{blue}{6}, \textcolor{blue}{q_0}, \{12, \textcolor{blue}{34}\} \{\textcolor{blue}{235}\}) & (6, q_0, \{12, 34\} \{235\}) & (6, q_0, \{12, 34\} \{235\}\{\textcolor{blue}{12}\})& (\textcolor{blue}{1}, \textcolor{blue}{q_0}, \{12, \textcolor{blue}{34}\}\{\textcolor{blue}{235}\})\\\hline p_3 & (\textcolor{blue}{6}, \textcolor{blue}{q_0}, \{\textcolor{blue}{12}, 34\} \{\textcolor{blue}{235}\})& (6, q_0, \{12, 34\} \{235\} \{\textcolor{blue}{34}\}) & (6, q_0, \{12, 34\} \{235\} \{34\})& (\textcolor{blue}{1}, \textcolor{blue}{q_0}, \{\textcolor{blue}{12}, 34\}\{\textcolor{blue}{235}\})\\\hline p_4 & (3, q_0, \{12, 34\} \{235\} \{34\}) & (\textcolor{blue}{6}, \textcolor{blue}{q_0}, \{12, 34\} \{235\} \{\textcolor{blue}{34}\}) & (6, q_0, \{12, 34\} \{235\} \{34\}) & (6, q_0, \{12, 34\} \{235\} \{34\})\\\hline p_5 & (\textcolor{blue}{6},\textcolor{blue}{q_0}, \{\textcolor{blue}{12}, \textcolor{blue}{34}\} \{\textcolor{blue}{235}\}) & (6, q_0, \{12, 34\} \{235\}) & (6, q_0, \{12, 34\} \{235\}) & (\textcolor{blue}{1}, \textcolor{blue}{q_0}, \{\textcolor{blue}{12}, \textcolor{blue}{34}\}\{\textcolor{blue}{235}\}) \end{array}\]

We now read letters \(12\; 34\); The synchronisation between \(p_1\) and \(p_2\) (and similarly for \(p_3\) and \(p_4\)) is between counter values \(6\) and \(1\): since counter values of potentially communicating processes cannot be more than \(d=4\) apart (by Lemma 4), the counter \(1\) is necessary ahead of \(6\) even if \(1<6\). Processes \(p_2\) and \(p_4\) thus know that they are late and can cut the corresponding number of letters to catch up.

\[\begin{array}{c|l|l} & 12 & 34 \\\hline p_1 & (\textcolor{blue}{1}, \textcolor{blue}{q_0}, \{12, \textcolor{blue}{34}\}\{\textcolor{blue}{235}\}\{\textcolor{blue}{12}\}) & (1, q_0, \{12, 34\}\{235\}\{12\})\\\hline p_2 & (1, q_0, \{12, 34\}\{235\}\{\textcolor{blue}{12}\}) & (1, q_0, \{12, 34\}\{235\}\{12\}) \\\hline p_3 & (1, q_0, \{12, 34\}\{235\}) & (1, q_0, \{12, 34\}\{235\}\{\textcolor{blue}{34}\})\\\hline p_4 & (6, q_0, \{12, 34\} \{235\} \{34\}) & (\textcolor{blue}{1}, \textcolor{blue}{q_0}, \{\textcolor{blue}{12}, 34\}\{\textcolor{blue}{235}\}\{\textcolor{blue}{34}\})\\\hline p_5 & (1, q_0, \{12, 34\}\{235\}) & (1, q_0, \{12, 34\}\{235\}) \end{array}\]

We continue by reading letters that exit the SCC \(\Gamma_1\), that are \(24\; 13\; 35\). The SCC \(\Gamma_2\) is fair with a delay constant \(2\), and we thus count modulo \(2\times 2-1 = 3\), while the SCC \(\Gamma_3\) is fair with a delay constant \(1\) for each of the participating processes, and we thus count modulo \(2\times 1-1=1\) which means that the counter value will always stay at \(0\) (as expected since participating processes \(p_2\) and \(p_4\) are now separated from all other processes). When reading \(24\), we already cut in \(\Gamma_3\), and thus create a new phase right away. For the SCC \(\Gamma_2\), we need to wait for the letter \(35\) to be able to cut the letter \(13\) and thus create a new phase.

\[\begin{array}{c|l|l|l} & 24 & 13 & 35 \\\hline p_1 & (1, q_0, \{12, 34\}\{235\}\{12\}) & (1, q_0, \{12, 34\}\{235\}\{12,\textcolor{blue}{34}\}\{\textcolor{blue}{13}\}) & (1, q_0, \{12, 34\}\{235\}\{12,34\}\{13\})\\\hline p_2 & (1, q_0, \{12, 34\}\{235\}\{12,\textcolor{blue}{34}\})(\textcolor{blue}{0},\textcolor{blue}{q_6},\textcolor{blue}{\varepsilon}) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) \\\hline p_3 & (1, q_0, \{12, 34\}\{235\}\{34\}) & (1, q_0, \{12, 34\}\{235\}\{\textcolor{blue}{12},34\}\{\textcolor{blue}{13}\})& (1, q_0, \{12, 34\}\{235\}\{12,34\})(\textcolor{blue}{1},\textcolor{blue}{q_4},\{\textcolor{blue}{35}\}) \\\hline p_4 & (1, q_0, \{12, 34\}\{235\}\{\textcolor{blue}{12},34\})(\textcolor{blue}{0},\textcolor{blue}{q_6},\textcolor{blue}{\varepsilon})& (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) \\\hline p_5 & (1, q_0, \{12, 34\}\{235\})& (1, q_0, \{12, 34\}\{235\})& (1, q_0, \{12, 34\}\{235\}\{\textcolor{blue}{12},\textcolor{blue}{34}\})(\textcolor{blue}{1},\textcolor{blue}{q_4},\{\textcolor{blue}{35}\}) \end{array}\]

On the next letter \(13\) that we read, process \(p_1\) learns about the phase cutting and that he needs to cut step \(\{13\}\): after expansion, the step \(\{35\}\) is known by the three processes \(p_1, p_3, p_5\) and is thus cut. When reading the last letter \(13\), process \(p_1\) has counter value \(2\) and process \(p_3\) has counter value \(0\): since processes are at most \(2-1=1\) counter value apart, they know that \(p_3\) is ahead and process \(p_1\) can thus catch up.

\[\begin{array}{c|l|l|l} & 13 & 35 & 13\\\hline p_1 & (1, q_0, \{12, 34\}\{235\}\{12,34\})(\textcolor{blue}{2},\textcolor{blue}{q_5},\{\textcolor{blue}{13}\}) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(2,q_5,\{13\}) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(\textcolor{blue}{1},\textcolor{blue}{q_5},\{\textcolor{blue}{13}\})\\\hline p_2 & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) \\\hline p_3 & (1, q_0, \{12, 34\}\{235\}\{12,34\})(\textcolor{blue}{2},\textcolor{blue}{q_5},\{\textcolor{blue}{13}\}) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(\textcolor{blue}{0},\textcolor{blue}{q_4},\{\textcolor{blue}{35}\}) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(\textcolor{blue}{1},\textcolor{blue}{q_5},\{\textcolor{blue}{13}\}) \\\hline p_4 & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_6,\varepsilon) \\\hline p_5 & (1, q_0, \{12, 34\}\{235\}\{12,34\})(1,q_4,\{35\}) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(\textcolor{blue}{0},\textcolor{blue}{q_4},\{\textcolor{blue}{35}\}) & (1, q_0, \{12, 34\}\{235\}\{12,34\})(0,q_4,\{35\}) \end{array}\]

When letter \(2\) and \(4\) are read, nothing is changing in the local states of processes \(p_2\) and \(p_4\) respectively, since every letter can now be cut with a counter value staying \(0\).

In the global state that we reach, processes \(p_1, p_3, p_5\) that are still potentially communicating, synchronise for a last time and get the global state:

To reconcile \(p_1\) (and \(p_3, p_5\)) with \(p_2\), we use the common knowledge of the state reached at the end of phase \(1\), that is \(q_3\), and the knowledge that \(p_1\) ended in \(q_4\) after the last phase, while \(p_2\) ended in \(q_6\): since \(\mathrm{diam}(q_3, q_4, q_6, \{p_1, p_2\}) = q_7\), and the fact that reconciling with \(p_4\) does not change anything, we declare the global state accepting.

References↩︎