Characterizing Stable and Deriving Valid Inequalities of Petri Nets

• Autorzy: Triebel M. , Sürmeli J.

Identyfikatory

DOI

10.3233/FI-2016-1374

• Konferencja: International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (Petri Nets 2015), (36; 21–26.06.2015; Brussels, Belgium)
• Języki publikacji: EN

Abstrakty

EN

One way to express correctness of a Petri net N is to specify a linear inequality U, requiring each reachable marking of N to satisfy U. A linear inequality U is stable if it is preserved along steps. If U is stable, then verifying correctness reduces to checking U in the initial marking of N. In this paper, we characterize classes of stable linear inequalities of a given Petri net by means of structural properties. We generalize classical results on traps, co-traps, and invariants. We show how to decide stability of a given inequality. For a certain class of inequalities, we present a polynomial time decision procedure. Furthermore, we show that stability is a local property and exploit this for the analysis of asynchronously interacting open net structures. Finally, we study the summation of inequalities as means of deriving valid inequalities.

Słowa kluczowe

EN

co-traps; inductive invariants; invariants; linear inequalities; Petri net analysis; stable properties; traps

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 146, nr 1
• Strony: 1--34
• Opis fizyczny: Bibliogr. 33 poz., rys., tab.

Twórcy

autor

Triebel M.

• Department of Computer Science, Humboldt-Universität zu Berlin, Germany

autor

Sürmeli J.

• Department of Computer Scienc, Humboldt-Universität zu Berlin, Germany

Bibliografia

