Foundations of Software Technology and Theoretical Computer Science 19th Conference, Proceedings, C. Pandu Rangan, V. Raman and R. Ramanujam (eds.) Springer Lecture Notes in Computer Science 1739 (1999), 219–231.

Synthesizing distributed transition systems from global specifications^{⋆}

Ilaria Castellani^{1}, Madhavan Mukund^{2}, and P S Thiagarajan^{2}

1 INRIA Sophia Antipolis, 2004 route des Lucioles, B.P. 93, 06092 Sophia Antipolis

    Cedex, France. E-mail: Ilaria.Castellani@sophia.inria.fr

2 Chennai Mathematical Institute, 92 G.N. Chetty Road, Chennai 600 017, India.

              E-mail: {madhavan,pst}@smi.ernet.in

Abstract. We study the problem of synthesizing distributed implementations from global specifications. In particular, we characterize when a global transition system can be implemented as a synchronized product of local transition systems. Our work extends a number of previous studies in this area which have tended to make strong assumptions about the specification—either in terms of determinacy or in terms of information concerning concurrency.

We also examine the more difficult problem where the correctness of the implementation in relation to the specification is stated in terms of bisimulation rather than isomorphism. As an important first step, we show how the synthesis problem can be solved in this setting when the implementation is required to be deterministic.

1 Introduction

Designing distributed systems has always been a challenging task. Interactions between the processes can introduce subtle errors in the system’s overall behaviour which may pass undetected even after rigorous testing. A fruitful approach in recent years has been to specify the behaviour of the overall system in a global manner and then automatically synthesize a distributed implementation from the specification.

The question of identifying when a sequential specification has an implementation in terms of a desired distributed architecture was first raised in the context of Petri nets. Ehrenfeucht and Rozenberg [ER90] introduced the concept of regions to describe how to associate places of nets with states of a transition system. In [NRT92], Nielsen, Rozenberg and Thiagarajan use regions to characterize the class of transition systems which arise from elementary net systems. Subsequently, several authors have extended this characterization to larger classes of nets (for a sample of the literature, see [BD98,Muk92,WN95]).

Here, we focus on product transition systems—networks of transition systems which coordinate by synchronizing on common actions [Arn94]. This model

⋆ This work has been sponsored by IFCPAR Project 1502-1. This work has also been supported in part by BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Aarhus University, Denmark.

comes with a natural notion of component and induced notions of concurrency and causality. It has a well-understood theory, at least in the linear-time setting [Thi95]. This model is also the basis for system descriptions in a number of model-checking tools [Kur94,Hol97].

We establish two main sets of results in this paper. First, we characterize when an arbitrary transition system is isomorphic to a product transition system with a specified distribution of actions. Our characterization is effective— for finite-state specifications, we can synthesize a finite-state implementation. We then show how to obtain implementations when concurrency is specified in terms of an abstract independence relation, in the sense of Mazurkiewicz trace theory [Maz89]. We also present realizability relationships between product transition systems in terms of a natural preorder over the distribution of actions across agents. Our result subsumes the work of Morin [Mor98] on synthesizing product systems from deterministic specifications.

Our second result deals with the situation when we have global specifications which are behaviourally equivalent to, but not necessarily isomorphic to, product systems. The notion of behavioural equivalence which we use is strong bisimulation [Mil89]. The synthesis problem here is to implement a global transition system T S as a product transition system T̃ S such that T S and T̃ S are bisimilar to each other. We show how to solve this problem when the implementation is deterministic. Notice that the specification itself may be nondeterministic. Since distributed systems implemented in hardware, such as digital controllers, are deterministic, the determinacy assumption is a natural one. Solving the synthesis problem modulo bisimulation in the general case where the implementation may be nondeterministic appears to be hard.

The problem of expressing a global transition system as a product of component transition systems modulo bisimilarity has also been investigated in the context of process algebras in [Mol89,MM93]. In [GM92], Groote and Moller examine the use of decomposition techniques for the verification of parallel systems. These results are established in the context of transition systems which are generated using process algebra expressions. Generalizing these results to arbitrary, unstructured, finite-state systems appears hard.

The paper is organized as follows. In the next section we formally introduce product transition systems and formulate the synthesis problem. In Section 3, we characterize the class of transition systems which are isomorphic to product transition systems. The subsequent section extends these results to the context where the distributed implementation is described using an independence relation. Next, we show that deterministic systems admit canonical minimal implementations. In Section 6, we present our second main result, characterizing the class of transition systems which are bisimilar to deterministic product systems.

2 The synthesis problem for product transition systems

Labelled transition systems provide a general framework for modelling computing systems. A labelled transition system is defined as follows.

