{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T18:01:51Z","timestamp":1771696911482,"version":"3.50.1"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2021,10,1]],"date-time":"2021-10-01T00:00:00Z","timestamp":1633046400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T00:00:00Z","timestamp":1639526400000},"content-version":"vor","delay-in-days":75,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["CRC 912"],"award-info":[{"award-number":["CRC 912"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660 as part of TRR 248"],"award-info":[{"award-number":["389792660 as part of TRR 248"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["BA-1679\/12-1"],"award-info":[{"award-number":["BA-1679\/12-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["EXC 2050\/1 (CeTI, project ID 390696704)"],"award-info":[{"award-number":["EXC 2050\/1 (CeTI, project ID 390696704)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Research Training Group QuantLA (GRK 1763)"],"award-info":[{"award-number":["Research Training Group QuantLA (GRK 1763)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Due to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of \u201crestricted\u201d nondeterminism have been considered with the aim of maintaining some of the benefits of deterministic automata, while at the same time allowing more efficient translations from LTL. One of them is the notion of <jats:italic>unambiguity<\/jats:italic>. This paper proposes a new algorithm for the generation of unambiguous B\u00fcchi automata (UBA) from LTL formulas. Unlike other approaches it is based on a known translation from <jats:italic>very weak alternating automata<\/jats:italic> (VWAA) to NBA. A notion of unambiguity for alternating automata is introduced and it is shown that the VWAA-to-NBA translation preserves unambiguity. Checking unambiguity of VWAA is determined to be PSPACE-complete, both for the explicit and symbolic encodings of alternating automata. The core of the LTL-to-UBA translation is an iterative disambiguation procedure for VWAA. Several heuristics are introduced for different stages of the procedure. We report on an implementation of our approach in the tool  and compare it to an existing LTL-to-UBA implementation in the  tool set. Our experiments cover model checking of Markov chains, which is an important application of UBA.<\/jats:p>","DOI":"10.1007\/s10703-021-00379-z","type":"journal-article","created":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T16:03:04Z","timestamp":1639584184000},"page":"42-82","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["From LTL to unambiguous B\u00fcchi automata via disambiguation of alternating automata"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1692-2408","authenticated-orcid":false,"given":"Simon","family":"Jantsch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,12,15]]},"reference":[{"key":"379_CR1","doi-asserted-by":"publisher","unstructured":"Artale A, Kontchakov R, Ryzhikov V, Zakharyaschev M (2013) The complexity of clausal fragments of LTL. In: McMillan K, Middeldorp A, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning, pp 35\u201352. Lecture notes in computer science. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-45221-5_3","DOI":"10.1007\/978-3-642-45221-5_3"},{"key":"379_CR2","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: Proceedings of the 27th international conference on computer aided verification (CAV). Lecture notes in computer science, vol\u00a09206. Springer, pp 479\u2013486","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"379_CR3","doi-asserted-by":"crossref","unstructured":"Babiak T, K\u0159et\u00ednsk\u00fd M, \u0158eh\u00e1k V, Strejc\u0306ek J (2012) LTL to B\u00fcchi automata translation: fast and more deterministic. In: Proceedings of the 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol\u00a07214. Springer, pp 95\u2013109","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"379_CR4","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press, London"},{"key":"379_CR5","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: Proceedings of the 28th international conference on computer aided verification (CAV)\u2014part I. Lecture notes in computer science, vol\u00a09779. Springer, pp 23\u201342","DOI":"10.1007\/978-3-319-41528-4_2"},{"key":"379_CR6","doi-asserted-by":"publisher","unstructured":"Bauland M, Schneider T, Schnoor H, Schnoor I, Vollmer H (Jan 2009) The complexity of generalized satisfiability for linear temporal logic. Log Methods Comput Sci 5(1):1 https:\/\/doi.org\/10.2168\/LMCS-5(1:1)2009","DOI":"10.2168\/LMCS-5(1:1)2009"},{"key":"379_CR7","doi-asserted-by":"crossref","unstructured":"Benedikt M, Lenhardt R, Worrell J (2013) LTL model checking of interval Markov chains. In: Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol\u00a07795. Springer, pp 32\u201346","DOI":"10.1007\/978-3-642-36742-7_3"},{"key":"379_CR8","doi-asserted-by":"crossref","unstructured":"Bousquet N, L\u00f6ding C (2010) Equivalence and inclusion problem for strongly unambiguous B\u00fcchi automata. In: Proceedings of the 4th international conference on language and automata theory and applications (LATA). Lecture notes in computer science, vol\u00a06031. Springer, pp 118\u2013129","DOI":"10.1007\/978-3-642-13089-2_10"},{"issue":"1\u20133","key":"379_CR9","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/S0304-3975(02)00618-7","volume":"297","author":"O Carton","year":"2003","unstructured":"Carton O, Michel M (2003) Unambiguous B\u00fcchi automata. Theor Comput Sci 297(1\u20133):37\u201381","journal-title":"Theor Comput Sci"},{"key":"379_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model checking","author":"EM Clarke","year":"2001","unstructured":"Clarke EM, Grumberg O, Peled DA (2001) Model checking. MIT Press, London"},{"key":"379_CR11","doi-asserted-by":"crossref","unstructured":"Colcombet T (2015) Unambiguity in automata theory. In: Proceedings of the 17th international workshop on descriptional complexity of formal systems (DCFS). Lecture notes in computer science, vol\u00a09118. Springer, pp 3\u201318","DOI":"10.1007\/978-3-319-19225-3_1"},{"key":"379_CR12","doi-asserted-by":"crossref","unstructured":"Couvreur J (1999) On-the-fly verification of linear temporal logic. In: Proceedings of the world congress on formal methods in the development of computing systems (FM). Lecture notes in computer science, vol\u00a01708. Springer, pp 253\u2013271","DOI":"10.1007\/3-540-48119-2_16"},{"key":"379_CR13","doi-asserted-by":"crossref","unstructured":"Couvreur J, Saheb N, Sutre G (2003) An optimal automata approach to LTL model checking of probabilistic systems. In: Proceedings of the 10th international conference on logic for programming artificial intelligence and reasoning (LPAR). Lecture notes in computer science, vol\u00a02850. Springer, pp 361\u2013375","DOI":"10.1007\/978-3-540-39813-4_26"},{"key":"379_CR14","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A (2013) Manipulating LTL formulas using Spot 1.0. In: Proceedings of the 11th international symposium on automated technology for verification and analysis (ATVA). Lecture notes in computer science, vol\u00a08172. Springer, pp 442\u2013445","DOI":"10.1007\/978-3-319-02444-8_31"},{"key":"379_CR15","unstructured":"Duret-Lutz A (2017) Contributions to LTL and $$\\omega $$-automata for model checking. Habilitation thesis, Universit\u00e9 Pierre et Marie Curie (Paris 6)"},{"key":"379_CR16","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A, Lewkowicz A, Fauchille A, Michaud T, Renault E, Xu L (Oct 2016) Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Proceedings of the 14th international symposium on automated technology for verification and analysis (ATVA). Lecture notes in computer science, vol\u00a09938. Springer, pp 122\u2013129","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"379_CR17","doi-asserted-by":"crossref","unstructured":"Etessami K, Holzmann G (2000) Optimizing B\u00fcchi automata. In: Proceedings of the 11th international conference on concurrency theory (CONCUR). Lecture notes in computer science, vol\u00a01877. Springer, pp 153\u2013167","DOI":"10.1007\/3-540-44618-4_13"},{"key":"379_CR18","doi-asserted-by":"crossref","unstructured":"Gastin P, Oddoux D (2001) Fast LTL to B\u00fcchi automata translation. In: Proceedings of the 13th international conference on computer aided verification (CAV). Lecture notes in computer science, vol\u00a02102. Springer, pp 53\u201365","DOI":"10.1007\/3-540-44585-4_6"},{"key":"379_CR19","doi-asserted-by":"crossref","unstructured":"Gerth R, Peled D, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the 15th IFIP WG6.1 international symposium on protocol specification (PSTV). IFIP conference proceedings, vol\u00a038. Chapman & Hall, pp 3\u201318","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"379_CR20","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del E, Thomas W, Wilke T (eds) (2002) Automata, logics, and infinite games: a guide to current research. Lecture notes in computer science, vol\u00a02500. Springer","DOI":"10.1007\/3-540-36387-4"},{"key":"379_CR21","unstructured":"Hahn EM, Li G, Schewe S, Turrini A, Zhang L (2015) Lazy probabilistic model checking without determinisation. In: 26th international conference on concurrency theory (CONCUR 2015). Leibniz international proceedings in informatics (LIPIcs), vol\u00a042, pp 354\u2013367. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany"},{"key":"379_CR22","doi-asserted-by":"crossref","unstructured":"Haverkort BR, Hermanns H, Katoen JP (2000) On the use of model checking techniques for dependability evaluation. In: 19th IEEE symposium on reliable distributed systems (SRDS). IEEE Computer Society, pp 228\u2013237","DOI":"10.1109\/RELDI.2000.885410"},{"issue":"14\u201315","key":"379_CR23","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1016\/j.ipl.2012.04.010","volume":"112","author":"D Isaak","year":"2012","unstructured":"Isaak D, L\u00f6ding C (2012) Efficient inclusion testing for simple classes of unambiguous $$\\omega $$-automata. Inf Process Lett 112(14\u201315):578\u2013582","journal-title":"Inf Process Lett"},{"key":"379_CR24","doi-asserted-by":"publisher","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\u2014the next 30 years. Lecture notes in computer science. Springer, Cham, pp. 262\u2013279. https:\/\/doi.org\/10.1007\/978-3-030-30942-8_17,","DOI":"10.1007\/978-3-030-30942-8_17"},{"issue":"1","key":"379_CR25","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10817-007-9067-0","volume":"39","author":"H Kleine B\u00fcning","year":"2007","unstructured":"Kleine B\u00fcning H, Subramani K, Zhao X (2007) Boolean functions as models for quantified Boolean formulas. J Autom Reason 39(1):49\u201375. https:\/\/doi.org\/10.1007\/s10817-007-9067-0","journal-title":"J Autom Reason"},{"key":"379_CR26","unstructured":"Kret\u00ednsk\u00fd J, Meggendorfer T, Sickert S (2018) LTL store: Repository of LTL formulae from literature and case studies. CoRR abs\/1807.03296. arXiv:1807.03296"},{"key":"379_CR27","doi-asserted-by":"crossref","unstructured":"Kupferman O, Rosenberg A (2011) The blow-up in translating LTL to deterministic automata. In: Proceedings of the 6th international workshop on model checking and artificial intelligence (MoChArt). Lecture notes in computer science, vol\u00a06572. Springer, pp 85\u201394","DOI":"10.1007\/978-3-642-20674-0_6"},{"issue":"2","key":"379_CR28","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/1055686.1055689","volume":"6","author":"O Kupferman","year":"2005","unstructured":"Kupferman O, Vardi MY (2005) From linear time to branching time. Trans Comput Logic 6(2):273\u2013294","journal-title":"Trans Comput Logic"},{"key":"379_CR29","doi-asserted-by":"crossref","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2012) The PRISM benchmark suite. In: Proceedings of the 9th international conference on quantitative evaluation of systems (QEST). IEEE Computer Society, pp 203\u2013204","DOI":"10.1109\/QEST.2012.14"},{"issue":"3","key":"379_CR30","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0020-0190(00)00183-6","volume":"79","author":"C L\u00f6ding","year":"2001","unstructured":"L\u00f6ding C (2001) Efficient minimization of deterministic weak $$\\omega $$-automata. Inf Process Lett 79(3):105\u2013109","journal-title":"Inf Process Lett"},{"key":"379_CR31","doi-asserted-by":"crossref","unstructured":"L\u00f6ding C, Thomas W (2000) Alternating automata and logics over infinite words. In: Theoretical computer science: exploring new frontiers of theoretical informatics IFIP TCS, pp 521\u2013535","DOI":"10.1007\/3-540-44929-9_36"},{"issue":"6","key":"379_CR32","doi-asserted-by":"publisher","first-page":"847","DOI":"10.1142\/S0129054113400224","volume":"24","author":"M Mohri","year":"2013","unstructured":"Mohri M (2013) On the disambiguation of finite automata and functional transducers. Int J Found Comput Sci 24(6):847\u2013862","journal-title":"Int J Found Comput Sci"},{"key":"379_CR33","doi-asserted-by":"crossref","unstructured":"M\u00fcller D, Sickert S (2017) LTL to deterministic Emerson-Lei automata. In: Proceedings of the 8th international symposium on games, automata, logics and formal verification (GandALF). Electronic proceedings in theoretical computer science, vol.\u00a0256. Open Publishing Association, pp 180\u2013194","DOI":"10.4204\/EPTCS.256.13"},{"key":"379_CR34","doi-asserted-by":"crossref","unstructured":"Muller DE, Saoudi A, Schupp PE (1988) Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of the third annual symposium on logic in computer science (LICS), pp 422\u2013427","DOI":"10.1109\/LICS.1988.5139"},{"key":"379_CR35","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"DE Muller","year":"1987","unstructured":"Muller DE, Schupp PE (1987) Alternating automata on infinite trees. Theoret Comput Sci 54:267\u2013276","journal-title":"Theoret Comput Sci"},{"issue":"1&2","key":"379_CR36","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"DE Muller","year":"1995","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 & 2):69\u2013107","journal-title":"Theor Comput Sci"},{"key":"379_CR37","doi-asserted-by":"publisher","unstructured":"Muscholl A, Walukiewicz I (2005) An NP-complete fragment of LTL. In: Calude CS, Calude E, Dinneen MJ (eds) Developments in language theory. Lecture notes in computer science. Springer, Heidelberg, pp 334\u2013344. https:\/\/doi.org\/10.1007\/978-3-540-30550-7_28","DOI":"10.1007\/978-3-540-30550-7_28"},{"key":"379_CR38","doi-asserted-by":"crossref","unstructured":"Safra S (1988) On the complexity of $$\\omega $$-automata. In: Proceedings of the 29th symposium on foundations of computer science (FOCS). IEEE Computer Society, pp 319\u2013327","DOI":"10.1109\/SFCS.1988.21948"},{"key":"379_CR39","doi-asserted-by":"publisher","unstructured":"Schobbens PY, Raskin JF (1999) The logic of \u201cinitially\u201d and \u201cnext\u201d: complete axiomatization and complexity. Inform Process Lett 69(5):221\u2013225 https:\/\/doi.org\/10.1016\/S0020-0190(99)00022-8","DOI":"10.1016\/S0020-0190(99)00022-8"},{"issue":"3","key":"379_CR40","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla AP, Clarke EM (1985) The complexity of propositional linear temporal logics. J ACM (JACM) 32(3):733\u2013749. https:\/\/doi.org\/10.1145\/3828.3837","journal-title":"J ACM (JACM)"},{"key":"379_CR41","doi-asserted-by":"crossref","unstructured":"Somenzi F, Bloem R (2000) Efficient B\u00fcchi automata from LTL formulae. In: Proceedings of the 12th international conference on computer aided verification (CAV). Lecture notes in computer science, vol.\u00a01855. Springer, pp 248\u2013263","DOI":"10.1007\/10722167_21"},{"key":"379_CR42","doi-asserted-by":"crossref","unstructured":"Stearns RE, Hunt HB (1985) On the equivalence and containment problem for unambiguous regular expressions, grammars, and automata. SIAM J Comput, pp 598\u2013611","DOI":"10.1137\/0214044"},{"key":"379_CR43","doi-asserted-by":"crossref","unstructured":"Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the 26th IEEE symposium on foundations of computer science (FOCS). IEEE Computer Society, pp 327\u2013338","DOI":"10.1109\/SFCS.1985.12"},{"key":"379_CR44","doi-asserted-by":"crossref","unstructured":"Vardi MY (1994) Nontraditional applications of automata theory. In: Proceedings of the international conference on theoretical aspects of computer software (TACS), pp 575\u2013597","DOI":"10.1007\/3-540-57887-0_116"},{"key":"379_CR45","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the 1st symposium on logic in computer science (LICS). IEEE Computer Society Press, pp 332\u2013344"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00379-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00379-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00379-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T15:52:59Z","timestamp":1661529179000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00379-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10]]},"references-count":45,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["379"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00379-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10]]},"assertion":[{"value":"6 March 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 June 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}