Skeleton abstraction for universal temporal properties

DOI10.1007/978-3-030-76983-3_10MaRDI QIDQ2117168zbMATH OpenOpenAlexFDO

Authors Sophie Wallner, Karsten Wolf

Publication date 21 March 2022

Full work available at URL https://arxiv.org/abs/2112.08884

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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. 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 $ACT{L}^{\ast }$ 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 $ACT{L}^{\ast }$ 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.

Recommendations

• Abstraction and abstraction refinement
• On the abstraction of coloured Petri Nets
• scientific article; zbMATH DE number 2110619
• A more efficient time Petri net state space abstraction useful to model checking timed linear properties
• scientific article; zbMATH DE number 1696463

Cites work

• Applying CEGAR to the Petri net state equation
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Coloured Petri Nets
• How Much Is Worth to Remember? A Taxonomy Based on Petri Nets Unfoldings
• scientific article; zbMATH DE number 4030998 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1487867 (Why is no real title available?)
• scientific article; zbMATH DE number 1515293 (Why is no real title available?)
• scientific article; zbMATH DE number 1756009 (Why is no real title available?)
• Simplification of CTL formulae for efficient model checking of Petri nets

Cited in

(1)

• Skeleton Abstraction for Universal Temporal Properties

This page was built for publication: Skeleton abstraction for universal temporal properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117168)