Definition 2.1. Let Σ be a finite nonempty set of actions. A labelled transition system over Σ is a structure T S = (Q, →, q_{in}), where Q is a set of states, q_{in} ∈ Q is the initial state and →⊆ Q × Σ × Q is the transition relation.

We abbreviate a transition sequence of the form q_{0} ⟶^{a_{1}} q_{1} ⋯ ⟶^{a_{n}} q_{n} as q_{0} ⟶^{a_{1}···a_{n}} q_{n}. In every transition system T S = (Q, →, q_{in}) which we encounter, we assume that each state in Q is reachable from the initial state—that is, for each q ∈ Q there exists a transition sequence q_{in} = q_{0} ⟶^{a_{1}···a_{n}} q_{n} = q.

A large class of distributed systems can be fruitfully modelled as networks of local transition systems whose moves are globally synchronized through common actions. To formalize this, we begin with the notion of a distributed alphabet.

Definition 2.2. A distributed alphabet over Σ, or a distribution of Σ, is a tuple of nonempty sets Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ such that ⋃_{1≤i≤k} Σ_{i} = Σ. For each action a ∈ Σ, the locations of a are given by the set locΣ̃(a) = {i | a ∈ Σ_{i}}. If Σ̃ is clear from the context, we write just loc(a) to denote locΣ̃(a).

We consider two distributions to be the same if they differ only in the order of their components.

Henceforth, for any natural number k, [1..k] denotes the set {1, 2, …, k}.

Definition 2.3. Let ⟨Σ_{1}, …, Σ_{k}⟩ be a distribution of Σ. For each i ∈ [1..k], let T S_{i} = (Q_{i}, →_{i}, q_{in}^{i}) be a transition system over Σ_{i}. The product (T S_{1} ∥ ⋯ ∥ T S_{k}) is the transition system T S = (Q, →, q_{in}) over Σ = ⋃_{1≤i≤k} Σ_{i}, where:

– q_{in} = (q_{in}^{1}, …, q_{in}^{k}).

– Q ⊆ (Q_{1} × ⋯ × Q_{k}) and →⊆ Q × Σ × Q are defined inductively by:

• q_{in} ∈ Q.

• Let q ∈ Q and a ∈ Σ. For i ∈ [1..k], let q[i] denote the i^{th} component of q. If for each i ∈ loc(a), T S_{i} has a transition q[i] ⟶^{a}_{i} q′_{i}, then q ⟶^{a} q′ and q′ ∈ Q where q′[i] = q′_{i} for i ∈ loc(a) and q′[j] = q[j] for j ∉ loc(a).

We often abbreviate the product (T S_{1} ∥ ⋯ ∥ T S_{k}) by ∥_{i∈[1..k]} T S_{i}.

The synthesis problem

The synthesis problem can now be formulated as follows. If T S = (Q, →, q_{in}) is a transition system over Σ, and Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ is a distribution of Σ, does there exist a Σ̃-implementation of T S—that is, a tuple of transition systems ⟨T S_{1}, …, T S_{k}⟩ such that T S_{i} is a transition system over Σ_{i} and the product ∥_{i∈[1..k]} T S_{i} is isomorphic to T S?

Example 2.4. Let Σ̃ = ⟨{a, c}, {b, c}⟩ be a distribution of {a, b, c}. The first transition system below is Σ̃-implementable—using expressions in the style of process algebra, we can write the product as (a+c) ∥ (bc+c). Similarly, the second transition system may be implemented as (ac + c) ∥ (bc + c).

a b  b a ab  b  cc ab  b a a c  c  c  c  cc

On the other hand, the system on the right is not Σ̃-implementable. Intuitively, the argument is as follows. If it were implementable in two components with alphabets {a, c} and {b, c}, c would be enabled at the initial state in both components. But c can also occur after both actions a and b have occurred. So, c is possible after a in the first component and after b in the second component. Thus, there are two c transitions in both components and the product should exhibit all their combinations, giving rise to the system in the centre. We can formalize this argument once we have proved the results in the next section.

3 A characterization of implementable systems

We now characterize Σ̃-implementable systems. In this section, unless otherwise specified, we assume that Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩, with Σ = ⋃_{i∈[1..k]} Σ_{i}.

The basic idea is to label each state of the given system by a k-tuple of local states (corresponding to a global state of a product system) such that the labelling function satisfies some consistency conditions. We formulate this labelling function in terms of local equivalence relations on the states of the original system—for each i ∈ [1..k], if two states q_{1} and q_{2} of the original system are i-equivalent, the interpretation is that the global states assigned to q_{1} and q_{2} by the labelling function agree on the i^{th} component. Our technique is similar to the one developed independently by Morin for the more restrictive class of deterministic transition system specifications [Mor98].

