Research On The Optimization For The LTL Probabilistic Model Checking

Probabilistic model checking is a formal verification technology which for probabilistic model,such as Markov Chains(MCs),Markov Decision Processes(MDPs)and so on.Comparing with traditional non-probabilistic model checking,probabilistic model checking can not only verify the system qualitatively,i.e.,determines whether the system satisfies a given specification,but also verify the probabilistic system quantitatively,or a system with probabilistic behaviors inspection,i.e.,the system satisfies the given specification in a probability intervals.In probabilistic model checking,linear temporal logic(Linear Temporal Logic,LTL)and computational tree logic(Computational Tree Logic,CTL)are used to describe the system properties in general.Although the expressive power of LTL and CTL have intersection,but some important properties,such as fairness can only be represented by LTL.However,compared to the CTL,the current complexity of LTL probabilistic model checking algorithm is very high,which could have a double exponential blow up,its verification efficiency is very low,and therefore there are probabilistic modeling tools such as PRISM and MRMC do not support the verification of LTL properties.In this thesis,according to the problem that the complexity of LTL probabilistic model checking algorithm is very high,through the study of current art,we translate LTL formula to a unambiguous Büchi automata,which circumvent the second exponential blow up of LTL probabilistic model checking,thereby reducing the complexity of LTL probabilistic model checking algorithm.On the basis of this optimization techniques,this paper presents an optimization technique based on probability preserved.This optimization technique reduce the time and space overhead of the algorithm execution by shortening the length of the formula to,and thus improve the efficiency of the algorithm,it can alleviate the problem of high complexity of LTL probabilistic model checking algorithm in a way.Based on the above manners,we designed and implemented a LTL probabilistic model checker,and for the case of existing probabilistic model checking,using the tool to test LTL probabilistic model checking to verify the validity of the algorithm.