Some Petri-Net-Based Methods Of Verifying Computation Tree Logic

Petri net is a formal model of describing order,choice,concurrency and synchronization.Nowadays,Petri-net-based model checking technique has obtained extensive research and application,but there are some defects and deficiencies in the existing work.First,for model checking technique of verifying prototype computation tree logic(CTL)based on prototype Petri nets,Reduced Ordered Binary Decision Diagram(ROBDD)is usually used as symbolic representation of its model checking process to alleviate the state space explosion problem,but the existing methods of generating ROBDD variable orders underperform.Besides,its existing model checking methods need to generate complete reachability graphs of prototype Petri nets to verify CTL formulas and it needs to occupy more computer storage space.Second,for secure multi-party computation protocols,the existing Petri nets can only model local state transitions of each part and interaction/collaboration among multiple parts,but cannot model epistemic evolution of each part.Therefore,the existing Petri-net-based model checking technique can only verify temporal properties of secure multi-party computation protocols,but cannot verify privacy/secrecy-related properties of secure multi-party computation protocols.Third,for model checking technique of verifying timed computation tree logic(TCTL)based on timed Petri nets,there are some limitations in the existing work from two aspects of modelling and specifying.On the one hand,the existing timed Petri nets can only model multi-processor preemptive real-time systems with a relatively simple structure.For multi-processor preemptive real-time systems with a more complex structure,the related work is lacking.On the other hand,the existing TCTL formulas can only specify real-time requirements with known time bounds,so it cannot be used to analyze system performance.In order to solve these problems,Petri nets(including prototype Petri nets and their extensions)as the theoretic foundation of this thesis,CTL(including prototype CTL and its extensions)as property specifications,ROBDD as the technical core of symbolic model checking technique,aiming to verify the correctness of control-flows of concurrent systems,secure multi-party computation protocols,and multi-processor preemptive real-time systems,this thesis proposes model checking methods and develops model checkers so that the achievements of this thesis extend and enrich the state-of-the-art model checking technique from three aspects of modelling,specifying and verifying,which not only improves its verification efficiency,but also extends its application range.The main contents and contributions of this thesis are given as follows:(1)For model checking technique of verifying prototype CTL based on prototype Petri nets,a heuristic method of ordering ROBDD variables is proposed,which combines the structural and behavioral characteristics of a Petri net to guide the generation of an ROBDD variable order and alleviates the ROBDD node explosion problem to some extent,and thus a symbolic model checking method of verifying prototype CTL without generating complete reachability graphs is proposed,i.e.,by ROBDD,it only generates all reachable markings of a prototype Petri net,and then dynamically generates those pairs of transition markings required in the process of verifying prototype CTL formulas via the corresponding net structure.The experiments show that these methods effectively improve the efficiency of model checking technique in verifying control-flows of concurrent systems.(2)Knowledge-oriented Petri nets(KPN)are proposed to model secure multi-party computation protocols from teo perspectives of control-flow and epistemic-flow,then reachability graphs with equivalence relation(RGER)are defined as their analysis tool,and thus a symbolic model checking method of verifying CTLK without generating RGER is proposed,i.e.,by ROBDD,it only generates all reachable markings of a KPN,and then dynamically generates those pairs of transition markings and equivalence markings required in the process of verifying CTLK formulas via the corresponding net structure.The experiments show that these methods effectively improve the efficiency of model checking technique in verifying multi-party computation protocols.(3)For model checking technique of verifying TCTL based on time Petri nets,prioritized time-point-interval Petri nets(PToPN)are proposed to model multi-processor preemptive real-time systems with a more complex structure,then the corresponding state graphs are defined as their analysis tool,and thus a model checking method of verifying TCTL based on PToPN is proposed.Besides,TCTL with unknown numbers of time(TCTL)is proposed to specify real-time requirements with unknown time bounds and thus a model checking method of analyzing TCTL based on PToPN is proposed.The experiments show that these methods effectively extend the application of model checking technique in real-time systems,which results in that it can not only verify a wider variety of real-time systems,but also analyze some of their time-related performances(e.g.the worst-case execution time of a task and the maximal idle time of a processor).Based on the above methods,the corresponding model checkers are developed.A series of examples are used to conduct the experiments comparing to the state-of-the-art model checkers and the experimental results are analyzed,which shows the effectiveness and efficiency of the above methods.