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 eventually 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 \pltl, an extension of LTL with the \emph{prompt-eventually} operator $\bF$. A system $S$ satisfies a \pltl 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 \pltl, 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.