Avoiding Distractions in Parity Games

We consider algorithms for parity games that use attractor decomposition, such as Zielonka’s recursive algorithm, priority promotion, and tangle learning. In earlier work, we identified the Two Counters parity game family that requires exponential time for many algorithms, including attractor decomposition algorithms, and we identified the main mechanism that slows down parity game algorithms as so-called distractions. We observe a fundamentally different approach in avoiding distractions between algorithms that use attractor decomposition and algorithms that compute progress measures. We now propose an alternative attractor-based method to avoid distractions by applying the attractor decomposition recursively. We demonstrate that this algorithm solves the Two Counters games efficiently, but that a modification of the Two Counters method can also delay the recursive algorithm exponentially.

1. 1.

   See generators counter_ortl and tc+ at https://www.github.com/trolando/oink.

2. 2.

   Available online via https://www.github.com/trolando/oink.

3. 3.

   Available online via https://www.github.com/trolando/oink.

Authors and Affiliations

1. Formal Methods and Tools, University of Twente, Enschede, The Netherlands

   Tom van Dijk

Corresponding author

Correspondence to Tom van Dijk .

Editors and Affiliations

1. University of Limerick, CSIS and Lero, Limerick, Ireland

   Tiziana Margaria

2. TU Dortmund University, Dortmund, Germany

   Bernhard Steffen

Data Availability Statement

The software, benchmarks and analysed dataset are available as [11] and on Github as: https://github.com/trolando/rtl-experiments. In addition, the version of the algorithms studied in the current paper is tagged in the Github repository of Oink as: https://github.com/trolando/oink/tree/ISOLA24.

Optimizations

We describe several optimizations for large practical games. These optimizations are all implemented in Oink^{Footnote 3}. Some of these optimizations were already described in the original paper on tangle learning [8].

1. 1.

   After attracting to all vertices of the highest priority: if the next highest priority is of the same parity, we simply continue attracting.

2. 2.

   To check if a region is closed, we only check the top vertices (that we attracted towards). We already know that attracted vertices of player \(\alpha \) play to the region and that attracted vertices of player \({\overline{\alpha }}\) cannot escape to the remaining subgame.

3. 3.

   If the highest region in the game is closed, then we immediately add it to the corresponding winning region and remove it from the game.

4. 4.

   We do not need to check if the lowest region is open, as it is always closed.

5. 5.

   When attracting vertices and tangles, we track the number of remaining edges towards the remaining game; when this number is 0, the vertex of player \({\overline{\alpha }}\) or the tangle can be attracted.

6. 6.

   We only run Tarjan’s algorithm starting from the top vertices. Tarjan’s algorithm may find SCCs that are existing tangles; in the example of Fig. 2b, if we had learned the tangle \(\{2,1\rightarrow 2\}\) before and we attracted that tangle to region 6 instead of attracting 1 to 8, then region 6 would be closed and contain two SCCs, but only one new tangle. We can avoid duplicate tangles by only running Tarjan’s algorithm starting from the top vertices.

7. 7.

   When running Tarjan’s algorithm, we immediately add dominions to a special queue so they can be processed afterwards, instead of separating dominions from other tangles later.

8. 8.

   An optional optimization that improves the solver for some parity games, but delays it for other parity games: if a region is open, remove all open vertices O and iteratively remove all player \({\overline{\alpha }}\) controlled vertices with an edge to the removed vertices and all player \(\alpha \) controlled vertices which have as the attractor strategy to play to a removed vertex. The remaining vertices, if any, now form a closed region from which new tangles can be obtained.

9. 9.

   If a tangle overlaps with a winning region, we delete the tangle on-the-fly.

Most optimizations for tl also work for rtl. Optimization 5 does not fully work; we need to reset the number of remaining edges for the recursion. Optimization 8 is obviously replaced with the recursive decomposition. For ortl, additionally, optimization 4 no longer works, as the lowest region could still be open. We include these optimizations even though we are not primarily interested in the practical performance of the proposed algorithms. The algorithms are slower on practical games because they perform extra work that is not necessary. They are only faster on games that are designed to be hard for other algorithms.

Reprints and permissions

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics