EnPAC: Petri Net Model Checking for Linear Temporal Logic

TL;DR

EnPAC introduces optimized state generation, direct encoding operations, and heuristic-guided search to significantly improve Petri net model checking for LTL, achieving faster performance and lower memory use.

Contribution

The paper presents novel optimization techniques for Petri net model checking, including on-demand transition calculation, direct read/write operations, and heuristic-guided exploration, integrated into the EnPAC tool.

Findings

Significant performance improvements over existing methods.

Reduced memory consumption during state exploration.

Effective counterexample search guided by heuristics.

Abstract

State generation and exploration (counterexample search) are two cores of explicit-state Petri net model checking for linear temporal logic (LTL). Traditional state generation updates a structure to reduce the computation of all transitions and frequently encodes/decodes to read each encoded state. We present the optimized calculation of enabled transitions on demand by dynamic fireset to avoid such a structure. And we propose direct read/write (DRW) operation on encoded markings without decoding and re-encoding to make state generation faster and reduce memory consumption. To search counterexamples more quickly under an on-the-fly framework, we add heuristic information to the Buchi automaton to guide the exploration in the direction of accepted states. The above strategies can optimize existing methods for LTL model checking. We implement these optimization strategies in a Petri net model-checking tool called EnPAC (Enhanced Petri-net Analyser and Checker) for linear temporal logic. Then, we evaluate it on the benchmarks of MCC (Model Checking Contest), which shows a drastic improvement over the existing methods.