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

Model Checking

On Partitioning and Symbolic Model Checking

Subramanian Iyer1, Debashis Sahoo2, E. Allen Emerson1 and Jawahar Jain3

(1)  University of Texas at Austin, Austin, TX 78712, USA
(2)  Stanford University, Stanford CA 94305, USA
(3)  Fujitsu Laboratoies of America, Sunnyvale CA 94085, USA
Abstract
State space partitioning-based approaches have been proposed in the literature to address the state-space explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of inter-partition (cross-over) image computations, which can be expensive. We present a model checking algorithm that aggregates these expensive cross-over images by localizing computation to individual partitions. It reduces the number of cross-over images and drastically outperforms extant approaches in terms of cross-over image computation cost as well as total model checking time, often by two orders of magnitude.
Keywords: Symbolic Model Checking, BDD, state partitioning, CTL.

Fulltext Preview (Small, Large)
Image of the first page of the fulltext


Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.84 • Server: mpweb02
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)