Decidability Of Propositional Projection Temporal Logic

This dessatation investigates the decidability of Propositional Projection Temporal Logic (PPTL). The syntax, semantics and logic laws of PPTL are briefly presented. Normal form and normal form graph (NFG) are defined for PPTL formulas. Further, based on NFG, a decision procedure for checking the satisfiability of PPTL formulas with infinite models are formalized, and examples are given to show how the algorithm works. In addition, a decision algorithm for checking the satisfiability of Propositional Interval Temporal Logic (PITL) formulas is also presented.Decidability of formulas is a fundamental issue in the model theory of a logic. Moreover, satisfiability plays an important role in the model checking approach. Based on the decision procedure for checking the satisfiability of PPTL formulas, model checking based on PPTL can be realized. At the end of this thesis, current model checkers are analyzed to show the advantages of the model checker based on PPTL. Also the model checker based on PPTL is briefly designed.