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 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 prompt-Büchi 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üchi automata, their properties, their relation to prompt temporal logic, and decision problems for them.
In particular, we show that regular nondeterministic prompt Büchi automata have equivalent nondeterministic Büchi automata on the same structure, and are exactly as expressive as nondeterministic co-Büchi automata. Also, we show that the regularity (is the language of a given prompt-Büchi automaton regular), universality, and containment problems for nondeterministic prompt Büchi automata are PSPACE-complete.