{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T18:43:19Z","timestamp":1783708999123,"version":"3.55.0"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,4,9]],"date-time":"2022-04-09T00:00:00Z","timestamp":1649462400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,4,9]],"date-time":"2022-04-09T00:00:00Z","timestamp":1649462400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Germany\u2019s Excellence Strategy","award":["ID 390696704"],"award-info":[{"award-number":["ID 390696704"]}]},{"name":"Germany\u2019s Excellence Strategy","award":["GRK 1763"],"award-info":[{"award-number":["GRK 1763"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2022,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The topic of this paper is the determinization problem of<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>-automata under the<jats:italic>transition-based Emerson-Lei<\/jats:italic>acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent<jats:italic>generalized B\u00fcchi automaton<\/jats:italic>(GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. The second part of the paper studies limit-determinization of TELA and we show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields<jats:italic>good-for-MDP<\/jats:italic>automata which can be used for quantitative probabilistic model checking.<\/jats:p>","DOI":"10.1007\/s11334-022-00445-7","type":"journal-article","created":{"date-parts":[[2022,4,9]],"date-time":"2022-04-09T08:02:39Z","timestamp":1649491359000},"page":"385-403","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["From Emerson-Lei automata to deterministic, limit-deterministic or good-for-MDP automata"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5855-6632","authenticated-orcid":false,"given":"Tobias","family":"John","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1692-2408","authenticated-orcid":false,"given":"Simon","family":"Jantsch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5321-9343","authenticated-orcid":false,"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1724-2586","authenticated-orcid":false,"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,4,9]]},"reference":[{"key":"445_CR1","doi-asserted-by":"crossref","unstructured":"Babiak T, Blahoudek F, Duret-Lutz A, Klein J, K\u0159et\u00ednsk\u00fd J, M\u00fcller D, Parker D, Strej\u010dek J (2015) The hanoi omega-automata format. In: Computer aided verification (CAV\u201915), LNCS. Springer","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"445_CR2","doi-asserted-by":"crossref","unstructured":"Baier C, Blahoudek F, Duret-Lutz A, Klein J, M\u00fcller D, Strej\u010dek J (2019) Generic emptiness check for fun and profit. In: Automated technology for verification and analysis (ATVA), LNCS. Springer","DOI":"10.1007\/978-3-030-31784-3_26"},{"key":"445_CR3","unstructured":"Baier C, Katoen JP (2008) Principles of model checking (representation and mind series). The MIT Press"},{"key":"445_CR4","doi-asserted-by":"crossref","unstructured":"Baier C, Kiefer S, Klein J, Kl\u00fcppelholz S, M\u00fcller D, Worrell J (2016) Markov chains and unambiguous B\u00fcchi automata. In: Computer aided verification (CAV), LNCS. Springer","DOI":"10.1007\/978-3-319-41528-4_2"},{"key":"445_CR5","unstructured":"Ben-Ari M (2008) Principles of the spin model checker. Springer-Verlag, London"},{"key":"445_CR6","unstructured":"Blahoudek F (2018) Automata for formal methods: little steps towards perfection. Ph.D. thesis, Masaryk University, Faculty of Informatics"},{"key":"445_CR7","unstructured":"Blahoudek F, Duret-Lutz A, Klokocka M, Kret\u00ednsk\u00fd M, Strejcek J (2017) Seminator: a tool for Semi-Determinization of Omega-Automata. In: International conference on logic for programming, artificial intelligence and reasoning (LPAR), EPiC Series in Computing"},{"key":"445_CR8","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-030-53291-8_2","volume-title":"Computer aided verification","author":"F Blahoudek","year":"2020","unstructured":"Blahoudek F, Duret-Lutz A, Strej\u010dek J (2020) Seminator 2 can complement generalized B\u00fcchi automata via improved semi-determinization. In: Lahiri SK, Wang C (eds) Computer aided verification. Springer International Publishing, Cham, pp 15\u201327"},{"key":"445_CR9","doi-asserted-by":"crossref","unstructured":"Blahoudek F, Major J, Strej\u010dek J (2019) LTL to smaller self-loop alternating automata and back. In: Theoretical aspects of computing (ICTAC), LNCS. Springer","DOI":"10.1007\/978-3-030-32505-3_10"},{"issue":"3","key":"445_CR10","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10009-019-00508-4","volume":"21","author":"V Bloemen","year":"2019","unstructured":"Bloemen V, Duret-Lutz A, van de Pol J (2019) Model checking with generalized Rabin and Fin-less automata. Int J Soft Tools Technol Transf 21(3):307\u2013324","journal-title":"Int J Soft Tools Technol Transf"},{"key":"445_CR11","doi-asserted-by":"crossref","unstructured":"Boker U (2018) Why these automata types? In: EPiC series in computing, 57, 143\u2013163. EasyChair","DOI":"10.29007\/c3bj"},{"key":"445_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Gaiser A, K\u0159et\u00ednsk\u00fd J (2013) Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Computer aided verification (CAV), LNCS. Springer","DOI":"10.1007\/978-3-642-39799-8_37"},{"key":"445_CR13","doi-asserted-by":"crossref","unstructured":"Colcombet T (2015) Unambiguity in automata theory. In: J.\u00a0Shallit, A.\u00a0Okhotin (eds.) Descriptional complexity of formal systems, lecture notes in computer science, pp. 3\u201318. Springer International Publishing, Cham. https:\/\/doi.org\/10.1007\/978-3-319-19225-3_1","DOI":"10.1007\/978-3-319-19225-3_1"},{"key":"445_CR14","doi-asserted-by":"crossref","unstructured":"Courcoubetis C, Yannakakis M (1988) Verifying temporal properties of finite-state probabilistic programs. In: [Proceedings 1988] 29th annual symposium on foundations of computer science, pp. 338\u2013345 . 10.1109\/SFCS.1988.21950","DOI":"10.1109\/SFCS.1988.21950"},{"issue":"4","key":"445_CR15","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42(4):857\u2013907","journal-title":"J ACM"},{"key":"445_CR16","doi-asserted-by":"crossref","unstructured":"Couvreur JM (1999) On-the-fly verification of linear temporal logic. In: Formal methods (FM), LNCS. Springer","DOI":"10.1007\/3-540-48119-2_16"},{"key":"445_CR17","unstructured":"Duret-Lutz A (2017) Contributions to LTL and $$\\omega $$-automata for model checking. Habilitation thesis, Universit\u00e9 Pierre et Marie Curie"},{"key":"445_CR18","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A, Lewkowicz A, Fauchille A, Michaud T, Renault \u00c9, Xu L (2016) Spot 2.0\u2013A framework for LTL and $$\\omega $$-automata manipulation. In: Automated technology for verification and analysis (ATVA), LNCS. Springer","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"445_CR19","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A, Poitrenaud D, Couvreur JM (2009) On-the-fly emptiness check of transition-based Streett automata. In: Automated technology for verification and analysis (ATVA), LNCS. Springer","DOI":"10.1007\/978-3-642-04761-9_17"},{"issue":"3","key":"445_CR20","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"EA Emerson","year":"1987","unstructured":"Emerson EA, Lei CL (1987) Modalities for model checking: branching time logic strikes back. Sci Comput Program 8(3):275\u2013306","journal-title":"Sci Comput Program"},{"key":"445_CR21","doi-asserted-by":"crossref","unstructured":"Esparza J, K\u0159et\u00ednsk\u00fd J, Sickert S (2018) One theorem to rule them all: a unified translation of LTL into $$\\omega $$-Automata. In: logic in computer science (LICS). ACM","DOI":"10.1145\/3209108.3209161"},{"key":"445_CR22","doi-asserted-by":"crossref","unstructured":"Giannakopoulou D, Lerda F (2002) From states to transitions: improving translation of LTL formulae to B\u00fcchi automata. In: Formal techniques for networked and distributed sytems (FORTE), LNCS. Springer","DOI":"10.1007\/3-540-36135-9_20"},{"key":"445_CR23","unstructured":"Hahn EM, Li G, Schewe S, Turrini A, Zhang L (2015) Lazy probabilistic model checking without determinisation. In: Concurrency theory (CONCUR)"},{"key":"445_CR24","doi-asserted-by":"crossref","unstructured":"Hahn EM, Perez M, Schewe S, Somenzi F, Trivedi A, Wojtczak D (2020) Good-for-MDPs automata for probabilistic analysis and reinforcement learning. In: Tools and algorithms for the construction and analysis of systems (TACAS), LNCS. Springer","DOI":"10.1007\/978-3-030-45190-5_17"},{"key":"445_CR25","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-030-30942-8_17","volume-title":"Formal methods\u2013the next 30 years, LNCS","author":"S Jantsch","year":"2019","unstructured":"Jantsch S, M\u00fcller D, Baier C, Klein J (2019) From LTL to unambiguous B\u00fcchi automata via disambiguation of alternating automata. In: ter Beek MH, McIver A, Oliveira JN (eds) Formal methods\u2013the next 30 years, LNCS. Springer International Publishing, Cham, pp 262\u2013279"},{"key":"445_CR26","doi-asserted-by":"crossref","unstructured":"John T, Jantsch S, Baier C, Kl\u00fcppelholz S (2021) Determinization and limit-determinization of emerson-lei automata. In: Z.\u00a0Hou, V.\u00a0Ganesh (eds.) Automated technology for verification and analysis (ATVA), pp. 15\u201331. Springer International Publishing, Cham . https:\/\/doi.org\/10.1007\/978-3-030-88885-5_2","DOI":"10.1007\/978-3-030-88885-5_2"},{"key":"445_CR27","doi-asserted-by":"crossref","unstructured":"John T, Jantsch S, Baier C, Kl\u00fcppelholz S (2021) Determinization and limit-determinization of Emerson-Lei automata-supplementary material (ATVA\u201921). https:\/\/doi.org\/10.6084\/m9.figshare.14838654.v1","DOI":"10.1007\/978-3-030-88885-5_2"},{"key":"445_CR28","doi-asserted-by":"crossref","unstructured":"Klein J, M\u00fcller D, Baier C, Kl\u00fcppelholz S (2014) Are good-for-games automata good for probabilistic model checking? In: Language and automata theory and applications (LATA), LNCS. Springer","DOI":"10.1007\/978-3-319-04921-2_37"},{"key":"445_CR29","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd J, Meggendorfer T, Sickert S (2018) Owl: a library for $$\\omega $$-words, automata, and LTL. In: Automated technology for verification and analysis, LNCS","DOI":"10.1007\/978-3-030-01090-4_34"},{"key":"445_CR30","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Computer aided verification (CAV), LNCS. Springer","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"445_CR31","unstructured":"L\u00f6ding C, Pirogov A (2019) Determinization of B\u00fcchi automata: unifying the approaches of Safra and Muller-Schupp. In: International colloquium on automata, languages, and programming (ICALP), leibniz international proceedings in informatics (LIPIcs)"},{"key":"445_CR32","doi-asserted-by":"crossref","unstructured":"Major J, Blahoudek F, Strej\u010dek J, Sasar\u00e1kov\u00e1 M, Zbon\u010d\u00e1kov\u00e1 T(2019) ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In: Automated technology for verification and analysis (ATVA)","DOI":"10.1007\/978-3-030-31784-3_21"},{"issue":"3","key":"445_CR33","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 (1984) Alternating finite automata on $$\\omega $$-words. Theor Comput Sci 32(3):321-330","journal-title":"Theor Comput Sci"},{"key":"445_CR34","unstructured":"M\u00fcller D (2019) Alternative automata-based approaches to probabilistic model checking. Ph.D. thesis, Technische Universit\u00e4t Dresden"},{"key":"445_CR35","doi-asserted-by":"crossref","unstructured":"M\u00fcller D, Sickert S (2017) LTL to deterministic Emerson-Lei automata. In: Games, automata, logics and formal verification (GandALF), EPTCS","DOI":"10.4204\/EPTCS.256.13"},{"key":"445_CR36","doi-asserted-by":"crossref","unstructured":"Muller DE, Schupp PE (1995) Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin. McNaughton and Safra. Theor Comput Sci 141(1):69\u2013107","DOI":"10.1016\/0304-3975(94)00214-4"},{"key":"445_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Symposium on principles of programming languages (POPL). Association for computing machinery (ACM), New York, NY, USA","DOI":"10.1145\/75277.75293"},{"issue":"3\u20134","key":"445_CR38","doi-asserted-by":"publisher","first-page":"393","DOI":"10.3233\/FI-2012-744","volume":"119","author":"RR Redziejowski","year":"2012","unstructured":"Redziejowski RR (2012) An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae 119(3\u20134):393\u2013406","journal-title":"Fundamenta Informaticae"},{"key":"445_CR39","doi-asserted-by":"crossref","unstructured":"Renkin F, Duret-Lutz A, Pommellet A (2020) Practical \u201cParitizing\u201d of Emerson-Lei automata. In: Automated technology for verification and analysis (ATVA), LNCS. Springer","DOI":"10.1007\/978-3-030-59152-6_7"},{"key":"445_CR40","unstructured":"Safra S (1989) Complexity of automata on infinite objects. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel"},{"key":"445_CR41","doi-asserted-by":"crossref","unstructured":"Safra S, Vardi MY (1989) On omega-automata and temporal logic. In: Symposium on theory of computing (STOC). Association for computing machinery (ACM), New York, NY, USA","DOI":"10.1145\/73007.73019"},{"key":"445_CR42","doi-asserted-by":"crossref","unstructured":"Schewe S, Varghese T (2012) Tight bounds for the determinisation and complementation of generalised B\u00fcchi Automata. In: Automated technology for verification and analysis (ATVA), LNCS. Springer","DOI":"10.1007\/978-3-642-33386-6_5"},{"key":"445_CR43","doi-asserted-by":"crossref","unstructured":"Sickert S, Esparza J, Jaax S, K\u0159et\u00ednsk\u00fd J (2016) Limit-deterministic B\u00fcchi automata for linear temporal logic. In: Computer aided verification (CAV), LNCS. Springer","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"445_CR44","doi-asserted-by":"crossref","unstructured":"Vardi MY (1985) Automatic verification of probabilistic concurrent finite state programs. In: Symposium on foundations of computer science (SFCS)","DOI":"10.1109\/SFCS.1985.12"}],"updated-by":[{"DOI":"10.1007\/s11334-022-00459-1","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2023,3,2]],"date-time":"2023-03-02T00:00:00Z","timestamp":1677715200000}}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00445-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-022-00445-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00445-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,21]],"date-time":"2024-09-21T21:39:57Z","timestamp":1726954797000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-022-00445-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,9]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9]]}},"alternative-id":["445"],"URL":"https:\/\/doi.org\/10.1007\/s11334-022-00445-7","relation":{"correction":[{"id-type":"doi","id":"10.1007\/s11334-022-00459-1","asserted-by":"object"}]},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,9]]},"assertion":[{"value":"24 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 April 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 March 2023","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s11334-022-00459-1","URL":"https:\/\/doi.org\/10.1007\/s11334-022-00459-1","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}