Designing Distributed Systems w.r.t. Conformance

The paper relooks at one of the classical problems in distributed computing: Given a labelled transition system (LTS), how to synthesize a distributed labelled transition system (DLTS) such that the global behaviour of the DLTS is equivalent to that of the given LTS. This problem has been addressed for various notions of behavioral equivalences, viz., isomorphism, language equivalence, bisimulation, etc. For all these equivalences it has been found that a DLTS cannot be synthesized for every given LTS. This holds true even if the given LTS is assumed to be acyclic. Here we address the same problem with respect to the relation Conf. This relation is not an equivalence. It is rather a preorder that is used to define the notion of conformance in the context of conformance testing [2]. We show that synthesizing a DLTS with respect to conformance has two big advantages. First, a DLTS can be synthesized for every given acyclic LTS. Secondly, a DLTS thus synthesized can be verified for correctness in a distributed and concurrent manner.