Luc Lapointe
LMF, Saclay, France
We consider a novel graph-based problem, in which a population of arbitrary size aims at achieving a common objective. More specifically, WinPop is a synthesis problem defined by a finite graph with edges labels in { ✓ , − , ⨯ }. The instance is positive if there exists a 2D-tiling problem with vertical and horizontal constraints: the horizontal constraint reflects the possible paths in the input graph, and the vertical one encodes that a ✓-label eventually occurs, before any ⨯-label. WinPop also corresponds to the existence of a coalition strategy for a reachability objective in parameterized concurrent games.
We use algebraic tools to show that the problem can be solved in polynomial space. First we exhibit a finite semigroup whose elements summarize coalition strategies over a finite interval of population sizes. Then, we characterize the existence of winning strategies by the existence of particular elements in this semigroup.