University of Leicester
Browse
full.pdf (210.31 kB)

From liveness to promptness

Download (210.31 kB)
journal contribution
posted on 2012-01-30, 14:09 authored by Orna Kupferman, Nir Piterman, Moshe Y. Vardi
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.

History

Citation

Formal Methods in System Design, 2009, 34 (2), pp. 83-103.

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Version

  • AM (Accepted Manuscript)

Published in

Formal Methods in System Design

Publisher

Springer

issn

0925-9856

eissn

1572-8102

Copyright date

2009

Available date

2012-01-30

Publisher version

http://www.springerlink.com/content/2112p18440032827/

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC