Advertisement

Formal Methods in System Design

, Volume 34, Issue 2, pp 83–103 | Cite as

From liveness to promptness

  • Orna Kupferman
  • Nir Piterman
  • Moshe Y. Vardi
Article

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.

Keywords

Temporal logic Verification Liveness 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur R, Etessami K, La Torre S, Peled D (2001) Parametric temporal logic for model measuring. ACM Trans Comput Log 2(3):388–407 CrossRefMathSciNetGoogle Scholar
  2. 2.
    Alpern B, Schneider FB (1985) Defining liveness. Inform Process Lett 21:181–185 MATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Beer I, Ben-David S, Geist D, Gewirtzman R, Yoeli M (1994) Methodology and system for practical formal verification of reactive hardware. In: Proc 6th conference on computer aided verification, Stanford, June 1994. Lecture notes in computer science, vol 818. Springer, New York, pp 182–193 Google Scholar
  4. 4.
    Biere A, Artho C, Schuppan V (2002) Liveness checking as safety checking. In: Proc 7th international workshop on formal methods for industrial critical systems. Electronic notes in theoretical computer science, vol 66:2 Google Scholar
  5. 5.
    Bloem R, Gabow HN, Somenzi F (2000) An algorithm for strongly connected component analysis in nlog n symbolic steps. In: Formal methods in computer aided design. Lecture notes in computer science, vol 1954. Springer, New York, pp 37–54 CrossRefGoogle Scholar
  6. 6.
    Büchi JR, Landweber LHG (1969) Solving sequential conditions by finite-state strategies. Trans Am Math Soc 138:295–311 CrossRefGoogle Scholar
  7. 7.
    Chatterjee K, Henzinger TA (2006) Finitary winning in ω-regular games. In: Proc 12th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 3920. Springer, New York, pp 257–271 CrossRefGoogle Scholar
  8. 8.
    Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York Google Scholar
  9. 9.
    Emerson EA (1990) Temporal and modal logic. In: Van Leeuwen J (ed) Handbook of theoretical computer science, vol B. MIT Press, Cambridge, pp 997–1072, chap 16 Google Scholar
  10. 10.
    Emerson EA, Jutla C (1991) Tree automata, μ-calculus and determinacy. In: Proc 32nd IEEE symp on foundations of computer science, San Juan, October 1991, pp 368–377 Google Scholar
  11. 11.
    Emerson EA, Lei C-L (1986) Efficient model checking in fragments of the propositional μ-calculus. In: Proc 1st symp on logic in computer science, Cambridge, June 1986, pp 267–278 Google Scholar
  12. 12.
    Emerson EA, Mok AK, Sistla AP, Srinivasan J (1990) Quantitative temporal reasoning. In: Proc 2nd conference on computer aided verification. Lecture notes in computer science, vol 531. Springer, New York, pp 136–145 CrossRefGoogle Scholar
  13. 13.
    Hafer T, Thomas W (1987) Computation tree logic CTL and path quantifiers in the monadic theory of the binary tree. In: Proc 14th international coll on automata, languages, and programming. Lecture notes in computer science, vol 267. Springer, New York, pp 269–279 Google Scholar
  14. 14.
    Horn F (2007) Faster algorithms for finitary games. In: Proc 13th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 4424. Springer, New York, pp 472–484 CrossRefGoogle Scholar
  15. 15.
    Janin D, Walukiewicz I (1995) Automata for the modal μ-calculus and related results. In: Proc 20th international symp on mathematical foundations of computer science. Lecture notes in computer science. Springer, New York, pp 552–562 Google Scholar
  16. 16.
    Janin D, Walukiewicz I (1996) On the expressive completeness of the propositional μ-calculus with respect to the monadic second order logic. In: Proc 7th conference on concurrency theory. Lecture notes in computer science, vol 1119. Springer, New York, pp 263–277 Google Scholar
  17. 17.
    Kupferman O, Vardi MY (2005) Safraless decision procedures. In: Proc 46th IEEE symp on foundations of computer science, Pittsburgh, October 2005, pp 531–540 Google Scholar
  18. 18.
    Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: Specification. Springer, Berlin Google Scholar
  19. 19.
    Muller DE, Schupp PE (1995) Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theor Comput Sci 141:69–107 MATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Pnueli A (1977) The temporal logic of programs. In: Proc 18th IEEE symp on foundation of computer science, pp 46–57 Google Scholar
  21. 21.
    Pnueli A (1985) In transition from global to modular temporal reasoning about programs. In: Apt K (ed) Logics and models of concurrent systems. NATO advanced summer institutes, vol F-13. Springer, New York, pp 123–144 Google Scholar
  22. 22.
    Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proc 16th ACM symp on principles of programming languages, Austin, January 1989, pp 179–190 Google Scholar
  23. 23.
    Rabin MO (1969) Decidability of second order theories and automata on infinite trees. Trans Am Math Soc 141:1–35 MATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Sistla AP, Vardi MY, Wolper P (1987) The complementation problem for Büchi automata with applications to temporal logic. Theor Comput Sci 49:217–237 MATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Tarjan RE (1972) Depth first search and linear graph algorithms. SIAM J Comput 1(2):146–160 MATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Vardi MY (2007) Automata-theoretic model checking revisited. In: 8th international conference on verification, model checking, and abstract interpretation. Lecture notes in computer science, vol 4349. Springer, New York, pp 137–150 CrossRefGoogle Scholar
  27. 27.
    Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proc 1st symp on logic in computer science, Cambridge, June 1986, pp 332–344 Google Scholar
  28. 28.
    Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1–37 MATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2009

Authors and Affiliations

  1. 1.Hebrew UniversityJerusalemIsrael
  2. 2.Imperial CollegeLondonUK
  3. 3.Rice UniversityHoustonUSA

Personalised recommendations