Focus Game for Projection Temporal Logic

Focus game is applied to Prepositional 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.