From Liveness to Promptness
===========================

Liveness temporal properties state that something ``good'' eventually
happens, e.g., every request is eventually granted. In Linear Temporal
Logic (LTL), there is no a priori bound on the ``wait time'' for an
eventuality to be fulfilled. That is, $F\theta$ asserts that $\theta$
holds eventually, but there is no bound on the time when $\theta$ will
hold.  This is troubling, as designers tend to interpret an
eventuality $F\theta$ as an abstraction of a bounded eventuality
$F^{\leq k}\theta$, for an unknown $k$, and satisfaction of a liveness
property is often not acceptable unless we can bound its wait time.
We introduce here Prompt-LTL, an extension of LTL with the
prompt-eventually operator $F_p$. A system $S$ satisfies a
Prompt-LTL formula $\varphi$ if there is some bound $k$ on the wait time
for all prompt-eventually subformulas of $\varphi$ in all computations
of $S$.  We study various problems related to Prompt-LTL, including
realizability, model checking, and assume-guarantee model checking,
and show that they can be solved by techniques that are quite close to
the standard techniques for LTL.