Theorem 3.1. A transition system T S = (Q, →, q_{in}) is Σ̃-implementable with respect to a distribution Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ if and only if for each i ∈ [1..k] there exists an equivalence relation ≡_{i} ⊆ (Q × Q) such that the following conditions are satisfied:

(i) If q ⟶^{a} q′ and a ∉ Σ_{i}, then q ≡_{i} q′.

(ii) If q ≡_{i} q′ for every i, then q = q′. (iii) Let q ∈ Q and a ∈ Σ. If for each i ∈ loc(a), there exist s_{i}, s′_{i} ∈ Q such that

s_{i} ≡_{i} q, and s_{i} ⟶^{a} s′_{i}, then for each choice of such s_{i}’s and s′_{i}’s there exists

q′ ∈ Q such that q ⟶^{a} q′ and for each i ∈ loc(a), q′ ≡_{i} s′_{i}.

Proof. (⇒) : Suppose ∥_{i∈[1..k]} T S_{i} is a Σ̃-implementation of T S. We must exhibit k equivalence relations {≡_{i}}_{i∈[1..k]}, such that conditions (i)—(iii) are satisfied. Assume, without loss of generality, that T S is not just isomorphic to ∥_{i∈[1..k]} T S_{i} but is in fact equal to ∥_{i∈[1..k]} T S_{i}.

For i ∈ [1..k], let T S_{i} = (Q_{i}, →_{i}, q_{in}^{i}). We then have Q ⊆ (Q_{1} × ⋯ × Q_{k}) and q_{in} = (q_{in}^{1}, …, q_{in}^{k}). Define ≡_{i}⊆ (Q × Q) as follows: q ≡_{i} q′ iff q[i] = q′[i].

Since T S is a product transition system, it is clear that conditions (i) and (ii) are satisfied. To establish condition (iii), fix q ∈ Q and a ∈ Σ. Suppose that for each i ∈ loc(a) there is a transition s_{i} ⟶^{a} s′_{i} such that s_{i} ≡_{i} q. Clearly, for each i ∈ loc(a), s_{i} ⟶^{a} s′_{i} implies s_{i}[i] ⟶^{a}_{i} s′_{i}[i]. Moreover s_{i}[i] = q[i] by the definition of ≡_{i}. Since T S is a product transition system, this implies q ⟶^{a} q′, where q′[i] = s′_{i}[i] for i ∈ loc(a) and q′[i] = q[i] otherwise.

(⇐) : Suppose we are given equivalence relations {≡_{i} ⊆ (Q × Q)}_{i∈[1..k]} which

satisfy conditions (i)—(iii). For each q ∈ Q and i ∈ [1..k], let [q]_{i} =^{def} {s | s ≡_{i} q}. For i ∈ [1..k], define the transition system T S_{i} = (Q_{i}, →_{i}, q_{in}^{i}) over Σ_{i} as follows:

– Q_{i} = {[q]_{i} | q ∈ Q}, with q_{in}^{i} = [q_{in}]_{i}.

– [q]_{i} ⟶^{a}_{i} [q′]_{i} iff a ∈ Σ_{i} and there exists s ⟶^{a} s′ with s ≡_{i} q and s′ ≡_{i} q′.

We wish to show that T S is isomorphic to ∥_{i∈[1..k]} T S_{i}. Let ∥_{i∈[1..k]} T S_{i} = (Q̂, ⇝, q̂_{in}). We claim that the required isomorphism is given by the function f : Q → Q̂, where f(q) = ([q]_{1}, …, [q]_{k}).

– We can show that f is well-defined—that is f(q) ∈ Q̂ for each q—by induction on the length of the shortest path from q_{in} to q. We omit the details.

– We next establish that f is a bijection. Clearly condition (ii) implies that f is injective. To argue that f is onto, let ([s_{1}]_{1}, …, [s_{k}]_{k}) ∈ Q̂ be reachable from q̂_{in} in n steps. We proceed by induction on n.

• Basis: If n = 0, ([s_{1}]_{1}, …, [s_{k}]_{k}) = q̂_{in} = f(q_{in}).

• Induction step:

