A Quick Modeling Approach in Model Checking

Model checking is an effective approach of verifying large and concurrent systems. Models have a direct impact on efficiency in model checking. Therefore, research on system modeling has always been one of the hot issues. Knowledge base system today occupies an important position in people´s production and life, thus the verification of knowledge base system becomes particularly important. However, transition system built by static modeling has a problem of information loss. We introduce a modeling approach based on fixed point directed towards model checking problems of production knowledge base system, using procedural features of production rules to model production knowledge base system. We also introduce the concept of conditions transition system based on conditions transition, besides, transition target is decided by action decision triggered by conditions, state transition of the system only happens when special conditions met. Fixed point calculation is introduced to build conditions transition system, and transforms build process to the process of solving the greatest fixed point in the constructor of state set. Experimental results show that, this modeling approach improves the efficiency of modeling significantly, solves the problem of information loss, and also improves the efficiency of error diagnosis.