Decidability, Complexity, Expressiveness And Model Checking Of Propositional Projection Temporal Logic  Posted on:20110608  Degree:Doctor  Type:Dissertation  Country:China  Candidate:C Tian  Full Text:PDF  GTID:1118330338950100  Subject:Computer application technology  Abstract/Summary:  PDF Full Text Request  Interval based temporal logics, such as Projection Temporal Logic (PTL) and Interval Temporal Logic (ITL), are useful formalisms for specification and verification of concurrent systems. However, most of researchers working in verification with interval based temporal logics mainly focus on the techniques based on theorem proving. The model checking approach with these logics have not well been developed since the model theory of the logics has not been well established, in particular, decidability, complexity and expressiveness of these logics, have not been solved.Motivated by this, in this thesis, decidability, complexity, and expressiveness as well as model checking algorithms for Propositional Projection Temporal Logic (PPTL) are investigated in details. Further, to verify open systems with interval based temporal logics, Alternating Interval Temporal Logic (AITL) and Alternating Projection Temporal Logic (APTL) are proposed by extending PITL and PPTL to concurrent game structures. In addition, to combat state space explosion problem in model checking, the current most efficient algorithm for producing stutterinvariant PLTL formulas and an efficient abstract refinement algorithm are presented in this thesis.The main contributions of the dissertation are as follows:(1) Normal forms of PPTL formulas are defined, and an inductive proof is given to show that any PPTL formula can be transformed into its normal form. Based on normal form, Normal Form Graph (NFG) and Labeled Normal Form Graph (LNFG) are defined for PPTL formulas. And the finiteness of the NFG and LNFG is proved. Further, a decision procedure for checking the satisfiability of PPTL formulas is given based on the construction of NFGs and LNFGs of PPTL formulas. As a complementary to the decision procedure, a transformation from PPTL to monadic second order logic with one successor (S1S) is given. Thus, the theoretical results of S1S can be automatically inherited by PPTL.(2) The lowerbound for the complexity of the satisfiability of PPTL and PITL formulas is first proved to be nonelementary by means of reducing the emptiness problem of starfree expressions to the problem of the satisfiability of PPTL formulas. Accordingly, the complexity of the decision procedure given for PPTL and PITL is also nonelementary.(3) PPTL is proved to represent exactly the full regular language by three transforming procedures among PPTL, Stutter Buchi Automata (SBA), and Extended Regular Expressions (ERE). Further, fragments of PPTL are defined and characterized, and finally, PPTL and its fragments are classified into five different language classes.(4) Based on the decision procedure, and a further transformation from LNFGs to Buchi automata, an automatabased model checking algorithm has been given for PPTL. Using this algorithm, a model checker based on SPIN has been developed.(5) Using the executable subset of PTL, namely, Modeling, Simulation and Verification Language (MSVL), as the modeling language, and PPTL as the property description language, a unified model checking approach based on SAT is formalized.(6) By applying normal form to Propositional Linear Temporal Logic (PLTL), a simpler and more efficient algorithm than the existing algorithms for producing stutter invariant PLTL formulas is obtained. This is useful in partial order model checking.(7) A novel method is given by adding extra variables to the abstract model for the refinement. With this method, not only the NPhard state separation problem can be avoided, but also a smaller refined abstract model can be obtained. This makes significant contribution to the abstract model checking.(8) To verify open systems with interval based temporal logics, Alternating Projection Temporal Logic (APTL) and Alternating Interval Temporal Logic (AITL) are proposed by introducing Concurrent Game Structures (CGS) to PPTL and PITL. Also the corresponding decision procedures and model checking algorithms are studied by means of the normal forms and NFGs techniques of AITL and APTL.  Keywords/Search Tags:  propositional projection temporal logic, decidability, complexity, expressiveness, model checking, game, abstraction refinement, partial order reduction  PDF Full Text Request  Related items 
 
