{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:25:28Z","timestamp":1743042328160,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_10","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"208-227","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Simple Rewrite System for\u00a0the\u00a0Normalization of\u00a0Linear Temporal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2983-3404","authenticated-orcid":false,"given":"Rub\u00e9n","family":"Rubio","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0280-8981","authenticated-orcid":false,"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-39176-7_6","volume-title":"Model Checking Software","author":"T Babiak","year":"2013","unstructured":"Babiak, T., Badie, T., Duret-Lutz, A., K\u0159et\u00ednsk\u00fd, M., Strej\u010dek, J.: Compositional approach to suspension and other improvements to LTL translation. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 81\u201398. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39176-7_6"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-030-99253-8_8","volume-title":"Foundations of Software Science and Computation Structures","author":"U Boker","year":"2022","unstructured":"Boker, U., Lehtinen, K., Sickert, S.: On the translation of automata to linear temporal logic. In: FoSSaCS 2022. LNCS, vol. 13242, pp. 140\u2013160. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_8"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-45138-9_26","volume-title":"Mathematical Foundations of Computer Science 2003","author":"I \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 318\u2013327. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45138-9_26"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/3-540-55719-9_97","volume-title":"Automata, Languages and Programming","author":"E Chang","year":"1992","unstructured":"Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474\u2013486. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_97"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-51803-7_36","volume-title":"Temporal Logic in Specification","author":"D Gabbay","year":"1989","unstructured":"Gabbay, D.: The declarative past and imperative future. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 409\u2013448. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51803-7_36"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543\u2013550. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"10_CR7","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":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-13754-9_12","volume-title":"Time for Verification","author":"O Maler","year":"2010","unstructured":"Maler, O.: On the Krohn-Rhodes cascaded decomposition theorem. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 260\u2013278. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13754-9_12"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Maler, O., Pnueli, A.: Tight bounds on the complexity of cascaded decomposition of automata. In: Proceedings of FOCS, pp. 672\u2013682 (1990). https:\/\/doi.org\/10.1109\/FSCS.1990.89589","DOI":"10.1109\/FSCS.1990.89589"},{"key":"10_CR10","unstructured":"Maler, O., Pnueli, A.: On the cascaded decomposition of automata, its complexity and its application to logic. Unpublished (1994). http:\/\/www-verimag.imag.fr\/maler\/Papers\/decomp.pdf"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC, pp. 377\u2013410. ACM (1990). https:\/\/doi.org\/10.1145\/93385.93442","DOI":"10.1145\/93385.93442"},{"issue":"1","key":"10_CR12","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 91\u2013130 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90041-Y","journal-title":"Theor. Comput. Sci."},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/11605157_20","volume-title":"Implementation and Application of Automata","author":"R Pel\u00e1nek","year":"2006","unstructured":"Pel\u00e1nek, R., Strej\u010dek, J.: Deeper connections between LTL and alternating automata. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 238\u2013249. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11605157_20"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-319-10575-8_2","volume-title":"Handbook of Model Checking","author":"N Piterman","year":"2018","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 27\u201373. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_2"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput. Sci. 13, 45\u201360 (1981). https:\/\/doi.org\/10.1016\/0304-3975(81)90110-9","journal-title":"Theor. Comput. Sci."},{"key":"10_CR17","unstructured":"Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. Ph.D. thesis, Technical University of Munich, Germany (2019). https:\/\/nbn-resolving.org\/urn:nbn:de:bvb:91-diss-20190801-1484932-1-4"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Sickert, S., Esparza, J.: An efficient normalisation procedure for linear temporal logic and very weak alternating automata. In: LICS, pp. 831\u2013844. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394743","DOI":"10.1145\/3373718.3394743"},{"key":"10_CR19","unstructured":"Zuck, L.D.: Past temporal logic. Ph.D. thesis, The Weizmann Institute of Science, Israel, August 1986"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:06:49Z","timestamp":1672358809000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}