Property Directed Reachability for Generalized Petri Nets

TL;DR

This paper introduces a semi-decision procedure based on Property Directed Reachability for verifying properties in generalized Petri nets, demonstrating improved capabilities over existing tools.

Contribution

It presents three novel versions of PDR-based methods tailored for generalized Petri nets, with an implementation that outperforms current state-of-the-art tools.

Findings

Successfully handles complex reachability problems

Outperforms existing verification tools

Demonstrates effectiveness on challenging benchmarks

Abstract

We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing difficulty. We have implemented our methods in a model-checker called SMPT and give empirical evidences that our approach can handle problems that are difficult or impossible to check with current state of the art tools.