Sciweavers

CHARME
2005
Springer

Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning

14 years 4 months ago
Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning
Abstract. We propose a new saturation-based symbolic state-space generation algorithm for finite discrete-state systems. Based on the structure of the high-level model specification, we first disjunctively partition the transition relation of the system, then conjunctively partition each disjunct. Our new encoding recognizes identity transformations of state variables and exploits event locality, enabling us to apply a recursive fixed-point image computation strategy completely different from the standard breadth-first approach employing a global fix-point image computation. Compared to breadth-first symbolic methods, saturation has already been empirically shown to be several orders more efficient in terms of runtime and peak memory requirements for asynchronous concurrent systems. With the new partitioning, the saturation algorithm can now be applied to completely general asynchronous systems, while requiring similar or better run-times and peak memory than previous saturatio...
Gianfranco Ciardo, Andy Jinqing Yu
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CHARME
Authors Gianfranco Ciardo, Andy Jinqing Yu
Comments (0)