Short witnesses and accepting lassos in ω-automata

Abstract

Emptiness checking of ω-automata is a fundamental part of the automata-theoretic toolbox and is frequently applied in many applications, most notably verification of reactive systems. In this particular application, the capability to extract accepted words or alternatively accepting runs in case of non-emptiness is particularly useful, as these have a diagnostic value. However, non-optimised such words or runs can become huge, limiting their usability in practice, thus solutions with a small representation should be preferred. In this paper, we review the known results on obtaining these and complete the complexity landscape for all commonly used automaton types. We also prove upper and lower bounds on the approximation hardness of these problems. © 2010 Springer-Verlag Berlin Heidelberg.