Sophie Wallner ; Karsten Wolf - Skeleton Abstraction for Universal Temporal Properties

fi:8862 - Fundamenta Informaticae, October 21, 2022, Volume 187, Issues 2-4: Petri Nets 2021
Skeleton Abstraction for Universal Temporal PropertiesArticle

Authors: Sophie Wallner ; Karsten Wolf

    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. For the application of the skeleton as an abstraction method in the model checking process, we need to establish a simulation relation 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. 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.


    Volume: Volume 187, Issues 2-4: Petri Nets 2021
    Published on: October 21, 2022
    Accepted on: July 4, 2022
    Submitted on: December 17, 2021
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 146 times.
    This article's PDF has been downloaded 121 times.