The Community for Technology Leaders
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
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
84 ms
(Ver 3.3 (11022016))