{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T21:44:19Z","timestamp":1790113459561,"version":"4.0.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030913830","type":"print"},{"value":"9783030913847","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91384-7_2","type":"book-chapter","created":{"date-parts":[[2021,12,2]],"date-time":"2021-12-02T13:03:12Z","timestamp":1638450192000},"page":"8-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["From Linear Temporal Logics to\u00a0B\u00fcchi Automata: The\u00a0Early and\u00a0Simple Principle"],"prefix":"10.1007","author":[{"given":"Yih-Kuen","family":"Tsay","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,1,1]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003. LNCS, vol. 2619, pp. 18\u201333. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_3","DOI":"10.1007\/3-540-36577-X_3"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second-order arithmetic. In: Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962). https:\/\/doi.org\/10.1007\/978-1-4613-8928-6_23, The doi refers to republication of the paper. In: Mac Lane S., Siefkes D. (eds) The Collected Works of J. Richard B\u00fcchi. Springer","DOI":"10.1007\/978-1-4613-8928-6_23"},{"key":"2_CR3","volume-title":"Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking. The MIT Press, Cambridge (2018)"},{"issue":"2\/3","key":"2_CR4","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods Syst. Des. 1(2\/3), 275\u2013288 (1992). https:\/\/doi.org\/10.1007\/BF00121128","journal-title":"Formal Methods Syst. Des."},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM\u201999 \u2014 Formal Methods, FM 1999. LNCS, vol. 1708, pp. 253\u2013271. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_16","DOI":"10.1007\/3-540-48119-2_16"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D. (eds.) Computer Aided Verification, CAV 1999. LNCS, vol. 1633, pp. 249\u2013260. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_23","DOI":"10.1007\/3-540-48683-6_23"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"De Wulf, M., Doyen, L., Maquet, N., Raskin, J.-F.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. LNCS, vol. 4963, pp. 63\u201377. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_6","DOI":"10.1007\/978-3-540-78800-3_6"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000 \u2014 Concurrency Theory, CONCUR 2000. LNCS, vol. 1877, pp. 153\u2013168. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44618-4_13","DOI":"10.1007\/3-540-44618-4_13"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Fritz, C.: Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating B\u00fcchi automata. In: Ibarra, O.H., Dang, Z. (eds.) Implementation and Application of Automata, CIAA 2003. LNCS, vol. 2759, pp. 35\u201348. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45089-0_5","DOI":"10.1007\/3-540-45089-0_5"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Fritz, C.: Concepts of automata construction from LTL. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005. LNCS (LNAI), vol. 3835, pp. 728\u2013742. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11591191_50","DOI":"10.1007\/11591191_50"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Gastin, P., Oddoux, Denis: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification, CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_6","DOI":"10.1007\/3-540-44585-4_6"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Gastin, P., Oddoux, D.: LTL with past and two-way very-weak alternating automata. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) Mathematical Foundations of Computer Science 2003, MFCS 2003. LNCS, vol. 2747, pp. 439\u2013448. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45138-9_38","DOI":"10.1007\/978-3-540-45138-9_38"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing and Verification XV, PSTV 1995. IAICT, pp. 3\u201318. Springer, Boston, MA (1996). https:\/\/doi.org\/10.1007\/978-0-387-34892-6_1","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Giannakopoulou, D., Lerda, F.: From States to Transitions: Improving Translation of LTL Formulae to B\u00fcchi Automata. In: Peled, D.A., Vardi, M.Y. (eds.) Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002, FORTE 2002. LNCS, vol. 2529, pp. 308\u2013326. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36135-9_20","DOI":"10.1007\/3-540-36135-9_20"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T.: Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4","DOI":"10.1007\/3-540-36387-4"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0304-3975(96)00069-2","volume":"167","author":"B Jonsson","year":"1996","unstructured":"Jonsson, B., Tsay, Y.K.: Assumption\/guarantee specifications in linear-time temporal logic. Theoret. Comput. Sci. 167, 47\u201372 (1996). https:\/\/doi.org\/10.1016\/0304-3975(96)00069-2","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) Computer Aided Verification, CAV 1993. LNCS, vol. 697, pp. 97\u2013109. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_9","DOI":"10.1007\/3-540-56922-7_9"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 383\u2013392. IEEE (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029846","DOI":"10.1109\/LICS.2002.1029846"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1985), pp. 97\u2013107. ACM (1985). https:\/\/doi.org\/10.1145\/318593.318622","DOI":"10.1145\/318593.318622"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196\u2013218. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15648-8_16"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin (1995). https:\/\/doi.org\/10.1007\/978-1-4612-4222-2","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"2_CR23","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on $$omega$$-words. Theoret. Comput. Sci. 32, 321\u2013330 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90049-5","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1989), pp. 179\u2013190. ACM (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"2_CR25","unstructured":"Rohde, G.S.: Alternating Automata and the Temporal Logic of Ordinals. Ph.D. thesis, University of Illinois at Urbana-Champaign, Champaign, IL, USA (1997). http:\/\/hdl.handle.net\/2142\/86954"},{"key":"2_CR26","unstructured":"Sistla, A.P.: Theoretical Issues in the Design and Verification of Distributed Systems. Ph.D. Thesis, Harvard (1983)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248\u2013263. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_21"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133\u2013191. MIT Press (1990). https:\/\/doi.org\/10.1016\/B978-0-444-88074-1.50009-3","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-78800-3_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y-K Tsay","year":"2008","unstructured":"Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Chan, W.-C., Luo, C.-J.: GOAL extended: towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 346\u2013350. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_26"},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1988), pp. 250\u2013259. ACM (1988). https:\/\/doi.org\/10.1145\/73560.73582","DOI":"10.1145\/73560.73582"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"MY Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238\u2013266. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60915-6_6"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) Automata, Languages and Programming, ICALP 1998. LNCS, vol. 1443, pp. 628\u2013641. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055090","DOI":"10.1007\/BFb0055090"},{"key":"2_CR33","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pp. 332\u2013344. IEEE (1986). http:\/\/hdl.handle.net\/2268\/116609"},{"issue":"1\u20132","key":"2_CR34","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. Comput. 56(1\u20132), 72\u201399 (1983). https:\/\/doi.org\/10.1016\/S0019-9958(83)80051-5","journal-title":"Inf. Comput."},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (extended abstract). In: Proceedings of the 24th Annual Symposium on Foundations of Computer Science (FOCS 1983). pp. 185\u2013194. IEEE (1983). https:\/\/doi.org\/10.1109\/SFCS.1983.51","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","Model Checking, Synthesis, and Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91384-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,2]],"date-time":"2021-12-02T13:03:20Z","timestamp":1638450200000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91384-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030913830","9783030913847"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91384-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"1 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}