Title :
Focus Game for Projection Temporal Logic
Author :
Tian, Cong ; Duan, Zhenhua
Author_Institution :
ICTT & ISN Lab., Xidian Univ., Xi´´an, China
Abstract :
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.
Keywords :
computability; formal verification; game theory; temporal logic; complete normal form; focus game; model checking; normal form; prepositional projection temporal logic with infinite model; projection temporal logic; satisfiability; Analytical models; Automata; Complexity theory; Computational modeling; Explosions; Games; Nickel; game; model checking; satisfiability; temporal logic;
Conference_Titel :
Theoretical Aspects of Software Engineering (TASE), 2011 Fifth International Symposium on
Conference_Location :
Xi´an, Shaanxi
Print_ISBN :
978-1-4577-1487-0
DOI :
10.1109/TASE.2011.45
