Model checking games for CTL

We define model checking games for the temporal logic CTL ∗ and prove their correctness. They provide a technique for using model checking interactively in a ver-ification/specification process. Their main feature is to construct paths in a transition system stepwise. That enables them to be the basis for a local model checking algo-rithm with a natural notion of justification. However, this requires configurations of a game to contain sets of formulas. Moreover, an additional structure on these sets, called focus, has to be used to guarantee correctness.