{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T22:47:30Z","timestamp":1792018050851,"version":"4.4.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe our implementation of downset-manipulating algorithms used to solve the realizability problem for linear temporal logic (LTL). These algorithms were introduced by Filiot et al.\u00a0in the 2010s and implemented in the tools Acacia and Acacia+ in C and Python. We identify degrees of freedom in the original algorithms and provide a complete rewriting of Acacia in C++20 articulated around genericity and leveraging modern techniques for better performance. These techniques include compile-time specialization of the algorithms, the use of SIMD registers to store vectors, and several preprocessing steps, some relying on efficient Binary Decision Diagram (BDD) libraries. We also explore different data structures to store downsets. The resulting tool is competitive against comparable modern tools.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_14","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"192-207","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9828-9129","authenticated-orcid":false,"given":"Micha\u00ebl","family":"Cadilhac","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1200-4952","authenticated-orcid":false,"given":"Guillermo A.","family":"P\u00e9rez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, Z., Benqu\u00e9, D., Berezin, S., Dahl, A.C.E., Fisher, J., Hall, B.A., Ishtiaq, S., Nanavati, J., Piterman, N., Riechert, M., Skoblov, N.: Bringing LTL model checking to biologists. In: VMCAI. Lecture Notes in Computer Science, vol. 10145, pp. 1\u201313. Springer (2017)","DOI":"10.1007\/978-3-319-52234-0_1"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y.: Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In: AAAI. pp. 9766\u20139774. AAAI Press (2020)","DOI":"10.1609\/aaai.v34i06.6528"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"de\u00a0Berg, M., Cheong, O., van Kreveld, M.J., Overmars, M.H.: Computational geometry: algorithms and applications, 3rd Edition. Springer (2008), https:\/\/www.worldcat.org\/oclc\/227584184","DOI":"10.1007\/978-3-540-77974-2"},{"key":"14_CR4","unstructured":"Bohy, A.: Antichain based algorithms for the synthesis of reactive systems. Ph.D. thesis, University of Mons (2014)"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV. LNCS, vol.\u00a07358, pp. 652\u2013657. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A decision tree approach to data classification using signal temporal logic. In: HSCC. pp. 1\u201310. ACM (2016)","DOI":"10.1145\/2883817.2883843"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Cadilhac, M., P\u00e9rez, G.A.: Acacia-Bonsai (TACAS\u201923 version) (Nov 2022). https:\/\/doi.org\/10.5281\/zenodo.7296659","DOI":"10.5281\/zenodo.7296659"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. In: ICAPS. pp. 621\u2013630. AAAI Press (2019)","DOI":"10.1609\/icaps.v29i1.3529"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - A framework for LTL and $$\\omega $$-automata manipulation. In: ATVA. Lecture Notes in Computer Science, vol.\u00a09938, pp. 122\u2013129 (2016)","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Raskin, J., Sickert, S.: From LTL and limit-deterministic b\u00fcchi automata to deterministic parity automata. In: TACAS (1). Lecture Notes in Computer Science, vol. 10205, pp. 426\u2013442 (2017)","DOI":"10.1007\/978-3-662-54577-5_25"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: From LTL to deterministic automata - A Safraless compositional approach. Formal Methods Syst. Des. 49(3), 219\u2013271 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0259-2","DOI":"10.1007\/s10703-016-0259-2"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS. LNCS, vol. 10205, pp. 354\u2013370 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_20","DOI":"10.1007\/978-3-662-54577-5_20"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.: An antichain algorithm for LTL realizability. In: CAV. Lecture Notes in Computer Science, vol.\u00a05643, pp. 263\u2013277. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Geeraerts, G., Goossens, J., Stainer, A.: Synthesising succinct strategies in safety and reachability games. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP. LNCS, vol.\u00a08762, pp. 98\u2013111. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_8","DOI":"10.1007\/978-3-319-11439-2_8"},{"key":"14_CR15","unstructured":"Giacomo, G.D., Vardi, M.Y.: LTL$${}_{\\text{f}}$$ and LDL$${}_{\\text{ f }}$$ synthesis under partial observability. In: IJCAI. pp. 1044\u20131050. IJCAI\/AAAI Press (2016)"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Gutierrez, J., Najib, M., Perelli, G., Wooldridge, M.J.: Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif. Intell. 287, 103353 (2020). https:\/\/doi.org\/10.1016\/j.artint.2020.103353","DOI":"10.1016\/j.artint.2020.103353"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems - Conference proceedings, Colle-sur-Loup (near Nice), France, 8-19 October 1984. NATO ASI Series, vol.\u00a013, pp. 477\u2013498. Springer (1984). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_17","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Basset, N., Bloem, R., Brenguier, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Michaud, T., P\u00e9rez, G.A., Raskin, J., Sankur, O., Tentrup, L.: The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results. In: SYNT@CAV. EPTCS, vol.\u00a0260, pp. 116\u2013143 (2017)","DOI":"10.4204\/EPTCS.260.10"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Jacobs, S., P\u00e9rez, G.A., Abraham, R., Bruy\u00e8re, V., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret-Lutz, A., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, K.J., Michaud, T., Pommellet, A., Renkin, F., Schlehuber-Caissier, P., Sakr, M., Sickert, S., Staquet, G., Tamines, C., Tentrup, L., Walker, A.: The reactive synthesis competition (SYNTCOMP): 2018-2021. CoRR abs\/2206.00251 (2022). https:\/\/doi.org\/10.48550\/arXiv.2206.00251","DOI":"10.48550\/arXiv.2206.00251"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: CAV. Lecture Notes in Computer Science, vol.\u00a04144, pp. 31\u201344. Springer (2006)","DOI":"10.1007\/11817963_6"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining (T). In: ASE. pp. 81\u201392. IEEE Computer Society (2015)","DOI":"10.1109\/ASE.2015.71"},{"key":"14_CR22","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 57(1-2), 3\u201336 (2020). https:\/\/doi.org\/10.1007\/s00236-019-00349-3","DOI":"10.1007\/s00236-019-00349-3"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Martin, D.A.: Borel determinacy. Annals of Mathematics 102(2), 363\u2013371 (1975), http:\/\/www.jstor.org\/stable\/1971035","DOI":"10.2307\/1971035"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 578\u2013586. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"14_CR25","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":"14_CR26","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007). https:\/\/doi.org\/10.2168\/LMCS-3(3:5)2007","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"14_CR27","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 - 1 November 1977. pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"14_CR28","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-13, 1989. pp. 179\u2013190. ACM Press (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"14_CR29","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-26 October 1988. pp. 319\u2013327. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"Shi, Y., Xiao, S., Li, J., Guo, J., Pu, G.: Sat-based automata construction for LTL over finite traces. In: 27th Asia-Pacific Software Engineering Conference, APSEC 2020, Singapore, December 1-4, 2020. pp. 1\u201310. IEEE (2020). https:\/\/doi.org\/10.1109\/APSEC51365.2020.00008","DOI":"10.1109\/APSEC51365.2020.00008"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., Yonezaki, N.: Safraless LTL synthesis considering maximal realizability. Acta Informatica 54(7), 655\u2013692 (2017). https:\/\/doi.org\/10.1007\/s00236-016-0280-3","DOI":"10.1007\/s00236-016-0280-3"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs (extended abstract). In: DeMillo, R.A. (ed.) Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1984, Washington, DC, USA. pp. 446\u2013456. ACM (1984). https:\/\/doi.org\/10.1145\/800057.808711","DOI":"10.1145\/800057.808711"},{"key":"14_CR33","doi-asserted-by":"publisher","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety LTL synthesis. In: Strichman, O., Tzoref-Brill, R. (eds.) HVC. LNCS, vol. 10629, pp. 147\u2013162. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10","DOI":"10.1007\/978-3-319-70389-3_10"}],"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-031-30820-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:04:13Z","timestamp":1690974253000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"169","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":"56","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":"6","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":"33% - 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":"11","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)"}}]}}