Skeleton Abstraction for Universal Temporal Properties

• Autorzy: Wallner Sophie , Wolf Karsten

Identyfikatory

DOI

10.3233/FI-222138

• Języki publikacji: EN

Abstrakty

EN

Uniform coloured Petri nets can be abstracted to their skeleton, the place/transition net that simply turns the coloured tokens into black tokens. A coloured net and its skeleton are related by a net morphism [1, 2]. For the application of the skeleton as an abstraction method in the model checking process, we need to establish a simulation relation [3] between the state spaces of the two nets. Then, universal temporal properties (properties of the ACTL* logic) are preserved. The abstraction relation induced by a net morphism is not necessarily a simulation relation, due to a subtle issue related to deadlocks [4]. We discuss several situations where the abstraction relation induced by a net morphism is as well a simulation relation, thus preserving ACTL* properties. We further propose a partition refinement algorithm for folding a place/transition net into a coloured net. This way, skeleton abstraction becomes available for models given as place/transition nets. Experiments demonstrate the capabilities of the proposed technology. Using skeleton abstraction, we are capable of solving problems that have not been solved before in the Model Checking Contest [5].

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: vol. 187 nr 2-4
• Strony: 245--272
• Opis fizyczny: Bibliogr. 25 poz., rys.

Twórcy

autor

Wallner Sophie

• University of Rostock, Germany

autor

Wolf Karsten

• University of Rostock, Germany

Bibliografia

• [1] Desel J. On abstractions of nets. In: Advances in Petri Nets 1991. Springer-Verlag, Berlin/ Heidelberg, 1991 pp. 78-92. doi:10.1007/BFb0019970.
• [2] Padbergx J, Gajewsky M, Ermel C. Rule-based refinement of high-level nets preserving safety properties. In: Proc. FASE, volume 1382, Springer, Berlin, Heidelberg, 1998 pp. 221-238. doi:10.1007/BFb0053593.
• [3] Milner R. Communication and Concurrency. Prentice Hall international series in computer science. Prentice Hall, New York, 1989. ISBN:978-0-13-114984-7.
• [4] Findlow G. Obtaining deadlock-preserving skeletons for coloured nets. In: Application and Theory of Petri Nets. Springer, Berlin, Heidelberg, 1992 pp. 173-192. doi:10.1007/3-540-55676-1 10.
• [5] Kordon F, Garavel H, Hillah LM, Hulin-Hubard F, Amparore E, Beccuti M, Berthomieu B, Ciardo G, Dal Zilio S, Liebke T, Li S, Meijer J, Miner A, Srba J, Thierry-Mieg Y, van de Pol J, van Dirk T, Wolf K. Complete Results for the 2019 Edition of the Model Checking Contest. http://mcc.lip6.fr/2019/results.php,2019.
• [6] Wallner S, Wolf K. Skeleton Abstraction for Universal Temporal Properties. In: Buchs D, Carmona J (eds.), Application and Theory of Petri Nets and Concurrency - 42nd International Conference, PETRI NETS 2021, Virtual Event, June 23-25, 2021, Proceedings, volume 12734 of Lecture Notes in Computer Science. Springer, 2021 pp. 186-207. doi:10.48550/arXiv.2112.08884.
• [7] Vautherin J. Parallel systems specifications with coloured Petri nets and algebraic specifications. In: Advances in Petri Nets. Springer, Berlin, Heidelberg, 1987 pp. 293-308. doi:10.1007/3-540-18086-9 31.
• [8] Rust C, B¨oke JTC. Pr/T-Net Based Seamless Design of Embedded Real-Time Systems. In: Applications and Theory of Petri Nets, Springer Berlin Heidelberg, Berlin, Heidelberg, 2001 pp. 343-362. doi:10.1007/3-540-45740-2 20.
• [9] Lilius J. On the folding of algebraic nets. Helsinki University of Technology, 1995.
• [10] Sliva V, Murataxx T, Shatz S. Protocol Specification Design Using an Object-Based Petri Net Formalism. Int. Journal of Software Engineering and Knowledge Engineering, 1999. 09(01):97-125. doi: 10.1142/S0218194099000073.
• [11] Jensen K, Kristensen L. Coloured Petri Nets. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009.
• [12] Pinna G. How Much Is Worth to Remember? A Taxonomy Based on Petri Nets Unfoldings. In: Applications and Theory of Petri Nets, volume 6709, Springer Berlin Heidelberg, Berlin, Heidelberg, 2011 pp. 109-128. doi:10.1007/978-3-642-21834-7 7.
• [13] Clarke E, Emerson E, Sistla A. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 1986. 8(2):244-263.
• [14] Grumberg O, Long D. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 1994. 16(3):843-871. doi:10.1145/177492.177725.
• [15] Penczek W, Szreter M, Gerth R, Kuiper R. Improving Partial Order Reductions for Universal Branching Time Properties. Fund. Inf., 2000. 43(1-4):245-267. doi:10.3233/FI-2000-43123413.
• [16] Katz S, Grumberg O, Geist D. ”Have I written enough Properties?” - A Method of Comparison between Specification and Implementation. In: Proc. CHARME. 1999 pp. 280-297. doi:10.1007/3-540-48153-2 21.
• [17] Schwarick M, Rohr C, Liu F, Assaf G, xChodak J, Heiner M. Efficient Unfolding of Coloured Petri Nets Using Interval Decision Diagrams. In: Proc. PETRI NETS, volume 12152 of LNCS. 2020 pp. 324-344. doi:10.1007/978-3-030-51831-8\16.
• [18] Chiola G, Dutheillet C, Franceschinis G, Haddad S. Stochastic well-formed colored nets and symmetric modeling applications. IEEE Transactions on Computers, 1993. 42(11):1343-1360. doi:10.1109/12.247838.
• [19] PNML Standard. https://www.pnml.org/index.php. Accessed: 2021-12-15.
• [20] 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 2020 Edition of the Model Checking Contest. http://mcc.lip6.fr/2021/results.php, 2021.
• [21] Wolf K. Portfolio Management in Explicit Model Checking. In: Proc. PNSE, volume 2651 of CEUR Workshop Proceedings. 2020 pp. 10-28. URL http://ceur-ws.org/Vol-2651/paper2.pdf.
• [22] Wolf K. Petri Net Model Checking with LoLA 2. In: Proc. PETRI NETS. 2018 pp. 351-362. doi: 10.1007/978-3-319-91268-418.
• [23] Wimmel H, Wolf K. Applying CEGAR to the Petri Net State Equation. Log. Methods Comput. Sci., 2012. 8(3). doi:10.2168/LMCS-8(3:27)2012.
• [24] Bønneland F, Dyhr J, Jensen PG, Johannsen M, Srba J. Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. In: Proc. PETRI NETS, volume 10877 of LNCS. 2018 pp. 143-163. doi:10.1007/978-3-319-91268-4\8.
• [25] Duret-Lutz A. LTL Translation Improvements in Spot 1.0. International Journal on Critical Computer-Based Systems, 2014. 5(1-2):31-54. doi:10.1504/IJCCBS.2014.059594.