For the most recent entries see the Petri Nets Newsletter.

A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis.

Chung, Ming-Ying; Ciardo, Gianfranco; Yu, Andy Jinqing

In: Lecture Notes in Computer Science : Automated Technology for Verification and Analysis, Volume 4218, 2006, pages 51-66. 2006. URL:

Abstract: Chaining can reduce the number of iterations required for symbolic state-space generation and model-checking, especially in Petri nets and similar asynchronous systems, but requires considerable insight and is limited to a static ordering of the events in the high-level model. We introduce a two-step approach that is instead fine-grained and dynamically applied to the decision diagrams nodes. The first step, based on a precedence relation, is guaranteed to improve convergence, while the second one, based on a notion of node fullness, is heuristic. We apply our approach to traditional breadth-first and saturation state-space generation, and show that it is effective in both cases.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography