Sciweavers

APN
2007
Springer

Improving Static Variable Orders Via Invariants

13 years 9 months ago
Improving Static Variable Orders Via Invariants
Abstract. Choosing a good variable order is crucial for making symbolic state-space generation algorithms truly efficient. One such algorithm is the MDD-based Saturation algorithm for Petri nets implemented in SmArT, whose efficiency relies on exploiting event locality. This paper presents a novel, static ordering heuristic that considers place invariants of Petri nets. In contrast to related work, we use the functional dependencies encoded by invariants to merge decision-diagram variables, rather than to eliminate them. We prove that merging variables always yields smaller MDDs and improves event locality, while eliminating variables may increase MDD sizes and break locality. Combining this idea of merging with heuristics for maximizing event locality, we obtain an algorithm for static variable order which outperforms competing approaches regarding both time-efficiency and memory-efficiency, as we demonstrate by extensive benchmarking.
Gianfranco Ciardo, Gerald Lüttgen, Andy Jinqi
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where APN
Authors Gianfranco Ciardo, Gerald Lüttgen, Andy Jinqing Yu
Comments (0)