In: International Journal of Intelligent Systems, Vol. 10, No. 4, pages 399-442. 1995.
Abstract: There has been a lack of analytic approaches to 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 in High Level Petri Nets proposed by Liu and Dillon [Proceedings of the International Conference on Modeling and Simulation, Melbourne, Australia, October 1987, pp. 68-73; Int. J. Intell. Syst. 6, pp. 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.
Keywords: high-level Petri nets, production systems, system specification.