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.
My Menu
Saved Items

Saturation: An Efficient Iteration Strategy for Symbolic State—Space Generation

Gianfranco CiardoContact Information, Gerald LüttgenContact Information and Radu SiminiceanuContact Information

(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.

Contact Information Gianfranco Ciardo
Email: ciardo@cs.wm.edu

Contact Information Gerald Lüttgen
Email: g.luettgen@dcs.shef.ac.uk

Contact Information Radu Siminiceanu
Email: radu@cs.wm.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Referenced by
3 newer articles

  1. Ciardo, Gianfranco (2009) Parallel symbolic state-space exploration is difficult, but what is the alternative?. Electronic Proceedings in Theoretical Computer Science 14
    [CrossRef]
  2. Xing, Liudong (2009) . IEEE Transactions on Dependable and Secure Computing 6(3)
    [CrossRef]
  3. Miner, A.S. (2006) . IEEE Transactions on Software Engineering 32(8)
    [CrossRef]
Remote Address: 38.107.191.109 • Server: mpweb19
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)