Research On Quantitative Model Checking Algorithm Based On Temporal Logic

With the increasing complexity of hardware and software systems,it is very important to ensure the security of the systems.Model checking is an effective technique for automatically verifying the correctness of the systems.It has been widely used in the analysis and verification of computer software and hardware systems,communication protocols,security protocols,etc.Aiming at the problem of formal verification of concurrent systems containing non-deterministic and incomplete information,this paper studies two quantitative model checking algorithms.(1)Based on the possibility theory and fuzzy logic,the generalized possibilistic ?-calculus model checking algorithm for decision process is studied.Firstly,the generalized possibilistic decision process is introduced as the system model.Then the classical proposition ?-calculus is improved and extended,and the concept of generalized possibilistic ?-calculus is given to describe the attribute characteristics of nondeterministic systems.Then the generalized possibilistic ?-calculus model checking algorithm is proposed,and the model checking problem is simplified to fuzzy matrix operation.Finally,the specific examples are analyzed and verified.Compared with the classical ?-calculus,the generalized possibilistic ?-calculus has a stronger expressive power and can better characterize the attributes of uncertain systems.The research results expand the application scope of generalized possibility measures in model checking.(2)Based on lattice theory and multi-valued logic,a multi-valued ?-calculus model checking algorithm based on multi-valued Kripke structure is studied.The multi-valued Kripke structure is used as the system model.The classical ?-calculus language is extended to describe the properties of the multi-valued systems,a multi-valued ?-calculus model checking algorithm is proposed,and the analysis and verification are carried out through specific examples.The research results provide a new idea and method for the model checking problem of non-deterministic systems.