Premium
Formal description and verification of production systems
Author(s) -
Liu N. K.,
Dillon T.
Publication year - 1995
Publication title -
international journal of intelligent systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 1.291
H-Index - 87
eISSN - 1098-111X
pISSN - 0884-8173
DOI - 10.1002/int.4550100404
Subject(s) - correctness , computer science , petri net , reachability , formal verification , completeness (order theory) , formal methods , consistency (knowledge bases) , predicate (mathematical logic) , model checking , identification (biology) , expert system , programming language , software engineering , artificial intelligence , theoretical computer science , mathematical analysis , botany , mathematics , biology
There has been a lack of analytic approaches for verifying and maintaining knowledge bases in expert systems. This article provides a formal description technique for verifying the correctness, consistency, and completeness of production‐based systems. It has its foundation on High Level Petri Nets proposed by Liu and Dillon [ Proceedings of the International Conference on Modelling and Simulation , Melbourne, Australia, October 1987, pp. 68‐73; Int. J. Intell. Syst . 6 , 255–276 (1991)], and Liu [“Formal description and verification of expert systems,” Ph.D. Dissertation, Dept. of Computer Science, La Trobe University, Australia, 1992; IEEE Proceedings of the Fifth International Conference on Computing and Information , Sudbury, Ontario, Canada, May 1993]. the approach emphasizes the uses of color tokens to represent the predicate states and the conditional states for the execution of production rules. It enables the detection, location, and identification of a variety of anomalies that could occur in a sequence of inferences. A description of the problems in terms of suitable verification is given. Formal analysis is proposed which is based on reachability markings generated by the transition firings in the Petri network. © 1995 John Wiley & Sons, Inc.