ω-Petri Nets : Algorithms and Complexity

• Autorzy: Geeraerts G. , Heußner A. , Praveen M. , Raskin J.-F.

Identyfikatory

DOI

10.3233/FI-2015-1169

• Języki publikacji: EN

Abstrakty

EN

We introduce ω-Petri nets (ωPN), an extension of plain Petri nets with ω-labeled input and output arcs, that is well-suited to analyse parametric concurrent systems with dynamic thread creation. Most techniques (such as the Karp and Miller tree or the Rackoff technique) that have been proposed in the setting of plain Petri nets do not apply directly to ωPN because ωPN define transition systems that have infinite branching. This motivates a thorough analysis of the computational aspects of ωPN. We show that an ωPN can be turned into a plain Petri net that allows us to recover the reachability set of the ωPN, but that does not preserve termination (an ωPN terminates iff it admits no infinitely long execution). This yields complexity bounds for the reachability, boundedness, place boundedness and coverability problems on ωPN. We provide a practical algorithm to compute a coverability set of the ωPN and to decide termination by adapting the classical Karp and Miller tree construction. We also adapt the Rackoff technique to ωPN, to obtain the exact complexity of the termination problem. Finally, we consider the extension of ωPN with reset and transfer arcs, and show how this extension impacts the decidability and complexity of the aforementioned problems.

Słowa kluczowe

EN

Petri nets; algorithms; parameter estimation; problem solving; data analysis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 137, nr 1
• Strony: 29--60
• Opis fizyczny: Bibliogr. 29 poz., rys., tab.

Twórcy

autor

Geeraerts G.

• Université libre de Bruxelles Département d’informatique, Bruxelles, Belgium

autor

Heußner A.

• Otto-Friedrich-Universit¨at Bamberg Bamberg, Germany

autor

Praveen M.

• Laboratoire Bordelais de Recherche en Informatique (LaBRI), France

autor

Raskin J.-F.

• Université libre de Bruxelles Département d’informatique, Bruxelles, Belgium

Bibliografia

• [1] P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General Decidability Theorems for Infinite-state Systems. In Proceedings of LICS’96, pages 313–321. IEEE Computer Society Press, 1996.
• [2] M. Blondin, A. Finkel, and P. McKenzie. Handling infinitely branching WSTS. In Proceedings of ICALP’14 – Part II, LNCS. Springer, 2014. To appear.
• [3] I. Borosh and L. Treybig. Bounds on positive integral solutions of linear diophantine equations. Proceedings of the American Mathematical Society, 55(2):299–304, March 1976.
• [4] T. Brázdil, P. Jančar, and A. Kučera. Reachability games on extended vector addition systems with states. In Proceedings of ICALP’10, volume 6199 of LNCS, pages 478–489. Springer, 2010.
• [5] G. Delzanno. Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design, 23(3):257–301, 2003.
• [6] G. Delzanno, J-F. Raskin, and L. Van Begin. Towards the Automated Verification of Multithreaded Java Programs. In Proceedings of TACAS’02, volume 2280 of LNCS, pages 173–187. Springer, 2002.
• [7] C. Dufourd. R´eseaux de Petri avec reset/transfert : D´ecidabilit´e et ind´ecidabilit´e. PhD thesis, ENS de Cachan, 1998.
• [8] C. Dufourd, A. Finkel, and Ph. Schnoebelen. Reset Nets Between Decidability and Undecidability. In Proceedings of ICALP’98, volume 1443 of LNCS, pages 103–115. Springer, 1998.
• [9] C. Dufourd, P. Jančar, and Ph. Schnoebelen. Boundedness of reset p/t nets. In Proceedings of ICALP’99, volume 1644 of LNCS, pages 301–310. Springer, 1999.
• [10] J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proceedings of LICS’99, pages 352–359. IEEE, 1999.
• [11] A. Finkel, P. McKenzie, and C. Picaronny. A well-structured framework for analysing petri net extensions. Inf. Comput., 195(1-2):1–29, November 2004.
• [12] A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63–92, 2001.
• [13] Pierre Ganty. mist2 home page. https://github.com/pierreganty/mist.
• [14] G. Geeraerts, A. Heußner, and J.F. Raskin. Queue-dispatch asynchronous systems. In Proceedings of ACSD 2013, pages 150–159. IEEE, 2013.
• [15] G. Geeraerts, J.-F. Raskin, and L. Van Begin. Well-Structured Languages. Acta Informatica, 44(3–4):249–288, 1997.
• [16] G. Geeraerts, J.-F. Raskin, and L. Van Begin. Expand, enlarge and check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci., 72(1):180–203, 2006.
• [17] G. Geeraerts, J.-F. Raskin, and L. Van Begin. On the efficient computation of the minimal coverability set of Petri nets. Int. J. Found. Comput. Sci., 21(2):135–165, 2010.
• [18] S. German and P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675–735, 1992.
• [19] P. Jančar. Decidability of weak fairness in Petri nets. In Proceedings of STACS’89, volume 349 of LNCS, pages 446–457. Springer, 1989.
• [20] R. M. Karp and R. E. Miller. Parallel Program Schemata. J. Comput.r and Syst. Sci., 3:147–195, 1969.
• [21] R. Lipton. The reachability problem requires exponential space. Technical Report 63, Yale, 1976.
• [22] E.W. Mayr. An algorithm for the general Petri net reachability problem. SIAM Journal of Computing, 3(13):441–460, 1984.
• [23] C. A. Petri. Kommunikation mit automaten. PhD thesis, Institut fur Instrumentelle Mathematik, Bonn, 1962.
• [24] C. Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6:223–231, 1978.
• [25] W. Reisig. Petri Nets: An Introduction. Springer-Verlag, 1985.
• [26] P.-A. Reynier and F. Servais. Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning. In Proceedings of Petri Nets 2011, volume 6709 of LNCS, pages 69–88. Springer, 2011.
• [27] P. Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In Proceedings of MFCS’10, volume 6281 of LNCS, pages 616–628. Springer, 2010.
• [28] R. Valk and M. Jantzen. The residue of vector sets with applications to decidability problems in Petri nets. Acta Informatica, 21(6):643–674, 1985.
• [29] A. Valmari and H. Hansen. Old and new algorithms for minimal coverability sets. Fundam. Inform., 131(1):1–25, 2014.