Methods for Efficient Unfolding of Colored Petri Nets

• Autorzy: Bilgram Alexander , Jensen Peter G. , Pedersen Thomas , Srba Jiří , Taankvist Peter H.

Identyfikatory

DOI

10.3233/FI-222162

• Języki publikacji: EN

Abstrakty

EN

Colored Petri nets offer a compact and user friendly representation of the traditional Place/Transition (P/T) nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach is competitive w.r.t. unfolding time, it also outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2021 Model Checking Contest.

Słowa kluczowe

EN

colored Petri nets; CPN; Model Checking Contest; MCC

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 189, nr 3-4
• Strony: 297--320
• Opis fizyczny: Bibliogr. 28 poz., rys., tab., wykr.

Twórcy

autor

Bilgram Alexander

• Aalborg University Department of Computer Science, Aalborg, Denmark

autor

Jensen Peter G.

• Aalborg University Department of Computer Science, Aalborg, Denmark

autor

Pedersen Thomas

• Aalborg University Department of Computer Science, Aalborg, Denmark

autor

Srba Jiří

• Aalborg University Department of Computer Science, Aalborg, Denmark

autor

Taankvist Peter H.

• Aalborg University Department of Computer Science, Aalborg, Denmark

Bibliografia

• 1] Petri C. Kommunikation mit Automaten. Ph.D. thesis, Institut für instrumentelle Mathematik, Bonn, 1962.
• [2] Murata T. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 1989. 77(4):541-580. doi:10.1109/5.24143.
• [3] Jensen K. Coloured Petri Nets and the Invariant-Method. Theoretical Computer Science, 1981. 14:317-336. doi:10.1016/0304-3975(81)90049-9.
• [4] Dal Zilio S. MCC: A Tool for Unfolding Colored Petri Nets in PNML Format. In: Application and Theory of Petri Nets and Concurrency. Springer International Publishing, Cham, 2020 pp. 426-435. doi: 10.1007/978-3-030-51831-8_23.
• [5] Liu F, Heiner M, Yang M. An efficient method for unfolding colored Petri nets. In: Proceedings of the 2012 Winter Simulation Conference (WSC). ISBN 978-1-4673-4779-2, 2012 pp. 1-12. doi:10.1109/WSC.2012.6465203.
• [6] Schwarick M, Rohr C, Liu F, Assaf G, Chodak J, Heiner M. Efficient Unfolding of Coloured Petri Nets Using Interval Decision Diagrams, pp. 324-344. Application and Theory of Petri Nets and Concurrency. ISBN 978-3-030-51830-1, 2020. doi:10.1007/978-3-030-51831-8_16.
• [7] Hillah L. Family Reunion. https://mcc.lip6.fr/pdf/FamilyReunion-form.pdf, 2021.
• [8] Ciaghi A, Weldemariam K, Villafiorita A, Kessler F. Law Modeling with Ontological Support and BPMN: a Case Study. In CYBERLAWS 2011, The Second International Conference on Technical and Legal Aspects of the e-Society, 2011. pp. 29-34.
• 9] Hillah L. A hot drink vending machine. https://mcc.lip6.fr/pdf/DrinkVendingMachine-form.pdf, 2021.
• [10] Muschevici R, Proença J, Clarke D. Modular Modelling of Software Product Lines with Feature Nets. In: Software Engineering and Formal Methods. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011 pp. 318-333. doi:10.1007/978-3-642-24690-6_22.
• [11] Kordon F, Bouvier P, Garavel H, Hillah LM, Hulin-Hubard F, Amat N, Amparore E, Berthomieu B, Biswal S, Donatelli D, Galla F, , Dal Zilio S, Jensen P, He C, Le Botlan D, Li S, , Srba J, Thierry-Mieg, Walner A, Wolf K. Complete Results for the 2021 Edition of the Model Checking Contest. http://mcc.lip6.fr/2021/results.php, 2021.
• [12] David A, Jacobsen L, Jacobsen M, Jørgensen K, Møller M, Srba J. TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets. In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), volume 7214 of LNCS. Springer-Verlag, 2012 pp. 492-497. doi:10.1007/978-3-642-28756-5_36.
• [13] Jensen J, Nielsen T, Oestergaard L, Srba J. TAPAAL and Reachability Analysis of P/T Nets. LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), 2016. 9930:307-318. doi: 10.1007/978-3-662-53401-4_16.
• [14] Heiner M, Herajy M, Liu F, Rohr C, Schwarick M. Snoopy - A Unifying Petri Net Tool. In: Application and Theory of Petri Nets. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-31131-4, 2012 pp. 398-407. doi:10.1007/978-3-642-31131-4_22.
• [15] Heiner M, Rohr C, Schwarick M. MARCIE - Model Checking and Reachability Analysis Done Efficiently. In: Application and Theory of Petri Nets and Concurrency. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013 pp. 389-399. doi:10.1007/978-3-642-38697-8_21.
• [16] Chodak J, Heiner M. Spike - Reproducible Simulation Experiments with Configuration File Branching. In: Computational Methods in Systems Biology. Springer International Publishing, Cham. ISBN 978-3- 030-31304-3, 2019 pp. 315-321. doi:10.1007/978-3-030-31304-3_19.
• [17] Berthomieu B, Ribet PO, Vernadat F. The tool TINA — construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research, 2004. 42:2741-2756. doi:10.1080/00207540412331312688.
• [18] Wolf K. Petri Net Model Checking with LoLA 2. In: Application and Theory of Petri Nets and Concurrency. Springer International Publishing, Cham. ISBN 978-3-319-91268-4, 2018 pp. 351-362. doi: 10.1007/978-3-319-91268-4_18.
• [19] Amparore EG, Balbo G, Beccuti M, Donatelli S, Franceschinis G. 30 Years of GreatSPN. In: Fiondella L, Puliafito A (eds.), Principles of Performance and Reliability Modeling and Evaluation: Essays in Honor of Kishor Trivedi on his 70th Birthday. Springer International Publishing, Cham. ISBN 978-3-319-30599-8, 2016 pp. 227-254. doi:10.1007/978-3-319-30599-8_9.
• [20] Thierry-Mieg Y. Symbolic Model-Checking Using ITS-Tools. In: Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-662-46681-0, 2015 pp. 231-237. doi:10.1007/978-3-662-46681-0_20.
• [21] Thierry-Mieg Y. Personal Correspondence with Y. Thierry-Mieg, 2021. [22] Thierry-Mieg Y, Dutheillet C, Mounier I. Automatic Symmetry Detection in Well-Formed Nets. In: van der Aalst W, Best E (eds.), Applications and Theory of Petri Nets 2003. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-44919-5, 2003 pp. 82-101.
• [23] Klostergaard A. Efficient Unfolding and Approximation of Colored Petri Nets with Inhibitor Arcs. Master’s thesis, Department of Computer Science, Aalborg University, 2018. URL https://projekter.aau.dk/projekter/files/281079031/main.pdf.
• [24] Bilgram A, Jensen P, Pedersen T, Srba J, Taankvist P. Improvements in Unfolding of Colored Petri Nets. In: Proceedings of the 15th International Conference on Reachability Problems (RP’21), volume 13035 of LNCS. Springer-Verlag, 2021 pp. 69-84. doi:10.1007/978-3-030-89716-1_5.
• [25] Jensen K, Kristensen LM. Coloured Petri Nets, Modelling and Validation of Concurrent Systems. Springer-Verlag Berlin Heidelberg, 1 edition, 2009. doi:10.1007/b95112.
• [26] Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Volume 1, volume 1. Springer-Verlag Berlin Heidelberg, 2 edition, 1996. doi:10.1007/978-3-662-03241-1.
• [27] Christensen N, Glavind M, Schmid S, Srba J. Latte: Improving the Latency of Transiently Consistent Network Update Schedules. SIGMETRICS Perform. Eval. Rev., 2021. 48(3):14-26. doi:10.1145/3453953.3453957.
• [28] Bilgram A, Peter G J, Pedersen T, Srba J, Taankvist PH. Repeatability package for: Methods for Efficient Unfolding of Colored Petri Nets, 2022. URL https://doi.org/10.5281/zenodo.6417272.