Using Petri nets to verify acyclic rule-based system

Abstract

A series of Petri net-based definitions were formulated for describing four types of structural errors in a rule-based system (RBS), including inconsistency, incompleteness, redundancy and circularity. A marked ?-Petri net model of acyclic RBS was constructed. Then, its reachability tree was generated to record all reachable relations between propositions in RBS. Moreover, a backward reasoning forest of a reachable marking was generated for explicitly representing reachable paths in RBS. Finally, a set of theorems and algorithms were provided to analyze and check structural errors. The usability of the research results presented in this paper was illustrated by an example.

Keywords

rule-based system (RBS) / horn clause / Petri net / verification