The Community for Technology Leaders
Design Automation Conference (2000)
Los Angeles, CA
June 5, 2000 to June 9, 2000
ISBN: 1-58113-1897-9
pp: 29-34
Kavita Ravi , Cadence Design Systems, New Providence, NJ
Roderick Bloem , University of Colorado, Boulder
Fabio Somenzi , University of Colorado, Boulder
ABSTRACT
CTL model checking of complex systems often suffers from the state-explosion problem. We propose using Symbolic Guided Search to avoid difficult-to-represent sections of the state space and prevent state explosion from occurring.Symbolic Guided Search applies hints to guide the exploration of the state space. In this way, the size of the BDDs involved in the computation is controlled, and the truth of a property may be decided before all states have been explored. In this work, we show how hints can be used in the computation of nested fixpoints. We show how to use hints to obtain overapproximations useful for greatest fixpoints, and we present the first results for backward search. Our experiments demonstrate the effectiveness of our approach.
INDEX TERMS
nanotechnology, quantum cellular automata
CITATION
Kavita Ravi, Roderick Bloem, Fabio Somenzi, "Symbolic Guided Search for CTL Model Checking", Design Automation Conference, vol. 00, no. , pp. 29-34, 2000, doi:10.1109/DAC.2000.855271
89 ms
(Ver 3.3 (11022016))