From Global Specifications to Distributed Implementations
Given a global transition system TS over a set of actions Σ together with a distribution of Σ into local components 〈Σ1, ... , Σ k 〉, does there exist a distributed transition system over 〈Σ1, ... , Σ k 〉 that is “equivalent” to TS?
We focus on two different types of distributed transition systems—loosely cooperating systems and synchronously communicating systems. For “equivalence” we consider three possibilities—state-space isomorphism, language equivalence and bisimulation.
We survey the current state of knowledge about the different versions of the problem that arise from choosing a concrete notion of equivalence and a specific model of distributed transition systems.
KeywordsTransition System Synthesis Problem Label Transition System Product Language Discrete Event System
Unable to display preview. Download preview PDF.
- A. Arnold: Finite transition systems and semantics of communicating systems, Prentice-Hall (1994).Google Scholar
- E. Badouel and Ph. Darondeau: Theory of Regions. Lectures on Petri nets I (Basic Models), LNCS 1491 (1998) 529–588.Google Scholar
- A. Ehrenfeucht and G. Rozenberg: Partial 2-structures; Part II, State spaces of concurrent systems, Acta Inf. 27 (1990) 348–368.Google Scholar
- G.J. Holzmann: The model checker SPIN, IEEE Trans. on Software Engineering, 23, 5 (1997) 279–295.Google Scholar
- R.P. Kurshan: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press (1994).Google Scholar
- 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.Google Scholar
- M. Mukund: Petri Nets and Step Transition Systems, Int. J. Found. Comput. Sci. 3, 4 (1992) 443–478.Google Scholar
- [ 13]
- M. Mukund, M. Sohoni: Gossiping, asynchronous automata and Zielonka’s theorem, Report TCS-94–2,Chennai Mathematical Institute (1994). Available via http://www.cmi.ac.in/techreps
- [ 16]P.S. Thiagarajan: A trace consistent subset of PTL, Proc. CONCUR’95, LNCS 962 (1995) 438–452.Google Scholar
- 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.Google Scholar
- W. Zielonka: Notes on finite asynchronous automata, R.A.LR.O.—Inform. Théor. Appl.,21(1987)99–135.Google Scholar