Satisfiability And Expressiveness Of Propositional Projection Temporal Logic

This thesis investigates the decision procedure for checking the satisfiability of Propositional Projection Temporal Logic (PPTL) and its expressiveness. Within this logic, besides the usual logic connectives, two basic temporal operators,○and prj are introduced. A normal form of PPTL is formalized and a proof for transforming a formula of PPTL into the normal form is given by induction on the structure of formulas in details. An algorithm transforming a formula into the normal form is presented. To find out a model for a given formula, the notation of Normal Form Graph (NFG) and an algorithm constructing NFG for the formula are introduced. A decision procedure for checking the satisfiability of PPTL formulas with finite models is demonstrated and some examples are given to illustrate how the algorithms work. Two versions of projection constructs in Interval Temporal Logic are presented and compared. Further, the expressiveness of two constructs is investigated.