{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,26]],"date-time":"2026-03-26T21:28:06Z","timestamp":1774560486659,"version":"3.50.1"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_2","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"27-73","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Temporal Logic and Fair Discrete Systems"],"prefix":"10.1007","author":[{"given":"Nir","family":"Piterman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"3","key":"2_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"2_CR2","volume-title":"Handbook of Model Checking","author":"R. Alur","year":"2018","unstructured":"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)"},{"key":"2_CR3","volume-title":"Handbook of Model Checking","author":"C.W. Barrett","year":"2018","unstructured":"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)"},{"issue":"2","key":"2_CR4","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1093\/comjnl\/30.2.134","volume":"30","author":"H. Barringer","year":"1987","unstructured":"Barringer, H.: Up and down the temporal way. Comput. J. 30(2), 134\u2013148 (1987)","journal-title":"Comput. J."},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Inform. 20, 207\u2013226 (1983)","journal-title":"Acta Inform."},{"key":"2_CR6","volume-title":"Handbook of Model Checking","author":"R. Bloem","year":"2018","unstructured":"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)"},{"key":"2_CR7","series-title":"LNCS","first-page":"172","volume-title":"Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS)","author":"M. Bojanczyk","year":"2008","unstructured":"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.\u00a04962, pp.\u00a0172\u2013185. Springer, Heidelberg (2008)"},{"key":"2_CR8","volume-title":"Handbook of Model Checking","author":"P. Bouyer","year":"2018","unstructured":"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)"},{"key":"2_CR9","volume-title":"Handbook of Model Checking","author":"R.E. Bryant","year":"2018","unstructured":"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)"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/BF01888216","volume":"2","author":"J. Carmo","year":"1990","unstructured":"Carmo, J., Sernadas, A.: Branching versus linear logics yet again. Form. Asp. Comput. 2(1), 24\u201359 (1990)","journal-title":"Form. Asp. Comput."},{"key":"2_CR11","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Boston (1988)"},{"key":"2_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/BFb0013029","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School\/Workshop","author":"E.M. Clarke","year":"1989","unstructured":"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.\u00a0354, pp.\u00a0428\u2013437. Springer, Heidelberg (1989)"},{"issue":"2","key":"2_CR13","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"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\u2013263 (1986)","journal-title":"Trans. Program. Lang. Syst."},{"key":"2_CR14","volume-title":"Handbook of Model Checking","author":"L. Doyen","year":"2018","unstructured":"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)"},{"key":"2_CR15","volume-title":"Handbook of Model Checking","author":"C. Eisner","year":"2018","unstructured":"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)"},{"key":"2_CR16","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, vol.\u00a0B: Formal Models and Semantics (B)","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuven, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B: Formal Models and Semantics (B), pp.\u00a0995\u20131072. Elsevier\/MIT Press, Amsterdam\/Cambridge (1990)"},{"issue":"3","key":"2_CR17","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"2_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1\u201324 (1985)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"2_CR19","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"2_CR20","first-page":"84","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Lei, C.L.: Modalities for model checking: branching time strikes back. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a084\u201396. ACM, New York (1985)"},{"issue":"3","key":"2_CR21","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"E.A. Emerson","year":"1984","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Inf. Control 61(3), 175\u2013201 (1984)","journal-title":"Inf. Control"},{"key":"2_CR22","first-page":"163","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"D.M. Gabbay","year":"1980","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0163\u2013173. ACM, New York (1980)"},{"key":"2_CR23","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-82453-1_17","volume-title":"Logics and Models of Concurrent Systems","author":"D. Harel","year":"1985","unstructured":"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.\u00a013, pp.\u00a0477\u2013498. Springer, Heidelberg (1985)"},{"key":"2_CR24","volume-title":"Handbook of Model Checking","author":"G.J. Holzmann","year":"2018","unstructured":"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)"},{"key":"2_CR25","volume-title":"Handbook of Model Checking","author":"R. Jhala","year":"2018","unstructured":"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)"},{"key":"2_CR26","unstructured":"Kamp, J.: Tense logic and the theory of order. Ph.D. thesis, University of California, Los Angeles (1968)"},{"issue":"1","key":"2_CR27","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10703-006-4342-y","volume":"28","author":"Y. Kesten","year":"2006","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.O., Shahar, E.: Model checking with strong fairness. Form. Methods Syst. Des. 28(1), 57\u201384 (2006)","journal-title":"Form. Methods Syst. Des."},{"issue":"1","key":"2_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S. Kripke","year":"1959","unstructured":"Kripke, S.: A completeness theorem in modal logic. J. Symb. Log. 24(1), 1\u201314 (1959)","journal-title":"J. Symb. Log."},{"key":"2_CR29","series-title":"Texts in Theoretical Computer Science","volume-title":"Temporal Logic and State Systems","author":"F. Kr\u00f6ger","year":"2008","unstructured":"Kr\u00f6ger, F., Merz, S.: Temporal Logic and State Systems. Texts in Theoretical Computer Science. Springer, Heidelberg (2008)"},{"key":"2_CR30","volume-title":"Handbook of Model Checking","author":"O. Kupferman","year":"2018","unstructured":"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)"},{"key":"2_CR31","first-page":"25","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"O. Kupferman","year":"1995","unstructured":"Kupferman, O., Pnueli, A.: Once and for all. In: Symp. on Logic in Computer Science (LICS), pp.\u00a025\u201335 (1995)"},{"key":"2_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45653-8_2","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"O. Kupferman","year":"2001","unstructured":"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.\u00a02250, pp.\u00a024\u201338. Springer, Heidelberg (2001)"},{"issue":"2","key":"2_CR33","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"2_CR34","first-page":"383","volume-title":"Symp. on Logic in Computer Science","author":"F. Laroussinie","year":"2002","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Symp. on Logic in Computer Science, vol.\u00a0LICS, pp.\u00a0383\u2013392. IEEE, Piscataway (2002)"},{"issue":"2","key":"2_CR35","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/0304-3975(95)00035-U","volume":"148","author":"F. Laroussinie","year":"1995","unstructured":"Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. Theor. Comput. Sci. 148(2), 303\u2013324 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"2_CR36","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1006\/inco.1999.2817","volume":"156","author":"F. Laroussinie","year":"2000","unstructured":"Laroussinie, F., Schnoebelen, P.: Specification in CTL+past for verification in CTL. Inf. Comput. 156(1\u20132), 236\u2013263 (2000)","journal-title":"Inf. Comput."},{"key":"2_CR37","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logic of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Logic of Programs, pp.\u00a0196\u2013218 (1985)"},{"key":"2_CR38","first-page":"643","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"M. Maidl","year":"2000","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0643\u2013652. IEEE, Piscataway (2000)"},{"key":"2_CR39","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/93385.93442","volume-title":"ACM Symposium on Principles of Distributed Computing","author":"Z. Manna","year":"1990","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: ACM Symposium on Principles of Distributed Computing, pp.\u00a0377\u2013410 (1990)"},{"issue":"2","key":"2_CR40","first-page":"225","volume":"7","author":"D. Peled","year":"2002","unstructured":"Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Autom. Lang. Comb. 7(2), 225\u2013246 (2002)","journal-title":"J. Autom. Lang. Comb."},{"issue":"3","key":"2_CR41","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"2_CR42","first-page":"46","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a046\u201357 (1977)"},{"key":"2_CR43","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-69850-0_11","volume-title":"25 Years of Model Checking","author":"A. Pnueli","year":"2008","unstructured":"Pnueli, A., Zaks, A.: On the merits of temporal testers. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a0172\u2013195. Springer, Heidelberg (2008)"},{"key":"2_CR44","volume-title":"Time and Modality","author":"A. Prior","year":"1957","unstructured":"Prior, A.: Time and Modality. Oxford University Press, Oxford (1957)"},{"key":"2_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Symp. on Programming","author":"J.P. Queille","year":"1982","unstructured":"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.\u00a0137, pp.\u00a0337\u2013351. Springer, Heidelberg (1982)"},{"key":"2_CR46","first-page":"1","volume-title":"Proc. Symp. Math. Logic and Foundations of Set Theory","author":"M. Rabin","year":"1970","unstructured":"Rabin, M.: Weakly definable relations and special automata. In: Bar-Hillel, Y. (ed.) Proc. Symp. Math. Logic and Foundations of Set Theory, pp.\u00a01\u201323. North-Holland, Amsterdam (1970)"},{"key":"2_CR47","volume-title":"Handbook of Model Checking","author":"S.A. Seshia","year":"2018","unstructured":"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)"},{"key":"2_CR48","volume-title":"Handbook of Model Checking","author":"N. Shankar","year":"2018","unstructured":"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)"},{"key":"2_CR49","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/323596.323600","volume-title":"ACM Symposium on Principles of Distributed Computing","author":"A.P. Sistla","year":"1985","unstructured":"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.\u00a039\u201348. ACM, New York (1985)"},{"issue":"3","key":"2_CR50","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"2_CR51","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR52","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"Intl. Colloq. on Automata, Languages, and Programming (ICALP)","author":"M.Y. Vardi","year":"1998","unstructured":"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.\u00a01443, pp.\u00a0628\u2013641. Springer, Heidelberg (1998)"},{"key":"2_CR53","series-title":"LNCS","first-page":"1","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M.Y. Vardi","year":"2001","unstructured":"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.\u00a02031, pp.\u00a01\u201322. Springer, Heidelberg (2001)"},{"issue":"1","key":"2_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"issue":"1\u20132","key":"2_CR55","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1\u20132), 72\u201399 (1983)","journal-title":"Inf. Control"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T18:18:36Z","timestamp":1693678716000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_2","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}