Let ([r_{1}]_{1}, …, [r_{k}]_{k}) be reachable from q̂_{in} in n−1 steps. Consider a move ([r_{1}]_{1}, …, [r_{k}]_{k}) ⇝^{a} ([s_{1}]_{1}, …, [s_{k}]_{k}). By the induction hypothesis there exists q ∈ Q such that f(q) = ([q]_{1}, …, [q]_{k}) = ([r_{1}]_{1}, …, [r_{k}]_{k}). Now, ([r_{1}]_{1}, …, [r_{k}]_{k}) ⇝^{a} ([s_{1}]_{1}, …, [s_{k}]_{k}) implies that [r_{i}]_{i} ⟶^{a}_{i} [s_{i}]_{i} for each i ∈ loc(a). Hence, for each i ∈ loc(a), there exist r′_{i}, s′_{i} such that r′_{i} ≡_{i} r_{i}, s′_{i} ≡_{i} s_{i} and r′_{i} ⟶^{a} s′_{i}. By condition (iii), since q ≡_{i} r_{i}, for any choice of such r′_{i}’s and s′_{i}’s there exists q′ such that q ⟶^{a} q′ and q′ ≡_{i} s′_{i} for each i ∈ loc(a). We want to show that f(q′) = ([s_{1}]_{1}, …, [s_{k}]_{k}). For i ∈ loc(a) we already know that q′ ≡_{i} s′_{i} ≡_{i} s_{i}. So suppose i ∉ loc(a). In this case q ⟶^{a} q′ implies [q′]_{i} = [q]_{i}, by condition (i). From [q]_{i} = [r_{i}]_{i} and [r_{i}]_{i} = [s_{i}]_{i} it follows that [q′]_{i} = [s_{i}]_{i}.

– It is now easy to argue that f is an isomorphism—we omit the details.

An effective synthesis procedure

Observe that Theorem 3.1 yields an effective synthesis procedure for finitestate specifications which is exponential in the size of the original transition system and the number of components in the distributed alphabet. The number of ways of partitioning a finite-state space using equivalence relations is bounded and we can exhaustively check each choice to see if it meets criteria (i)–(iii) in the statement of the theorem.

4 Synthesis and independence relations

An abstract way of enriching a labelled transition system with information about concurrency is to equip the underlying alphabet with an independence relation— intuitively, this relation specifies which pairs of actions in the system can be executed independent of each other.

Definition 4.1. An independence relation over Σ is a symmetric, irreflexive relation I ⊆ Σ × Σ.

Each distribution Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ induces a natural independence relation IΣ̃ over Σ—two actions are independent if they are performed at nonoverlapping sets of locations across the system. Formally, for a, b ∈ Σ, a IΣ̃ b ⇔ loc(a) ∩ loc(b) = ∅. The following example shows that different distributions may yield the same independence relation.

Example 4.2. If Σ = {a, b, c, d} and I = {(a, b), (b, a)}, then the distributions Σ̃ = ⟨{a, c, d}, {b, c, d}⟩, Σ̃′ = ⟨{a, c, d}, {b, c}, {b, d}⟩ and Σ̃′′ = ⟨{a, c}, {a, d}, {b, c}, {b, d}, {c, d}⟩ all give rise to the independence relation I.

However for each independence relation I there is a standard distribution inducing I, whose components are the maximal cliques of the dependency relation D = (Σ × Σ) − I. In the example above, the standard distribution is the one denoted Σ̃. Henceforth, we will denote the standard distribution for I by Σ̃_{I}.

The synthesis problem with respect to an independence relation

We can phrase the synthesis problem in terms of independence relations as follows. Given a transition system T S = (Q, →, q_{in}) and a nonempty independence relation I over Σ, does there exist an I-implementation of T S, that is a Σ̃-implementation of T S such that Σ̃ induces I?

We show that if a transition system admits a Σ̃-implementation then it also admits a Σ̃_{IΣ̃}-implementation. Thus the synthesis problem with respect to independence relations reduces to the synthesis problem for standard distributions.

We begin by showing that a system that has an implementation over a distribution Σ̃ also has an implementation over any coarser distribution Γ̃, obtained by merging some components of Σ̃ and possibly adding some new ones.

Definition 4.3. Let Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ and Γ̃ = ⟨Γ_{1}, …, Γ_{ℓ}⟩ be distributions of Σ. Then Σ̃ ≲ Γ̃ if for each i ∈ [1..k], there exists j ∈ [1..ℓ] such that Σ_{i} ⊆ Γ_{j}. If Σ̃ ≲ Γ̃ we say that Σ̃ is finer than Γ̃, or Γ̃ is coarser than Σ̃.

We then have the following simple observation.

Proposition 4.4. If Σ̃ ≲ Γ̃ then IΓ̃ ⊆ IΣ̃.

Note that ≲ is not a preorder in general. In fact Σ̃ ≲ Γ̃ means that the maximal elements of Σ̃ are included in those of Γ̃. Let us denote by ≃ the relation ≲ ∩ ≳. Then, Σ̃ ≃ Γ̃ just means that Σ̃ and Γ̃ have the same maximal elements—in general, it does not guarantee that they are identical. However, when restricted to distributions “without redundancies”, ≲ becomes a preorder.

Definition 4.5. A distribution Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ of Σ is said to be simple if for each i, j ∈ [1..k], i ≠ j implies that Σ_{i} ⊈ Σ_{j}.

