PeCAn: Compositional verification of petri nets made easy

Abstract

This paper introduces PeCAn, a tool supporting compositional verification of Petri nets. Beyond classical features (such as onthe- fly analysis and synchronisation between multiple Petri nets), PeCAn generates Symbolic Observation Graphs (SOG), and uses their composition to support modular abstractions of multiple Petri nets for more efficient verification. Furthermore, PeCAn implements an incremental strategy based on counter-examples for model-checking, thus improving significantly the cost of execution time and memory space. PeCAn also provides users with the visualisation of the input Petri nets and their corresponding SOGs.We experimented PeCAn with benchmark datasets from the Petri Nets’ model checking contests, showing promising results.