Decidability, Complexity, Expressiveness And Model Checking Of Propositional Projection Temporal Logic

Interval based temporal logics, such as Projection Temporal Logic (PTL) and In-terval 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 Tem-poral 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 stutter-invariant 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 lower-bound for the complexity of the satisfiability of PPTL and PITL for-mulas is first proved to be non-elementary by means of reducing the emptiness problem of star-free expressions to the problem of the satisfiability of PPTL formulas. Ac-cordingly, the complexity of the decision procedure given for PPTL and PITL is also non-elementary.(3) PPTL is proved to represent exactly the full regular language by three trans-forming procedures among PPTL, Stutter Buchi Automata (SBA), and Extended Reg-ular 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 automata-based 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 Verifica-tion 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 NP-hard 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 Pro-jection 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.