Abstract
The first part of this paper gives an algebraic semantics for Place/Transition nets in terms of an algebra which is based on the process algebra ACP. The algebraic semantics is such that a P/T net and its term representation have the same operational behavior. As opposed to other approaches in the literature, the actions in the algebra do not correspond to the firing of a transition, but to the consumption or production of tokens. Equality of P/T nets can be determined in a purely equational way.
The second part of this paper extends the results to hierarchical P/T nets. It gives a compositional algebraic semantics for both their complete operational behavior and their high-level, observable behavior. By means of a non-trivial example, the Alternating-Bit Protocol, it is shown that the notions of abstraction and verification in the process algebra ACP can be used to verify in an equational way whether a hierarchical P/T net satisfies some algebraic specification of its observable behavior. Thus, the theory in this paper can be used to determine whether two hierarchical P/T nets have the same observable behavior. As an example, it is shown that the Alternating-Bit Protocol behaves as a simple one-place buffer. The theory forms a basis for a modular, top-down design methodology based on Petri nets.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
ASPT Foundation, Eindhoven University of Technology. ExSpect 4.2 User Manual, 1994.
J.C.M. Baeten and J.A. Bergstra. Non Interleaving Process Algebra. In proc. CONCUR '93, LNCS 715, pages 308–323. Springer-Verlag, 1993.
J.C.M. Baeten and C. Verhoef. A Congruence Theorem for Structured Operational Semantics with Predicates. In proc. CONCUR '93, LNCS 715, pages 477–492. Springer-Verlag, 1993.
J.C.M. Baeten and W.P. Weijland. Process Algebra, Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.
T. Basten and M. Voorhoeve. An Algebraic Semantics for Hierarchical P/T Nets. Computing Science Report, Eindhoven University of Technology, 1995. To appear.
J.A. Bergstra, I. Bethke, and A. Ponse. Process Algebra with Iteration and Nesting. The Computer Journal, 37(4):241–258, 1994.
J.A. Bergstra and J.W. Klop. The Algebra of Recursively Defined Processes and the Algebra of Regular Processes. In proc. ICALP '84, LNCS 172, pages 82–95. Springer-Verlag, 1984.
E. Best, R. Devillers, and J.G. Hall. The Box Calculus: A New Causal Algebra with Multilabel Communication. In APN '92, LNCS 609, pages 21–69. Springer-Verlag, 1992.
G. Boudol, G. Roucairol, and R. de Simone. Petri Nets and Algebraic Calculi of Processes. In APN '85, LNCS 222, pages 41–58. Springer-Verlag, 1985.
W. Brauer, R. Gold, and W. Vogler. A Survey of Behaviour and Equivalence Preserving Refinements of Petri Nets. In APN '90, LNCS 483, pages 1–46. Springer-Verlag, 1990.
P. Degano, R. De Nicola, and U. Montanari. A Distributed Operational Semantics for CCS Based on Condition/Event Systems. Acta Informatica, 26(1/2):59–91, October 1988.
C. Dietz and G. Schreibert. A Term Representation of P/T Systems. In proc. ATPN '94, LNCS 815, pages 239–257. Springer-Verlag, 1994.
R. van Glabbeek. Comparative Concurrency Semantics and Refinements of Actions. PhD thesis, Free University, Amsterdam, The Netherlands, 1990.
R. van Glabbeek. What is Branching Time Semantics and Why to Use It? In Bulletin of the EATCS 53, pages 191–198. June 1994.
R.J. van Glabbeek and F.W. Vaandrager. Petri Net Models for Algebraic Theories of Concurrency. In proc. PARLE '87, vol. II, LNCS 259, pages 224–242. Springer-Verlag, 1987.
U. Goltz. On Representing CCS Programs by Finite Petri Nets. In proc. MFCS '88, LNCS 324, pages 339–350. Springer-Verlag, 1988.
K.M. van Hee. Information Systems Engineering: A Formal Approach. Cambridge University Press, 1994.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
K. Jensen. Coloured Petri Nets. Basic Consepts, Analysis Methods and Practical Use, EATCS monographs on Theoretical Computer Science 28. Springer-Verlag, 1992.
S.C. Kleene. Representation of Events in Nerve Nets and Finite Automata. In Automata Studies, Annals of Mathematics Studies 34, pages 3–41. Princeton University Press, 1956.
S. Mauw and G.J. Veltink, editors. Algebraic Specification of Communication Protocols, Cambridge Tracts in Theoretical Computer Science 36. Cambridge University Press, 1993.
Meta Software Corporation, Cambridge, Massachusetts, USA. Design/CPN Manual, 1991.
R. Milner. A Calculus of Communcating Systems, LNCS 92. Springer-Verlag, 1980.
U. Montanari and D. Yankelevich. Combining CCS and Petri Nets via Structural Axioms. Fundamenta Informaticae, 20(1–3):193–229, May 1994.
E.-R. Olderog. Petri Nets and Algebraic Calculi of Processes. In APN '87, LNCS 266, pages 196–223. Springer-Verlag, 1987.
L. Pomello, G. Rozenberg, and C. Simone. A Survey of Equivalence Notions for Net Based Systems. In APN '92, LNCS 609, pages 410–472. Springer-Verlag, 1992.
W. Reisig. Petri Nets: An Introduction, EATCS monographs on Theoretical Computer Science 4. Springer-Verlag, 1985.
D. Taubner. Finite Representations of CCS and TCSP Programs by Automata and Petri Nets, LNCS 369. Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basten, T., Voorhoeve, M. (1995). An algebraic semantics for hierarchical P/T nets. In: De Michelis, G., Diaz, M. (eds) Application and Theory of Petri Nets 1995. ICATPN 1995. Lecture Notes in Computer Science, vol 935. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60029-9_33
Download citation
DOI: https://doi.org/10.1007/3-540-60029-9_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60029-9
Online ISBN: 978-3-540-49408-9
eBook Packages: Springer Book Archive