Proposition 4.6. Let Σ̃ and Γ̃ be simple distributions of Σ. If Σ̃ ≃ Γ̃ then Σ̃ = Γ̃.

For any independence relation I over Σ, the associated standard distribution Σ̃_{I} is a simple distribution, and is the coarsest distribution inducing I. At the other end of the spectrum, we can define the finest distribution inducing I as follows:

Definition 4.7. Let I be an independence relation over Σ, and D = (Σ×Σ)−I. The distribution Δ̃_{I} over Σ is defined by:

Δ̃_{I} = {{x, y} | (x, y) ∈ D, x ≠ y} ∪ {{x} | x I y for each y ≠ x}

Proposition 4.8. Let I be an independence relation over Σ. Then the distribution Δ̃_{I} is the finest simple distribution over Σ that induces I.

A finer distribution can be faithfully implemented by a coarser distribution.

Lemma 4.9. Let Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ and Γ̃ = ⟨Γ_{1}, …, Γ_{ℓ}⟩ be distributions of Σ such that Σ̃ ≲ Γ̃. Then, for each product transition system ∥_{i∈[1..k]} T S_{i} over Σ̃, there exists an isomorphic product transition system ∥_{i∈[1..ℓ]} T̂ S_{i} over Γ̃.

Proof. For each i ∈ [1..k] let f(i) denote the least index j in [1..ℓ] such that Σ_{i} ⊆ Γ_{j}. For each j ∈ [1..ℓ], define T̂ S_{j} = (Q̂_{j}, ⇝_{j}, q̂_{in}^{j}) as follows.

– If j is not in the range of f, then Q̂_{j} = {q̂_{in}^{j}}, and q̂_{in}^{j} ⇝^{a}_{j} q̂_{in}^{j} for each a ∈ Σ_{j}.

– If j is in the range of f, let f^{−1}(j) = {i_{1}, i_{2}, …, i_{m}}. Set T̂ S_{j} = (T S_{i_{1}} ∥ ⋯ ∥ T S_{i_{m}}).

It is then straightforward to verify that ∥_{i∈[1..k]} T S_{i} is isomorphic to ∥_{i∈[1..ℓ]} T̂ S_{i}. We omit the details.

Corollary 4.10. Let T S = (Q, →, q_{in}) be a transition system over Σ, and Σ̃ and Γ̃ be two distributions of Σ such that Σ̃ ≲ Γ̃. If T S is Σ̃-implementable it is also Γ̃-implementable.

Let I be an independence relation over Σ. We have already observed that Σ̃_{I} is the coarsest distribution of Σ whose induced independence relation is I. Coupling this remark with the preceding corollary, we can now settle the synthesis problem with respect to independence relations.

Corollary 4.11. Let T S = (Q, →, q_{in}) be a transition system over Σ, and Σ̃ be a distribution of Σ inducing the independence relation I. Then if T S is Σ̃- implementable it is also Σ̃_{I}-implementable. Moreover T S is I-implementable if and only if it is Σ̃_{I}-implementable.

We remark that the converse of Lemma 4.9 is not true—if Σ̃ ≲ Γ̃, it may be the case that T S is Γ̃-implementable but not Σ̃-implementable. Details can be found in the full paper [CMT99].

5 Canonical implementations and determinacy

A system may have more than one Σ̃-implementation for a fixed distribution Σ̃. For instance, the system

d c  c b  a b a  b  a a  b

has two implementations with respect to the distributed alphabet Σ̃ = ⟨{a, c, d}, {b, c, d}⟩, namely ca + c(a + d) ∥ c(b + d) and c(a + d) ∥ cb + c(b + d).

One question that naturally arises is whether there exists a unique minimal or maximal family of equivalence relations {≡_{1}, …, ≡_{k}} on states that makes Theorem 3.1 go through. We say that a family {≡_{1}, …, ≡_{k}} is minimal (respectively, maximal) if there is no other family {≡′_{1}, …, ≡′_{k}} with respect to which T S is Σ̃-implementable with ≡′_{i} ⊆ ≡_{i} (respectively, ≡_{i} ⊆ ≡′_{i}) for each i ∈ [1..k].

It turns out that for deterministic systems, we can find unique minimal implementations. A transition system T S = (Q, →, q_{in}) is deterministic if q ⟶^{a} q′ and q ⟶^{a} q′′ imply that q′ = q′′.

Theorem 5.1. Suppose T S = (Q, →, q_{in}) is deterministic and Σ̃-implementable. Then there exists a unique minimal family { ≡_{1}, …, ≡_{k}} of equivalence relations on states with respect to which T S is Σ̃-implementable.

