Studying the Behaviour of Petri Nets through a Formalization as Term Rewriting Systems
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.
KeywordsWord Problem Theorem Prove Function Symbol Equational Theory Critical Pair
Unable to display preview. Download preview PDF.
- 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
- B. Buchberger, R. Loos, 1983, Algebraic simplification, in Computer Algebra: Symbolic and Algebraic Computation, Springer Verlag, Wien.Google Scholar
- N. Dershowitz, 1989, Completion and its applications, in Resolution of Equations in Algebraic Structures, pp. 31-48.Google Scholar
- J. Hsiang, M. Rusinovitch, 1987, On word problems in equational theories, Proceedings 14th Int. Conf. on Automata Languages and Programming, Karlsrhue.Google Scholar
- J.M. Hullot, 1980, A catalogue of canonical term rewriting systems, Rept. CSL-113, SRI International, Menlo Park, CA.Google Scholar
- 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
- A. Paccanaro, 1991, KBLAb 1.7: user manual, Technical Report, Department of Computer Science, University of Milan.Google Scholar
- J.L. Peterson, 1981, Petri Net Theory and the Modeling of Systems, Prentice Hall, Englewood Cliffs, N.J.Google Scholar
- W. Reising, 1985, Petri Nets: An Introduction, Springer-Verlag, Berlin-New YorkGoogle Scholar