In: Margaria, T.; Yi, W.: LNCS 2031: Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 328-342. Genova, Italy: Springer-Verlag, April 2001.
Abstract: We present a novel algorithm for generating state spaces of asynchronous systems using Multi--valued Decision Diagrams. In contrast to related work, we encode the next--state function of a system not as a single Boolean function, but as cross--products of integer functions. This permits the application of various iteration strategies to build a system's state space. In particular, we introduce a new elegant strategy, called saturation, and implement it in the tool SMART. On top of usually performing several orders of magnitude faster than existing BDD--based state--space generators, our algorithm's required peak memory is often close to the final memory needed for storing the overall state space.