This paper investigates the complexity of Propositional Projection Temporal Logic with Star (PPTL~*). To this end, Propositional Projection Temporal Logic (PPTL) is first extended to include projection star. Then, by reducing the emptiness problem of star-free expressions to the problem of the satisfiability of PPTL~* formulas, the lower bound of the complexity for the satisfiability of PPTL~* formulas is proved to be non-elementary. Then, to prove the decidability of PPTL~*, the normal form, normal form graph (NFG) and labelled normal form graph (LNFG) for PPTL~* are defined. Also, algorithms for transforming a formula to its normal form and LNFG are presented. Finally, a decision algorithm for checking the satisfiability of PPTL~* formulas is formalised using LNFGs.
展开▼
