For the most recent entries see the Petri Nets Newsletter.

Saturation: An efficient iteration strategy for symbolic state space generation.

Ciardo, Gianfranco; Luettgen, Gerald; Siminiceanu, Radu

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography