{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:31Z","timestamp":1740108331937,"version":"3.37.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T00:00:00Z","timestamp":1640822400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T00:00:00Z","timestamp":1640822400000},"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":["Verified Model Checkers (No. 317422601)","Statistical Unbounded Verification (No. 383882557)"],"award-info":[{"award-number":["Verified Model Checkers (No. 317422601)","Statistical Unbounded Verification (No. 383882557)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100005156","name":"alexander von humboldt-stiftung","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100005156","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Transforming <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches.<\/jats:p>","DOI":"10.1007\/s00236-021-00412-y","type":"journal-article","created":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T04:19:27Z","timestamp":1640837967000},"page":"585-618","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Index appearance record with preorders"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6019-7130","authenticated-orcid":false,"given":"Clara","family":"Waldmann","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0163-2152","authenticated-orcid":false,"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,12,30]]},"reference":[{"issue":"1","key":"412_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R Alur","year":"2004","unstructured":"Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log. 5(1), 1\u201325 (2004). https:\/\/doi.org\/10.1145\/963927.963928","journal-title":"ACM Trans. Comput. Log."},{"key":"412_CR2","doi-asserted-by":"publisher","unstructured":"Babiak, T., Blahoudek, F., Kret\u00ednsk\u00fd, M., Strejcek, J.: Effective translation of LTL to deterministic Rabin automata: beyond the (F, G)-fragment. In: Automated Technology for Verification and Analysis\u201411th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15\u201318, 2013. Proceedings, pp. 24\u201339 (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_4","DOI":"10.1007\/978-3-319-02444-8_4"},{"key":"412_CR3","unstructured":"Bj\u00f6rklund, H., Sandberg, S., Vorobyov, S.: On fixed-parameter complexity of infinite games. In: The Nordic Workshop on Programming Theory (NWPT 2003), vol. 34, pp. 29\u201331. Citeseer (2003)"},{"issue":"4","key":"412_CR4","doi-asserted-by":"publisher","first-page":"1171","DOI":"10.2307\/2273681","volume":"48","author":"JR B\u00fcchi","year":"1983","unstructured":"B\u00fcchi, J.R.: State-strategies for games in F G. J. Symb. Log. 48(4), 1171\u20131198 (1983). https:\/\/doi.org\/10.2307\/2273681","journal-title":"J. Symb. Log."},{"key":"412_CR5","doi-asserted-by":"publisher","unstructured":"Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of games and automata using Muller conditions. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12\u201316, 2021, Glasgow, Scotland (Virtual Conference), LIPIcs, vol. 198, pp. 123:1\u2013123:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.123","DOI":"10.4230\/LIPIcs.ICALP.2021.123"},{"key":"412_CR6","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Gaiser, A., Kret\u00ednsk\u00fd, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 559\u2013575. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_37","DOI":"10.1007\/978-3-642-39799-8_37"},{"key":"412_CR7","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis\u201414th International Symposium, ATVA 2016, Chiba, Japan, October 17\u201320, 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":"412_CR8","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Ardis, M.A, Atlee, J.M. (eds.) Proceedings of the Second Workshop on Formal Methods in Software Practice, March 4\u20135, 1998, Clearwater Beach, Florida, USA, pp. 7\u201315. ACM (1998). https:\/\/doi.org\/10.1145\/298595.298598","DOI":"10.1145\/298595.298598"},{"issue":"3","key":"412_CR9","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10703-016-0259-2","volume":"49","author":"J Esparza","year":"2016","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: From LTL to deterministic automata\u2014a safraless compositional approach. Form. Methods Syst. Des. 49(3), 219\u2013271 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0259-2","journal-title":"Form. Methods Syst. Des."},{"key":"412_CR10","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: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09\u201312, 2018, pp. 384\u2013393. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209161","DOI":"10.1145\/3209108.3209161"},{"key":"412_CR11","doi-asserted-by":"publisher","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000\u2014Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22\u201325, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1877, pp. 153\u2013167. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-44618-4_13","DOI":"10.1007\/3-540-44618-4_13"},{"key":"412_CR12","doi-asserted-by":"publisher","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14\u201316, 2009. Proceedings, pp. 182\u2013196 (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_15","DOI":"10.1007\/978-3-642-04761-9_15"},{"key":"412_CR13","doi-asserted-by":"publisher","unstructured":"Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5\u20137, 1982, San Francisco, California, USA, pp. 60\u201365 (1982). https:\/\/doi.org\/10.1145\/800070.802177","DOI":"10.1145\/800070.802177"},{"key":"412_CR14","unstructured":"Hole\u010dek, J., Kratochv\u00edla, T., \u0158eh\u00e1k, V., \u0160afr\u00e1nek, D., \u0160ime\u010dek, P.: Verification Results in Liberouter Project (2004)"},{"issue":"2","key":"412_CR15","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/j.tcs.2006.07.022","volume":"363","author":"J Klein","year":"2006","unstructured":"Klein, J., Baier, C.: Experiments with deterministic omega-automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), 182\u2013195 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.07.022","journal-title":"Theor. Comput. Sci."},{"key":"412_CR16","doi-asserted-by":"publisher","unstructured":"Kom\u00e1rkov\u00e1, Z., K\u0159et\u00ednsk\u00fd, J.: Rabinizer 3: safraless translation of LTL to small deterministic automata. In: Automated Technology for Verification and Analysis\u201412th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3\u20137, 2014, Proceedings, pp. 235\u2013241 (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_17","DOI":"10.1007\/978-3-319-11936-6_17"},{"key":"412_CR17","doi-asserted-by":"publisher","unstructured":"K\u0159et\u00ednsk\u00fd, J., Esparza, J.: Deterministic automata for the (F, G)-fragment of LTL. In: Computer Aided Verification\u201424th International Conference, CAV 2012, Berkeley, CA, USA, July 7\u201313, 2012 Proceedings, pp. 7\u201322 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_7","DOI":"10.1007\/978-3-642-31424-7_7"},{"key":"412_CR18","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Manta, A., Meggendorfer, T.: Semantic labelling and learning for parity game solving in LTL synthesis. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis\u201417th International Symposium, ATVA 2019, Taipei, Taiwan, October 28\u201331, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11781, pp. 404\u2013422. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_24","DOI":"10.1007\/978-3-030-31784-3_24"},{"key":"412_CR19","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis\u201416th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7\u201310, 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":"412_CR20","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: from LTL to your favourite deterministic automaton. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification\u201430th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14\u201317, 2018, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10981, pp. 567\u2013577. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_30","DOI":"10.1007\/978-3-319-96145-3_30"},{"key":"412_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: Legay, A., Margaria, T. (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\u201329, 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":"412_CR22","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 23\u201325 October 2005, Pittsburgh, PA, SA, Proceedings, pp. 531\u2013542 (2005). https:\/\/doi.org\/10.1109\/SFCS.2005.66","DOI":"10.1109\/SFCS.2005.66"},{"key":"412_CR23","unstructured":"L\u00f6ding, C.: Methods for the transformation of automata: complexity and connection to second order logic. Master\u2019s thesis, Institute of Computer Science and Applied Mathematics, Christian-Albrechts-University of Kiel, Germany (1999)"},{"key":"412_CR24","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C.: Optimal bounds for transformations of $$\\omega $$-automata. In: Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13\u201315, 1999, Proceedings, pp. 97\u2013109 (1999). https:\/\/doi.org\/10.1007\/3-540-46691-6_8","DOI":"10.1007\/3-540-46691-6_8"},{"key":"412_CR25","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Tollk\u00f6tter, A.: State space reduction for parity automata. In: Fern\u00e1ndez, M., Muscholl, A. (eds.) 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13\u201316, 2020, Barcelona, Spain, LIPIcs, vol. 152, pp. 27:1\u201327:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.27","DOI":"10.4230\/LIPIcs.CSL.2020.27"},{"key":"412_CR26","unstructured":"Luttenberger, M., Meyer, P., Sickert, S.: On the optimal and practical conversion of Emerson\u2013Lei automata into parity automata. To appear (2021)"},{"key":"412_CR27","doi-asserted-by":"publisher","unstructured":"Meggendorfer, T.: Artefact for: index appearance record with preorders (2021). https:\/\/doi.org\/10.5281\/zenodo.4651156","DOI":"10.5281\/zenodo.4651156"},{"key":"412_CR28","doi-asserted-by":"publisher","unstructured":"Meyer, P.J., Luttenberger, M.: Solving mean-payoff games on the GPU. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis\u201414th International Symposium, ATVA 2016, Chiba, Japan, October 17\u201320, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9938, pp. 262\u2013267 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_17","DOI":"10.1007\/978-3-319-46520-3_17"},{"key":"412_CR29","doi-asserted-by":"publisher","unstructured":"Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) Computation Theory\u2014Fifth Symposium, Zabor\u00f3w, Poland, December 3\u20138, 1984, Proceedings, Lecture Notes in Computer Science, vol. 208, pp. 157\u2013168. Springer (1984). https:\/\/doi.org\/10.1007\/3-540-16066-3_15","DOI":"10.1007\/3-540-16066-3_15"},{"key":"412_CR30","doi-asserted-by":"publisher","unstructured":"Muller, D.E.: Infinite sequences and finite machines. In: 4th Annual Symposium on Switching Circuit Theory and Logical Design, pp. 3\u201316. IEEE Computer Society, Chicago, Illinois, USA (1963). https:\/\/doi.org\/10.1109\/SWCT.1963.8","DOI":"10.1109\/SWCT.1963.8"},{"key":"412_CR31","doi-asserted-by":"publisher","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Bosnacki, D., Edelkamp, S. (eds.) Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1\u20133, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4595, pp. 263\u2013267. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_17","DOI":"10.1007\/978-3-540-73370-6_17"},{"key":"412_CR32","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12\u201315 August 2006, Seattle, WA, USA, Proceedings, pp. 255\u2013264 (2006). https:\/\/doi.org\/10.1109\/LICS.2006.28","DOI":"10.1109\/LICS.2006.28"},{"key":"412_CR33","doi-asserted-by":"publisher","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8\u201310, 2006, Proceedings, pp. 364\u2013380 (2006). https:\/\/doi.org\/10.1007\/11609773_24","DOI":"10.1007\/11609773_24"},{"key":"412_CR34","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October\u20131 November 1977, pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"412_CR35","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11\u201313, 1989, pp. 179\u2013190 (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"412_CR36","first-page":"1","volume":"141","author":"MO Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1\u201335 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"412_CR37","doi-asserted-by":"publisher","unstructured":"Renkin, F., Duret-Lutz, A., Pommellet, A.: Practical \u201cparitizing\u201d of Emerson\u2013Lei automata. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis\u201418th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19\u201323, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12302, pp. 127\u2013143. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_7","DOI":"10.1007\/978-3-030-59152-6_7"},{"key":"412_CR38","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of $$\\omega $$-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24\u201326 October 1988, pp. 319\u2013327 (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"412_CR39","doi-asserted-by":"publisher","unstructured":"Safra, S.: Exponential determinization for $$\\omega $$-automata with strong-fairness acceptance condition (extended abstract). In: Proceedings of the 24th Annual ACM Symposium on Theory of Computing, May 4\u20136, 1992, Victoria, British Columbia, Canada, pp. 275\u2013282 (1992). https:\/\/doi.org\/10.1145\/129712.129739","DOI":"10.1145\/129712.129739"},{"key":"412_CR40","doi-asserted-by":"publisher","unstructured":"Schewe, S.: Tighter bounds for the determinisation of B\u00fcchi automata. In: Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22\u201329, 2009. Proceedings, pp. 167\u2013181 (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_13","DOI":"10.1007\/978-3-642-00596-1_13"},{"key":"412_CR41","doi-asserted-by":"publisher","unstructured":"Schwoon, S.: Determinization and complementation of Streett automata. In: Automata, Logics, and Infinite Games: A Guide to Current Research [Outcome of a Dagstuhl Seminar, February 2001], pp. 79\u201391 (2001). https:\/\/doi.org\/10.1007\/3-540-36387-4_5","DOI":"10.1007\/3-540-36387-4_5"},{"key":"412_CR42","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: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification\u201428th International Conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, Proceedings, Part II, Lecture Notes in Computer Science, vol. 9780, pp. 312\u2013332. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"412_CR43","doi-asserted-by":"publisher","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15\u201319, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1855, pp. 248\u2013263. Springer (2000). https:\/\/doi.org\/10.1007\/10722167_21","DOI":"10.1007\/10722167_21"},{"issue":"1\/2","key":"412_CR44","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"RS Streett","year":"1982","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Inf. Control 54(1\/2), 121\u2013141 (1982). https:\/\/doi.org\/10.1016\/S0019-9958(82)91258-X","journal-title":"Inf. Control"},{"key":"412_CR45","doi-asserted-by":"publisher","unstructured":"Tsai, M., Tsay, Y., Hwang, Y.: GOAL for games, omega-automata, and logics. In: Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, pp. 883\u2013889 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_62","DOI":"10.1007\/978-3-642-39799-8_62"},{"issue":"1\u20132","key":"412_CR46","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(98)00009-7","journal-title":"Theor. Comput. Sci."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-021-00412-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-021-00412-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-021-00412-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,24]],"date-time":"2022-09-24T09:03:09Z","timestamp":1664010189000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-021-00412-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,30]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["412"],"URL":"https:\/\/doi.org\/10.1007\/s00236-021-00412-y","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2021,12,30]]},"assertion":[{"value":"18 June 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 October 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 December 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}