Proof. Suppose that {≡_{1}, …, ≡_{k}} and {≡′_{1}, …, ≡′_{k}} are two families which represent Σ̃-implementations of T S. Let {ˆ≡_{1}, …, ˆ≡_{k}} be the intersection family, given by q ˆ≡_{i} q′ ⇔ q ≡_{i} q′ ∧ q ≡′_{i} q′.

By definition, ˆ≡_{i} ⊆ ≡_{i} and ˆ≡_{i} ⊆ ≡′_{i}. Thus, it suffices to show that {ˆ≡_{1}, …, ˆ≡_{k}} represents a Σ̃-implementation of T S. From the definition of the relations {ˆ≡_{1}, …, ˆ≡_{k}}, it is obvious that both conditions (i) and (ii) of Theorem 3.1 are satisfied. Now suppose that q ∈ Q and a ∈ Σ. For every i ∈ loc(a), let s_{i}, s′_{i} ∈ Q be such that s_{i} ˆ≡_{i} q and s_{i} ⟶^{a} s′_{i}. This means that for every i ∈ loc(a), both s_{i} ≡_{i} q and s_{i} ≡′_{i} q. Hence by condition (iii) there exists q′ such that q ⟶^{a} q′ and q′ ≡_{i} s′_{i} for every i ∈ loc(a). Similarly, there exists q′′ such that q ⟶^{a} q′′ and q′′ ≡_{i} s′_{i} for every i ∈ loc(a). Since T S is deterministic, it must be q′ = q′′. Thus, q′ = q′′ is such that q′ ˆ≡_{i} s′_{i} for each i ∈ loc(a).

This result leads us to conjecture that the synthesis problem for deterministic systems is much less expensive computationally than the synthesis problem in the general case, since it suffices to look for the unique minimal family of equivalence relations which describe the implementation.

a  b b  c a  ba b  a

We conclude this section by observing that a deterministic system may have more than one maximal family { ≡_{1}, …, ≡_{k}} for which it is Σ̃-implementable. For instance the system on the left has two distinct maximal implementations with respect to the distribution ⟨{a, c}, {b, c}⟩, namely (fix X. a + cX) ∥ b + cb and a + ca ∥ (fix Y. b + cY), whose components are not even language equivalent.

6 Synthesis modulo bisimulation

In the course of specifying a system, we may accidentally destroy its inherent product structure. This may happen, for example, if we optimize the design and eliminate redundant states. In such situations, we would like to be able to reconstruct a product transition system from the reduced specification. Since the synthesized system will not, in general, be isomorphic to the specification, we need a criterion for ensuring that the two systems are behaviourally equivalent. We use strong bisimulation [Mil89] for this purpose.

In general, synthesizing a behaviourally equivalent product implementation from a reduced specification appears to be a hard problem. In this section, we show how to solve the problem for reduced specifications which can be implemented as deterministic product transition systems—that is, the global transition system generated by the implementation is deterministic. Notice that the specification itself may be nondeterministic. Since many distributed systems implemented in hardware, such as digital controllers, are actually deterministic, our characterization yields a synthesis result for a large class of useful systems.

We begin by recalling the definition of bisimulation.

Definition 6.1. A bisimulation between a pair of transition systems T S_{1} = (Q_{1}, →_{1}, q_{in}^{1}) and T S_{2} = (Q_{2}, →_{2}, q_{in}^{2}) is a relation R ⊆ (Q_{1} × Q_{2}) such that:

– (q_{in}^{1}, q_{in}^{2}) ∈ R.

– If (q_{1}, q_{2}) ∈ R and q_{1} ⟶^{a}_{1} q′_{1}, there exists q′_{2}, q_{2} ⟶^{a}_{2} q′_{2} and (q′_{1}, q′_{2}) ∈ R.

– If (q_{1}, q_{2}) ∈ R and q_{2} ⟶^{a}_{2} q′_{2}, there exists q′_{1}, q_{1} ⟶^{a}_{1} q′_{1} and (q′_{1}, q′_{2}) ∈ R.

The synthesis problem modulo bisimilarity

The synthesis problem modulo bisimilarity can now be formulated as follows. If T S = (Q, →, q_{in}) is a transition system over Σ, and Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ is a distribution of Σ, does there exist a product system ∥_{i∈[1..k]} T S_{i} over Σ̃ such that ∥_{i∈[1..k]} T S_{i} is bisimilar to T S?

To settle this question for deterministic implementations, we need to consider product languages.

Languages Let T S = (Q, →, q_{in}) be a transition system over Σ. The language of T S is the set L(T S) ⊆ Σ^{∗} consisting of the labels along all runs of T S. In other words, L(T S) = {w | q_{in} ⟶^{w} q, q ∈ Q}.

Notice that L(T S) is always prefix-closed and always contains the empty word. Moreover, L(T S) is regular whenever T S is finite. For the rest of this section, we assume all transition systems which we encounter are finite.

