Saturation: An Efficient Iteration Strategy for Symbolic State-space Generation
Abstract
This paper presents a novel algorithm for generating state spaces of asynchronous systems using Multi?valued Decision Diagrams. In contrast to related work, the next?state function of a system is not encoded 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, this paper introduces a new elegant strategy, called saturation, and implements it in the tool SMART. On top of usually performing several orders of magnitude faster than existing BDD?based state?space generators, the algorithm's required peak memory is often close to the nal memory needed for storing the overall state spaces.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 2001
- Accession Number
- ADA387711
Entities
People
- Gerald Luttgen
- Gianfranco Ciardo
- Radu Siminiceanu