Iterative synthesis of control guards ensuring invariance and inevitability in discrete-decision games

Abstract

Reactive and hybrid systems are modeled by games where players make strategic decisions in a temporally discrete manner. The dynamics of players use dense or discrete time. In order to guarantee invariance and inevitability properties, the proponent moves are restricted by "winning guards". The winning strategy determined by these guards does not exclude any initial state from which a winning strategy exists. Sets of such initial states constitute winning regions and are defined by fixed points. The iterates which yield winning regions are structured as unions of iterates which yield winning guards. © Springer-Verlag Berlin Heidelberg 2004.