Product languages Let L ⊆ Σ^{∗} and let Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ be a distribution of Σ. For w ∈ Σ^{∗}, let w↾_{Σ_{i}} denote the projection of w onto Σ_{i}, obtained by erasing all letters in w which do not belong to Σ_{i}.

The language L is a product language over Σ̃ if for each i ∈ [1..k] there is a language L_{i} ⊆ Σ_{i}^{∗} such that L = {w | w↾_{Σ_{i}} ∈ L_{i}, i ∈ [1..k]}.

For deterministic transition systems, bisimilarity coincides with language equivalence. We next show that we can extend this result to get a simple characterization of transition systems which are bisimilar to deterministic product transition systems. We first recall a basic definition.

Bisimulation quotient Let T S = (Q, →, q_{in}) be a transition system and let ∼_{T S} be the largest bisimulation relation between T S and itself. The relation ∼_{T S} defines an equivalence relation over Q. For q ∈ Q, let [q] denote the ∼_{T S}- equivalence class containing q. The bisimulation quotient of T S is the transition system T S/_{∼_{T S}} = (Q̂, ⇝, [q_{in}]) where

– Q̂ = {[q] | q ∈ Q}.

– [q] ⇝^{a} [q′] if there exist q_{1} ∈ [q] and q′_{1} ∈ [q′] such that q_{1} ⟶^{a} q′_{1}.

The main result of this section is the following.

Theorem 6.2. Let T S be a transition system over Σ and let Σ̃ be a distribution of Σ. The system T S is bisimilar to a deterministic product transition system over Σ̃ iff T S satisfies the following two conditions.

– The bisimulation quotient T S/_{∼_{T S}} is deterministic.

– The language L(T S) is a product language over Σ̃.

To prove this theorem, we first recall the following basic connection between product languages and product systems [Thi95].

Lemma 6.3. L(∥_{i∈[1..i]} T S_{i}) = {w | w↾_{Σ_{i}} ∈ L(T S_{i}), i ∈ [1..k]}.

We also need the useful fact that a product language is always the product of its projections [Thi95].

Lemma 6.4. Let L ⊆ Σ^{∗} and let Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩ be a distribution of Σ. For i ∈ [1..k], let L_{i} = {w ↾_{Σ_{i}} | w ∈ L}. Then, L is a product language iff L = {w | w↾_{Σ_{i}} ∈ L_{i}, i ∈ [1..k]}.

Notice that Lemma 6.4 yields an effective procedure for checking if a finitestate transition system accepts a product language over a distribution ⟨Σ_{1}, …, Σ_{k}⟩. For i ∈ [1..k], construct the finite-state system T S_{i} such that L(T S_{i}) = L↾_{Σ_{i}} and then verify that L(T S) = L(∥_{i∈[1..k]} T S_{i}).

Next, we state without proof some elementary facts about bisimulations.

Lemma 6.5. (i) Let T S be a deterministic transition system. Then, T S/_{∼_{T S}}

is also deterministic. (ii) Let T S_{1} and T S_{2} be deterministic transition systems over Σ. If L(T S_{1}) =

L(T S_{2}) then T S_{1} is bisimilar to T S_{2}. (iii) Let T S_{1} and T S_{2} be bisimilar transition systems. Then T S_{1}/_{∼_{T S_{1}}} and

T S_{2}/_{∼_{T S_{2}}} are isomorphic. Further L(T S_{1}) = L(T S_{2}).

We now prove both parts of Theorem 6.2.

Lemma 6.6. Suppose that a transition system T S is bisimilar to a deterministic product transition system. Then, T S/_{∼_{T S}} is deterministic and L(T S) is a product language.

Proof. Let T̂ S =∥_{i∈[1..i]} T̂ S_{i} be a deterministic product transition system such that T S is bisimilar to T̂ S.

By Lemma 6.5 (iii), L(T S) = L(T̂ S). Since L(T̂ S) is a product language, it follows that L(T S) is a product language.

To check that T S/_{∼_{T S}} is deterministic, we first observe that T̂ S/_{∼T̂ S} is deterministic, by Lemma 6.5 (i). By part (iii) of the same lemma, T S/_{∼_{T S}} must be isomorphic to T̂ S/_{∼T̂ S}. Hence, T S/_{∼_{T S}} is also deterministic.

Lemma 6.7. Let T S be a transition system over Σ and Σ̃ be a distribution of Σ, such that T S/_{∼_{T S}} is deterministic and L(T S) is a product language over Σ̃. Then, T S is bisimilar to a deterministic product transition system over Σ̃.

