Game Constructions that
Are Safe for Bisimulation

Marc Pauly

CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands


The notion of bisimulation is extended to {Game Logic} ( GL ), a logic for reasoning about winning strategies in 2-player games. We show that all game constructions of GL are safe for bisimulation, i.e. that an atomic bisimulation can be lifted to non-atomic games constructed by the operations of GL . As a consequence, bisimilar states satisfy the same GL -formulas.

Bibtex Entry