Improved Algorithms for Parity and Streett objectives

TL;DR

This paper introduces faster algorithms for computing winning sets in graphs and game graphs with parity and Streett objectives, significantly improving efficiency for dense graphs and marking the first such improvements in 15 years.

Contribution

It presents novel algorithms that reduce the computational complexity of solving parity-3 and k-pair Streett objectives in graphs and game graphs.

Findings

Faster algorithms for parity-3 objectives in game graphs (O(n^{5/2}))

Improved algorithms for k-pair Streett objectives in graphs (O(n^2 + nk log n))

First asymptotic improvements in 15 years for these problems.

Abstract

The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on $n$ vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time $O(n^{5/2})$ and for (2) k-pair Streett objectives in graphs in time $O(n^2 + nk \log n)$. For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years.