Sciweavers

ATVA
2006
Springer

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

13 years 7 months ago
A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis
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.
Ming-Ying Chung, Gianfranco Ciardo, Andy Jinqing Y
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATVA
Authors Ming-Ying Chung, Gianfranco Ciardo, Andy Jinqing Yu
Comments (0)