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.
Comment by Nir Piterman: Sadly, during the preparation of this manuscript, in November 2009, Amir passed away. While I tried to keep the chapter in the spirit of our plans I cannot be sure that Amir would have agreed with the final outcome. All faults and inaccuracies are definitely my own. In addition, opinions or judgements passed in this chapter may not reflect Amir’s view. I would like to take this opportunity to convey my deep gratitude to Amir; my teacher, supervisor, mentor, and friend.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)
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)
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)
Barringer, H.: Up and down the temporal way. Comput. J. 30(2), 134–148 (1987)
Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Inform. 20, 207–226 (1983)
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)
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)
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)
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)
Carmo, J., Sernadas, A.: Branching versus linear logics yet again. Form. Asp. Comput. 2(1), 24–59 (1990)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Boston (1988)
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)
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)
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)
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)
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)
Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982)
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)
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)
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)
Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Inf. Control 61(3), 175–201 (1984)
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)
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)
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)
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)
Kamp, J.: Tense logic and the theory of order. Ph.D. thesis, University of California, Los Angeles (1968)
Kesten, Y., Pnueli, A., Raviv, L.O., Shahar, E.: Model checking with strong fairness. Form. Methods Syst. Des. 28(1), 57–84 (2006)
Kripke, S.: A completeness theorem in modal logic. J. Symb. Log. 24(1), 1–14 (1959)
Kröger, F., Merz, S.: Temporal Logic and State Systems. Texts in Theoretical Computer Science. Springer, Heidelberg (2008)
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)
Kupferman, O., Pnueli, A.: Once and for all. In: Symp. on Logic in Computer Science (LICS), pp. 25–35 (1995)
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)
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)
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)
Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. Theor. Comput. Sci. 148(2), 303–324 (1995)
Laroussinie, F., Schnoebelen, P.: Specification in CTL+past for verification in CTL. Inf. Comput. 156(1–2), 236–263 (2000)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Logic of Programs, pp. 196–218 (1985)
Maidl, M.: The common fragment of CTL and LTL. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 643–652. IEEE, Piscataway (2000)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: ACM Symposium on Principles of Distributed Computing, pp. 377–410 (1990)
Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Autom. Lang. Comb. 7(2), 225–246 (2002)
Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)
Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 46–57 (1977)
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)
Prior, A.: Time and Modality. Oxford University Press, Oxford (1957)
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)
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)
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)
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)
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)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)
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)
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)
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)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)
Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1–2), 72–99 (1983)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Piterman, N., Pnueli, A. (2018). Temporal Logic and Fair Discrete Systems. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-10575-8_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10574-1
Online ISBN: 978-3-319-10575-8
eBook Packages: Computer ScienceComputer Science (R0)