Temporal Logic and Fair Discrete Systems

Chapter

Abstract

Temporal logic has been used by philosophers to reason about the way the world changes over time. Its modern use in specification and verification of systems describes the evolution of states of a program/design giving rise to descriptions of executions. Temporal logics can be classified by their view of the evolution of time as either linear or branching. In the linear-time view, we see time ranging over a linear total order and executions are sequences of states. When the system has multiple possible executions (due to nondeterminism or reading input) we view them as separate possible evolutions and the system has a set of possible behaviors. In the branching-time view, a point in time may have multiple possible successors and accordingly executions are tree-like structures. According to this view, a system has exactly one execution, which takes the form of a tree. We start this chapter by introducing Fair Discrete Structures, the model on which we evaluate the truth and falsity of temporal logic formulas. Fair Discrete Structures describe the states of a system and their possible evolution. We then proceed with the linear-time view and introduce Propositional Linear Temporal Logic (LTL). We explain the distinction between safety and liveness properties and introduce a hierarchy of liveness properties of increasing expressiveness. We study the expressive power of full LTL and cover extensions that increase its expressive power. We introduce algorithms for checking the satisfiability of LTL and model checking LTL. We turn to the branching-time framework and introduce Computation Tree Logic (CTL). As before, we discuss its expressive power, consider extensions, and cover satisfiability and model checking. We then dedicate some time to examples of formulas in both LTL and CTL and stress the differences between the two. We end with a formal comparison of LTL and CTL and, in view of this comparison, introduce CTL*, a hybrid of LTL and CTL that combines the linear and branching views into one logic.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987) CrossRefGoogle Scholar
  2. 2.
    Alur, R., Bouajjani, A., Esparza, J.: Model checking procedural programs. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  3. 3.
    Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  4. 4.
    Barringer, H.: Up and down the temporal way. Comput. J. 30(2), 134–148 (1987) CrossRefGoogle Scholar
  5. 5.
    Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Inform. 20, 207–226 (1983) MathSciNetCrossRefGoogle Scholar
  6. 6.
    Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  7. 7.
    Bojanczyk, M.: The common fragment of CTL and LTL needs existential modalities. In: Amadio, R.M. (ed.) Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol. 4962, pp. 172–185. Springer, Heidelberg (2008) Google Scholar
  8. 8.
    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  9. 9.
    Bryant, R.E.: Binary decision diagrams. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  10. 10.
    Carmo, J., Sernadas, A.: Branching versus linear logics yet again. Form. Asp. Comput. 2(1), 24–59 (1990) CrossRefGoogle Scholar
  11. 11.
    Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Boston (1988) MATHGoogle Scholar
  12. 12.
    Clarke, E.M., Draghicescu, I.A.: Expressibility results for linear-time and branching-time logics. In: de Bakker, G.R.J.W., de Roever, W.P. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop. LNCS, vol. 354, pp. 428–437. Springer, Heidelberg (1989) CrossRefGoogle Scholar
  13. 13.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. Trans. Program. Lang. Syst. 8(2), 244–263 (1986) CrossRefGoogle Scholar
  14. 14.
    Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  15. 15.
    Eisner, C., Fisman, D.: Functional specification of hardware via temporal logic. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  16. 16.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuven, J. (ed.) Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics (B), pp. 995–1072. Elsevier/MIT Press, Amsterdam/Cambridge (1990) Google Scholar
  17. 17.
    Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982) CrossRefGoogle Scholar
  18. 18.
    Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1–24 (1985) MathSciNetCrossRefGoogle Scholar
  19. 19.
    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986) MathSciNetCrossRefGoogle Scholar
  20. 20.
    Emerson, E.A., Lei, C.L.: Modalities for model checking: branching time strikes back. In: Symp. on Principles of Programming Languages (POPL), pp. 84–96. ACM, New York (1985) Google Scholar
  21. 21.
    Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Inf. Control 61(3), 175–201 (1984) MathSciNetCrossRefGoogle Scholar
  22. 22.
    Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: Symp. on Principles of Programming Languages (POPL), pp. 163–173. ACM, New York (1980) Google Scholar
  23. 23.
    Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series, vol. 13, pp. 477–498. Springer, Heidelberg (1985) CrossRefGoogle Scholar
  24. 24.
    Holzmann, G.J.: Explicit-state model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  25. 25.
    Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  26. 26.
    Kamp, J.: Tense logic and the theory of order. Ph.D. thesis, University of California, Los Angeles (1968) Google Scholar
  27. 27.
    Kesten, Y., Pnueli, A., Raviv, L.O., Shahar, E.: Model checking with strong fairness. Form. Methods Syst. Des. 28(1), 57–84 (2006) CrossRefGoogle Scholar
  28. 28.
    Kripke, S.: A completeness theorem in modal logic. J. Symb. Log. 24(1), 1–14 (1959) MathSciNetCrossRefGoogle Scholar
  29. 29.
    Kröger, F., Merz, S.: Temporal Logic and State Systems. Texts in Theoretical Computer Science. Springer, Heidelberg (2008) MATHGoogle Scholar
  30. 30.
    Kupferman, O.: Automata theory and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  31. 31.
    Kupferman, O., Pnueli, A.: Once and for all. In: Symp. on Logic in Computer Science (LICS), pp. 25–35 (1995) Google Scholar
  32. 32.
    Kupferman, O., Vardi, M.Y.: On bounded specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 2250, pp. 24–38. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  33. 33.
    Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000) MathSciNetCrossRefGoogle Scholar
  34. 34.
    Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Symp. on Logic in Computer Science, vol. LICS, pp. 383–392. IEEE, Piscataway (2002) Google Scholar
  35. 35.
    Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. Theor. Comput. Sci. 148(2), 303–324 (1995) MathSciNetCrossRefGoogle Scholar
  36. 36.
    Laroussinie, F., Schnoebelen, P.: Specification in CTL+past for verification in CTL. Inf. Comput. 156(1–2), 236–263 (2000) MathSciNetCrossRefGoogle Scholar
  37. 37.
    Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Logic of Programs, pp. 196–218 (1985) CrossRefGoogle Scholar
  38. 38.
    Maidl, M.: The common fragment of CTL and LTL. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 643–652. IEEE, Piscataway (2000) Google Scholar
  39. 39.
    Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: ACM Symposium on Principles of Distributed Computing, pp. 377–410 (1990) Google Scholar
  40. 40.
    Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Autom. Lang. Comb. 7(2), 225–246 (2002) MathSciNetMATHGoogle Scholar
  41. 41.
    Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981) CrossRefGoogle Scholar
  42. 42.
    Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 46–57 (1977) Google Scholar
  43. 43.
    Pnueli, A., Zaks, A.: On the merits of temporal testers. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 172–195. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  44. 44.
    Prior, A.: Time and Modality. Oxford University Press, Oxford (1957) MATHGoogle Scholar
  45. 45.
    Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Symp. on Programming. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982) CrossRefGoogle Scholar
  46. 46.
    Rabin, M.: Weakly definable relations and special automata. In: Bar-Hillel, Y. (ed.) Proc. Symp. Math. Logic and Foundations of Set Theory, pp. 1–23. North-Holland, Amsterdam (1970) Google Scholar
  47. 47.
    Seshia, S.A., Sharygina, N., Tripakis, S.: Modeling for verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  48. 48.
    Shankar, N.: Combining model checking and deduction. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  49. 49.
    Sistla, A.P.: On characterization of safety and liveness properties in temporal logic. In: Malcolm, M.A., Strong, H.R. (eds.) ACM Symposium on Principles of Distributed Computing, pp. 39–48. ACM, New York (1985) Google Scholar
  50. 50.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985) MathSciNetCrossRefGoogle Scholar
  51. 51.
    Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217–237 (1987) CrossRefGoogle Scholar
  52. 52.
    Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) Intl. Colloq. on Automata, Languages, and Programming (ICALP). LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998) CrossRefGoogle Scholar
  53. 53.
    Vardi, M.Y.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001) Google Scholar
  54. 54.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994) MathSciNetCrossRefGoogle Scholar
  55. 55.
    Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1–2), 72–99 (1983) MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.University of LeicesterLeicesterUK
  2. 2.New York UniversityNew YorkUSA
  3. 3.The Weizmann Institute of ScienceRehovotIsrael

Personalised recommendations