Synthesis of Nondeterministic Asynchronous Automata

Giovanni Pighizzini ^{∗} Dipartimento di Scienze dell’Informazione Università degli Studi di Milano Via Comelico 39, 20135 Milano, Italy

                    pighizzi@imiucca.csi.unimi.it

Abstract In this paper we state a new characterization of the class of recognizable trace languages [Maz77]: we prove that this class coincides with the minimal class of trace languages containing finite languages and closed under union, product and two new operations called α– restriction and restricted iteration. Using this characterization, we give a “modular” construction of an asynchronous automaton [Zie87] accepting a given recognizable trace language.

1 Introduction

Asynchronous Automata were introduced by W. Zielonka [Zie87] as algebraic abstractions of distributed systems. These automata are very interesting since they work, using a finite number of states, in a distributed and concurrent way and, despite that, they characterize the class of recognizable trace languages [BBMS81], that is the same class of languages accepted by finite state automata over free partially commutative monoids, i.e., sequential devices.

This surprising result was obtained by Zielonka [Zie87], who gave a construction for building a deterministic asynchronous automaton recognizing the same trace language accepted by a given automaton over a free partially commutative monoid. However, the automaton so costructed is very big; in fact its number of states is superexponential in the number of states of the given automaton. Furthermore, the constuction and its correctness proof are rather complicated, and it seems difficult to simplify they, despite all efforts, e.g. [CM88].

∗Supported in part by the ESPRIT Basic Research Action No. 3166: “Algebraic and Syntactic Methods in Computer Science (ASMICS)” and by MURST 40%.

Another characterization of the class of recognizable trace languages was discovered by E. Ochmański [Och85], proving that this class coincides with the minimal class containing finite trace languages and closed under union, product and a new operation called concurrent iteration. Thus, Ochmański’s characterization suggests a different approach to the construction of asynchronous automata, similar to the usual proof of Kleene’s Theorem.

In this paper, we afford the problem of giving a “modular” construction of asynchronous automata. We do not use directly Ochmański’s characterization, since many difficults arise in trying of finding an algorithm for building an asynchronous automaton accepting the concurrent iteration of the language accepted by a given asynchronous automaton. However, using Ochmański’s results and a property of the iteration of trace languages stated in this paper, we are able of finding a new characterization of the class of recognizable trace languages: in fact, we prove that the class of recognizable trace languages coincides with the minimal class of trace languages containing finite trace languages and closed under union, product and the new operations of α–restriction and restricted iteration. Thus, as nontrivial generalizations of the usual constructions for finite automata (see for example [HU79]), we give algorithms for building asynchronous automata accepting the union, the product, the α–restriction and the restricted iteration of the languages accepted by given asynchronous automata. All these algorithms build automata whose number of states is polynomial in the number of states of the given automata.

Unfortunately, our algorithms permit only the synthesis of nondeterministic asynchronous automata, and, up to date, the only known determinization procedure is founded on Zielonka’s construction. Nevertheless, the construction provided in our paper is much simpler than that of Zielonka, and, in our opinion, by its modularity, it can be easily understood.

The paper is organized as follows. In Section 2 we briefly recall notions and notations concerning trace languages. In Section 3 we prove an useful property of the iteration of trace languages and, using it, we state a new characterization of the class of recognizable trace languages. In Section 4 we recall the definition of Asynchronous Automata and in Section 5 we give the algorithms for the synthesis of nondeterministic asynchronous automata.

2 Traces and trace languages

In this section we briefly recall the basic notions concerning trace languages.

Definition 2.1 A concurrent alphabet is a pair (A, θ), where A is a finite alphabet and θ ⊆ A × A is a symmetric and irreflexive relation, called independency relation. If (a, b) ∈ θ then we will say that a and b are independent letters; otherwise a and b are dependent. Cliques(A, θ) denotes a (fixed) family of cliques covering the complement of θ.

The free partially commutative monoid (fpcm, for short) generated by (A, θ) is defined as the initial object in the category of monoids generated by A and satisfying, besides the usual monoid axioms, the set of “commutativity laws” {ab = ba | aθb}. A trace is an element of M(A, θ). A trace language is a subset of M(A, θ).

It is well–known that M(A, θ) is isomorphic to the quotient structure A/≡_{θ} where ≡_{θ} is the least congruence over A^{∗} extending the set of commutativity laws. Then, a trace is an equivalence class of words. The equivalence class containing the word w ∈ A^{∗} will be denoted as [w]_{θ} or by [w] if θ is understood. A trace x is said to be a prefix (suffix) of a trace t if and only if there is a trace z such that t = xz (t = zx, respectively).

The set of symbols of a trace t ∈ M(A, θ) will be denoted by alph(t), i.e. alph(ϵ) = ∅ and alph(ta) = alph(t) ∪ {a} for t ∈ M(A, θ), a ∈ A. Moreover, alph(T) = ⋃_{t∈T} alph(t) for every T ⊆ M(A, θ). A subset α ⊆ A is said to be connected if for a, b ∈ α we can find a_{0}, a_{1},…, a_{n} ∈ α such that a_{0} = a, a_{n} = b and (a_{i−1}, a_{i}) ∉ θ for i = 1,…, n. A trace t is connected if alph(t) is connected. A trace language T is connected if and only if every trace of T is connected.

A trace u is a component of a trace t if u is connected and there exists a trace v such that t = uv and alph(u)×alph(v) ⊆ θ. The set of all components of a trace t will be denoted as c(t).

We are interested in the usual regular operations (union, product and iteration, denoted, as usual, with the symbols ·, ∪ and ^{∗}, respectively), and in the operations on trace languages defined as follows:

Definition 2.2 Let T be a trace language over a fpcm M(A, θ), and α be a subset of A. The decomposition of T, denoted by c(T) is the set of all components of traces of T, i.e. c(T) = ⋃_{t∈T} c(t). The concurrent iteration (coiteration, for short) of T is the language T^{co−∗} = c(T)^{∗}. The α–restriction of T is the set T_{α} = {t ∈ T | alph(t) = α}. Finally, the restricted iteration of T is the language T^{⊕} defined as follows:

