{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:50:40Z","timestamp":1742975440317,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995263"},{"type":"electronic","value":"9783030995270"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In 2021, Casares, Colcombet, and Fijalkow introduced the Alternating Cycle Decomposition (ACD) to study properties and transformations of Muller automata. We present the first practical implementation of the ACD in two different tools, Owl and Spot, and adapt it to the framework of Emerson-Lei automata, i.e., <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 whose acceptance conditions are defined by Boolean formulas. The ACD provides a transformation of Emerson-Lei automata into parity automata with strong optimality guarantees: the resulting parity automaton is minimal among those automata that can be obtained by duplication of states. Our empirical results show that this transformation is usable in practice. Further, we show how the ACD can generalize many other specialized constructions such as deciding typeness of automata and degeneralization of generalized B\u00fcchi automata, providing a framework of practical algorithms for <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.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_6","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"99-117","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Practical Applications of the Alternating Cycle Decomposition"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6539-2020","authenticated-orcid":false,"given":"Antonio","family":"Casares","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6623-2512","authenticated-orcid":false,"given":"Alexandre","family":"Duret-Lutz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1334-9079","authenticated-orcid":false,"given":"Klara J.","family":"Meyer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5066-1726","authenticated-orcid":false,"given":"Florian","family":"Renkin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0280-8981","authenticated-orcid":false,"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Baarir, S., Duret-Lutz, A.: Mechanizing the minimization of deterministic generalized B\u00fcchi automata. In: Proceedings of the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE\u201914), Lecture Notes in Computer Science, vol. 8461, pp. 266\u2013283, Springer (Jun 2014), https:\/\/doi.org\/10.1007\/978-3-662-43613-4_17","DOI":"10.1007\/978-3-662-43613-4_17"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Babiak, T., Badie, T., Duret-Lutz, A., K\u0159et\u00ednsk\u00fd, M., Strej\u010dek, J.: Compositional approach to suspension and other improvements to LTL translation. In: Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN\u201913), Lecture Notes in Computer Science, vol. 7976, pp. 81\u201398, Springer (Jul 2013), https:\/\/doi.org\/10.1007\/978-3-642-39176-7_6","DOI":"10.1007\/978-3-642-39176-7_6"},{"key":"6_CR3","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.: The hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 479\u2013486, Springer International Publishing (2015)","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Battiti, R., , Protasi, M.: Handbook of Combinatorial Optimization: Volume 1\u20133, chap. Approximate Algorithms and Heuristics for MAX-SAT, pp. 77\u2013148. Springer US (1998), ISBN 978-1-4613-0303-9, https:\/\/doi.org\/10.1007\/978-1-4613-0303-9_2","DOI":"10.1007\/978-1-4613-0303-9_2"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Carton, O., Maceiras, R.: Computing the Rabin index of a parity automaton. Informatique th\u00e9orique et applications 33(6), 495\u2013505 (1999), URL http:\/\/www.numdam.org\/item\/ITA_1999__33_6_495_0\/","DOI":"10.1051\/ita:1999129"},{"key":"6_CR6","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.) Proceedings of the 48th International Colloquium on Automata, Languages, and Programming (ICALP\u201921), Leibniz International Proceedings in Informatics (LIPIcs), vol. 198, pp. 123:1\u2013123:14, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021), https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.123","DOI":"10.4230\/LIPIcs.ICALP.2021.123"},{"key":"6_CR7","unstructured":"Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of muller conditions. Extended version of [6], on ArXiv. (2021), https:\/\/arxiv.org\/abs\/2011.13041"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Casares, A., Duret-Lutz, A., Meyer, K.J., Renkin, F., Sickert, S.: Artifact for the paper \u201cPractical applications of the alternating cycle decomposition\u201d. https:\/\/doi.org\/10.5281\/zenodo.5572613 (2021)","DOI":"10.5281\/zenodo.5572613"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201916), Lecture Notes in Computer Science, vol. 9938, pp. 122\u2013129, Springer (Oct 2016), https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Lei, C.L.: Modalities for model checking (extended abstract): Branching time strikes back. In: Proceedings of the 12th ACM symposium on Principles of Programming Languages (POPL\u201985), pp. 84\u201396, ACM (1985), https:\/\/doi.org\/10.1145\/318593.318620","DOI":"10.1145\/318593.318620"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Raskin, J.F., Sickert, S.: From LTL and limit-deterministic B\u00fcchi automata to deterministic parity automata. In: Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201917), Lecture Notes in Computer Science, vol. 10205, pp. 426\u2013442, Springer-Verlag (2017), https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25","DOI":"10.1007\/978-3-662-54577-5_25"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM 67(6) (Oct 2020), https:\/\/doi.org\/10.1145\/3417995","DOI":"10.1145\/3417995"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u201901), Lecture Notes in Computer Science, vol. 2102, pp. 53\u201365, Springer-Verlag (2001), https:\/\/doi.org\/10.1007\/3-540-44585-4_6","DOI":"10.1007\/3-540-44585-4_6"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formul\u00e6 to B\u00fcchi automata. In: Peled, D., Vardi, M. (eds.) Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201902), Lecture Notes in Computer Science, vol. 2529, pp. 308\u2013326, Springer-Verlag, Houston, Texas (Nov 2002)","DOI":"10.1007\/3-540-36135-9_20"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. Springer, Berlin, Heidelberg (2002), https:\/\/doi.org\/10.1007\/3-540-36387-4","DOI":"10.1007\/3-540-36387-4"},{"key":"6_CR16","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 (STOC\u201982), pp. 60\u201365 (1982), https:\/\/doi.org\/10.1145\/800070.802177","DOI":"10.1145\/800070.802177"},{"key":"6_CR17","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), URL http:\/\/arxiv.org\/abs\/1904.07736"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: A library for $$\\omega $$-words, automata, and LTL. In: Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201918), 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":"6_CR19","doi-asserted-by":"crossref","unstructured":"Krishnan, Sriram C.and\u00a0Puri, A., Brayton, R.K.: Deterministic $$\\omega $$ automata vis-a-vis deterministic buchi automata. In: Algorithms and Computation, pp. 378\u2013386, Springer Berlin Heidelberg, Berlin, Heidelberg (1994)","DOI":"10.1007\/3-540-58325-4_202"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"K\u0159et\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.) Proceedings of the 23st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201917), 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":"6_CR21","doi-asserted-by":"publisher","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Waldmann, C., Weininger, M.: Index appearance record with preorders. Acta Informatica (2021), https:\/\/doi.org\/10.1007\/s00236-021-00412-y","DOI":"10.1007\/s00236-021-00412-y"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C.: Optimal bounds for transformations of $$\\omega $$-automata. In: Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201999), Lecture Notes in Computer Science, vol. 1738, pp. 97\u2013109, Springer (1999), https:\/\/doi.org\/10.1007\/3-540-46691-6_8","DOI":"10.1007\/3-540-46691-6_8"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica pp. 3\u201336 (2020), https:\/\/doi.org\/10.1007\/s00236-019-00349-3","DOI":"10.1007\/s00236-019-00349-3"},{"key":"6_CR24","unstructured":"L\u00f6ding, C.: Methods for the Transformation of $$\\omega $$-Automata: Complexity and Connection to Second Order Logic. Master\u2019s thesis, Institute of Computer Science and Applied Mathematics Christian-Albrechts-University of Kiel (1998), URL https:\/\/old.automata.rwth-aachen.de\/users\/loeding\/diploma_loeding.pdf"},{"key":"6_CR25","unstructured":"Meyer, P., Sickert, S.: On the optimal and practical conversion of Emerson-Lei automata into parity automata. Unpublished manuscript, obsoleted by the work of Casares et al. [6]. (2021)"},{"key":"6_CR26","unstructured":"Michaud, T., Colange, M.: Reactive synthesis from LTL specification with Spot. In: Proceedings of the 7th Workshop on Synthesis, SYNT@CAV 2018, Electronic Proceedings in Theoretical Computer Science (2018)"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL\u201989), pp. 179\u2014190 (1989), https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Renkin, F., Duret-Lutz, A., Pommellet, A.: Practical \u201cparitizing\u201d of Emerson-Lei automata. In: Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201920), Lecture Notes in Computer Science, vol. 12302, pp. 127\u2013143, Springer (Oct 2020), https:\/\/doi.org\/10.1007\/978-3-030-59152-6_7","DOI":"10.1007\/978-3-030-59152-6_7"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency: Structure versus Automata, volume 1043 of Lecture Notes in Computer Science, pp. 238\u2013266, Springer-Verlag (1996)","DOI":"10.1007\/3-540-60915-6_6"},{"key":"6_CR30","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st Symposium on Logic in Computer Science (LICS\u201986), pp. 332\u2013344, IEEE Computer Society Press (Jun 1986)"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1), 135\u2013183 (1998), https:\/\/doi.org\/10.1016\/S0304-3975(98)00009-7","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:46:12Z","timestamp":1710233172000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}