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θ asserts that θ holds eventually, but there is no bound on the time when θ will hold. This is troubling, as s tend to interpret an eventuality Fθ as an abstraction of a bounded eventuality F≤k θ, 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 Fp. A system S satisfies a PROMPT-LTL formula ϕ if there is some bound k on the wait time for all prompt-eventually subformulas of ϕ 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 tha...

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Orna Kupferman, Nir Piterman, Moshe Y. Vardi
• Keywords: CAV 2007, Eventuality, Formal Methods, Liveness Temporal Properties, Wait Time