Short Witnesses and Accepting Lassos in omega-automata
Rüdiger Ehlers
Emptiness checking of omega-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.
4th International Conference on Language and Automata Theory and Applications (LATA 2010).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.