IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Fabio Somenzi

University of Colorado at Boulder


Guided Search and Approximation Techniques for Symbolic Model Checking

CTL model checking of complex systems often suffers from the state-explosion problem. Symbolic Guided Search can be used 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 talk, we show how hints can be used in the computation of nested fixpoints. We show how to use hints to obtain both underapproximations and overapproximations.

Approximation techniques help model checking in two distinct ways: On the one hand, the validity of a property can often be established on a simplified model of the system. On the other hand, we can successively refine an abstraction to compute the exact result. This method is often more efficient than computing the exact result directly, because we can direct the search of the state space to avoid large BDDs. This use of approximations is one of the salient features of symbolic model checking.

Under- and overapproximations can be obtained using methods that can be broadly classified into three groups: Changing the formula, changing the model, or changing the computation. In this talk we discuss the last two.