Sciweavers

Share
TABLEAUX
2007
Springer

Bounded Model Checking with Description Logic Reasoning

10 years 6 months ago
Bounded Model Checking with Description Logic Reasoning
Abstract. Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the system is unfolded until a given depth, and translated into a CNF formula. A SAT solver is then applied to the CNF formula, to find a satisfying assignment. Such a satisfying assignment, if found, demonstrates an error in the model of the concurrent system. Description Logic (DL) is a family of knowledge representation formalisms, for which reasoning is based on tableaux techniques. We show how Description Logic can serve as a natural setting for representing and solving a BMC problem. We formulate a bounded model checking problem as a consistency problem in the DL dialect ALCI. Our formulation results in a compact representation of the model, one that is linear in the size of the model description, and does not involve any unfolding of the model. Experimental results, using the DL reasoner FaCT++ , significan...
Shoham Ben-David, Richard J. Trefler, Grant E. Wed
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TABLEAUX
Authors Shoham Ben-David, Richard J. Trefler, Grant E. Weddell
Comments (0)
books