ParaGraphs

ParaGraphs is a C++20 library to compute the winning region of a concurrent parametric game. In short, a concurrent parametric game is a game on graph with n players. The first one, which we call Eve, must find a strategy from a given vertex of the game that is winning no matter the number of opponents. The edges of the graph are labeled with an action and a constraint over the number of opponents of Eve. That is, a concurrent parametric game yields infinitely many "concrete" games: one for every possible number of opponents (which is a nonzero natural). See [1] and [2] for the theoretical background.

Details on benchmarks can be found on a dedicated page.

Instructions to compile and set up the library are given on the repository's README. Once it is done, the easiest way to include everything in the correct order is to add a line #include "paragraphs/paragraphs.hpp". The namespace paragraphs will be populated with all the classes and functions.

As much as possible, the library enforces using move semantics. In particular, most of the copy assignments are disabled.

Implemented algorithms

ParaGraphs supports the following algorithms:

• The DFS-like algorithm of [1], which is called explicit in the code. This algorithm determines whether Eve has a winning strategy from the vertices that are considered initial in the provided arena. That is, it does not compute the winning region of Eve. The main entry point of this algorithm is hasWinningStrategy.
• The two antichains-based algorithms of [2]:
  • The W method which iterates over a complete lattice, called an arena-coherent set. This set is built from the constraints appearing on the edges of the arena. Two implementations of this algorithm are provided:
    • One that keeps the constraints of the arena as they are.
    • One that constructs a symbolic arena, where a constraint is represented by its index inside the lattice.
  • The WAlt method which is more operational, and computes the relevant sets on the fly (i.e., performs the unions, intersections, and set differences as needed). That is, unlike W, WAlt only considers sets that are actually needed.

More precisely, the antichains-based algorithms are split into two different groups.

• The first group keeps the arena as it is. The main loop is implemented in computeWinningRegion. Implementations in this group are expected to work with SetOfConstraints. See KPredArenaCoherentSet and KPredAlt for the implementations of W and WAlt. See also the concept KPredFunctionConstraints. Each implementation can perform its own specific computations. For instance, KPredArenaCoherentSet constructs a lattice, while KPredAlt does not.
• The second group necessarily constructs the arena-coherent set and a symbolic version of the arena (SymbolicArena). The main loop is implemented in computeWinningRegion. Implementations in this group are expected to work with SymbolicSetOfKnowledge. See KPredArenaCoherentSetSymbolic for the symbolic implementation of W. See also the concept KPredFunctionSymbolic.

Notice that both main functions have the same name. However, no confusion (for the compiler) is possible, due to the different requirements on the template arguments. Namely, the first forces to use a symbolic representation for the set of knowledges, while the second keeps the sets without abstracting them.

While ParaGraphs only supports finite unions of intervals for the constraints appearing on the edges, none of these implementations makes any assumptions about the actual type. That is, everything is hidden behind the templates arguments. Importantly, every algorithm requires that the type for the constraints satisfies the Constraint requirement.

How to extend ParaGraphs

To add more types for the constraints of the edges of a parametric arena, it suffices to create a new structure or class that satisfies the concept Constraint. As long as the required functions are implemented, the explicit and antichains-based algorithms will work out of the box with the new type.

It is also possible to overload the explicit and antichains-based algorithms, if the type allows for an approach that is more performant than the general one. To do so, define a new implementation of the classes (KPredArenaCoherentSet, KPredArenaCoherentSetSymbolic, KPredAlt, or Explicit) for the specific constraints type.

Finally, to add a new antichains-based algorithm, select which concept you want to follow between KPredFunctionConstraints (working on the concrete constraints of the arena) and KPredFunctionSymbolic (working with an arena-coherent set and a symbolic arena). Then, add a new class that satisfies the concept and call computeWinningRegion with the appropriate arguments. You can refer to the implementation of the existing algorithms for examples.

Remarks

The memory consumed by the program can only be measured under a Linux operating system. Under any other OS, the measure will always be zero.

Bibliography

[1]: Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Concurrent Parameterized Games. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 31:1-31:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPIcs.FSTTCS.2019.31

[2]: Nathalie Bertrand, Patricia Bouyer, and Gaëtan Staquet. Antichains for Concurrent Parameterized Games. https://arxiv.org/abs/2505.13460