@article{Kupferman:2009aa,
    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 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 that are quite close to the standard techniques for LTL.},
    Author = {Kupferman, Orna and Piterman, Nir and Vardi, Moshe Y.},
    File = {From liveness to promptness - Kupferman2009\_Article\_FromLivenessToPromptness - a - f.pdf},
    ISBN = {1572-8102},
    Journal = {Formal Methods in System Design},
    Number = {2},
    Pages = {83--103},
    Title = {From liveness to promptness},
    URL = {https://doi.org/10.1007/s10703-009-0067-z},
    Volume = {34},
    Year = {2009},
    bdsk-url-1 = {https://doi.org/10.1007/s10703-009-0067-z},
    da = {2009/04/01},
    date-added = {2020-05-06 09:58:55 +0200},
    date-modified = {2020-05-06 09:58:55 +0200},
    id = {Kupferman2009},
    ty = {JOUR},
    doi = {10.1007/s10703-009-0067-z}
}

@article{Kupferman:2009aa, 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 thewait 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 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 that are quite close to the standard techniques for LTL.}, Author = {Kupferman, Orna and Piterman, Nir and Vardi, Moshe Y.}, File = {From liveness to promptness - Kupferman2009_Article_FromLivenessToPromptness - a - f.pdf}, ISBN = {1572-8102}, Journal = {Formal Methods in System Design}, Number = {2}, Pages = {83--103}, Title = {From liveness to promptness}, URL = {https://doi.org/10.1007/s10703-009-0067-z}, Volume = {34}, Year = {2009}, bdsk-url-1 = {https://doi.org/10.1007/s10703-009-0067-z}, da = {2009/04/01}, date-added = {2020-05-06 09:58:55 +0200}, date-modified = {2020-05-06 09:58:55 +0200}, id = {Kupferman2009}, ty = {JOUR}, doi = {10.1007/s10703-009-0067-z} }