On Concurrent Games with Payoff

The paper considers an extension of concurrent games with a payoff, i.e. a numerical value resulting from the interaction of two players. We extend a recent determinacy result on concurrent games [5] to a value theorem, i.e. a value that both players can get arbitrarily close to, whatever the behaviour of their opponent. This value is not reached in general, i.e. there is not always an optimal strategy for one of the players (there is for finite games). However when they exist, we show that optimal strategies are closed under composition, which opens up the possibility of computing optimal strategies for complex games compositionally from optimal strategies for their component games.