Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Saturation: An Efficient Iteration Strategy for Symbolic State—Space Generation
| |
|
Saturation: An Efficient Iteration Strategy for Symbolic State—Space Generation
Gianfranco Ciardo6 , Gerald Lüttgen7 and Radu Siminiceanu6 
| (6) |
Department of Computer Science, College of William and Mary, Williamsburg, VA 23187, USA |
| (7) |
Department of Computer Science, Sheffield University, 211 Portobello Street, Sheffield, S1 4DP, UK |
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.
This work was partially supported by the National Aeronautics and Space Administration under NASA Contract No. NAS1-97046
while the authors were in residence at the Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley
Research Center, Hampton, VA 23681, USA. G. Ciardo and R. Siminiceanu were also partially supported by NASA grant No. NAG-1-2168.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|