{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:11:27Z","timestamp":1755997887736,"version":"3.37.3"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T00:00:00Z","timestamp":1480550400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1007\/s10703-016-0259-2","type":"journal-article","created":{"date-parts":[[2016,12,3]],"date-time":"2016-12-03T11:26:45Z","timestamp":1480764405000},"page":"219-271","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["From LTL to deterministic automata"],"prefix":"10.1007","volume":"49","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,12,3]]},"reference":[{"key":"259_CR1","doi-asserted-by":"crossref","unstructured":"Vardi MY (1999) Probabilistic linear-time model checking: an overview of the automata-theoretic approach. In: Formal methods for real-time and probabilistic systems, 5th international AMAST workshop, pp 265\u2013276","DOI":"10.1007\/3-540-48778-6_16"},{"key":"259_CR2","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp 332\u2013344"},{"issue":"1","key":"259_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1\u201337","journal-title":"Inf Comput"},{"key":"259_CR4","doi-asserted-by":"crossref","unstructured":"Couvreur J-M (1999) On-the-fly verification of linear temporal logic. In: World congress on formal, methods, pp 253\u2013271","DOI":"10.1007\/3-540-48119-2_16"},{"key":"259_CR5","doi-asserted-by":"crossref","unstructured":"Gastin P, Oddoux D (2001) Fast LTL to B\u00fcchi automata translation. In: CAV. LNCS, vol 2102. Springer, Berlin, pp 53\u201365. http:\/\/www.lsv.ens-cachan.fr\/~gastin\/ltl2ba\/","DOI":"10.1007\/3-540-44585-4_6"},{"key":"259_CR6","unstructured":"Gerth R, Peled D, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of the fifteenth IFIP WG6.1 international symposium on protocol specification, testing and verification protocol specification, testing and verification XV, pp 3\u201318"},{"key":"259_CR7","doi-asserted-by":"crossref","unstructured":"Babiak T, K\u0159et\u00ednsk\u00fd M, Reh\u00e1k V, Strej\u010dek J (2012) LTL to B\u00fcchi automata translation: fast and more deterministic. In: TACAS, pp 95\u2013109","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"259_CR8","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A (2013) Manipulating LTL formulas using spot 1.0. In: ATVA, pp 442\u2013445","DOI":"10.1007\/978-3-319-02444-8_31"},{"key":"259_CR9","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge, MA"},{"key":"259_CR10","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: CAV, pp 559\u2013575","DOI":"10.1007\/978-3-642-39799-8_37"},{"key":"259_CR11","unstructured":"Safra S (1988) On the complexity of $$\\omega $$ \u03c9 -automata. In: FOCS. IEEE Computer Society, Los Alamitos, pp 319\u2013327"},{"key":"259_CR12","doi-asserted-by":"crossref","unstructured":"Piterman N (2006) From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: LICS, pp 255\u2013264","DOI":"10.1109\/LICS.2006.28"},{"key":"259_CR13","doi-asserted-by":"crossref","unstructured":"Schewe S (2009) Tighter bounds for the determinisation of B\u00fcchi automata. In: FOSSACS, pp 167\u2013181","DOI":"10.1007\/978-3-642-00596-1_13"},{"key":"259_CR14","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: CAV, pp 585\u2013591"},{"key":"259_CR15","unstructured":"Klein J (2005) Linear time logic and deterministic omega-automata. Master\u2019s thesis, Rheinische Friedrich-Wilhelms Universit\u00e4t Bonn. The tool ltl2dstar\u2014LTL to deterministic Streett and Rabin automata. http:\/\/www.ltl2dstar.de\/"},{"key":"259_CR16","doi-asserted-by":"crossref","unstructured":"Kupferman O (2012) Recent challenges and ideas in temporal synthesis. In: SOFSEM. LNCS, vol 7147. Springer, New York, pp 88\u201398","DOI":"10.1007\/978-3-642-27660-6_8"},{"key":"259_CR17","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd J, Esparza J (2012) Deterministic automata for the (F,G)-fragment of LTL. In: CAV, pp 7\u201322","DOI":"10.1007\/978-3-642-31424-7_7"},{"key":"259_CR18","doi-asserted-by":"crossref","unstructured":"Gaiser A, K\u0159et\u00ednsk\u00fd J, Esparza J (2012) Rabinizer: small deterministic automata for LTL(F,G). In: ATVA, pp 72\u201376","DOI":"10.1007\/978-3-642-33386-6_7"},{"key":"259_CR19","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd J, Ledesma-Garza R (2013) Rabinizer 2: small deterministic automata for LTL $$\\setminus $$ \\ GU. In: ATVA, pp 446\u2013450","DOI":"10.1007\/978-3-319-02444-8_32"},{"key":"259_CR20","doi-asserted-by":"crossref","unstructured":"Esparza J, K\u0159et\u00ednsk\u00fd J (2014) From LTL to deterministic automata: a safraless compositional approach. In: CAV, pp 192\u2013208","DOI":"10.1007\/978-3-319-08867-9_13"},{"key":"259_CR21","doi-asserted-by":"crossref","unstructured":"Daniele M, Giunchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. In: CAV, pp 249\u2013260","DOI":"10.1007\/3-540-48683-6_23"},{"key":"259_CR22","doi-asserted-by":"crossref","unstructured":"Etessami K, Holzmann GJ (2000) Optimizing B\u00fcchi automata. In: CONCUR, pp 153\u2013167","DOI":"10.1007\/3-540-44618-4_13"},{"key":"259_CR23","doi-asserted-by":"crossref","unstructured":"Fritz C (2003) Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating B\u00fcchi automata. In: CIAA, pp 35\u201348","DOI":"10.1007\/3-540-45089-0_5"},{"key":"259_CR24","doi-asserted-by":"crossref","unstructured":"Giannakopoulou D, Lerda F (2002) From states to transitions: improving translation of LTL formulae to B\u00fcchi automata. In: FORTE, pp 308\u2013326","DOI":"10.1007\/3-540-36135-9_20"},{"key":"259_CR25","doi-asserted-by":"crossref","unstructured":"Somenzi F, Bloem R (2000) Efficient B\u00fcchi automata from LTL formulae. In: CAV. LNCS, vol 1855. Springer, Heidelberg, pp 248\u2013263","DOI":"10.1007\/10722167_21"},{"key":"259_CR26","unstructured":"Klein J, Baier C (2007) On-the-fly stuttering in the construction of deterministic $$\\omega $$ \u03c9 -automata. In: CIAA. LNCS, vol 4783. Springer, New York, pp 51\u201361"},{"key":"259_CR27","doi-asserted-by":"crossref","unstructured":"Blahoudek F, K\u0159et\u00ednsk\u00fd M, Strej\u010dek J (2013) Comparison of LTL to deterministic Rabin automata translators. In: LPAR, pp 164\u2013172","DOI":"10.1007\/978-3-642-45221-5_12"},{"key":"259_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli A, Zaks A (2008) On the merits of temporal testers. In: 25 years of model checking\u2014history, achievements, perspectives, pp 172\u2013195","DOI":"10.1007\/978-3-540-69850-0_11"},{"key":"259_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1988) A framework for the synthesis of reactive modules. In Concurrency. LNCS, vol 335. Springer, Heidelberg, pp 4\u201317","DOI":"10.1007\/3-540-50403-6_28"},{"key":"259_CR30","doi-asserted-by":"crossref","unstructured":"Di Giampaolo B, Geeraerts G, Raskin J-F, Sznajder N (2010) Safraless procedures for timed specifications. In: FORMATS, pp 2\u201322","DOI":"10.1007\/978-3-642-15297-9_2"},{"key":"259_CR31","doi-asserted-by":"crossref","unstructured":"Kupferman O, Piterman N, Vardi MY (2006) Safraless compositional synthesis. In: CAV. LNCS, vol 4144. Springer, New York, pp 31\u201344","DOI":"10.1007\/11817963_6"},{"key":"259_CR32","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi MY (2005) Safraless decision procedures. In: FOCS. IEEE Computer Society, Los Alamitos, pp 531\u2013542","DOI":"10.1109\/SFCS.2005.66"},{"issue":"1","key":"259_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R Alur","year":"2004","unstructured":"Alur R, La Torre S (2004) Deterministic generators and games for LTL fragments. ACM Trans Comput Log 5(1):1\u201325","journal-title":"ACM Trans Comput Log"},{"key":"259_CR34","doi-asserted-by":"crossref","unstructured":"Kom\u00e1rkov\u00e1 Z, K\u0159et\u00ednsk\u00fd J (2014) Rabinizer 3: safraless translation of LTL to small deterministic automata. In: ATVA, pp 235\u2013241","DOI":"10.1007\/978-3-319-11936-6_17"},{"key":"259_CR35","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: CAV, pp 479\u2013486","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"259_CR36","doi-asserted-by":"crossref","unstructured":"Babiak T, Blahoudek F, K\u0159et\u00ednsk\u00fd M, Strej\u010dek J (2013) Effective translation of LTL to deterministic Rabin automata: beyond the (F, G)-fragment. In: ATVA, pp 24\u201339","DOI":"10.1007\/978-3-319-02444-8_4"},{"key":"259_CR37","doi-asserted-by":"crossref","unstructured":"Babiak T, Badie T, Duret-Lutz A, K\u0159et\u00ednsk\u00fd M, Strej\u010dek J (2013) Compositional approach to suspension and other improvements to LTL translation. In: SPIN, pp 81\u201398","DOI":"10.1007\/978-3-642-39176-7_6"},{"key":"259_CR38","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek R (2007) Beem: benchmarks for explicit model checkers. In: Proc of SPIN Workshop. LNCS, vol 4595. Springer, Heidelberg, pp 263\u2013267","DOI":"10.1007\/978-3-540-73370-6_17"},{"issue":"2","key":"259_CR39","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/j.tcs.2006.07.022","volume":"363","author":"J Klein","year":"2006","unstructured":"Klein J, Baier C (2006) Experiments with deterministic $$\\omega $$ \u03c9 -automata for formulas of linear temporal logic. Theor Comput Sci 363(2):182\u2013195","journal-title":"Theor Comput Sci"},{"key":"259_CR40","doi-asserted-by":"crossref","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE, pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"259_CR41","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL: a proof assistant for higher-order logic., Lecture notes in computer scienceSpringer, Heidelberg"},{"key":"259_CR42","doi-asserted-by":"crossref","unstructured":"Esparza J, Lammich P, Neumann R, Nipkow T, Schimpf A, Smaus J-G (2013) A fully verified executable LTL model checker. In: CAV, pp 463\u2013478","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"259_CR43","unstructured":"Sickert S (2015) Converting linear temporal logic to deterministic (generalized) Rabin automata. Archive of Formal Proofs. http:\/\/isa-afp.org\/entries\/LTL_to_DRA.shtml (Formal proof development)"},{"key":"259_CR44","unstructured":"Wenzel M (2007) Isabelle\/isar-a generic framework for human-readable proof documents. In: From insight to proof-festschrift in honour of Andrzej Trybulec, vol 10(23), pp 277\u2013298"},{"key":"259_CR45","unstructured":"Wenzel M (2014) The Isabelle\/Isar reference manual"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0259-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0259-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0259-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,16]],"date-time":"2019-09-16T02:43:07Z","timestamp":1568601787000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0259-2"}},"subtitle":["A safraless compositional approach"],"short-title":[],"issued":{"date-parts":[[2016,12]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["259"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0259-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2016,12]]}}}