Revisiting the Algebra of Petri Net Processes under the Collective Token Philosophy

• Autorzy: Coja-Oghlan A. , Stehr M-O.
• Języki publikacji: EN

Abstrakty

EN

Revisiting the view of ``Petri nets as monoids'' suggested by Meseguer and Montanari, we give a direct proof of the well-known result that the class of Best/Devillers processes, which represents the behavior of Petri nets under the collective token semantics, has a sound and complete axiomatization in terms of symmetric monoidal categories. Using membership equational logic for the axiomatization, we prove the result by an explicit construction of a natural isomorphism between suitable functors. Our interest in the collective token semantics is motivated by earlier work on the use of rewriting logic as a uniform framework for different Petri net classes, especially including high-level Petri nets, where individuality of tokens can be already expressed at the system level.

Słowa kluczowe

EN

place/transition Petri net; Best/Devillers processes; collective token philosophy; member ship equational logic; rewriting logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 54, nr 2,3
• Strony: 151--164
• Opis fizyczny: bibliogr. 30 poz.

Twórcy

autor

Coja-Oghlan A.

autor

Stehr M-O.

• Humboldt-Universität zu Berlin, Institut für Informatik, Unter den Linden 6, D-10099 Berlin,

Bibliografia

• [1] Barr, M., Wells, C.: Category Theory for Computing Science, International Series in Computer Science, Prentice Hall, 1990.
• [2] Best, E., Devillers, R.: Sequential and Concurrent Behaviour in Petri Net Theory, Theoretical Computer Science, 55, 1987, 87-136.
• [3] Best, E., Fern´andez, C.: Nonsequential Processes - A Petri Net View, vol. 13 of EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1988.
• [4] Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and Proof in Membership Equational Logic, Theoretical Computer Science, 236, 2000, 35-132.
• [5] Bruni, R., Meseguer, J., Montanari, U., Sassone, V.: A Comparison of Petri Net Semantics under the Collective Token Philosophy, Proceedings of ASIAN’98, 4th Asian Computing Science Conference (J. Hsiang, A. Ohori, Eds.), 1538, Springer-Verlag, 1998.
• [6] Bruni, R., Meseguer, J., Montanari, U., Sassone, V.: Functorial semantics for Petri nets under the individual token philosophy, CTCS’99, Conference on Category Theory and Computer Science Edinburgh, UK, 10-12 September 1999, Proceedings, 29, Elsevier, 1999.
• [7] Bruni, R., Meseguer, J., Montanari, U., Sassone, V.: Functorial Semantics for Petri Nets, Information and Computation, 170(2), 2001, 207-236.
• [8] Bruni, R., Sassone, V.: Algebraic Models for Contextual Nets, Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings (U. Montanari, J. D. P. Rolim, E. Welzl, Eds.), 1853, Springer-Verlag, 2000.
• [9] Clavel, M., Dur´an, F., Eker, S., Lincoln, P., Mart´ı-Oliet, N., Meseguer, J., Quesada, J.: Maude: Specification and Programming in Rewriting Logic, SRI International, January 1999.
• [10] Coja-Oghlan, A.: Der Zusammenhang zwischen P/T-Netzen und Termersetzungslogik in kategorientheoretischer Darstellung, Fachbereichsbericht FBI-HH-B-236/02, University of Hamburg, Germany, February 2002, Studienarbeit am Arbeitsbereich Theoretische Grundlagen.
• [11] Degano, P., Meseguer, J., Montanari, U.: Axiomizing the algebra of net computations and processes, Acta Informatica, 33, 1996, 641-667.
• [12] Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL Model Checker, 2002, Submitted for publication.
• [13] Genrich, H. J., Lautenbach, K., Thiagarajan, P. S.: Elements of General Net Theory., Net Theory and Applications, Proc. of the Advanced Course on General Net Theory of Processes and Systems, Hamburg, 1979 (W. Brauer, Ed.), 84, Springer-Verlag, 1980.
• [14] van Glabbeek, R. J., Plotkin, G.: Configuration Structures, Tenth Annual Symposium on Logic in Computer Science, San Diego, California, 26-29 June 1995, Proceedings (D. Kozen, Ed.), IEEE, 1995.
• [15] Goltz, U., Reisig, W.: The nonsequential behaviour of Petri nets, Information and Control, 57(2–3), 1983, 125-147.
• [16] Jensen, K.: Coloured Petri Nets and the Invariant-Method, Theoretical Computer Science, 1981, 317-336.
• [17] Kummer, O., Stehr, M. O.: Petri’s axioms of concurrency – A selection of recent results, Proceedings of the 18th International Conference on Applications and Theory of Petri Nets, 1248, Springer, 1997.
• [18] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, 96, 1992, 73-155.
• [19] Meseguer, J.: Membership algebra as a logical framework for equational specification, Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 3–7, 1997, Selected Papers (F. Parisi-Presicce, Ed.), 1376, Springer-Verlag, 1998.
• [20] Meseguer, J., Montanari, U.: Petri Nets are Monoids, Information and Computation, 88(2), October 1990, 105-155.
• [21] Meseguer, J., Montanari, U., Sassone, V.: On the semantics of Petri nets, CONCUR ’92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992. Proceedings (R. Cleaveland, Ed.), 630, Springer-Verlag, 1992.
• [22] Meseguer, J., Montanari, U., Sassone, V.: Representation Theorems for Petri nets, Foundations of Computer Science: Potential – Theory – Cognition (C. Freska, M. Jantzen, R. Valk, Eds.), 1337, Springer-Verlag, 1997.
• [23] Petri, C. A.: Nicht-sequentielle Prozesse, ISF-Bericht ISF-76-6, Gesellschaft f¨ur Mathematik und Datenverarbeitung, St. Augustin, June 1977, 3. revidierte und erg¨anzte Auflage.
• [24] Petri, C. A.: Concurrency Theory., Advances in Petri Nets 1986 (W. Brauer, W. Reisig, G. Rozenberg, Eds.), 254, Springer-Verlag, 1987.
• [25] Petri, C. A.: Nets, Time and Space, Theoretical Computer Science, 153(1–2), 1996, 3-48.
• [26] Reisig, W.: Petri Nets and Algebraic Specifications, Theoretical Computer Science, 80, 1991, 1-34.
• [27] Stehr, M.-O.: Programming, Specification, and Interactive Theorem Proving — Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory, Doctoral Thesis, Universit¨at Hamburg, Fachbereich Informatik, Germany, 2002, .
• [28] Stehr, M.-O.: A Rewriting Semantics for Algebraic Nets, in: Petri Nets for System Engineering – A Guide to Modeling, Verification, and Applications (C. Girault, R. Valk, Eds.), Springer-Verlag, 2002, To appear.
• [29] Stehr, M.-O., Meseguer, J., ¨Olveczky, P. C.: Representation and Execution of Petri Nets Using Rewriting Logic as a Uniform Framework, UNIGRA’2001, Uniform Approaches to Graphical Process Specification Techniques, Genova, Italy, March 31st and April 1st, 2001, Proceedings (H. Ehrig, C. Ermel, J. Padberg, Eds.), 44, 2001.
• [30] Stehr, M.-O., Meseguer, J., ¨Olveczky, P. C.: Rewriting Logic as a Unifying Framework for Petri Nets, Unifying Petri Nets, Advances in Petri Nets (H. Ehrig, G. Juhas, J. Padberg, G. Rozenberg, Eds.), 2128, Springer-Verlag, 2001.