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.

• Type: Conference
• Year: 2006
• Where: ATVA
• Authors: Ming-Ying Chung, Gianfranco Ciardo, Andy Jinqing Yu
• Keywords: ATVA 2006, Hardware, Similar Asynchronous Systems, State-space Generation, Symbolic State-space Generation