Please use this identifier to cite or link to this item:
Title: From liveness to promptness
Authors: Kupferman, Orna
Piterman, Nir
Vardi, Moshe Y.
First Published: 28-Jan-2009
Publisher: Springer
Citation: Formal Methods in System Design, 2009, 34 (2), pp. 83-103.
Abstract: 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 designers 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 F p . 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 that are quite close to the standard techniques for LTL.
DOI Link: 10.1007/s10703-009-0067-z
ISSN: 0925-9856
eISSN: 1572-8102
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: © Springer Science+Business Media, LLC 2009. Deposited with reference to the publisher's archiving policy available on the SHERPA/RoMEO website. The original publication is available at
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
full.pdf210.31 kBUnknownView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.