From Liveness to Promptness

11 years 11 months ago
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...
Orna Kupferman, Nir Piterman, Moshe Y. Vardi
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CAV
Authors Orna Kupferman, Nir Piterman, Moshe Y. Vardi
Comments (0)