Symbolic state-space generation of asynchronous systems using extensible decision diagrams. (English)
Nielsen, Mogens (ed.) et al., SOFSEM 2009: Theory and practice of computer science. 35th conference on current trends in theory and practice of computer science, Špindlerův Mlýn, Czech Republic, January 24‒30, 2009. Proceedings. Berlin: Springer (ISBN 978-3-540-95890-1/pbk). Lecture Notes in Computer Science 5404, 582-594 (2009).
Summary: 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 saturation-based 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.