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

Abstract

<!-- /* Font Definitions */ @font-face {font-family:??; panose-1:2 1 6 0 3 1 1 1 1 1; mso-font-alt:SimSun; mso-font-charset:134; mso-generic-font-family:auto; mso-font-pitch:variable; mso-font-signature:3 135135232 16 0 262145 0;} @font-face {font-family:"\@??"; panose-1:2 1 6 0 3 1 1 1 1 1; mso-font-charset:134; mso-generic-font-family:auto; mso-font-pitch:variable; mso-font-signature:3 135135232 16 0 262145 0;} /* Style Definitions */ p.MsoNormal, li.MsoNormal, div.MsoNormal {mso-style-parent:""; margin:0cm; margin-bottom:.0001pt; text-align:justify; text-justify:inter-ideograph; mso-pagination:none; font-size:10.5pt; mso-bidi-font-size:12.0pt; font-family:"Times New Roman"; mso-fareast-font-family:??; mso-font-kerning:1.0pt;} /* Page Definitions */ @page {mso-page-border-surround-header:no; mso-page-border-surround-footer:no;} @page Section1 {size:612.0pt 792.0pt; margin:72.0pt 90.0pt 72.0pt 90.0pt; mso-header-margin:36.0pt; mso-footer-margin:36.0pt; mso-paper-source:0;} div.Section1 {page:Section1;} -->

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.