{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T09:10:41Z","timestamp":1774775441376,"version":"3.50.1"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030992521","type":"print"},{"value":"9783030992538","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the complexity of translating deterministic<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03c9<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular automata to LTL.<\/jats:p><jats:p>Our first contribution consists of tight bounds for LTL over a unary alphabet: alternating, nondeterministic and deterministic automata can be exactly exponentially, quadratically and linearly more succinct, respectively, than any equivalent LTL formula. Our main contribution consists of a translation of general counter-free deterministic<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03c9<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular automata into LTL formulas of double exponential temporal-nesting depth and triple exponential length, using an intermediate Krohn-Rhodes cascade decomposition of the automaton. To our knowledge, this is the first elementary bound on this translation. Furthermore, our translation preserves the acceptance condition of the automaton in the sense that it turns a looping, weak, B\u00fcchi, coB\u00fcchi or Muller automaton into a formula that belongs to the matching class of the syntactic future hierarchy. In particular, it can be used to translate an LTL formula recognising a safety language to a formula belonging to the safety fragment of LTL (over both finite and infinite words).<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_8","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"140-160","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["On the Translation of Automata to Linear Temporal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4322-8892","authenticated-orcid":false,"given":"Udi","family":"Boker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1171-8790","authenticated-orcid":false,"given":"Karoliina","family":"Lehtinen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0280-8981","authenticated-orcid":false,"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Birget, J.C.: Two-way automata and length-preserving homomorphisms. Mathematical Systems Theory 29(3), 191\u2013226 (1996)","DOI":"10.1007\/BF01201276"},{"key":"8_CR2","unstructured":"Boja\u0144czyk, M.: Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic (2020)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Boker, U.: Why these automata types? In: Proc. of LPAR. pp. 143\u2013163 (2018)","DOI":"10.29007\/c3bj"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Boker, U., Kupferman, O.: The quest for a tight translation of B\u00fcchi to co-B\u00fcchi automata. In: Fields of Logic and Computation, pp. 147\u2013164. Springer (2010)","DOI":"10.1007\/978-3-642-15025-8_8"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Boker, U., Lehtinen, K., Sickert, S.: On the translation of automata to linear temporal logic (2022), https:\/\/arxiv.org\/abs\/2201.10267, full version","DOI":"10.1007\/978-3-030-99253-8_8"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Cern\u00e1, I., Pel\u00e1nek, R.: Relating hierarchy of temporal properties to model checking. In: MFCS. Lecture Notes in Computer Science, vol.\u00a02747, pp. 318\u2013327. Springer (2003)","DOI":"10.1007\/978-3-540-45138-9_26"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (Jan 1981)","DOI":"10.1145\/322234.322243"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings. Lecture Notes in Computer Science, vol.\u00a0623, pp. 474\u2013486. Springer (1992)","DOI":"10.1007\/3-540-55719-9_97"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Chrobak, M.: Finite automata and unary languages. Theoretical Computer Science 47, 149\u2013158 (1986)","DOI":"10.1016\/0304-3975(86)90142-8"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Cohen, J., Perrin, D., Pin, J.E.: On the expressive power of temporal logic. Journal of computer and System Sciences 46(3), 271\u2013294 (1993)","DOI":"10.1016\/0022-0000(93)90005-H"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cohen-Chesnot, J.: On the expressive power of temporal logic for infinite words. Theoretical Computer Science 83(2), 301\u2013312 (1991)","DOI":"10.1016\/0304-3975(91)90281-6"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Colcombet, T., Zdanowski, K.: A tight lower bound for determinization of transition labeled B\u00fcchi automata. In: International Colloquium on Automata, Languages, and Programming. pp. 151\u2013162. Springer (2009)","DOI":"10.1007\/978-3-642-02930-1_13"},{"key":"8_CR13","unstructured":"Diekert, V., Gastin, P.: First-order definable languages. In: Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]. Texts in Logic and Games, vol.\u00a02, pp. 261\u2013306 (2008)"},{"key":"8_CR14","unstructured":"Eilenberg, S.: Automata, Languages, and Machines Volume B. Academic Press, Inc., USA (1976)"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279\u2013295 (2002)","DOI":"10.1006\/inco.2001.2953"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. of POPL. p. 163\u2013173. New York, NY, USA (1980)","DOI":"10.1145\/567446.567462"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Geffert, V., Mereghetti, C., Pighizzini, G.: Complementing two-way finite automata. Information and Computation 205(8), 1173\u20131187 (2007)","DOI":"10.1016\/j.ic.2007.01.008"},{"key":"8_CR18","unstructured":"Kamp, J.A.W.: Tense logic and the theory of linear order. University of California, Los Angeles (1968)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Rosenberg, A.: The blowup in translating LTL to deterministic automata. In: Proc. of Model Checking and Artificial Intelligence. pp. 85\u201394 (2010)","DOI":"10.1007\/978-3-642-20674-0_6"},{"key":"8_CR20","unstructured":"Kupferman, O., Ta-Shma, A., Vardi, M.Y.: Counting with automata. In: Proc. of LICS (1999)"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic (TOCL) 2(3), 408\u2013429 (2001)","DOI":"10.1145\/377978.377993"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Ladner, R.E.: Application of model theoretic games to discrete linear orders and finite automata. Information and Control 33(4), 281\u2013303 (1977)","DOI":"10.1016\/S0019-9958(77)90443-0"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Leiss, E.: Succinct representation of regular languages by boolean automata. Theoretical computer science 13(3), 323\u2013330 (1981)","DOI":"10.1016\/S0304-3975(81)80005-9"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C.: Optimal bounds for transformations of $$\\omega $$-automata. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science. pp. 97\u2013109. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)","DOI":"10.1007\/3-540-46691-6_8"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Maler, O.: On the Krohn-Rhodes cascaded decomposition theorem. In: Time for Verification, Essays in Memory of Amir Pnueli. Lecture Notes in Computer Science, vol.\u00a06200, pp. 260\u2013278. Springer (2010)","DOI":"10.1007\/978-3-642-13754-9_12"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Maler, O., Pnueli, A.: Tight bounds on the complexity of cascaded decomposition of automata. In: Proc. of FOCS. pp. 672\u2013682 (1990)","DOI":"10.1109\/FSCS.1990.89589"},{"key":"8_CR27","unstructured":"Maler, O., Pnueli, A.: On the cascaded decomposition of automata, its complexity and its application to logic. Unpublished. Available at: http:\/\/www-verimag.imag.fr\/~maler\/Papers\/decomp.pdf (1994)."},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC. pp. 377\u2013410. ACM (1990)","DOI":"10.1145\/93385.93442"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Maretic, G.P., Dashti, M.T., Basin, D.A.: LTL is closed under topological closure. Inf. Process. Lett. 114(8), 408\u2013413 (2014)","DOI":"10.1016\/j.ipl.2014.03.001"},{"key":"8_CR30","unstructured":"Markey, N.: Temporal logic with past is exponentially more succinct. Bull. EATCS 79, 122\u2013128 (2003)"},{"key":"8_CR31","unstructured":"McNaughton, R., Papert, S.A.: Counter-Free Automata (MIT research monograph no. 65). The MIT Press (1971)"},{"key":"8_CR32","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris 15 (1988)"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings Third Annual Symposium on Logic in Computer Science. pp. 422\u2013423. IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5139"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Perrin, D.: Recent results on automata and infinite words. In: International Symposium on Mathematical Foundations of Computer Science. pp. 134\u2013148. Springer (1984)","DOI":"10.1007\/BFb0030294"},{"key":"8_CR35","unstructured":"Safra, S.: Complexity of automata on infinite objects. Ph.D. thesis, Weizmann Institute, Rehovot, Israel (1989)"},{"key":"8_CR36","unstructured":"Schewe, S.: B\u00fcchi Complementation Made Tight. In: Albers, S., Marion, J.Y. (eds.) Proc. of 26th International STACS. Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a03, pp. 661\u2013672 (2009)"},{"key":"8_CR37","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3373718.3394743"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Star-free regular sets of $$\\omega $$-sequences. Information and Control 42(2), 148\u2013156 (1979)","DOI":"10.1016\/S0019-9958(79)90629-6"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Thomas, W.: A combinatorial approach to the theory of $$\\omega $$-automata. Information and Control 48(3), 261\u2013283 (1981)","DOI":"10.1016\/S0019-9958(81)90663-X"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: Formal Models and Semantics, pp. 133\u2013191. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"8_CR41","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. of LICS. pp. 332\u2013344 (1986)"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Wilke, T.: Classifying discrete temporal properties. In: Annual symposium on theoretical aspects of computer science. pp. 32\u201346. Springer (1999)","DOI":"10.1007\/3-540-49116-3_3"},{"key":"8_CR43","unstructured":"Wilke, T.: Past, present, and infinite future. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)"},{"key":"8_CR44","unstructured":"Wilke, T.: Backward deterministic B\u00fcchi automata on infinite words. In: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)"},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Temporal logic can be more expressive 56(1\u20132), 72\u201399 (1983)","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"8_CR46","unstructured":"Zuck, L.D.: Past Temporal Logic. Ph.D. thesis, The Weizmann Institute of Science, Israel (Aug 1986)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,21]],"date-time":"2024-09-21T04:22:28Z","timestamp":1726892548000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}