Abstract
The notion of refinement of concurrent and distributed systems is a crucial one in any concurrency model. There are (at least) two distinct notions under the name of refinement, namely refinement of specifications and refinement of machines (automata). It is important to keep these two concepts distinct since their properties, and their mathematical formulation, are, or should be, quite different. A specification describes a whole class of machines and refinement here yields a smaller class of models, whereas a refinement of a machine yields a new, more complex, machine. It is not always clear which of these two notions is under consideration, because sometimes a mixture of the two approaches is appropriate and even because some formalisms allow different interpretations [1], [4], [16].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. Composing specifications. In Stepwise Refinement of Distributed Systems, number 430 in LNCS, pages 1–41, 1987.
K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
I. Czaja, Ft. von Glabbeek, and U. Golz. Interleaving semantics and action refinement with atomic choice. Preprint.
P. Degano, R. Gorrieri, and G. Rosolini. A categorical view of process refinement. In Semantics: Foundations and Applications, number 666 in LNCS.
C. Elgot. Monadic computation and iterative algebraic theories. Studies in Logic and the Foundations of Mathematics, 80:175–230, 1975.
P. Godefroid, D. Pirottin. Refining dependencies improves partial order verification methods. In C. Courcoubetis, editor, CAV 93, number 697 in LNCS, 1993.
A. Heller. An existence theorem for recursion categories. Journal of Symbolic Logic, 55(3):1252–1268, 1990.
W. Janssen, M. Poel, J. Zwiers. Action systems and action refinement in the development of parallel systems. In J.C.M. Baeten, J.F. Groote, editors, CONCUR 91, number 527 in LNCS, 1991.
D.E. Knuth. The Art of Computer Programming. Addison-Wesley, 1973.
W. Khalil and R.F.C. Walters. An imperative language based on distributive categories H. RAIRO Informatique Théorique et Applications.To appear.
W. Khalil, E.G. Wagner, and R.F.C. Walters. Fixed-point semantics for programs in distributive categories. In preparation.
N.A. Lynch. Multivalued possibility mappings. In Stepwise Refinement of Distributed Systems, number 430 in LNCS, pages 519–543, 1987.
R. Milner. An algebraic definition of simulation between programs. In Proc. of the 2nd Joint Conference on Artificial Intelligence, pages 481–489. BCS, 1971.
J. Meseguer and U. Montanari. Petri nets are monoids. Info, and Co., 88:105–155, 1990.
N. Sabadini and R.F.C. Walters. On functions and processors: an automata theoretic approach to concurrency through distributive categories. Mathematics Report 93–97, Sydney University, 1993.
W. Vogler. Modular construction and partial order semantics of Petri nets. Number 625 in LNCS, 1992.
R.F.C. Walters. Categories and Computer Science. Carslaw Publications (1991), Cambridge University Press (1992).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 British Computer Society
About this paper
Cite this paper
Sabadini, N., Vigna, S., Walters, R.F.C. (1994). A notion of refinement for automata. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds) Algebraic Methodology and Software Technology (AMAST’93). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3227-1_34
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3227-1_34
Publisher Name: Springer, London
Print ISBN: 978-3-540-19852-9
Online ISBN: 978-1-4471-3227-1
eBook Packages: Springer Book Archive