Abstract
The paper presents a notion of preorder with related equivalence between concurrent systems which supports functional abstraction and refinement. Such abstraction and refinement disregard action names (the action alphabet can be changed) while they require to preserve local state transformations. Since Petri Nets explicitly model both states and state transformations, concurrent systems are considered as modelled by Petri nets, precisely by contact-free Elementary Net systems in which some states are observable (S-labelled systems). The proposed preorder, called State transformation (ST) preorder, is defined on the basis of morphisms between the OLST-algebras associated to the compared systems. OLST-algebras describe the state space of S-labelled systems characterizing system behaviour in terms of observable local state transformations. The paper presents the construction of the unique canonical representative of each ST-equivalence class of S-observable systems, a subclass of S-labelled systems, and discusses ST-preorder and equivalence over S-observable systems in the framework of system development.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
8. References
S. Abramsky, Observation Equivalence as a Testing Equivalence, Theor.Comp. Science 53, pp. 225–241, 1987
G. Berthelot, Checking Properties of Nets Using Transformations,LNCS Lecture Notes in Computer Science, 222, pp. 19–40, 1986.
E. Best, R. Devillers, A. Kiehn, L. Pomello, Fully Concurrent Bisimulation, submitted paper 1989.
W. Brauer, W. Reisig, G. Rozenberg (eds.),Petri Nets: Central Models and Their Properties, LNCS Lecture Notes in Computer Sciences 254, 1987.
S.D. Brookes, C.A.R. Hoare, A.W. Roscoe, A Theory of Communicating Sequential Processes, J. ACM 31, N.3, July '84, 1984.
L. Castellano, G. De Michelis, L. Pomello, Concurrency vs Interleaving: an instructive example, EATCS Bull., N. 31, pp. 12–15, 1987.
P. Degano, R. De Nicola, U. Montanari, Observational equivalences for concurrency models, in ‘Formal description of Programming Concepts III’ (M. Virsing ed.), North Holland, 1987.
F. De Cindio, G. De Michelis, C. Simone, GAMERU: a language for the analysis and design of human communication pragmatics, in G. Rozemberg (ed) "Advances in Petri Nets 86'", LNCS Lecture Notes in Computer Sciences, 266, 1987.
F. De Cindio, G. De Michelis, L. Pomello, C. Simone, Exhibited-Behaviour Equivalence and Organizational Abstraction in Concurrent System Design, Proc. 5th International Conference on Distributed Computing, IEEE, Denver, 1985.
F. De Cindio, G. De Michelis, L. Pomello, C. Simone, A State Transformation Equivalence for Concurent Systems: Exhibited Functionality Equivalence, in F.H. Vogt (ed) "CONCURRENCY 88", LNCS Lecture Notes in Computer Sciences, 335, 1988.
R. De Nicola, M. Hennessy, Testing equivalences for processes, TCS 34, 83–134, 1984.
R. van Glabbeek, U. Goltz, Refinement of actions in causality based models, in this volume, 1989.
M. Hennessy, Algebraic Theory of Processes, The MIT Press, 1988.
He Jifeng, Various Refinements and Simulations, in this volume, 1989.
L. Lamport, On Interprocess Communication, Part 1: Basic Formalism, Distributed Computing, Vol. 1, pp. 77–85, 1986.
K. Larsen, An Operational Semantics of Context, in this volume, 1989.
B.J. Meseguer, U. Montanari, Petri Nets are Monoids, SRI-CSL-88-3, january 1988.
R. Milner, A Calculus for Communicating Systems, LNCS Lecture Notes in Computer Sciences, 92, 1980.
D. Park, Concurrency and Automata on Infinite Sequences, Proc. 5th Gl Conference, LNCS Lecture Notes in Computer Sciences, 104, pp. 167–183, 1981.
C.A. Petri, Concepts in Net Theory, Mathematical Foundations of Computer Science: Proc. of Symposium and Summer School, High Tatras, sept. 1973, Math. Inst. of the Slovak Acad. of Sciences, pp.137–146, 1973.
C.A. Petri, Perfect Nets, Invited talk at the X Int. Conf. On Application and Theory of Petri Nets, Bonn, june 1989.
L. Pomello, Some Equivalence Notions for Concurrent Systems: An Overview, in "Advances in Petri Nets 1985" (G. Rozenberg ed.), LNCS Lecture Notes in Computer Sciences, 222, pp. 381–400, 1986.
L. Pomello, C. Simone, A State Transformation Preorder over a class of EN-systems, Proc X Int. Conf. On Application and Theory of Petri Nets, Bonn, pp. 247–271, june 1989.
L. Pomello, C. Simone, Concurrent Systems as Local State Transformation Algebras: the case of Elementary Net Systems, in "Proc. 3rd Italian Conference on Theoretical Computer Science, Mantova, Nov.89, eds. Bertoni, Bohem, Miglioli, World Scientific Publ. Co., 1989.
G. Rozenberg, P.S. Thiagarajan, Petri Nets: basic notions, structure, behaviour, in "Current trends in Concurrency" ed. J.W. de Bakker, W.P. de Rover and G. Rozenberg, LNCS Lecture Notes in Computer Sciences, 224, pp. 585–668, 1986.
P.S. Thiagarajan, Elementary Net Systems, in [Bra87], pp. 26–59, 1987.
R. Valette, Analysis of Petri Nets by Stewise Refinements, J. of Computer and System Science, vol.18-1, 1979.
K. Voss, Interface as a Basic Concept for Systems Specification and Verification, in "Concurrency and Nets" (eds) K. Voss, H.J. Genrich, G. Rozenberg, Springer Verlag, Berlin, pp.585–604, 1987.
G. Winskel, A New Definition of Morphism on Petri Nets, in LNCS Lecture Notes in Computer Sciences, 166, pp.140–150, 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pomello, L. (1990). Refinement of concurrent systems based on local state transformations. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness. REX 1989. Lecture Notes in Computer Science, vol 430. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52559-9_82
Download citation
DOI: https://doi.org/10.1007/3-540-52559-9_82
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52559-2
Online ISBN: 978-3-540-47035-9
eBook Packages: Springer Book Archive