Mathematical Structures in Computer Science


Complexity of propositional projection temporal logic with star


a1 Institute of Computing Theory and Technology, Xidian University, Xi'an, 710071, P. R. China


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.

(Received October 19 2007)


c1 Corresponding author.


This research is supported by the NSFC Grant No. 60433010, and Defence Pre-Research Project of China, No. 51315050105, and NSFC Grant No. 60873018 jointly sponsored by Microsoft Asia Research Academy.