文章基本信息

标题：Model Checking the Inconsistency and Circularity in Rule-Based Expert Systems
本地全文：下载
作者：Desheng Xu ; Kejian Xia ; Dezheng Zhang 等
期刊名称：Computer and Information Science
印刷版ISSN：1913-8989
电子版ISSN：1913-8997
出版年度：2009
卷号：2
期号：1
页码：12
DOI：10.5539/cis.v2n1P12
出版社：Canadian Center of Science and Education
摘要：Normal 0 7.8 ? 0 2 false false false MicrosoftInternetExplorer4  /* Style Definitions */ table.MsoNormalTable {mso-style-name:????; mso-tstyle-rowband-size:0; mso-tstyle-colband-size:0; mso-style-noshow:yes; mso-style-parent:""; mso-padding-alt:0cm 5.4pt 0cm 5.4pt; mso-para-margin:0cm; mso-para-margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:10.0pt; font-family:"Times New Roman"; mso-fareast-font-family:"Times New Roman"; mso-ansi-language:#0400; mso-fareast-language:#0400; mso-bidi-language:#0400;} 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.