{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T03:30:56Z","timestamp":1771471856131,"version":"3.50.1"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,7,23]],"date-time":"2022-07-23T00:00:00Z","timestamp":1658534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,7,23]],"date-time":"2022-07-23T00:00:00Z","timestamp":1658534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005713","name":"Technische Universit\u00e4t M\u00fcnchen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005713","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper, we describe a single exponential translation from limit-deterministic B\u00fcchi automata (LDBA) to DPA and show that it can be concatenated with a recent efficient translations from LTL to LDBA to yield a double exponential, \u2018Safraless\u2019 LTL-to-DPA construction. We also report on an implementation and a comparison with other LTL-to-DPA translations on several sets of formulas from the literature.<\/jats:p>","DOI":"10.1007\/s10009-022-00663-1","type":"journal-article","created":{"date-parts":[[2022,7,23]],"date-time":"2022-07-23T08:05:02Z","timestamp":1658563502000},"page":"635-659","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["From linear temporal logic and limit-deterministic B\u00fcchi automata to deterministic parity automata"],"prefix":"10.1007","volume":"24","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[]},{"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,23]]},"reference":[{"key":"663_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-28756-5_8","volume":"7214","author":"Babiak T","year":"2012","unstructured":"T, Babiak, K\u0159et\u00ednsk\u00fd, M., Reh\u00e1k, V., Strejcek, J.: LTL to B\u00fcchi automata translation: Fast and more deterministic. In: TACAS. LNCS 7214, 95\u2013109 (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_8","journal-title":"LNCS"},{"key":"663_CR2","doi-asserted-by":"publisher","first-page":"770","DOI":"10.1007\/978-3-662-49674-9_49","volume":"9636","author":"F Blahoudek","year":"2016","unstructured":"Blahoudek, F., Heizmann, M., Schewe, S., Strejcek, J., Tsai, M.: Complementing semi-deterministic B\u00fcchi automata. In: TACAS. LNCS 9636, 770\u2013787 (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_49","journal-title":"LNCS"},{"key":"663_CR3","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: E.M. Clarke, T.A. Henzinger, H.\u00a0Veith, R.\u00a0Bloem (eds.) Handbook of Model Checking, pp. 921\u2013962. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_27","DOI":"10.1007\/978-3-319-10575-8_27"},{"issue":"4","key":"663_CR4","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995). https:\/\/doi.org\/10.1145\/210332.210339","journal-title":"J. ACM"},{"key":"663_CR5","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - A framework for LTL and $$\\omega $$-automata manipulation. In: C.\u00a0Artho, A.\u00a0Legay, D.\u00a0Peled (eds.) Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9938, pp. 122\u2013129 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"663_CR6","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: M.A. Ardis, J.M. Atlee (eds.) Proceedings of the Second Workshop on Formal Methods in Software Practice, March 4-5, 1998, Clearwater Beach, Florida, USA, pp. 7\u201315. ACM (1998). https:\/\/doi.org\/10.1145\/298595.298598","DOI":"10.1145\/298595.298598"},{"key":"663_CR7","doi-asserted-by":"publisher","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J.: From LTL to deterministic automata: a safraless compositional approach. In: CAV, LNCS, vol. 8559, pp. 192\u2013208 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_13","DOI":"10.1007\/978-3-319-08867-9_13"},{"key":"663_CR8","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Raskin, J., Sickert, S.: From LTL and limit-deterministic b\u00fcchi automata to deterministic parity automata. In: A.\u00a0Legay, T.\u00a0Margaria (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201423rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10205, pp. 426\u2013442 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25","DOI":"10.1007\/978-3-662-54577-5_25"},{"key":"663_CR9","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: One theorem to rule them all: A unified translation of LTL into $$\\omega $$-automata. In: A.\u00a0Dawar, E.\u00a0Gr\u00e4del (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pp. 384\u2013393. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209161","DOI":"10.1145\/3209108.3209161"},{"issue":"3","key":"663_CR10","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10703-016-0259-2","volume":"49","author":"J Esparza","year":"2016","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Sickert, S.: From LTL to deterministic automata: a safraless compositional approach. Formal Methods in Syst. Des. 49(3), 219\u2013271 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0259-2","journal-title":"Formal Methods in Syst. Des."},{"key":"663_CR11","doi-asserted-by":"publisher","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing b\u00fcchi automata. In: CONCUR, pp. 153\u2013167 (2000). https:\/\/doi.org\/10.1007\/3-540-44618-4_13","DOI":"10.1007\/3-540-44618-4_13"},{"key":"663_CR12","unstructured":"Finkbeiner, B.: Automata, games, and verification . (2015)https:\/\/www.react.uni-saarland.de\/teaching\/automata-games-verification-15\/downloads\/notes.pdf"},{"key":"663_CR13","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.ic.2014.12.021","volume":"245","author":"S Fogarty","year":"2015","unstructured":"Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Profile trees for b\u00fcchi word automata, with application to determinization. Inf. Comput. 245, 136\u2013151 (2015). https:\/\/doi.org\/10.1016\/j.ic.2014.12.021","journal-title":"Inf. Comput."},{"key":"663_CR14","doi-asserted-by":"publisher","unstructured":"Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: SPIN. LNCS 3925, 53\u201370 (2006). https:\/\/doi.org\/10.1007\/11691617_4","DOI":"10.1007\/11691617_4"},{"key":"663_CR15","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Basset, N., Bloem, R., Brenguier, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Michaud, T., P\u00e9rez, G.A., Raskin, J., Sankur, O., Tentrup, L.: The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results. In: D.\u00a0Fisman, S.\u00a0Jacobs (eds.) Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017, EPTCS, vol. 260, pp. 116\u2013143 (2017). https:\/\/doi.org\/10.4204\/EPTCS.260.10","DOI":"10.4204\/EPTCS.260.10"},{"key":"663_CR16","unstructured":"Jacobs, S., Bloem, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, P.J., Michaud, T., Sakr, M., Sickert, S., Tentrup, L., Walker, A.: The 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, participants & results. CoRR abs\/1904.07736 (2019)"},{"key":"663_CR17","doi-asserted-by":"publisher","unstructured":"K\u00e4hler, D., Wilke, T.: Complementation, disambiguation, and determinization of b\u00fcchi automata unified. In: L.\u00a0Aceto, I.\u00a0Damg\u00e5rd, L.A. Goldberg, M.M. Halld\u00f3rsson, A.\u00a0Ing\u00f3lfsd\u00f3ttir, I.\u00a0Walukiewicz (eds.) Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games, Lecture Notes in Computer Science, vol. 5125, pp. 724\u2013735. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-70575-8_59","DOI":"10.1007\/978-3-540-70575-8_59"},{"key":"663_CR18","doi-asserted-by":"publisher","unstructured":"Kini, D., Viswanathan, M.: Limit deterministic and probabilistic automata for LTL $$\\setminus $$ GU. In: TACAS, LNCS, vol. 9035, pp. 628\u2013642 (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_57","DOI":"10.1007\/978-3-662-46681-0_57"},{"key":"663_CR19","doi-asserted-by":"crossref","unstructured":"Kret\u00ednsk\u00fd, J., Manta, A., Meggendorfer, T.: Semantic labelling and learning for parity game solving in LTL synthesis. In: ATVA, Lecture Notes in Computer Science, vol. 11781, pp. 404\u2013422. Springer (2019)","DOI":"10.1007\/978-3-030-31784-3_24"},{"key":"663_CR20","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: A library for $$\\omega $$-words, automata, and LTL. In: S.K. Lahiri, C.\u00a0Wang (eds.) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, Lecture Notes in Computer Science, vol. 11138, pp. 543\u2013550. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34","DOI":"10.1007\/978-3-030-01090-4_34"},{"key":"663_CR21","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Waldmann, C., Weininger, M.: Index appearance record for transforming rabin automata into parity automata. In: A.\u00a0Legay, T.\u00a0Margaria (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10205, pp. 443\u2013460 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_26","DOI":"10.1007\/978-3-662-54577-5_26"},{"key":"663_CR22","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Rosenberg, A.: The blowup in translating LTL to deterministic automata. In: MoChArt, LNCS, vol. 6572, pp. 85\u201394. Springer (2010)","DOI":"10.1007\/978-3-642-20674-0_6"},{"issue":"3","key":"663_CR23","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(3), 408\u2013429 (2001). https:\/\/doi.org\/10.1145\/377978.377993","journal-title":"ACM Trans. Comput. Log."},{"key":"663_CR24","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C.: Optimal bounds for transformations of omega-automata. In: C.P. Rangan, V.\u00a0Raman, R.\u00a0Ramanujam (eds.) Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13\u201315, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1738, pp. 97\u2013109. Springer (1999)","DOI":"10.1007\/3-540-46691-6_8"},{"key":"663_CR25","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Pirogov, A.: Determinization of b\u00fcchi automata: Unifying the approaches of safra and muller-schupp. In: C.\u00a0Baier, I.\u00a0Chatzigiannakis, P.\u00a0Flocchini, S.\u00a0Leonardi (eds.) 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9\u201312, 2019, Patras, Greece, LIPIcs, vol. 132, pp. 120:1\u2013120:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.120","DOI":"10.4230\/LIPIcs.ICALP.2019.120"},{"key":"663_CR26","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Pirogov, A.: New optimizations and heuristics for determinization of b\u00fcchi automata. In: Y.\u00a0Chen, C.\u00a0Cheng, J.\u00a0Esparza (eds.) Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28\u201331, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11781, pp. 317\u2013333. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_18","DOI":"10.1007\/978-3-030-31784-3_18"},{"key":"663_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-019-00349-3","author":"M Luttenberger","year":"2019","unstructured":"Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Inf (2019). https:\/\/doi.org\/10.1007\/s00236-019-00349-3","journal-title":"Acta Inf"},{"key":"663_CR28","doi-asserted-by":"publisher","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: CAV (I), pp. 578\u2013586 (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"663_CR29","doi-asserted-by":"publisher","unstructured":"M\u00fcller, D., Sickert, S.: LTL to deterministic emerson-lei automata. In: GandALF, pp. 180\u2013194 (2017). https:\/\/doi.org\/10.4204\/EPTCS.256.13","DOI":"10.4204\/EPTCS.256.13"},{"key":"663_CR30","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. (2007). https:\/\/doi.org\/10.2168\/LMCS-3(3:5)2007","DOI":"10.2168\/LMCS-3(3:5)2007"},{"issue":"3\u20134","key":"663_CR31","doi-asserted-by":"publisher","first-page":"393","DOI":"10.3233\/FI-2012-744","volume":"119","author":"RR Redziejowski","year":"2012","unstructured":"Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundam. Inf. 119(3\u20134), 393\u2013406 (2012). https:\/\/doi.org\/10.3233\/FI-2012-744","journal-title":"Fundam. Inf."},{"key":"663_CR32","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of omega-automata. In: FOCS, pp. 319\u2013327 (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"663_CR33","unstructured":"Sickert, S.: Linear temporal logic. Archive of Formal Proofs (2016). https:\/\/www.isa-afp.org\/entries\/LTL.shtml"},{"key":"663_CR34","unstructured":"Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. Ph.D. thesis, Technical University of Munich, Germany (2019). http:\/\/nbn-resolving.de\/urn:nbn:de:bvb:91-diss-20190801-1484932-1-4"},{"key":"663_CR35","doi-asserted-by":"crossref","unstructured":"Sickert, S., Esparza, J.: An efficient normalisation procedure for linear temporal logic and very weak alternating automata. In: LICS 2020 (under submission)","DOI":"10.1145\/3373718.3394743"},{"key":"663_CR36","doi-asserted-by":"publisher","unstructured":"Sickert, S., Esparza, J., Jaax, S., Kret\u00ednsk\u00fd, J.: Limit-deterministic b\u00fcchi automata for linear temporal logic. In: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, pp. 312\u2013332 (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"663_CR37","doi-asserted-by":"publisher","unstructured":"Somenzi, F., Bloem, R.: Efficient b\u00fcchi automata from LTL formulae. In: CAV, pp. 248\u2013263 (2000). https:\/\/doi.org\/10.1007\/10722167_21","DOI":"10.1007\/10722167_21"},{"issue":"3","key":"663_CR38","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for systemC. Formal Methods Syst. Des. 41(3), 236\u2013268 (2012). https:\/\/doi.org\/10.1007\/s10703-011-0139-8","journal-title":"Formal Methods Syst. Des."},{"key":"663_CR39","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338 (1985). https:\/\/doi.org\/10.1109\/SFCS.1985.12","DOI":"10.1109\/SFCS.1985.12"},{"key":"663_CR40","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332\u2013344 (1986)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00663-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00663-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00663-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T10:07:42Z","timestamp":1659434862000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00663-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,23]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["663"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00663-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,23]]},"assertion":[{"value":"7 June 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 July 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}