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

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Logic, Reasoning, and Knowledge
