Studying the Behaviour of Petri Nets through a Formalization as Term Rewriting Systems

  • Alberto Paccanaro


Some elementary concepts on Equational Theories and Rewriting Systems are introduced, followed by a brief review on the main ideas of the Knuth-Bendix completion procedure. Then a formalization of Petri Nets as Term Rewriting Systems is proposed, which allows the use of rewriting techniques for studying the behaviour of general deterministic Petri Nets. Particularly the simplification of Term Rewriting Systems obtained formalizing Petri Nets proves to be a powerful method to obtain an efficient system for detecting deadlock situations.

Experiments have been carried out using KBLab, an Automated Theorem Prover for equational theories based on the Knuth-Bendix algorithm.


Word Problem Theorem Prove Function Symbol Equational Theory Critical Pair 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. L. Bachmair, N. Dershowitz, J. Hsiang, 1986, Orderings for equational proofs, in Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, Cambridge, MA, pp. 346-357.Google Scholar
  2. B. Buchberger, R. Loos, 1983, Algebraic simplification, in Computer Algebra: Symbolic and Algebraic Computation, Springer Verlag, Wien.Google Scholar
  3. N. Dershowitz, 1982, Orderings for term rewriting systems, J. of Theoretical Computer Science 17, pp. 279–301.MathSciNetzbMATHCrossRefGoogle Scholar
  4. N. Dershowitz, 1989, Completion and its applications, in Resolution of Equations in Algebraic Structures, pp. 31-48.Google Scholar
  5. J. Hsiang, M. Rusinovitch, 1987, On word problems in equational theories, Proceedings 14th Int. Conf. on Automata Languages and Programming, Karlsrhue.Google Scholar
  6. J.M. Hullot, 1980, A catalogue of canonical term rewriting systems, Rept. CSL-113, SRI International, Menlo Park, CA.Google Scholar
  7. D.E. Knuth, P. Bendix, 1970, Simple word problems in universal algebras”, Proceedings of the Conf. on Computational Problems in Abstract Algebras, Pergamon Press, pp. 263-298.Google Scholar
  8. A. Paccanaro, 1991, KBLAb 1.7: user manual, Technical Report, Department of Computer Science, University of Milan.Google Scholar
  9. J.L. Peterson, 1981, Petri Net Theory and the Modeling of Systems, Prentice Hall, Englewood Cliffs, N.J.Google Scholar
  10. W. Reising, 1985, Petri Nets: An Introduction, Springer-Verlag, Berlin-New YorkGoogle Scholar

Copyright information

© Springer Science+Business Media New York 1994

Authors and Affiliations

  • Alberto Paccanaro
    • 2
    • 1
  1. 1.Laboratorio de Electrónica DigitalUniversidad Católica “Nuestra Señora de la Asunción”AsunciónParaguay
  2. 2.Dipartimento di Scienze dell’InformazioneUniversità degli Studi di MilanoMilanoItaly

Personalised recommendations