On the determinacy of concurrent games on event structures with infinite winning sets

• A generalisation of the Gale–Stewart determinacy theorem to a partial order setting.
• A model of games on event structures where infinite winning sets are allowed.
• A new technique for constructing concurrent strategies as maps of event structures.

We consider nondeterministic concurrent games played on event structures and study their determinacy problem—the existence of winning strategies. It is known that when the winning conditions of the games are characterised by a collection of finite winning sets/plays, a restriction (called race-freedom) on the boards where the games are played guarantees determinacy. However the games may no longer be determined when the winning sets are infinite. This paper provides a study of concurrent games and nondeterministic winning strategies by analysing conditions that ensure determinacy when infinitely many events are played, that is, when the winning sets are infinite. The main result is a determinacy theorem for a class of games with a bounded concurrency property and infinite winning sets shown to be finitely decidable.