Game Over: The Foci Approach to LTL Satisfiability and Model Checking

Focus games have been shown to yield game-theoretical characterisations for the satisfiability and the model checking problem for various temporal logics. One of the players is given a tool – the focus – that enables him to show the regeneration of temporal operators characterised as least or greatest fixpoints. His strategy usually is build upon a priority list of formulas and, thus, is not positional. This paper defines foci games for satisfiability of LTL formulas. Strategies in these games are trivially positional since they parallelise all of the focus player's choices, thus resulting in a 1-player game in effect. The games are shown to be correct and to yield smaller (counter-)models than the focus games. Finally, foci games for model checking LTL are defined as well