Symbolic guided search for CTL model checking

CTL model checking of complex systems often suffers from the stare-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 stares 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.