Model Checking the Inconsistency and Circularity in Rule-Based Expert Systems

In the past several years, various techniques were proposed to analyze various types of structural errors, such as inconsistency (conflict rules), and circularity (circular depending rules), of rule-based systems. Model checking is a technique for the verification of temporal logic specifications in state transition systems. In this paper, we model the rule-based systems as finite state transition systems and express consistency and acyclic as Linear Temporal Logic (LTL) logic formula and then use the technique of model checking to detect inconsistency and circularity in Rule-Based Systems with the model checker NuSMV.