Justifications and a Reconstruction of Parity Game Solving Algorithms

TL;DR

This paper introduces a new operation called Justify for parity games, enabling the reconstruction of existing algorithms and advancing strategies for solving these games in formal verification.

Contribution

It defines parametrized parity games and the Justify operation, providing a unified framework to reconstruct and analyze known parity game solving algorithms.

Findings

Reconstructed three well-known algorithms using Justify

Provided a new perspective on parity game solving techniques

Enhanced understanding of strategy determination in parity games

Abstract

Parity games are infinite two-player games played on directed graphs. Parity game solvers are used in the domain of formal verification. This paper defines parametrized parity games and introduces an operation, Justify, that determines a winning strategy for a single node. By carefully ordering Justify steps, we reconstruct three algorithms well known from the literature.