Skeleton Abstraction for Universal Temporal Properties

Issue title: Application and Theory of Petri Nets and Concurrency: Special Issue of Selected Papers from Petri Nets 2021

Guest editors: Didier Buchs, Josep Carmona and Jetty Kleijn

Article type: Research Article

Authors: Wallner, Sophie^{; *} | Wolf, Karsten

Affiliations: University of Rostock, Germany. sophie.wallner@uni-rostock.de

Correspondence: [*] Address for correspondence: University of Rostock, 18051 Rostock, Germany

Abstract: 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].

DOI: 10.3233/FI-222138

Journal: Fundamenta Informaticae, vol. 187, no. 2-4, pp. 245-272, 2022