{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:26:29Z","timestamp":1750843589000,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377082"},{"type":"electronic","value":"9783031377099"}],"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,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"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 present a flexible and efficient toolchain to<jats:italic>symbolically<\/jats:italic>solve (standard) Rabin games, fair-adversarial Rabin games, and \"Image missing\"-player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using these flexible game solvers as a back-end, we implemented a tool for computing correct-by-construction controllers for stochastic dynamical systems under LTL specifications. Our implementations use the recent theoretical result that all of these games can be solved using the same symbolic fixpoint algorithm but utilizing different, domain specific calculations of the involved predecessor operators. The main feature of our toolchain is the utilization of two programming abstractions: one to separate the symbolic fixpoint computations from the predecessor calculations, and another one to allow the integration of different BDD libraries as back-ends. In particular, we employ a multi-threaded execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan, which leads to enormous computational savings.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_1","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"3-15","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Flexible Toolchain for\u00a0Symbolic Rabin Games under Fair and\u00a0Stochastic Uncertainties"],"prefix":"10.1007","author":[{"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[]},{"given":"Kaushik","family":"Mallik","sequence":"additional","affiliation":[]},{"given":"Mateusz","family":"Rychlicki","sequence":"additional","affiliation":[]},{"given":"Anne-Kathrin","family":"Schmuck","sequence":"additional","affiliation":[]},{"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"1_CR1","unstructured":"Abate, A., et al.: ARCH-COMP21 category report: stochastic models. In: 8th International Workshop on Applied Verification of Continuous and Hybrid Systems, pp. 55\u201389 (2021)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., et al.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-030-99527-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Banerjee","year":"2022","unstructured":"Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., Soudjani, S.: A direct symbolic algorithm for solving stochastic Rabin games. In: TACAS 2022. LNCS, vol. 13244, pp. 81\u201398. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_5"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.K., Soudjani, S.: Fast symbolic algorithms for omega-regular games under strong transition fairness. TheoretiCS (to appear) (2023). arXiv preprint arXiv:2202.07480","DOI":"10.46298\/theoretics.23.4"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"878","DOI":"10.1007\/11523468_71","volume-title":"Automata, Languages and Programming","author":"K Chatterjee","year":"2005","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of stochastic Rabin and Streett games. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 878\u2013890. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11523468_71"},{"issue":"2","key":"1_CR6","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s10703-012-0170-4","volume":"42","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., De Alfaro, L., Faella, M., Majumdar, R., Raman, V.: Code aware resource management. Formal Methods Syst. Des. 42(2), 146\u2013174 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Coogan, S., Arcak, M.: Efficient finite abstraction of mixed monotone systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 58\u201367 (2015)","DOI":"10.1145\/2728606.2728607"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-319-96142-2_14","volume-title":"Computer Aided Verification","author":"T Dijk","year":"2018","unstructured":"Dijk, T.: Attracting tangles to solve parity games. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 198\u2013215. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_14"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-89960-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Dijk","year":"2018","unstructured":"Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 291\u2013308. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16"},{"key":"1_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2022.101204","volume":"45","author":"M Dutreix","year":"2022","unstructured":"Dutreix, M., Huh, J., Coogan, S.: Abstraction-based synthesis for stochastic systems with omega-regular objectives. Nonlinear Anal. Hybrid Syst 45, 101204 (2022)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Geretti, L., et al.: ARCH-COMP20 category report: continuous and hybrid systems with nonlinear dynamics. In: Proceedings of the 7th International Workshop on Applied Verification of Continuous and Hybrid Systems, pp. 49\u201375 (2020)","DOI":"10.29007\/zkf6"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543\u2013550. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-58179-0_66","volume-title":"Computer Aided Verification","author":"DE Long","year":"1994","unstructured":"Long, D.E., Browne, A., Clarke, E.M., Jha, S., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 338\u2013350. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_66"},{"key":"1_CR14","unstructured":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.K., Soudjani, S.: A flexible toolchain for symbolic Rabin games under fair and stochastic uncertainties (2023). https:\/\/kmallik.github.io\/assets\/pdf\/cav23-toolpaper.pdf"},{"issue":"5","key":"1_CR15","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.ifacol.2021.08.486","volume":"54","author":"R Majumdar","year":"2021","unstructured":"Majumdar, R., Mallik, K., Schmuck, A.K., Soudjani, S.: Symbolic qualitative control for stochastic systems via finite parity games. IFAC-PapersOnLine 54(5), 127\u2013132 (2021)","journal-title":"IFAC-PapersOnLine"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Mallik, K., Soudjani, S.: Symbolic controller synthesis for b\u00fcchi specifications on stochastic systems. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2020)","DOI":"10.1145\/3365365.3382214"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS\u201906), pp. 275\u2013284. IEEE (2006)","DOI":"10.1109\/LICS.2006.23"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Rungger, M., Zamani, M.: Scots: a tool for the synthesis of symbolic controllers. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pp. 99\u2013104 (2016)","DOI":"10.1145\/2883817.2883834"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-540-87531-4_27","volume-title":"Computer Science Logic","author":"S Schewe","year":"2008","unstructured":"Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 369\u2013384. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87531-4_27"},{"key":"1_CR20","unstructured":"Somenzi, F.: Cudd: CU decision diagram package release 3.0.0 (2015). https:\/\/github.com\/ivmai\/cudd"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-662-46681-0_60","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T van Dijk","year":"2015","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 677\u2013691. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_60"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1), 135\u2013183 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(98)00009-7, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397598000097","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37709-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T06:56:13Z","timestamp":1729752973000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","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":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","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":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"0","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":"26% - 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)"}}]}}