Local Model Checking For Propositional ?-Calculus

With the development of computer software system and hardware system,the system is becoming more and more complex.So the correctness and reliability of the system are becoming more and more important.Therefore,many scholars have put forward many theories and methods.Because of the high degree of automation,Model Checking has attracted the attention of scholars.Model Checking is a formal verification technique that to verify whether the model of system satisfies some given properties.There are many logic languages in Model Checking,and the propositional ?-calculus is a logic language of Model Checking,it has attracted many scholars' interest.Propositional ?-calculus is proposed by Kozen,it is a logic language with strong expression ability.The strong expression ability is mainly derived from the alternation of fixpoint and fixpoint.At present,there are a lot of algorithms about Model Checking which can be divided into global model checking algorithm and local model checking algorithm.Model Checking requires exhaustive searching the whole system state space.When we verify a concurrent system,the state number is growing exponentially.At present,the index of time complexity of existing local model checking algorithm is d(d is the alternation depth of the formula).This thesis studies the relationship of the intermediate results of the nested iteration and design an efficient local model checking algorithm,then analyze complexity of algorithm.This thesis mainly consists of three parts:The first part analyze local model checking algorithm based on propositional ?-calculus and the iterative process of fixpoint.A local model checking algorithm based on three-decision is presented.The second part analyze a set of relationships of intermediate results of fixpoint and design a local model checking algorithm.The third part mainly designe the parser of MuFPAL-MC which is a model checker based on ?-calculus and first-order predicate ambient logic.