T^{⊕} = \{ \begin{matrix}T^{+} & if T = T_{α} for some connected set α ⊆ A \\ ∅ & otherwise, \end{matrix}

where, as usual, T^{+} denotes the language T · T^{∗}.

The class Reg(A, θ) of regular trace languages over (A, θ) [Maz77] is defined as the smallest class containing the languages ∅, {[ϵ]}, {[a]}, for all a ∈ A, and closed with respect to the regular operations. On the other hand, the class Rec(A, θ) of recognizable trace languages over (A, θ) can be defined in a standard way using the notion of automata over free partially commutative monoids, or M(A, θ)–automata [BBMS81]. It is known that if the independency relation θ is not empty then the class Rec(A, θ) is properly included in the class Reg(A, θ).

The following characterization of the class Rec(A, θ) was obtained by Ochmański [Och85]:

Theorem 2.1 For every concurrent alphabet (A, θ), the class Rec(A, θ) of recognizable trace languages over (A, θ) is the smallest class of trace languages containing the languages ∅, {[ϵ]}, {[a]}, for all a ∈ A, and closed under union, product and coiteration.

As a consequence of the last theorem, every recognizable trace language can be denoted by a recognizable expression, i.e. an expression involving operators representing the operations of union, product and coiteration of trace languages.

Given a set S, the family of all subsets of S will be denoted as P(S).

Lemma 2.1 Let P ⊆ P(A) be a family of subsets of A and T ⊆ M(A, θ) a trace language. If T is recognizable then also the language ⋃_{α∈P} T_{α} is recognizable.

As a consequence of this lemma, for every recognizable language T the following sets are recognizable: the α–restriction of T (T_{α}, for α ⊆ A), the set of all connected traces in T, the set of all nonconnected traces in T, the set {t ∈ T | γ ⊆ alph(t) ⊆ α} = ⋃_{γ⊆β⊆α} T_{β}, for γ ⊆ α ⊆ A.

3 A new chacterization of the class of recognizable trace languages

In this section we state our main result concerning the iteration of trace languages.

Given a set α ⊆ A, α ≠ ∅, a composition of α is an ordered partition of α, i.e. a sequence p_{1},…, p_{s}, s ≥ 1, of nonempty subsets of α whose union is equal to α and such that p_{i} ∩ p_{j} = ∅ for i ≠ j. The set of all compositions of α will be denoted by Π(α).

Theorem 3.1 Given a language T ⊆ M(A, θ) and a set α ⊆ A, consider the language Z ⊆ M(A, θ) so defined:

Z = \{ \begin{matrix}⋃_{(p_{1},...,p_{s})∈Π(α)} XY_{p_{1}}XY_{p_{2}} … Y_{p_{s}}X, & if α ≠ ∅; \\ \{[ϵ]\}, & otherwise, \end{matrix}

where X = ⋃_{β⊂α}(T^{∗})_{β}, and Y_{p_{j}} = ⋃_{p_{j}⊆β⊆α} T_{β}, for j = 1,…, s. Then, (T^{∗})_{α} = Z^{+} and alph(t) = α for every trace t ∈ Z,i.e. Z = Z_{α}.

Proof. Before of proving the Theorem we remark that in the definition of X the union operation is extended to every subset β strictly included in α. For α = ∅ the proof is trivial. Then, we suppose α ≠ ∅.

The inclusion Z^{+} ⊆ (T^{∗})_{α} can be easily verified. The converse inclusion is a consequence of the following lemma:

Lemma 3.1 For every trace u ∈ (T^{∗})_{α}, either u ∈ Z or there are traces u′, u′′ such that u = u′u′′, u′ ∈ Z, |u′′| < |u| and u′′ ∈ (T^{∗})_{α}.

Proof. Since u ∈ (T^{∗})_{α} and α ≠ ∅, we can find traces u_{1},…, u_{m} ∈ T, m ≥ 1 such that u = u_{1} … u_{m}. Since alph(u) = α, there is an index k, 1 ≤ k ≤ m, such that alph(u_{1} … u_{k}) = α and alph(u_{1} … u_{k−1}) ≠ α. We consider the sequence α_{1},…, α_{k} of subsets of α such that α_{i} = alph(u_{i}) − ⋃_{j=1}^{i−1} α_{j}, for j = 1,…, k. Clearly, ⋃_{j=1}^{k} α_{j} = α and α_{i} ∩ α_{j} = ∅, for i ≠ j. From the sequence α_{1},…, α_{k}, we extract the subsequence α_{j_{1}},…, α_{j_{s}} by eliminating the empty subsets (observe that j_{s} = k). This sequence is a composition of α and α_{j_{r}} ⊆ alph(u_{j_{r}}) ⊆ α, for r = 1,…, s. Then, u_{j_{r}} ∈ Y_{α_{jr}}. By construction, the set β = alph(u_{j_{r−1}+1} … u_{j_{r}−1}) is strictly included in α, for r = 1,…, s, j_{0} = 0. On the other hand, u_{j_{r−1}+1} … u_{j_{r}−1} ∈ T^{∗}. So:

u_{j_{r−1}+1} … u_{j_{r}−1} ∈ (T^{∗})_{β} ⊆ ⋃_{β⊂α}(T^{∗})_{β} = X.

This permits us to conclude that u_{1} … u_{k} ∈ XY_{α_{j_{1}}} X… XY_{α_{js}} and, observing that [ϵ] ∈ X, we have: u_{1} … u_{k} ∈ XY_{α_{j_{1}}} X… XY_{α_{js}} X ⊆ Z. Now, we set u′ = u_{1} … u_{k} and u′′ = u_{k+1} … u_{m}. Observe that |u′| > 1 Clearly, alph(u′′) ⊆ α. If alph(u′′) = α then u′′ ∈ (T^{∗})_{α} and |u′′| < |u| and the statement is proved. On the other hand, if alph(u′′) ≠ α then u′′ ∈ (T^{∗})_{alph(u′′)} ⊆ X. Recalling that u_{1} … u_{k} ∈ XY_{α_{j_{1}}} X… XY_{α_{js}}, it turns out that u = u′u′′ ∈ (XY_{α_{j_{1}}} X… XY_{α_{js}})X ⊆ Z. Then u ∈ Z. This concludes the proof of the lemma.

Now, using the previous lemma, it is possible to show by induction on the length of traces t ∈ M(A, θ) that t ∈ (T^{∗})_{α} implies t ∈ Z^{+}. Then (T^{∗})_{α} ⊆ Z^{+}.

Using Theorem 3.1, we are now able of proving the following characterization of the class Rec(A, θ) of recognizable trace languages.

Theorem 3.2 The class Rec(A, θ) of recognizable trace languages over a concurrent alphabet (A, θ) is the smallest class containing the languages ∅, {[ϵ]}, and {[a]} (for a ∈ A) and closed with respect to the operations of union, product, restricted iteration and α–restriction.

Proof. First, we recall that as an immediate consequence of the results contained in [Och85], a characterization of the class of recognizable trace languages slightly different from that given in Theorem 2.1 can be formulated, proving that a trace language is recognizable if and only if it can be denoted by a regular expression where iterations are applied only to connected trace languages. Using this result, the proof of this theorem is quite simple. The more difficult point is to show that the iteration T^{∗} of a connected recognizable trace language T can be expressed using the operations of union, product, α–restriction and restricted iteration. To prove that we recall that T^{∗} = ⋃_{α⊆A}(T^{∗})_{α} and we show that every language (T^{∗})_{α} can be expressed inductively from T and (T^{∗})_{β}, where β is strictly included in α, using the above mentioned operations.

For α = ∅, we have (T^{∗})_{∅} = {[ϵ]}. Suppose now that α ≠ ∅. If α is nonconnected, we have (T^{∗})_{α} = (T^{+})_{α_{1}} · . . . · (T^{+})_{α_{k}}, where the sets α_{1},…, α_{k} are the connected components of α; then (T^{+})_{α_{j}} = (T^{∗})_{α_{j}}, with α_{j} ⊂ α, j = 1,…, k.

On the other hand, if α is connected, then by Theorem 3.1 we have: (T^{∗})_{α} = Z^{+}, with Z = ⋃_{(p_{1},...,p_{s})∈Π(α)} XY_{p_{1}}XY_{p_{2}} … Y_{p_{s}}X, X = ⋃_{β⊂α}(T^{∗})_{β}, and, for j = 1,…, s, Y_{p_{j}} = ⋃_{p_{j}⊆β⊆α} c(T)_{β}. Moreover, alph(t) = α, for every trace t ∈ Z. Then Z^{+} = Z^{⊕}. This implies that (T^{∗})_{α} = Z^{⊕}.

4 Asynchronous Automata

In this section we briefly recall the definition and some properties of Asynchronous Automata.

Definition 4.1 A nondeterministic asynchronous automaton (NAA) M with n processes, over a concurrent alphabet (A, θ), is a tuple (P_{1},…, P_{n}, {δ_{a}}_{a∈A}, I, F), where:

• for i = 1,…, n, P_{i} = (A_{i}, S_{i}) is the ith process, where S_{i} is its set of local states and A_{i} is its local alphabet, such that {A_{1},…, A_{n}} = Cliques(A, θ);

• let us denote by P roc the set (of indices) of processes of the asynchronous automaton M, i.e., P roc = {1,…, n}, and, for a ∈ A, by Dom(a) the set of (indices of) processes that execute a, i.e., Dom(a) = {i ∈ P roc | a ∈ A_{i}}; then δ_{a} : ∏_{i∈Dom(a)} S_{i} → P(∏_{i∈Dom(a)} S_{i}) is the local transition function associated to the letter a;

• let S = ∏_{i∈P roc} S_{i} be the set of global states; then I ⊆ S is the set of the initial states and F ⊆ S is the set of final states.

A global state will be denoted by a boldface letter, as s, while its ith component as s_{i}; given a global state s ∈ S and a set of (indices of) processes α = {i_{1},…, i_{k}} ⊆ P roc, we will denote by s_{|α} the vector whose components correspond to local states in α, i.e. s_{|α} = (s_{i_{1}},…, s_{i_{k}}).

The global transition function Δ : S ×M(A, θ) → P(S) of the automaton M is defined on the ground of local transition functions as follows. For every s, u ∈ S, a ∈ A, we have: u ∈ Δ(s, a) if and only if u_{|Dom(a)} ∈ δ_{a}(s_{|Dom(a)}) and u_{|\overline{Dom(a)}} = s_{|\overline{Dom(a)}}. The extension to traces can be obtained in a standard way.

The language accepted by the automaton M is defined as the set:

T (M) = {t ∈ M(A, θ) | Δ(I, t) ∩ F ≠ ∅}.

If #I = 1 and # (δ_{a}(s_{i_{1}},…, s_{i_{k}})) ≤ 1 for every (s_{i_{1}},…, s_{i_{k}}) ∈ ∏_{i∈Dom(a)} S_{i}, a ∈ A, the automaton M is said to be a deterministic asynchronous automaton (DAA).

It is immediate to verify that to every asynchronous automaton can be associated a finite state automaton recognizing the same trace language. Moreover, given a finite automaton over the the fpcm M(A, θ) it is possible to construct a DAA with the same concurrent alphabet, accepting the same language. This very surprising result was obtained by W. Zielonka.

Theorem 4.1 [Zie87] The class of languages accepted by deterministic asynchronous automata over (A, θ) coincides with the class Rec(A, θ) of trace languages recognized by M(A, θ)–automata.

Another proof of Theorem 4.1 can be found in [CM88].

From this point on, we consider a fixed concurrent alphabet (A, θ) with a fixed clique cover Cliques(A, θ) = {A_{1},…, A_{n}} of the dependency relation. For all notations concerning NAA the reader is referred to this section. When we deal with different NAA M, M′ and M′′, we always suppose that A_{i} = A′_{i} = A′′_{i} and S′_{i} ∩ S′′_{i} = ∅ for i ∈ P roc.

4.1 Asynchronous automata with ϵ–moves

Here, we consider an extension of NAA useful in our algorithm. In the model we will consider every process can change its internal state, independently from the states of other processes and from the next input symbol, using an internal transition called ϵ–move. The ϵ–moves are represented extending every local alphabet with a new symbol. More precisely, we consider the concurrent alphabet (Â, θ̂) such that Â = A ∪ {e_{1},…, e_{n}}, where {e_{1},…, e_{n}} ∩ A = ∅, and

θ̂ = θ ∪ {(e_{i}, e_{j}) | i ≠ j} ∪ {(a, e_{i}), (e_{i}, a) | a ∈ A − A_{i}}.

Then Cliques(Â, θ̂) = {Â_{1},…, Â_{n}}, where Â_{i} = A_{i} ∪ {e_{i}}, i = 1,…, n.

To every trace t̂ ∈ M(Â, θ̂) we associate the trace ψ(t̂) ∈ M(A, θ) obtained erasing from t̂ all letters not belonging to A. Given a language T̂ ⊆ M(Â, θ̂) we denote by ψ(T̂) the set ⋃_{t̂∈_{T}} ψ(t̂).

The following theorem states an important relationship between NAA over M(Â, θ̂) and NAA over M(A, θ).

Theorem 4.2 Let T̂ ⊆ M(Â, θ̂) be the language accepted by a NAA M̂. Then, there exists a NAA over M(A, θ) accepting the language ψ(T̂).

Proof (outline). The automaton M is defined as follows: S_{i} = Ŝ_{i}, i = 1,…, n; I = {s ∈ S | ∃w ∈ M(Â, θ̂) s.t. alph(w) ⊆ {e_{1},…, e_{n}} and s ∈ Δ̂(Î, w)}; F = F̂; for a ∈ A with Dom(a) = {i_{1},…, i_{k}}, s ∈ ∏_{i∈Dom(a)} S_{i}:

δ′_{a}(s) = {u ∈ ∏_{i∈Dom(a)} S_{i} | ∃s′, u′ ∈ Ŝ s.t. s′_{|Dom(a)} = s, u′_{|Dom(a)} = u,

∃w ∈ M(Â, θ̂) s.t. alph(w) ⊆ {e_{i_{1}},…, e_{i_{k}}}, and u′ ∈ Δ̂(s′, aw)}.

It is easy to prove that for t ∈ M(A, θ) it holds: Δ(I, t) = ⋃_{t̂∈ψ^{−1}(t)} Δ̂(I, t̂).

5 Synthesis of Asynchronous Automata

In this section we state our modular construction of nondeterministic asynchronous automata.

First, we observe that asynchronous automata accepting the languages ∅, {[ϵ]} and {[a]}, a ∈ A, can be trivially constructed. Thus, we will give synthesis algorithms corresponding to operations of union, product, α–restriction and restricted iteration. It is not difficult to verify that the number of states of the automata obtained using all constructions stated here is polynomial in the number of states of the given automata.

5.1 Union

The construction of a NAA M accepting the union of the languages accepted by two given NAA M′ and M′′ is trivial. Then we give it without any comment.

We define M as follows: S_{i} = S′_{i} ∪ S′′_{i}, i = 1,…, n; I = I′ ∪ I′′; F = F′ ∪ F′′; for a ∈ A and s ∈ ∏_{i∈Dom(a)} S_{i}:

δ_{a}(s) = \{ \begin{matrix}δ′_{a}(s) & if s ∈ ∏_{i∈Dom(a)} S′_{i} \\ δ′′_{a}(s) & if s ∈ ∏_{i∈Dom(a)} S′′_{i} \\ ∅ & otherwise. \end{matrix}

It is easy to verify that for every global state s ∈ I and for every trace t ∈ M(A, θ) Δ(s, t) is equal to Δ′(s, t) (Δ′′(s, t)) if s ∈ I′ (s ∈ I′′, respectively). So, M can simulate the computations of M′ and M′′ and it recognizes the language T (M′) ∪ T (M′′).

5.2 Product

Given two NAA M′ and M′′, for every s ∈ S′, let M′_{s} be the NAA M′_{s} = (P′_{1},…, P′_{n}, {δ′_{a}}_{a∈A}, I′, {s}) and for every s ∈ S′′ let _{s}M′′ be the NAA sM′′ = (P′′_{1},…, P′′_{n}, {δ′′_{a}}_{a∈A}, {s}, F′′). Then, the equality T (M′) · T (M′′) = ∪_{(s′,s′′)∈F′×I′′}T (M′_{s′})·T (_{s′′}M′′) can be immediately proved. Thus, it sufficies to consider in this section only automata M′ and M′′ such that #F′ = 1 and #I′′ = 1. We will denote by F′ = (F′_{1},…, F′_{n}) the only final state of M′ and by I′′ = (I′′_{1},…, I′′_{n}) the only initial state of M′′.

We define the following automaton M with ϵ–moves.

• S_{i} = S′_{i} ∪ S′′_{i}, i = 1,…, n;

• I = I′;

• F = F′′;

• for a ∈ A with Dom(a) = {i_{1},…, i_{k}}, s_{i_{j}} ∈ S_{i_{j}}, j = 1,…, k:

δ_{a}(s_{i_{1}},…, s_{i_{k}}) = \{ \begin{matrix}δ′_{a}(s_{i_{1}},…, s_{i_{k}}) & if s_{i_{j}} ∈ S′_{i_{j}}, 1 ≤ j ≤ k, \\ δ′′_{a}(s_{i_{1}},…, s_{i_{k}}) & if s_{i_{j}} ∈ S′′_{i_{j}}, 1 ≤ j ≤ k, \\ ∅ & otherwise; \end{matrix}

• for i = 1,…, n, s_{i} ∈ S_{i}:

δ_{e_{i}}(s_{i}) = \{ \begin{matrix}\{I′′_{i}\} & if s_{i} = F′_{i}, \\ ∅ & otherwise. \end{matrix}

Now, we prove that T (M) = T (M′){[e_{1} … e_{n}]}T (M′′). First, we get the following immediate remarks. Remarks

(a) For every trace t ∈ M(A, θ) (i.e., T does not contain any symbol corresponding to an ϵ–move) and for every s ∈ S′: Δ(s, t) = Δ′(s, t);

(b) for every trace t ∈ M(A, θ) and for every s ∈ S′′: Δ(s, t) = Δ′′(s, t);

(c) Δ(F′, [e_{1} … e_{n}]) = I′′;

(d) for every t ∈ T (M) every process P_{i} on input t executes exactly one ϵ-move, i.e. |t|_{e_{i}} = 1. Now, we can prove the following theorem.

Theorem 5.1 T (M) = T (M′){e_{1} … e_{n}}T (M′′).

Proof. The inclusion of T (M′){[e_{1} … e_{n}]}T (M′′) in T (M) is an immediate consequence of previous remarks. In order to prove the converse inclusion, we consider a trace t ∈ T (M). From Remark (d), we can find traces u_{0},…, u_{n} ∈ M(A, θ) and a permutation (i_{1},…, i_{n}) of (1,…, n) such that t = u_{0}e_{i_{1}}u_{1}e_{i_{2}} … e_{i_{n}}u_{n}. Let be 1 ≤ k ≤ n and a ∈ alph(u_{k}). Then u_{k} = vaw for suitable traces v, w ∈ M(A, θ) and t = u_{0} … e_{i_{k}}vawe_{i_{k+1}} … u_{n}. Since M accepts t, there are global states s′, s′′ ∈ S such that:

s′ ∈ Δ(I′, u_{0} … e_{i_{k}}v),

s′′ ∈ Δ(s′, a) and

Δ(s′′, we_{i_{k+1}} … u_{n}) ∩ F ≠ ∅. More precisely, we can observe that both local states s′_{i_{j}}, s′′_{i_{j}} belong to S′_{i_{j}}, for j > k, while both s′_{i_{j}}, s′′_{i_{j}} belong to S′′_{i_{j}} for j ≤ k. Then, from the definition of δ_{a} and from Δ(s′, a) ≠ ∅ it follows that either Dom(a) ⊆ {i_{k+1},…, i_{n}} or Dom(a) ⊆ {i_{1},…, i_{k}}. So, we can decompose u_{k} as product of two independent traces u′_{k} and u′′_{k}, s.t. Dom(u′_{k}) ⊆ {i_{k+1},…, i_{n}} and Dom(u′′_{k}) ⊆ {i_{1},…, i_{k}}. Moreover Dom(u′′_{k}) ∩ Dom(u′_{j}) = ∅ for j > k. Then, we can rewrite t as u′_{0} … u′_{n}[e_{1} … e_{n}]u′′_{0} … u′′_{n}. Finally, let s ∈ I′, q ∈ F′′ be the states corresponding to the start and to the end of such an accepting computation. More precisely:

s′ ∈ Δ(s, u_{0} … e_{i_{k}}v) and q ∈ Δ(s′′, we_{i_{k+1}} … u_{n}). It is easy to observe that:

F′ ∈ Δ′(s, u′_{0} … u′_{n}) and q ∈ Δ′′(I′′, u′′_{0} … u′′_{n}). Then u′_{0} … u′_{n} ∈ T (M′) and u′′_{0} … u′′_{n} ∈ T (M′′).

Finally, applying the construction given in the proof of Theorem 4.2, we can obtain a NAA accepting the language T (M′)T (M′′).

5.3 α–restriction

Here, we briefly describe how it is possible to build a NAA accepting the restriction of the language accepted by a given NAA. The idea is essentialy that of keeping in every local state the alphabet of the trace executed so far. More precisely, we consider the sets of local states S′_{i} = S_{i} × P(A_{i}), i ∈ P roc, the set of initial global states I′ = {((s_{1}, ∅),…, (s_{n}, ∅)) | s ∈ I}, and the local transition functions δ_{a}, a ∈ A, such that:

δ′_{a}((s_{i_{1}}, α_{i_{1}}),…, (s_{i_{k}}, α_{i_{k}})) = {((u_{i_{1}}, α_{i_{1}} ∪ {a}),…, (u_{i_{k}}, α_{i_{k}} ∪ {a})) | (u_{i_{1}},…, u_{i_{k}}) ∈ δ_{a}(s_{i_{1}},…, s_{i_{k}})},

for s_{i_{j}} ∈ S_{i_{j}}, α_{i_{j}} ⊆ A_{i_{j}}, j = 1,…, k, where {i_{1},…, i_{k}} = Dom(a). It is not difficult to verify that for every trace t ∈ M(A, θ), it holds:

Δ′(I′, t) = {((s_{1}, alph(t) ∩ A_{1}),…, (s_{n}, alph(t) ∩ A_{n})) | s ∈ Δ(I, t)}.

We now define two NAAs M_{k} = (P′_{1},…, P′_{n}, {δ′_{a}}, I′, F_{k}), k = 1, 2. M_{1} is obtained choosing as set of final states the set:

F_{1} = {((s_{1}, α_{1}),…, (s_{n}, α_{n}))|(s_{1},…, s_{n}) ∈ F }.

Of course, the language accepted by M_{1} coincides with the language accepted by M, i.e., T (M_{1}) = T (M). Fixed a set α ⊆ A, in order to recognize the α–restriction of T (M) we have to accept all traces of T (M) whose alphabet is exactly α. This goal can be achieved setting

F_{2} = {((s_{1}, α_{1}),…, (s_{n}, α_{n}))|(s_{1},…, s_{n}) ∈ F and ⋃_{i=1}^{n} α_{i} = α}.

It is clear that T (M_{2}) = (T (M))_{α}.

5.4 Restricted iteration

First, we observe that given a NAA M accepting a trace language T ⊆ M(A, θ) we can decide if T = T_{α} for some connected set α ⊆ A, by constructing a finite state automaton M accepting T and verifying if M is equivalent to some automaton M_{α} accepting the language T_{α} for a connected α ⊆ A.

Since the asynchronous automaton recognizing the empty language can be trivially constructed, from this point on we will consider the problem of building an asynchronous automaton accepting T^{⊕} = T^{+}, when T = T_{α} for some connected alphabet α ⊆ A.

Let M be a NAA accepting a trace language T, such that T = T_{α}, for some connected set α ⊆ A. There is none loss of generality assuming that the following conditions hold:

1. α = A;

2. there exists a map ϕ : ⋃_{i=1}^{n} S_{i} → P(A) such that if Δ(I, t) = s then ϕ(s_{i}) = alph(t) ∩ A_{i}, for i = 1,…, n, t ∈ M(A, θ) (this means that the automaton M records the letters of traces. Observe that if s_{i} is a compontent of some final state p, then ϕ(s_{i}) = A_{i}).

Suppose in fact that α ⊂ A. From the asynchronous automaton M it is possible to obtain an automaton M̃ by removing all the processes P_{i} such that A_{i} ∩ α = ∅ and all transitions involving letters not belonging to α. Applying the construction presented below, we will obtain an automaton M̃′ over the concurrent alphabet (α, θ ∩ (α × α)). This automaton can be easily extended to the concurrent alphabet (A, θ), by introducing dummy processes and null transition functions. We observe that for the automaton M_{1} defined in Section 5.3, the second condition holds.

For sake of simplicity, first we suppose that #I = #F = 1. Then, we will denote by I = (I_{1},…, I_{n}) and by F = (F_{1},…, F_{n}) the only initial and the only final state of M, respectively.

In the classical construction of the finite automaton N′ recognizing the iteration of the language recognized by a given finite automaton N (see e.g. [HU79]), an empty transition from the final state to the initial state is added to N. In our case, we want to construct an automaton M′ recognizing all traces of the form t_{1}[e_{1} … e_{n}]t_{2}[e_{1} … e_{n}] … [e_{1} … e_{n}]t_{m} such that m > 0 and t_{i} ∈ T (M), i = 1,…, m. However, as shown in the following example, the immediate generalization to asynchronous automata of the strategy used for finite automata does not work.

Example Let (A, θ) be the concurrent alphabet with:

A = {a, b, c, d}, θ = {(a, c), (c, a), (a, d), (d, a), (b, d), (d, b)},

and Cliques(A, θ) = {A_{1}, A_{2}, A_{3}}, where A_{1} = {a, b}, A_{2} = {b, c} and A_{3} = {c, d}. Let M be the asynchronous automaton represented in Figure 1. It is not difficult to see that M accepts the set T (M) = {[acbd]}.

[figure: I_{1}; r_{1}; F_{1}; I_{2}; r_{2}; F_{2}; I_{3}; r_{3}; F_{3}; a; a; b; c; d]

Figure 1: automaton M

Moreover, M satisfies the hypothesis stated above (that is α = A and there exists the map ϕ). Now, if we add, for every i ∈ P roc, a transition from the component F_{i} of the final state to the component I_{i} of the initial state, the resulting automaton can recognize a set that properly includes (T (M))^{+}. The automaton obtained applying this procedure in our specific case, is represented in Figure 2. Such an automaton accepts, for example, the trace [acbade_{2}e_{3}cbd]. Observe that Dom(b) = {1, 2}, but before the last occurrence of b, the process P_{2} executes one ϵ–move, while none ϵ–move is execute by P_{1}.

[figure: I_{1}; r_{1}; F_{1}; I_{2}; r_{2}; F_{2}; I_{3}; r_{3}; F_{3}; a; a; b; c; d; e_{1}; e_{3}; e_{2}]

Figure 2: automaton constructed introducing an ϵ–move from every component of the final state to the corresponding component of the initial state

We will show that, in order to avoid the problems arising in previous example, we have to circularly rearrange two isomorphic copies of the given NAA M.

Formally, we define M′ in the following way:

• S′_{i} = S_{i} × {0, 1}, i = 1,…, n;

• I′ = {((I_{1}, 0),…, (I_{n}, 0))};

• for a ∈ A, Dom(a) = {i_{1},…, i_{k}}, s_{i_{j}} ∈ S_{i_{j}}, j = 1,…, k, b_{i_{1}},…, b_{i_{k}} ∈ {0, 1}:

δ′_{a}((s_{i_{1}}, b_{i_{1}}),…, (s_{i_{k}}, b_{i_{k}})) =
= {((u_{i_{1}}, b),…, (u_{i_{k}}, b)) | (u_{i_{1}},…, u_{i_{k}}) ∈ δ_{a}(s_{i_{1}},…, s_{i_{k}})},

if there exists b ∈ {0, 1} s.t. b_{i_{1}} = … = b_{i_{k}} = b;

δ′_{a}((s_{i_{1}}, b_{i_{1}}),…, (s_{i_{k}}, b_{i_{k}})) = ∅

otherwise.

• for i = 1,…, n, s_{i} ∈ S_{i}, b ∈ {0, 1}:

δ′_{e_{i}}(s_{i}, b) = \{ \begin{matrix}\{(I_{i}, 1 − b)\} & if s_{i} = F_{i} \\ ∅ & otherwise; \end{matrix}

• F′ = {((F_{1}, b),…, (F_{n}, b)) | b ∈ {0, 1}}.

[figure: (I_{1},0); (r_{1},0); (F_{1},0); (I_{2},0); (r_{2},0); (F_{2},0); (I_{3},0); (r_{3},0); (F_{3},0); a; a; b; c; d; (I_{1},1); (r_{1},1); (F_{1},1); (I_{2},1); (r_{2},1); (F_{2},1); (I_{3},1); (r_{3},1); (F_{3},1); a; a; b; c; d; e_{1}; e_{2}; e_{3}; e_{1}; e_{3}; e_{2}]

Figure 3: automaton M′

In Figure 3, the automaton M′ obtained applying this costruction to the automaton M of Figure 1, is represented.

To prove the correctness of the construction, we will show that the automaton M′ recognizes the set of all traces of the form

t_{1}[e_{1} … e_{n}]t_{2}[e_{1} … e_{n}] … [e_{1} … e_{n}]t_{m},

where m ≥ 1 and t_{i} ∈ T, i = 1,…, m.

It is not difficult to see that every trace of such a form is accepted by M′. Then, we prove the converse result.

First, we will prove the following remarks:

Remarks

(a) Between two ϵ–moves of a process P′_{i} in an accepting computation, there is at least one occurence of every letter of A_{i}.

(b) In every accepting computation of M′, before of the execution of a symbol a there is either at least one ϵ–move of every process in Dom(a) or none ϵ–move of processes in Dom(a).

(c) If some process of M′ performs an ϵ–move on an accepted trace then every process performs an ϵ–move.

Remarks (a),(b) and (c) are consequences of the following lemmas, respectively.

Lemma 5.1 If t ∈ (Â, θ̂) is accepted by M′ and t = t_{0}e_{i}t_{1}e_{i}t_{2}, for suitable traces t_{0}, t_{1}, t_{2} ∈ (Â, θ̂), then A_{i} ⊆ alph(t_{0}), A_{i} ⊆ alph(t_{1}), A_{i} ⊆ alph(t_{2}).

Proof. We prove that A_{i} ⊆ alph(t_{1}). The other proofs are very similar. First, we suppose that e_{i} ∉ alph(t_{1}). Since t ∈ T (M′), we can find suitable global states of M′ such that:

((s_{1}, b_{1}),…, (s_{n}, b_{n})) ∈ Δ′(I′, t_{0}e_{i}),

((u_{1}, b′_{1}),…, (u_{n}, b′_{n})) ∈ Δ′(((s_{1}, b_{1}),…, (s_{n}, b_{n})), t_{1}) and Δ′(((u_{1}, b′_{1}),…, (u_{n}, b′_{n})), e_{i}t_{2}) ∩ F′ ≠ ∅.

Since e_{i} ∉ alph(t_{1}), we have b_{i} = b′_{i}. Moreover (s_{i}, b_{i}) is reached after one ϵ–move of the process P_{i}. Then s_{i} = I_{i} and ϕ(s_{i}) = ∅. Since δ_{e_{i}}(u_{i}, b′_{i}) ≠ ∅, we have u_{i} = F_{i}. Then ϕ(u_{i}) = A_{i}. This implies that A_{i} ⊆ alph(t_{1}).

If e_{i} ∈ alph(t_{1}), then there are traces v_{1},…, v_{m} such that t_{1} = v_{1}e_{i}v_{2}e_{i}… e_{i}v_{m} and e_{i} ∉ alph(v_{j}), j = 1,…, m. Using the previous argument it can be shown that A_{i} ⊆ alph(v_{j}).

Lemma 5.2 Let t ∈ M(Â, θ̂) be a trace accepted by the automaton M′, with t = ue_{i}vaw, for some u, v, w ∈ M(Â, θ̂), a ∈ A, i ∈ P roc, such that e_{i} ∉ alph(u), and let j ∈ P roc be an index such that e_{j} ∉ alph(ue_{i}v). Then {i, j} cannot be a subset of Dom(a).

Proof. Since t ∈ T (M′), there are s, s′, s′′ ∈ S, and b_{1},…, b_{n}, b′_{1},…, b′_{n}, b′′_{1},…, b′′_{n} ∈ {0, 1} such that:

((s_{1}, b_{1}),…, (s_{n}, b_{n})) ∈ Δ′(((I_{1}, 0),…, (I_{n}, 0)), ue_{i}), ((s′_{1}, b′_{1}),…, (s′_{n}, b′_{n})) ∈ Δ′(((s_{1}, b_{1}),…, (s_{n}, b_{n})), v), ((s′′_{1}, b′′_{1}),…, (s′′_{n}, b′′_{n})) ∈ Δ′(((s′_{1}, b′_{1}),…, (s′_{n}, b′_{n})), a), Δ′(((s′′_{1}, b′′_{1}),…, (s′′_{n}, b′′_{n})), w) ∩ F′ ≠ ∅.

If both i, j belong to Dom(a) then from Δ(((s′_{1}, b′_{1}),…, (s′_{n}, b′_{n})), a) ≠ ∅ and from e_{j} ∉ alph(uv), it turns out that b′_{i} = b′_{j} = 0. On the other hand, observing that after the ϵ–move of the process P_{i} it holds b_{i} = 1 and s_{i} = I_{i}, we can conclude that e_{i} ∈ alph(v), i.e. v = z′e_{i}z′′ for suitable traces z′ and z′′. From Lemma 5.1 we have a ∈ alph(z′) and |v| ≠ 0. Then t = ue_{i}v_{1}aw_{1}, for suitable traces v_{1}, w_{1}, with |v_{1}| < |v|. We can iterate the proof for this decomposition. So, we will find a countable sequence of traces v_{1}, v_{2},… such that for every k |v_{k}| < |v_{k−1}| and |v_{k}| ≠ 0. This is contradictory. Then Dom(a) cannot contain both indices i and j.

Lemma 5.3 Let t ∈ M(Â, θ̂) be a trace accepted by the automaton M′. If there is an index i ∈ P roc such that e_{i} ∈ alph(t), then e_{j} ∈ alph(t), for every j ∈ P roc.

Proof. First, we prove the result for A_{i} ∩ A_{j} ≠ ∅. Since t is accepted, there exists a global state ((p_{1}, b),…, (p_{n}, b)) belonging to Δ′(I′, t) ∩ F′. Suppose that e_{j} ∉ alph(t). This means that the component P_{j} does not perform ϵ–moves and then b = 0. On the other hand e_{i} ∈ alph(t). Then, this ϵ–move of the component P_{i} changes the last component of the local state of P_{i} from 0 to 1. So, at least another ϵ–move must be performed by P_{i} in order to have b = 0. Then, we can decompose t as t = t_{0}e_{i}t_{1}e_{i}t_{2}. As a consequence of Lemma 5.1, for every a letter a ∈ A_{i} ∩ A_{j}, we have a ∈ alph(t_{1}). From Lemma 5.2, it turns out that {i, j} cannot be a subset of Dom(a). This is a contradiction. Then we conclude that e_{i} ∈ alph(t).

To prove the lemma in the general case, we recall that the alphabet A is connected. Then, we can find a sequence P_{i_{0}},…, P_{i_{m}} of processes such that i_{0} = i, i_{m} = j and A_{i_{k−1}} ∩ A_{i_{k}} ≠ ∅, k = 1,…, m. The proof of the lemma follows applying the previous argument to every pair (i_{k−1}, i_{k}).

Now, we can prove the correctness of the construction stated here.

Theorem 5.2 Let M′ the NAA above defined. Then:

T (M′) = {t_{1}[e_{1} … e_{n}] … [e_{1} … e_{n}]t_{m} | m ≥ 1 and t_{1},…, t_{m} ∈ T (M)}.

Proof. The difficult point is to prove that every trace accepted by the automaton M′ has the form t_{1}[e_{1} … e_{n}]t_{2} … t_{m−1}[e_{1} … e_{n}]t_{m}, with m ≥ 1, t_{i} ∈ T, i = 1,…, m. First, we observe that every trace t accepted by M′ without ϵ–moves, i.e. alph(t) ⊆ A, is accepted also by the automaton M. Then, t ∈ T (M)^{+}. Suppose now that t is accepted using at least one ϵmove. From Remark (c) it turns out that every process executes at least one ϵ-move, i.e. e_{i} ∈ alph(t) for every i ∈ P roc. So, we can decompose t as u_{0}e_{i_{1}}u_{1}e_{i_{2}} … e_{i_{n}}u_{n} where (i_{1},…, i_{n}) is a permutation of (1,…, n) and e_{i_{j}} ∉ alph(u_{k}) for k < j. By Remark (b), either Dom(a) ⊆ {i_{1},…, i_{k}} or Dom(a) ⊆ {i_{k+1},…, i_{n}}, for every letter a ∈ alph(u_{k}), k = 1,…, n. Then, u_{k} = u′_{k}u′′_{k}, where Dom(u′_{k}) ⊆ {i_{k+1},…, i_{n}} and Dom(u′′_{k}) ⊆ {i_{1},…, i_{k}}. It is easy to verify that t = u′_{0} … u′_{n}[e_{1} … e_{n}]u′′_{0} … u′′_{n}.

Let be t′ = u′_{0} … u′_{n} and t′′ = u′′_{0} … u′′_{n}. We now briefly prove that t′ ∈ T (M) and t′′ ∈ T (M′). By definition of M′, we can find b ∈ {0, 1} such that:

((F_{1}, b),…, (F_{n}, b)) ∈ Δ′(((I_{1}, 0),…, (I_{n}, 0)), t′[e_{1} … e_{n}]t′′). More precisely, observing the definition of δ′_{e_{i}}, we obtain:

((F_{1}, 0),…, (F_{n}, 0)) ∈ Δ′(((I_{1}, 0),…, (I_{n}, 0)), t′);

((I_{1}, 1),…, (I_{n}, 1)) ∈ Δ′(((F_{1}, 0),…, (F_{n}, 0)), [e_{1} … e_{n}]);

((F_{1}, b),…, (F_{n}, b)) ∈ Δ′(((I_{1}, 1),…, (I_{n}, 1)), t′′). Since e_{i} ∉ alph(t′), i = 1,…, n, it turns out that F ∈ Δ(I, t′) and then t′ ∈ T (M). Furthermore, from these relationships, we can easily obtain:

((F_{1}, 1 − b),…, (F_{n}, 1 − b)) ∈ Δ′(((I_{1}, 0),…, (I_{n}, 0)), t′′), that implies t′′ ∈ T (M′).

At this point, iterating the previous proof on the trace t′′ it turns out that t is of the form t_{1}[e_{1} … e_{n}]t_{2} … t_{m−1}[e_{1} … e_{n}]t_{m}, with t_{j} ∈ T (M), j = 1,…, m.

Applying Theorem 4.2 to the automaton M′, we can obtain a NAA accepting the language T (M)^{+}.

Now, we briefly discuss how it is possible to generalize the previous construction when there are no restrictions on the cardinality of sets I and F.

The idea is very similar to particular case above considered. When a process P_{i} reaches a component of a final state, it can change its state, using an ϵ–move, to go in a component of an initial state.

The problem is to assure that all processes choose the same final and the same initial global state. This problem is solved in this way. At the start of the computation all processes are synchronized and an initial state s ∈ I and a final state p ∈ F are chosen. Then, the computation starts and every process simulates the corresponding process of M, keeping the pair (s, p) in its local state.

When the process P_{i} arrives to simulate the local state p_{i} of M, it can perform an empty transition choosing a new pair (s′, p′) ∈ I × F.

When a symbol a ∈ A is executed, all processes in Dom(a) are synchronized and they compare the pairs of initial and final states contained in their proper memories. If these pairs do not coincide then none transition is possible. Since all traces in the language accepted by M are connected and since the automaton M records the letters of traces, this method assures that in an accepting computation of M′ all kth empty transitions of processes correspond to the same initial and to the same final state. Formally, the automaton M is defined as follows:

• S′_{i} = S_{i} × I × F × {0, 1}, i = 1,…, n;

• I′ = {((s_{1}, s, p, 0),…, (s_{n}, s, p, 0)) | s ∈ I, p ∈ F };

• for a ∈ A, Dom(a) = {i_{1},…, i_{k}}, s_{j} ∈ S_{i_{j}}, j = 1,…, k, q_{1},…, q_{k} ∈ I, p_{1},…, p_{k} ∈ F, b_{1},…, b_{k} ∈ {0, 1}:

δ′_{a}((s_{1}, q_{1}, p_{1}, b_{1}),…, (s_{k}, q_{k}, p_{k}, b_{k})) = = {((u_{1}, q, p, b),…, (u_{k}, q, p, b)) | (u_{1},…, u_{k}) ∈ δ_{a}(s_{1},…, s_{k})},

if there are q ∈ I, p ∈ F, b ∈ {0, 1}, s.t. q_{1} = … = q_{k} = q, p_{1} = … = p_{k} = p, and b_{1} = … = b_{k} = b;

δ′_{a}((s_{1}, q_{1}, p_{1}, b_{1}),…, (s_{k}, q_{k}, p_{k}, b_{k})) = ∅,

otherwise.

• for i = 1,…, n, s_{i} ∈ S_{i}, q ∈ I, p ∈ F, b ∈ {0, 1}:

δ′_{e_{i}}(s_{i}, q, p, b) = \{ \begin{matrix}\{(q′_{i}, q′, p′, 1 − b) | q′ ∈ I, p′ ∈ F \} & if s_{i} = p_{i} \\ ∅ & otherwise; \end{matrix}

• F′ = {((p_{1}, q, p, b),…, (p_{n}, q, p, b)) | q ∈ I, p ∈ F, b ∈ {0, 1}}.

Previous remarks (a), (b) and (c) hold also in this case. The correctness proof given in Theorem 5.2 can be easily generalized.

Acknowledgement Thanks to the anonymous referee who suggested me the possibility of giving the synthesis algorithm without considering the decomposition operation.

References

[BBMS81] A. Bertoni, M. Brambilla, G. Mauri, and N. Sabadini. An application of the theory of free partially commutative monoids: asymptotic densities of trace languages. In Proc. 10th MFCS, Lecture Notes in Computer Science 118, pages 205–215, 1981.

[CM88] R. Cori and Y. Métivier. Approximation of a trace, asynchronous automata and the ordering of events in a distributed system. In Proc. 15th ICALP, Lecture Notes in Computer Science 317, pages 147–161, 1988.

[HU79] J. Hopcroft and J. Ullman. Introduction to automata theory, languages and computations. Addison–Wesley, 1979.

[Maz77] A. Mazurkiewicz. Concurrent program schemes and their interpretations. Technical Report DAIMI Rep. PB–78, Aarhus University, 1977.

[Och85] E. Ochmański. Regular behaviour of concurrent systems. EATCS Bullettin, 27:56–67, 1985.

[Zie87] W. Zielonka. Notes on finite asynchronous automata. RAIRO Inf. Theor., 21:99–135, 1987.