Stop-transitions of Petri Nets

• Autorzy: Desel Jörg , Finthammer Marc

Identyfikatory

DOI

10.3233/FI-2020-1951

• Języki publikacji: EN

Abstrakty

EN

A transition t stops a place/transition Petri net if each reachable marking of the net enables only finite occurrence sequences without occurrences of t (i.e., every infinite occurrence sequence enabled at this marking contains occurrences of t ). Roughly speaking, when t is stopped then all transitions of the net stop eventually. This contribution shows how to identify stop-transitions of unbounded nets using the coverability graph. Furthermore, the developed technique is adapted to a more general question considering a set of stop-transitions and focussing on a certain part of the net to be stopped. Finally, an implementation of the developed algorithm is presented.

Słowa kluczowe

EN

coverability graphs; minimal coverability sets; stop-transitions; termination of Petri nets; unbounded Petri nets

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 175, nr 1-4
• Strony: 143--172
• Opis fizyczny: Bibliogr. 19 poz., rys.

Twórcy

autor

Desel Jörg

• Fern Universität in Hagen, Hagen, Germany

autor

Finthammer Marc

• Fern Universität in Hagen, Hagen, Germany

Bibliografia

• [1] Desel J. Can a Single Transition Stop an Entire Net? In: Proceedings of the International Workshop on Algorithms & Theories for the Analysis of Event Data 2019 Satellite event of the conferences: 40th International Conference on Application and Theory of Petri Nets and Concurrency Petri Nets 2019 and 19th International Conference on Application of Concurrency to System Design ACSD 2019, ATAED@Petri Nets/ACSD 2019, Aachen, Germany, June 25, 2019. 2019 pp. 23-35. URL http://ceur-ws.org/Vol-2371/ATAED2019-23-35.pdf.
• [2] Esparza J. Decidability of Model Checking for Infinite-State Concurrent Systems. Acta Inf., 1997. 34(2):85-107. doi:10.1007/s002360050074.
• [3] Lefaucheux E, Giua A, Seatzu C. Basis Coverability Graph for Partially Observable Petri Nets with Application to Diagnosability Analysis. In: Khomenko V, Roux OH (eds.), Application and Theory of Petri Nets and Concurrency - 39th International Conference, PETRI NETS 2018, Bratislava, Slovakia, June 24-29, 2018, Proceedings, volume 10877 of Lecture Notes in Computer Science. Springer, 2018 pp. 164-183. doi:10.1007/978-3-319-91268-4_9.
• [4] Schmidt K. Model-Checking with Coverability Graphs. Formal Methods Syst. Des., 1999. 15(3):239-254. doi:10.1023/A:1008753219837.
• [5] Cabasino MP, Giua A, Seatzu C. Introduction to Petri Nets. In: Seatzu C, Silva M, van Schuppen JH (eds.), Control of Discrete-Event Systems, volume 433 of Lecture Notes in Control and Information Sciences, pp. 191-211. Springer, 2013. doi:10.1007/978-1-4471-4276-8_10.
• [6] Desel J. Basic Linear Algebraic Techniques for Place/Transition Nets. In: Reisig and Rozenberg [19], 1996 pp. 257-308. doi:10.1007/3-540-65306-6_18.
• [7] Desel J. On Cyclic Behaviour of Unbounded Petri Nets. In: Carmona J, Lazarescu MT, Pietkiewicz-Koutny M (eds.), 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013. IEEE Computer Society. ISBN 978-0-7695-5035-0, 2013 pp. 110-119. doi:10.1109/ACSD.2013.14.
• [8] Reisig W. Petri Nets: An Introduction, volume 4 of EATCS Monographs on Theoretical Computer Science. Springer, 1985. ISBN 3-540-13723-8. doi:10.1007/978-3-642-69968-9.
• [9] Desel J, Reisig W. Place/Transition Petri Nets. In: Reisig and Rozenberg [19], 1996 pp. 122-173. doi:10.1007/3-540-65306-6_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] Chubarov D, Voronkov A. Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. In: Jedrzejowicz J, Szepietowski A (eds.), Mathematical Foundations of Computer Science 2005, 30th International Symposium, MFCS 2005, Gdansk, Poland, August 29 - September 2, 2005, Proceedings, volume 3618 of Lecture Notes in Computer Science. Springer. ISBN 3-540-28702-7, 2005 pp. 260-270. doi:10.1007/11549345_23.
• [12] Desel J, Finthammer M, Frank A. Cyclon - A Tool for Determining Stop-Transitions of Petri Nets. In: Janicki R, Sidorova N, Chatain T (eds.), Application and Theory of Petri Nets and Concurrency - 41st International Conference, PETRI NETS 2020, Paris, France, June 24-25, 2020, Proceedings, volume 12152 of Lecture Notes in Computer Science. Springer, 2020 pp. 392-402. doi:10.1007/978-3-030-51831-8_20.
• [13] Finkel A. The Minimal Coverability Graph for Petri Nets. In: Advances in Petri Nets 1993, Papers from the 12th International Conference on Applications and Theory of Petri Nets, Gjern, Denmark, June 1991. 1991 pp. 210-243. doi:10.1007/3-540-56689-9_45.
• [14] Reynier P, Servais F. On the Computation of the Minimal Coverability Set of Petri Nets. In: Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings. 2019 pp. 164-177. doi:10.1007/978-3-030-30806-3_13.
• [15] Reynier P, Servais F. Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning. Fundam. Inform., 2013. 122(1-2):1-30. doi:10.3233/FI-2013-781.
• [16] Geeraerts G, Raskin J, Begin LV. On the Efficient Computation of the Minimal Coverability Set for Petri Nets. In: Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings. 2007 pp. 98-113. doi:10.1007/978-3-540-75596-8_9.
• [17] Piipponen A, Valmari A. Constructing Minimal Coverability Sets. Fundam. Inform., 2016. 143(3-4):393-414. doi:10.3233/FI-2016-1319.
• [18] Valmari A, Hansen H. Old and New Algorithms for Minimal Coverability Sets. Fundam. Inform., 2014. 131(1):1-25. doi:10.3233/FI-2014-1002.
• [19] Reisig W, Rozenberg G (eds.). Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, based on the Advanced Course on Petri Nets, Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science. Springer, 1998. ISBN 3-540-65306-6. doi:10.1007/3-540-65306-6.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).