Behavioural Equivalences of Petri Nets with Invisible Transitions
Abstract
We investigate behavioural equivalences of concurrent systems modeled by Petri nets with invisible transitions labeled by silent actions. τ-equivalences are the relations which abstract from silent actions corresponding to internal activity of the modeled system. The basic τ-equivalences known from the literature are supplemented by new notions. The interrelations of all the equivalences are determined on the whole class of Petri nets as well as on two subclasses: Petri nets with visible transitions, where no transitions are labeled by the invisible action, and sequential Petri nets, where no concurrent transition firings exist. We present an example of equivalence-preserving reduction of a Petri net that models the well-known dining philosophers system. The decidability results for basic τ-equivalences are outlined.
References
1. Autant C., Schnoebelen Ph. Place bisimulations in Petri nets // Lecture Notes in Computer Science. June 1992. Vol. 616. 45-61.
2. Autant C. Petri nets for the semantics and the implementation of parallel processes // Ph. D. thesis. Institut National Polytechnique de Grenoble, France. May 1993 (in French).
3. Best E., Devillers R. Sequential and concurrent behaviour in Petri net theory // Theoretical Computer Science. 1987. Vol. 55. 87-136.
4. Best E., Devillers R., Kiehn A., Pomello L. Concurrent bisimulations in Petri nets // Acta Informatica. 1991. Vol. 28. № 3. 231-264.
5. Devillers R. Maximality preservation and the ST-idea for action refinements // Lecture Notes in Computer Science. 1992. Vol. 609. 108-151.
6. Engelfriet J. Branching processes of Petri nets // Acta Informatica. 1991. Vol. 28. № 6. 575-591.
7. van Glabbeek R.J. The linear time - branching time spectrum II: the semantics of sequential systems with silent moves. Extended abstract // Lecture Notes in Computer Science. 1993. Vol. 715. 66-81.
8. van Glabbeek R.J., Weijland W.P. Branching time and abstraction in bisimulation semantics (extended abstract) // Proceedings of 11th World Computer Congress on Information Processing - 89. San Francisco, USA. North-Holland. August 1989. 613-618.
9. Jancar P. High decidability of weak bisimularity for Petri nets // Lecture Notes in Computer Science. 1995. Vol. 915. 349-363.
10. Jategaonkar L., Meyer A.R. Deciding true concurrency equivalences on safe, finite nets // Theoretical Computer Science. 1996. Vol. 154. 107-143.
11. Mayr R. Undecidability of weak bisimulation equivalence for 1-counter processes // Lecture Notes in Computer Science. 2003. Vol. 2719. 570-583.
12. Milner R.A.J. A calculus of communicating systems // Lecture Notes in Computer Science. 1980. Vol. 92. 172-180.
13. Nielsen M., Plotkin G.,Winskel G. Petri nets, event structures and domains // Theoretical Computer Science. 1981. Vol. 13. 85-108.
14. Peterson J.L. Petri net theory and modeling of systems // Prentice-Hall. 1981.
15. Petri C.A. Kommunikation mit Automaten // Ph. D. thesis. Universitat Bonn, Schriften des Instituts fur Instrumentelle Mathematik, Germany. 1962 (in German).
16. Pinchinat S. Bisimulations for the semantics of reactive systems // Ph. D. thesis. Institut National Politechnique de Grenoble, France. January 1993 (in French).
17. Pomello L. Some equivalence notions for concurrent systems. An overview // Lecture Notes in Computer Science. 1986. Vol. 222. 381-400.
18. Pratt V.R. On the composition of processes // Proceedings of 9th POPL. 1982. 213-223.
19. Pomello L., Rozenberg G., Simone C. A survey of equivalence notions for net based systems // Lecture Notes in Computer Science. 1992. Vol. 609. 410-472.
20. Tarasyuk I.V. ?-equivalences and refinement // Proceedings of IRW/FMP'98, Work-in-Progress Papers, Canberra, Australia. Joint Computer Science Technical Report Series. The Australian National University. September 1998. № TR-CS-98-09. 110-128.
21. Tarasyuk I.V. Place bisimulation equivalences for design of concurrent and sequential systems // Proceedings of MFCS'98 Workshop on Concurrency, Brno, Czech Republic. Electronic Notes in Theoretical Computer Science. 1998. Vol. 18. 191-206.
22. Tarasyuk I.V. ?-equivalences and refinement for Petri nets based design // Technische Berichte. Fakult?at Informatik, Technische Universit?at Dresden, Germany. November 2000. № TUD-FI00-11. 41 p.
23. Vogler W. Bisimulation and action refinement // Lecture Notes in Computer Science. 1991. Vol. 480. 309-321.
24. Vogler W. Partial words versus processes: a short comparison // Lecture Notes in Computer Science. 1992. Vol. 609. 292-303.
Review
For citations:
Tarasyuk I.V. Behavioural Equivalences of Petri Nets with Invisible Transitions. The Herald of the Siberian State University of Telecommunications and Information Science. 2012;(3):105-135. (In Russ.)
Views:
164
Email this article 
