Occam's Razor Applied to the Petri Net Coverability Problem

TL;DR

This paper introduces a new, simple method for solving the Petri net coverability problem by combining forward invariant generation with backward reachability, showing promising experimental results.

Contribution

It presents a novel, generic approach that integrates invariant generation and backward reachability, improving efficiency in Petri net coverability analysis.

Findings

Demonstrates the effectiveness of the approach through experiments

Achieves improved performance over existing methods

Provides a scalable solution for Petri net verification

Abstract

The verification of safety properties for concurrent systems often reduces to the coverability problem for Petri nets. This problem was shown to be ExpSpace-complete forty years ago. Driven by the concurrency revolution, it has regained a lot of interest over the last decade. In this paper, we propose a generic and simple approach to solve this problem. Our method is inspired from the recent approach of Blondin, Finkel, Haase and Haddad. Basically, we combine forward invariant generation techniques for Petri nets with backward reachability for well- structured transition systems. An experimental evaluation demonstrates the efficiency of our approach.