• [1] Cardoza E, Lipton RJ, Meyer AR. Exponential Space Complete Problems for Petri Nets and Commutative Semigroups: Preliminary Report. In: Chandra AK, Wotschke D, Friedman EP, Harrison MA, editors. Proceedings of the 8th Annual ACM Symposium on Theory of Computing, May 3-5, 1976, Hershey, Pennsylvania, USA. ACM; 1976. p. 50–54. doi:10.1145/800113.803630.
• [2] Esparza J. Decidability and Complexity of Petri Net Problems - An Introduction. In: Reisig W, Rozenberg G, editors. Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996. vol. 1491 of Lecture Notes in Computer Science. Springer; 1996. p. 374–428. doi:10.1007/3-540-65306-6_20.
• [3] Desel J. Struktur und Analyse von Free-Choice-Petrinetzen. DUV Informatik. Deutscher Universitätsverlag; 1992.
• [4] Starke PH. Analyse von Petri-Netz-Modellen. Leitfäden und Monographien der Informatik. Teubner; 1990. doi:10.1007/978-3-663-09262-9.
• [5] Triebel M, Sürmeli J. Characterizing Stable Inequalities of Petri Nets. In: Devillers RR, Valmari A, editors. Application and Theory of Petri Nets and Concurrency - 36th International Conference, PETRI NETS 2015, Brussels, Belgium, June 21-26, 2015, Proceedings. vol. 9115 of Lecture Notes in Computer Science. Springer; 2015. p. 266–286. doi:10.1007/978-3-319-19488-2_14.
• [6] Reisig W. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer; 2013. doi:10.1007/978-3-642-33278-4.
• [7] Mitchell JE. Branch-and-cut algorithms for combinatorial optimization problems. Handbook of applied optimization. 2002 nov;40(03):65–77. doi:10.5860/choice.40-1593.
• [8] Papadimitriou CH. On the complexity of integer programming. J ACM. 1981;28(4):765–768. doi:10.1145/322276.322287.
• [9] Kindler E, Martens A, Reisig W. Inter-operability of Workflow Applications: Local Criteria for Global Soundness. In: van der Aalst WMP, Desel J, Oberweis A, editors. Business Process Management, Models, Techniques, and Empirical Studies. vol. 1806 of Lecture Notes in Computer Science. Springer; 2000. p.235–253. doi:10.1007/3-540-45594-9_15.
• [10] Karp RM, Miller RE. Parallel Program Schemata. J Comput Syst Sci. 1969;3(2):147–195. doi:10.1016/S0022-0000(69)80011-5.
• [11] Finkel A. The Minimal Coverability Graph for Petri Nets. In: Rozenberg G, editor. Advances in Petri Nets 1993, Papers from the 12th International Conference on Applications and Theory of Petri Nets, Gjern, Denmark, June 1991. vol. 674 of Lecture Notes in Computer Science. Springer; 1991. p. 210–243. doi:10.1007/3-540-56689-9_45.
• [12] Murata T. Petri nets: Properties, analysis and applications. Proceedings of the IEEE. 1989 Apr;77(4):541–580. doi:10.1109/5.24143.
• [13] Garey MR, Johnson DS. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman; 1979.
• [14] Lautenbach K. Linear Algebraic Techniques for Place/Transition Nets. In: Brauer W, Reisig W, Rozenberg G, editors. Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part I, Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986. vol. 254 of Lecture Notes in Computer Science. Springer; 1986. p. 142–167. doi:10.1007/BFb0046839.
• [15] Pascoletti KH. Diophantische Systeme und Lösungsmethoden zur Bestimmung aller Invarianten in Petri-Netzen. GMD-Bericht Nr. 160. R. Oldenbourg Verlag; 1986.
• [16] Silva M, Teruel E, Colom JM. Linear Algebraic and Linear Programming Techniques for the Analysis of Place or Transition Net Systems. In: Reisig W, Rozenberg G, editors. Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996. vol. 1491 of Lecture Notes in Computer Science. Springer; 1996. p. 309–373. doi:10.1007/3-540-65306-6_19.
• [17] Hack MHT. Analysis production schemata by Petri nets [Master’s Thesis]. Massachusetts Institute of Technology. Cambridge, Mass.; 1972.
• [18] Ezpeleta J, Couvreur J, Silva M. A New Technique for Finding a Generating Family of Siphons, Traps and st-Components. Application to Colored Petri Nets. In: Rozenberg G, editor. Advances in Petri Nets 1993, Papers from the 12th International Conference on Applications and Theory of Petri Nets, Gjern, Denmark, June 1991. vol. 674 of Lecture Notes in Computer Science. Springer; 1991. p. 126–147. doi:10.1007/3-540-56689-9_42.
• [19] Heiner M, Gilbert DR, Donaldson R. Petri Nets for Systems and Synthetic Biology. In: Bernardo M, Degano P, Zavattaro G, editors. Formal Methods for Computational Systems Biology, 8th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2008, Bertinoro, Italy, June 2-7, 2008, Advanced Lectures. vol. 5016 of Lecture Notes in Computer Science. Springer; 2008. p. 215–264. doi:10.1007/978-3-540-68894-5_7.
• [20] Abdallah IB, ElMaraghy HA. Deadlock prevention and avoidance in FMS: A Petri net based approach. The International Journal of Advanced Manufacturing Technology. 1998; 14(10):704–715. doi:10.1007/BF01438223.
• [21] Ezpeleta J, Colom JM, Martínez J. A Petri net based deadlock prevention policy for flexible manufacturing systems. IEEE Trans Robotics and Automation. 1995;11(2):173–184. doi:10.1109/70.370500.
• [22] Colom JM, Silva M. Convex geometry and semiflows in P/T nets. A comparative study of algorithms for computation of minimal P-semiflows. In: Rozenberg G, editor. Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings]. vol. 483 of Lecture Notes in Computer Science. Springer; 1989. p. 79–112. doi:10.1007/3-540-53863-1_22.
• [23] Colón M, Sankaranarayanan S, Sipma H. Linear Invariant Generation Using Non-linear Constraint Solving. In: Jr WAH, Somenzi F, editors. Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. vol. 2725 of Lecture Notes in Computer Science. Springer; 2003. p. 420–432. doi:10.1007/978-3-540-45069-6_39.
• [24] Sankaranarayanan S, Sipma H, Manna Z. Petri Net Analysis Using Invariant Generation. In: Dershowitz N, editor. Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. vol. 2772 of Lecture Notes in Computer Science. Springer; 2003. p. 682–701. doi:10.1007/978-3-540-39910-0_29.
• [25] Farkas J. Theorie der einfachen Ungleichungen. Journal fĂL’r die reine und angewandte Mathematik (Crelle’s Journal). 1902;1902(124):1–27. doi:10.1515/crll.1902.124.1.
• [26] Dräger K, Finkbeiner B. Subsequence Invariants. In: van Breugel F, Chechik M, editors. CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings. vol. 5201 of Lecture Notes in Computer Science. Springer; 2008. p. 172–186. doi:10.1007/978-3-540-85361-9_17.
• [27] Leroux J. The General Vector Addition System Reachability Problem by Presburger Inductive Invariants. Logical Methods in Computer Science. 2010;6(3). doi:10.2168/LMCS-6(3:22)2010.
• [28] Ginsburg S, Spanier E. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics. 1966 feb;16(2):285–296. doi:10.2140/pjm.1966.16.285.
• [29] Fischer MJ, Rabin MO. Super-Exponential Complexity of Presburger Arithmetic. In: Karp RM, editor. Complexity of Computation, SIAM/AMS Proceedings. vol. 7. American Mathematical Society; 1974. p. 27–41.
• [30] Leroux J. Vector Addition Systems Reachability Problem (A Simpler Solution). In: Voronkov A, editor. Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012. vol. 10 of EPiC Series. EasyChair; 2012. p. 214–228. Available from: http://www.easychair.org/publications/?page=1673703727.
• [31] Desel J, Neuendorf K, Radola MD. Proving Nonreachability by Modulo-Invariants. Theor Comput Sci. 1996;153(1&2):49–64. doi:10.1016/0304-3975(95)00117-4.
• [32] Wimmel H, Wolf K. Applying CEGAR to the Petri Net State Equation. Logical Methods in Computer Science. 2012;8(3). doi:10.2168/LMCS-8(3:27)2012.
• [33] Emerson EA, Halpern JY. “Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time Temporal Logic. J ACM. 1986;33(1):151–178. doi:10.1145/4904.4999.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).