Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

TL;DR

This paper introduces a novel method that combines strategy improvement and recursive algorithms to efficiently solve large 2.5 player parity games, addressing both reachability and parity objectives within a unified framework.

Contribution

It presents a new approach that integrates strategy improvement and recursive techniques directly on 2.5 player parity games, enabling scalable solutions for large state spaces.

Findings

Handles games with several million states

Effectively combines two algorithmic approaches

Improves scalability over existing methods

Abstract

2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that - in contrast to existing techniques - tackles both aspects with the best suited approach and works exclusively on the 2.5 player game itself. The resulting technique is powerful enough to handle games with several million states.