Proof. Let Σ̃ = ⟨Σ_{1}, …, Σ_{k}⟩. For i ∈ [1..k], let L_{i} = {w↾_{Σ_{i}} | w ∈ L(T S)}. We know that each L_{i} is a regular prefix-closed language which contains the empty word. Thus, we can construct the minimal deterministic finite-state automaton A_{i} = (Q_{i}, →_{i}, q_{in}^{i}, F_{i}) recognizing L_{i}. Since L_{i} contains the empty word, q_{in}^{i} ∈ F_{i}. Consider the restricted transition relation →′_{i}=→_{i} ∩(F_{i} × Σ × F_{i}). It is easy to verify that the transition system T S_{i} = (F_{i}, →′_{i}, q_{in}^{i}) is a deterministic transition system such that L(T S_{i}) = L_{i}.

Consider the product T̂ S =∥_{i∈[1..k]} T S_{i}. Lemma 6.3 tell us that L(T̂ S) = {w | w↾_{Σ_{i}} ∈ L_{i}, i ∈ [1..k]}. From Lemma 6.4, it follows that L(T̂ S) = L(T S).

We claim that T S is bisimilar to T̂ S. Consider the quotient T S/_{∼_{T S}}. Both T S/_{∼_{T S}} and T̂ S are deterministic and L(T S/_{∼_{T S}}) = L(T S) = L(T̂ S). Thus, by Lemma 6.5 (ii), it must be the case that T S/_{∼_{T S}} is bisimilar to T̂ S. By transitivity, T S is also bisimilar to T̂ S.

Using standard automata theory, we can derive the following result from Theorem 6.2.

Corollary 6.8. Given a finite-state transition system T S = (Q, →, q_{in}) and a distributed alphabet Σ̃, we can effectively decide whether T S is bisimilar to a deterministic product system over Σ̃.

The synthesis problem modulo bisimilarity appears to be quite a bit more difficult when the product implementation is permitted to be nondeterministic. We have a characterization of the class of systems which are bisimilar to nondeterministic product systems [CMT99]. Our characterization is phrased in terms of the structure of the execution tree obtained by unfolding the specification. Unfortunately, the execution tree may be infinite, so this characterization is not effective, even if the initial specification is finite-state. The difficulty lies in bounding the number of transitions in the product implementation which can collapse, via the bisimulation, to a single transition in the specification.

References

[Arn94] A. Arnold: Finite transition systems and semantics of communicating sytems, Prentice-Hall (1994).

[BD98] E. Badouel and Ph. Darondeau: Theory of Regions. Lectures on Petri nets I (Basic Models), LNCS 1491 (1998) 529–588.

[CMT99] I. Castellani, M. Mukund and P.S. Thiagarajan: Characterizing decomposable transition systems, Internal Report, Chennai Mathematical Institute (1999).

[ER90] A. Ehrenfeucht and G. Rozenberg: Partial 2-structures; Part II, State spaces of concurrent systems, Acta Inf. 27 (1990) 348–368.

[GM92] J.F. Groote and F. Moller: Verification of Parallel Systems via Decomposition, Proc. CONCUR’92, LNCS 630 (1992) 62–76.

[Hol97] G.J. Holzmann: The model checker SPIN, IEEE Trans. on Software Engineering, 23, 5 (1997) 279–295.

[Kur94] R.P. Kurshan: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press (1994).

[Maz89] A. Mazurkiewicz: Basic notions of trace theory, in: J.W. de Bakker, W.- P. de Roever, G. Rozenberg (eds.), Linear time, branching time and partial order in logics and models for concurrency, LNCS 354 (1989) 285–363.

[Mil89] R. Milner: Communication and Concurrency, Prentice-Hall, London (1989).

[Mol89] F. Moller: Axioms for Concurrency, Ph.D. Thesis, University of Edinburgh (1989).

[MM93] F. Moller and R. Milner: Unique decomposition of processes, Theor. Comput. Sci. 107 (1993) 357–363.

[Mor98] R. Morin: Decompositions of asynchronous systems, Proc. CONCUR’98, LNCS 1466 (1998) 549–564.

[Muk92] M. Mukund: Petri Nets and Step Transition Systems, Int. J. Found. Comput. Sci. 3, 4 (1992) 443–478.

[NRT92] M. Nielsen, G. Rozenberg and P.S. Thiagarajan: Elementary transition systems, Theor. Comput. Sci. 96 (1992) 3–33.

[Thi95] P.S. Thiagarajan: A trace consistent subset of PTL, Proc. CONCUR’95, LNCS 962 (1995) 438-452.

[WN95] G. Winskel and M. Nielsen: Models for concurrency, in S. Abramsky, D. Gabbay and T.S.E. Maibaum, eds, Handbook of Logic in Computer Science, Vol 4, Oxford (1995) 1–148.