Seminar by Dr. Mukul Goyal
Symbolic Model Checking by Implicit Decomposition
Dr. Supratik Chakraborty
Department of Computer Science and Engineering
Indian Institute of Technology Bombay
Mumbai, India
Date: Wednesday, August 6, 2003
Time: 2:30 PM
Venue: CS-101
Abstract
Model checking is a technique for verifying temporal properties of finite state systems. Symbolic model checking involves reasoning about sets of states represented implicitly using Boolean predicates. Binary decision diagrams (BDDs) have been popularly used to represent and manipulate Boolean functions in symbolic model checkers. Recent approaches have also looked at the applicability of SAT techniques for symbolic model checking. Practical experience indicates that BDD based techniques are eventually limited by space considerations, while SAT based techniques are eventually limited by the time complexity of finding a satisfying assignment. Two key problems in the context of model checking are: (P1) detecting if a target set of states is reachable from an initial set of states, and (P2) detecting if a cycle of states satisfying a predicate is reachable from the initial states. Symbolic algorithms for solving these problems exist, but involve extensive use of quantification -- an operation that is known to be expensive in both SAT and BDD-based approaches. In this talk, I will present an alternative approach to address the above problems by limiting the number of quantifications, and using repeated function compositions instead. Our approach proceeds by decomposing a state transition graph additively. The decomposition is done implicitly and on demand, often obviating the need for a complete decomposition. Exploration of the decomposed graph is performed by means of repeated function compositions. Empirical evidence indicates that this leads to better space efficiency compared to the quantification-based approach for BDD methods, and leads to better time efficiency for SAT-based methods. I will discuss our recent findings in this area, along with algorithms for solving problems P1 and P2 using the decomposition appraoch. I will also discuss a few techniques for implicit decomposition of a state transition relation.