Modal vs. Propositional Reasoning for model checking with Description Logics.
Shoham Ben-David, Richard Trefler, Grant Weddell · Description Logics · 2007
Model checking ([7, 13], c.f.[6]) is a technique for verifying finite-state concurrent systems that has proven effective in the verification of industrial hardware and software programs. In model checking, a model M , given as a set of state variables V and their next-state relations, is verified against a temporal logic formula φ. In this work we consider only safety formulas of the form AG(b), with b being a Boolean expression over the state variables of the model, meaning that b is an invariant of M . The main challenge in model checking is known as the state space explosion problem, where the number of states in the model grows exponentially in the number of program variables. To cope with this problem, model checking is done symbolically, by representing the system under verification as sets of states and transitions, and by using Boolean functions to manipulate those sets. Two main symbolic methods are used to perform model checking. The first, implemented in SMV [10], is based on Binary Decision Diagrams (BDDs) [5]. The second is known as Bounded Model Checking (BMC) [4]. Using this method, the model under verification and its specification are unfolded to depth k (for a given bound k), and translated into a propositional CNF formula. This results in an encoding of the model checking problem that is essentially k times the size of the textual description of M . A SAT solver is then applied to the formula to find a satisfying assignment. Such an assignment, if found, demonstrates an error in the model. We investigate the possibility of using a Description Logic reasoner for bounded model checking. Recent work [3] showed how to embed BMC problems as concept consistency problems in the DL dialect ALCI. The encoding as a terminology resulted in a natural symbolic representation of the sets of states and transitions that is significantly smaller than the one obtained by translating a model into a CNF formula. This translation works as follows. Let M be a model defined by a set V of Boolean state variables and their next-state transitions R. We represent each variable vi ∈ V as a concept Vi, and the transition relation as a single role R. We then introduce concept inclusions of the type