Checking Inevitability and Invariance Using Description Logic Technology
Shoham Ben-David, Richard Trefler, Dmitry Tsarkov, Grant Weddell · 2008
1. David R. Cheriton School of Computer Science, University of Waterloo2. Department of Computer Science, University of Manchester, UKAbstract. Description Logic is a family of knowledge representation formalisms,mainly used to specify ontologies for information systems. We show how De-scription Logic can serve as a natural setting for representing and solving sym-bolic model checking problems. We concentrate on inevitability (AF(p)) spec-ification and invariance ( AG(p)) formulas. Experimental results, using the De-scription Logic reasoner FaCT++, outperform existing methods for inevitabilityformulas. For invariance formulas we give new encodings that significantly im-prove on previous implementations using DL technology.