Symbolic algorithms identify winning strategies in multiplayer games
Antichains for Concurrent Parameterized Games
Logic in Computer Science
Summary
Deciding if a player can guarantee winning in complex games with many opponents is tough and can require huge computations. The authors developed new methods using a concept called 'antichains' to efficiently find the minimal information a player needs to win such games. They made two algorithms implementing this idea and tested their performance compared to existing methods. Their work helps simplify understanding strategies in multiplayer games where moves happen at the same time.
What this means in practice
- •For game engine developers: Generate efficient winning strategies in multiplayer games with many players using fewer computational resources than before.
- •For network protocol designers: Analyze protocols with many concurrent participants by computing minimal necessary knowledge to ensure communication goals under adversarial conditions.
Authors
Nathalie Bertrand, Patricia Bouyer, Gaëtan Staquet
Abstract
Concurrent parameterized games involve a fixed yet arbitrary number of players. They are described by finite arenas in which the edges are labeled with languages that describe the possible move combinations leading from one vertex to another (n players yield a word of length n). Previous work showed that, when edge labels are regular languages, one can decide whether a distinguished player, called Eve, has a strategy to ensure a reachability objective, against any strategy profile of her arbitrarily many opponents. This decision problem is known to be PSPACE-complete. A basic ingredient in the PSPACE-membership proof is the reduction to the exponential-size knowledge game, a 2-player game that reflects the knowledge Eve has on the number of opponents. In this paper, we provide a symbolic approach, based on antichains, to compute Eve's winning region in the knowledge game. In words, it gives the minimal knowledge Eve needs at every vertex to win the concurrent parameterized reachability game. More precisely, we propose two fixed-point algorithms that compute, as an antichain, the maximal elements of the winning region for Eve in the knowledge game. We implemented these two algorithms in C++, as well as the one initially proposed, and report on their relative performances on various benchmarks.