Antichains for Concurrent Parameterized Games
Nathalie Bertrand, Patricia Bouyer, Gaëtan Staquet
TL;DR
This work addresses the problem of determining Eve's ability to uniformly win a reachability objective in concurrent parameterized games with an arbitrary number of opponents, a problem known to be PSPACE-complete. It reframes the challenge via the knowledge game Know_G, where Eve's knowledge about the number of opponents evolves along plays, and introduces a symbolic, antichain-based approach to compute Eve's winning region as a fixed point over antichains of knowledge sets. Two concrete algorithms are developed: a fixed-point method operating on a finite lattice of relevant knowledge sets and an iterative, operational procedure; both are proven correct and terminating and are implemented in C++20. Empirical results on large, QBF-derived arenas demonstrate scalability and highlight regimes where the antichain methods outperform the DFS baseline, while also providing the full winning region rather than a single decision predicate. The approach advances parameterized verification by enabling compact symbolic representations of knowledge and enabling efficient computation of Eve’s minimal knowledge requirements across the game graph.
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 uniform 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 algorithm 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 in C++ these two algorithms, as well as the one initially proposed, and report on their relative performances on various benchmarks.