Mathematical Structures in Computer Science

Paper

Complexity of propositional projection temporal logic with star

CONG TIANa1 and ZHENHUA DUANa1 c1

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

Abstract

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)

Correspondence

c1 Corresponding author.

Footnotes

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.