Applying CEGAR to the Petri Net State Equation

TL;DR

This paper introduces a novel reachability verification method for Petri nets that combines the state equation with CEGAR, enabling efficient negative result detection and diagnostic insights.

Contribution

It presents a new technique integrating Petri net state equations with CEGAR, improving efficiency and diagnostics over traditional state space methods.

Findings

Effective on real-world examples

Quick termination for negative reachability queries

Provides diagnostic information for unreachability

Abstract

We propose a reachability verification technique that combines the Petri net state equation (a linear algebraic overapproximation of the set of reachable states) with the concept of counterexample guided abstraction refinement. In essence, we replace the search through the set of reachable states by a search through the space of solutions of the state equation. We demonstrate the excellent performance of the technique on several real-world examples. The technique is particularly useful in those cases where the reachability query yields a negative result: While state space based techniques need to fully expand the state space in this case, our technique often terminates promptly. In addition, we can derive some diagnostic information in case of unreachability while state space methods can only provide witness paths in the case of reachability.