A Formal Method for Verifying Production Knowledge Base

The most important thing of using model checking technology to verify production knowledge base is to build system model from rule set. It is a fundamental but time-consuming job. This paper presents an efficient formal method to verify production knowledge base. Two main contributions of this paper are as follows. Firstly, we propose a dynamic modeling method to build system model of knowledge base, this method utilizes the dynamic procedural nature of production rule to build system model, and it improves the modeling efficiency significantly; Secondly, a conditional transition system based on the standard transition system is given to represent system model, our conditional transition system contains the whole information about the actual state transition process, which solves the information loss problem of the static transition system built by static modeling method and improves the efficiency of error diagnosis.