On Compositionality of Boundedness and Liveness for Nested Petri Nets

• Autorzy: Dworzański L. W. , Lomazova I.A.
• Języki publikacji: EN

Abstrakty

EN

Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level NP-nets [14]. Boundedness is in EXPSPACE and liveness is in EXPSPACE or worse for plain Petri nets [6]. However, for some restricted classes, e.g. for plain free-choice Petri nets, problems become more amenable to analysis. There is a polynomial time algorithm to check if a free-choice Petri net is live and bounded [4]. In this paper we prove, that for NP-nets boundedness can be checked in a compositional way, and define restrictions, under which liveness is also compositional. These results give a base to establish boundedness and liveness for NP-nets by checking these properties for separate plain components, which can belong to tractable Petri net subclasses, or be small enough for model checking.

Słowa kluczowe

EN

nested Petri nets; liveness

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 120, nr 3/4
• Strony: 275--293
• Opis fizyczny: Bibliogr. 16 poz., wykr.

Twórcy

autor

Dworzański L. W.

autor

Lomazova I.A.

• National Research University Higher School of Economics, Moscow, 101000, Russia,

Bibliografia

• [1] M. A. Bednarczyk, L. Bernardinello, W. Pawlowski, and L. Pomello. Modelling mobility with Petri Hypernets. In Recent Trends in Algebraic Development Techniques, volume 3423 of Lecture Notes in Computer Science, pages 28-44. Springer, 2005.
• [2] L. Bernardinello, E. Monticelli, and L. Pomello. On Preserving Structural and Behavioural Properties by Composing Net Systems on Interfaces. Fundam. Inform. 80(1-3): 31-47, 2007.
• [3] P. Drabik, A. Maggiolo-Schettini, and P. Milazzo. On Conditions for Modular Verification in Systems of Synchronising Components. In Marcin Szczuka, Ludwik Czaja, Andrzej Skowron, and Magdalena Kacprzak, editors, Proceedings of the InternationalWorkshop on Concurrency, Specification, and Programming (CS&P 2011), Pułtusk, Poland, pages 322-333. Białystok University of Technology, 2011.
• [4] J. Desel and J. Esparza. Free Choice Petri Nets. Cambridge University Press, New York, NY, USA, 1995.
• [5] J. Esparza. A Polynomial-Time Algorithm for Checking Consistency of Free-Choice Signal Transition Graphs. Fundam. Inform. 62(2): 197-220, 2004.
• [6] J. Esparza and M. Nielsen. Decidability issues for Petri nets - a survey. Journal of Informatics Processing and Cybernetics, 30(3):143-160, 1994.
• [7] K. Hoffmann, H. Ehrig, and T. Mossakowski. High-level nets with nets and rules as tokens. In Gianfranco Ciardo and Philippe Darondeau, editors, Applications and Theory of Petri Nets, volume 3536 of Lecture Notes in Computer Science, pages 268-288. Springer, 2005.
• [8] K. Jensen and L. M. Kristensen. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, 2009.
• [9] M. Köhler and Berndt Farwer. Object nets for mobility. In Jetty Kleijn and Alexandre Yakovlev, editors, Applications and Theory of Petri Nets, volume 4546 of Lecture Notes in Computer Science, pages 244-262. Springer, 2007.
• [10] M. Köhler-Bussmeier. Hornets: Nets within nets combined with net algebra. In Giuliana Franceschinis and Karsten Wolf, editors, Applications and Theory of Petri Nets, volume 5606 of Lecture Notes in Computer Science, pages 243-262. Springer, 2009.
• [11] M. Köhler-Bussmeier and F. Heitmann. Liveness and Reachability for Elementary Object Systems. In Marcin Szczuka, Ludwik Czaja, Andrzej Skowron, and Magdalena Kacprzak, editors, Proceedings of the International Workshop on Concurrency, Specification, and Programming (CS&P 2011), Pułtusk, Poland, pages 322-333. Białystok University of Technology, 2011.
• [12] M. Köhler-Bussmeier and F. Heitmann. Liveness of Safe Object Nets. Fundam. Inform. 112(1):73-97, 2011.
• [13] I. A. Lomazova. Nested Petri nets - a Formalism for Specification and Verification of Multi-Agent Distributed Systems. Fundam. Inform., 43(1-4):195-214, 2000.
• [14] I.A. Lomazova. Nested Petri nets for adaptive process modeling. Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800 of Lecture Notes in Computer Science, pages 413-426. Springer, 2008.
• [15] T. Murata. Petri Nets: Properties, Analysis and Applications, an invited survey paper. Proceedings of the IEEE, Vol.77, No.4 pp.541-580, April, 1989.
• [16] R. Valk. Object Petri nets: Using the nets-within-nets paradigm. Lectures on Concurrency and Petri Nets, volume volume 3098 of Lecture Notes in Computer Science, pages 819-848. Springer, 2004