Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
In the automata-theoretic approach to formal verification, the
satisfiability and the model-checking problems for linear temporal
logics are reduced to the nonemptiness problem of automata on infinite
words. Modifying the nonemptiness algorithm to return a shortest
witness to the nonemptiness (that is, a word of the form $uv^\omega$
that is accepted by the automaton and for which $|uv|$ is minimal) has
applications in synthesis and counterexample analysis. Unlike
shortest accepting runs, which have been studied in the literature,
the definition of shortest witnesses is semantic and is independent on
the specification formalism of the property or the system. In
particular, its robustness makes it appropriate for analyzing
counterexamples of concurrent systems.
We study the problem of finding shortest witnesses in automata with
various types of concurrency. We show that while finding shortest
witnesses is more complex than just checking nonemptiness in the
nondeterministic and in the concurrent models of computation, it is
not more complex in the alternating model. It follows that when the
system is the composition of concurrent components, finding a shortest
counterexample to its correctness is not harder than finding some
counterexample. Our results give a computational motivation to
translating temporal logic formulas to alternating automata, rather
than going all the way to nondeterministic automata.