Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
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 eventually to be fulfilled. That is, 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 as an abstraction of a bounded eventuality , for an unknown , and satisfaction of a liveness property is often not acceptable unless we can bound its wait time. We introduce here \pltl, an extension of LTL with the \emph{prompt-eventually} operator . A system satisfies a \pltl formula if there is some bound on the wait time for all prompt-eventually subformulas of in all computations of . We study various problems related to \pltl, 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.