Skeleton Abstraction for Universal Temporal Properties

TL;DR

This paper introduces a skeleton abstraction method for coloured Petri nets that preserves universal temporal properties, enabling more effective model checking of complex systems.

Contribution

It establishes conditions under which skeleton abstraction preserves ACTL* properties and proposes a partition refinement algorithm for applying this to place/transition nets.

Findings

Skeleton abstraction preserves ACTL* properties under certain conditions.

The proposed algorithm enables model checking of larger systems.

Experiments show improved problem-solving in the Model Checking Contest.

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 $ 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.