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 May 2010
Contact Data Privacy Policy Imprint
Home People Publications
More