Download PDFOpen PDF in browser

EnPAC: Petri Net Model Checking for Linear Temporal Logic

EasyChair Preprint no. 11276

6 pagesDate: November 10, 2023


In linear temporal logic (LTL) model checking using Petri nets, two important aspects are state generation and exploration for counterexample search. Traditional state generation involves updating a structure of enabled transitions and frequently encoding/decoding to read each encoded state, which can be expensive. This paper proposes an optimized approach that calculates enabled transitions on demand using a dynamic fireset, avoiding the need for such a structure. Additionally, a set of direct read/write (DRW) operations on encoded markings is proposed to speed up state generation and reduce memory usage without the need for decoding and re-encoding. Heuristic information is incorporated into the Büchi automaton for counterexample search to guide exploration toward accepted states. These strategies improve existing methods for LTL model checking with Petri nets. The optimization strategies are implemented in a tool called EnPAC (Enhanced Petri-net Analyser and Checker) for linear temporal logic and evaluated on MCC (Model Checking Contest) benchmarks, demonstrating a significant improvement over previous methods.

Keyphrases: ENCODE, heuristic, Linear Temporal Logic (LTL), model checking, Petri nets, state explosion

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Zhijun Ding and Cong He and Shuo Li},
  title = {EnPAC: Petri Net Model Checking for Linear Temporal Logic},
  howpublished = {EasyChair Preprint no. 11276},

  year = {EasyChair, 2023}}
Download PDFOpen PDF in browser