Parallelization Of LTL Model Detection Based On Likelihood Measure

Model checking is a formalized automatic verification technique,which is used to exhaustively search the system state space to verify whether or not the system properties described by temporal logic formulas can be satisfied in the model.Model checking can be performed automatically and can provide anti-example path when the system does not satisfy the property.Therefore,model checking has made re-markable achievements and is widely used in the verification of computer hardware,communication protocol,control system and security authentication protocol,ect.With the development of IT,new systems become more and more complex.The bottleneck problem,i.e.,the state explosion,of model checking has restricted its applications.Moreover,more systems contain uncertain information,which cannot be proceed by classic model checking technologies.Li Yongming's research team presented the model checking methods based on the possibility measure,which can be used to deal with uncertain information in systems.In this thesis,the parallelization of LTL model checking based on the possibility measure has been studied,which aims to provide a practicable method to solve the state explosion problem in the LTL model checking under the possibility measure.The research work of this thesis as follows:1.A new dynamic state partition method is presented.First,a component of the system is selected and its state space is divided by the relationships of the states,which aims to allocate the related states to the same computing node;then,the partition results are adjusted for the load balance of the system;finally,the partition results product the states of the rest components to complete the state partition of the system.The experiment proves that this method not only insures the load balance of the system,but also provides a good foundation for model checking.2.A parallel quantitative model checking algorithm is given.The system model is conserved into Kripke structure,a property into a Nodeterministic finite automa-ton.On the product of the two parts,the distributed quantitative model checking algorithm based on nested DFS is performed.The contribution of this thesis is providing a practicable method to solve the state explosion problem of LTL model checking under the possibility measure.