|
Abstract : |
Abstract. Bounded Model Checking (BMC) is a technique for encoding an LTL model checking problem into a problem of propositional satis-ability. Since the seminal paper [Biere et al., 1999a] , the research on BMC has been primarily directed to the achieving eciency for solving reachability properties. In this paper, we tackle the problem of improving BMC encodings for the full class of LTL properties. We start noticing some properties of the encoding of [Biere et al., 1999a] , and we exploit them to propose improvements that make the resulting boolean formulas smaller or simpler to solve. 1 Motivations and goals Model Checking [ Clarke et al., 1986; Clarke et al., 1994] is a powerful technique for verifying systems and detecting errors at early stages of the design process, which is obtaining wide acceptance in industrial settings. In Model Checking, the specication is expressed in temporal logic |either Computation Tree Logic (CTL) or Linear temporal Logic (LTL) | and the system is modeled as a nite state machine (FSM). A traversal algorithm veries exhaustively whether the FSM veries the property or not. Symbolic Model Checking uses Ordered Boolean Decision Diagrams (OBDDs) [ Bryant, 1992] to encode the FSM [ Burch et al., 1992; McMillan, 1993]. Recently a new approach for Symbolic Model Checking has been proposed, called Bounded Model Checking, which is based on SAT techniques [ Biere et al., 1999a]. Given a FSM M and an LTL specication f, the idea is to look for counter-examples of maximum length k, and to generate a boolean formula which is satisable if and only if such counter-example exists. The boolean formula is then given as input to a SAT decider. If the formula is satisable, the satisfying assignment returned is converted into a counter-example execution path., |
