Small witnesses, accepting lassos and winning strategies in omega-automata and games

TL;DR

This paper surveys the complexity and hardness of finding small accepting lassos, witnesses, and winning strategies in omega-automata and games, emphasizing approximation hardness relevant to practical applications.

Contribution

It completes the complexity landscape for small certificate problems in omega-automata and games, including new results on approximation hardness.

Findings

Hardness results for obtaining small certificates are surveyed.

Completes the complexity landscape for these problems.

Highlights the importance of approximation hardness in practice.

Abstract

Obtaining accepting lassos, witnesses and winning strategies in omega-automata and games with omega-regular winning conditions is an integral part of many formal methods commonly found in practice today. Despite the fact that in most applications, the lassos, witnesses and strategies found should be as small as possible, little is known about the hardness of obtaining small such certificates. In this paper, we survey the known hardness results and complete the complexity landscape for the cases not considered in the literature so far. We pay particular attention to the approximation hardness of the problems as approximate small solutions usually suffice in practice.