2011 Fifth International Conference on Theoretical Aspects of Software Engineering (2011)
Xi'an, Shaanxi China
Aug. 29, 2011 to Aug. 31, 2011
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2011.45
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.
temporal logic, game, satisfiability, model checking
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.