Symbolic state-space generation of asynchronous systems using extensible decision diagrams

Abstract

We propose a new type of canonical decision diagrams, which allows a more efficient symbolic state-space generation for general asynchronous systems by allowing on-the-fly extension of the possible state variable domains. After implementing both breadth-first and saturationbased state-space generation with this new data structure in our tool SmArT, we are able to exhibit substantial efficiency improvements with respect to traditional "static" decision diagrams. Since our previous works demonstrated that saturation outperforms breadth-first approaches, saturation with this new structure is now arguably the state-of-the-art algorithm for symbolic state-space generation of asynchronous systems. © Springer-Verlag Berlin Heidelberg 2009.