2011 Fifth International Conference on Theoretical Aspects of Software Engineering (2011)

Xi'an, Shaanxi China

Aug. 29, 2011 to Aug. 31, 2011

ISBN: 978-0-7695-4506-6

pp: 45-51

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2011.45

ABSTRACT

Focus game is applied to Propositional Projection Temporal Logic with infinite models (PPTL) for the satisfiability and model checking of PPTL formulas. To this end, normal form and complete normal form are introduced, and through which sub-formulas are defined for PPTL formulas. Accordingly, focus game $G(R)$ is constructed for checking the satisfiability of PPTL formula $R$; and $G(s,R)$ is built for checking whether a system with $s$ being the initial state satisfies formula $R$. Finally, complexity of the decision procedure and the model checking algorithm is analyzed.

INDEX TERMS

temporal logic, game, satisfiability, model checking

CITATION

C. Tian and Z. Duan, "Focus Game for Projection Temporal Logic,"

*2011 Fifth International Conference on Theoretical Aspects of Software Engineering(TASE)*, Xi'an, Shaanxi China, 2011, pp. 45-51.

doi:10.1109/TASE.2011.45

CITATIONS