Promptness in $\omega$-regular Automata
=======================================
Liveness properties of on-going reactive systems assert that something
good will happen eventually. In satisfying liveness properties, there
is no bound on the ``wait time'', namely the time that may elapse
until an eventuality is fulfilled. The traditional ``unbounded''
semantics of liveness properties nicely corresponds to the classical
semantics of automata on infinite objects. Indeed, acceptance is
defined with respect to the set of states the run visits infinitely
often, with no bound on the number of transitions taken between
successive visits.
In many applications, it is important to bound the wait time in
liveness properties. Bounding the wait time by a constant is not
always possible, as the bound may not be known in advance. It may also
be very large, resulting in large specifications. Researchers have
studied {\em prompt eventualities}, where the wait time is bounded,
but the bound is not known in advance. We study the automata-theoretic
counterpart of prompt eventually. In a {\em prompt-B\"uchi} automaton,
a run $r$ is accepting if there exists a bound $k$ such that $r$
visits an accepting state every at most $k$ transitions. We study the
expressive power of nondeterministic and deterministic prompt-B\"uchi
automata, their properties, and decision problems for them.
In particular, we show that regular nondeterministic prompt B\"uchi
automata are exactly as expressive as nondeterministic
co-B\"uchi automata.