Game Constructions that
Are Safe for Bisimulation

Marc Pauly

CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands
pauly@cwi.nl
http://www.cwi.nl/~pauly/

Abstract

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.

Dvi-file
PS-File
PDF-File
Bibtex Entry