[{"citation":{"ieee":"R. Majumdar, K. Mallik, A. K. Schmuck, and S. Soudjani, “Symbolic control for stochastic systems via finite parity games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 51. Elsevier, 2023.","apa":"Majumdar, R., Mallik, K., Schmuck, A. K., &#38; Soudjani, S. (2023). Symbolic control for stochastic systems via finite parity games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">https://doi.org/10.1016/j.nahs.2023.101430</a>","chicago":"Majumdar, Rupak, Kaushik Mallik, Anne Kathrin Schmuck, and Sadegh Soudjani. “Symbolic Control for Stochastic Systems via Finite Parity Games.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2023. <a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">https://doi.org/10.1016/j.nahs.2023.101430</a>.","ama":"Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic systems via finite parity games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2023;51. doi:<a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">10.1016/j.nahs.2023.101430</a>","mla":"Majumdar, Rupak, et al. “Symbolic Control for Stochastic Systems via Finite Parity Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 51, 101430, Elsevier, 2023, doi:<a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">10.1016/j.nahs.2023.101430</a>.","ista":"Majumdar R, Mallik K, Schmuck AK, Soudjani S. 2023. Symbolic control for stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems. 51, 101430.","short":"R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid Systems 51 (2023)."},"publication_status":"epub_ahead","abstract":[{"lang":"eng","text":"We consider the problem of computing the maximal probability of satisfying an \r\n-regular specification for stochastic, continuous-state, nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we show that a lower bound on this probability can be obtained by (I) computing an under-approximation of the qualitative winning region, i.e., states from which the parity condition can be enforced almost surely, and (II) computing the maximal probability of reaching this qualitative winning region.\r\nThe heart of our approach is a technique to symbolically compute the under-approximation of the qualitative winning region in step (I) via a finite-state abstraction of the original system as a \r\n-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We prove that the winning set in the abstract -player game induces an under-approximation of the qualitative winning region in the original synthesis problem, along with a policy to solve it. By combining these contributions with (a) a symbolic fixpoint algorithm to solve \r\n-player games and (b) existing techniques for reachability policy synthesis in stochastic nonlinear systems, we get an abstraction-based algorithm for finding a lower bound on the maximal satisfaction probability.\r\nWe have implemented the abstraction-based algorithm in Mascot-SDS, where we combined the outlined abstraction step with our tool Genie (Majumdar et al., 2023) that solves \r\n-player parity games (through a reduction to Rabin games) more efficiently than existing algorithms. We evaluated our implementation on the nonlinear model of a perturbed bistable switch from the literature. We show empirically that the lower bound on the winning region computed by our approach is precise, by comparing against an over-approximation of the qualitative winning region. Moreover, our implementation outperforms a recently proposed tool for solving this problem by a large margin."}],"author":[{"last_name":"Majumdar","full_name":"Majumdar, Rupak","first_name":"Rupak"},{"orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","last_name":"Mallik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"full_name":"Schmuck, Anne Kathrin","last_name":"Schmuck","first_name":"Anne Kathrin"},{"last_name":"Soudjani","full_name":"Soudjani, Sadegh","first_name":"Sadegh"}],"arxiv":1,"article_processing_charge":"No","volume":51,"oa":1,"date_updated":"2023-12-13T12:58:56Z","publication_identifier":{"issn":["1751-570X"]},"_id":"14400","quality_controlled":"1","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"}],"oa_version":"Published Version","acknowledgement":"We thank Daniel Hausmann and Nir Piterman for their valuable comments on an earlier version of the manuscript of our other paper [22] where we present, among other things, the parity fixpoint for 2 1/2-player games (for a slightly more general class of games) with a different and indirect proof of correctness. Based on their comments we observed that, unlike the other fixpoints that we present in [22], the parity fixpoint does not follow the exact same structure as its counterpart for 2-player games, which we also use int his paper.\r\nWe also thank Thejaswini Raghavan for observing that our symbolic parity fixpoint algorithm can be solved in quasi-polynomial time using recent improved algorithms for solving \r\n-calculus expressions. This significantly improved the complexity bounds of our algorithm in this paper.\r\nThe work of R. Majumdar and A.-K. Schmuck are partially supported by DFG, Germany project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG, Germany project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1016/j.nahs.2023.101430","year":"2023","ec_funded":1,"external_id":{"isi":["001093188100001"],"arxiv":["2101.00834"]},"title":"Symbolic control for stochastic systems via finite parity games","main_file_link":[{"url":"https://doi.org/10.1016/j.nahs.2023.101430","open_access":"1"}],"isi":1,"article_number":"101430","day":"27","type":"journal_article","intvolume":"        51","status":"public","publication":"Nonlinear Analysis: Hybrid Systems","month":"09","date_published":"2023-09-27T00:00:00Z","article_type":"original","scopus_import":"1","publisher":"Elsevier","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"date_created":"2023-10-08T22:01:15Z"},{"publication":"23rd International Conference on Runtime Verification","page":"291-311","intvolume":"     14245","status":"public","day":"01","type":"conference","conference":{"end_date":"2023-10-06","location":"Thessaloniki, Greece","name":"RV: Conference on Runtime Verification","start_date":"2023-10-03"},"date_created":"2023-10-29T23:01:15Z","department":[{"_id":"ToHe"}],"scopus_import":"1","publisher":"Springer Nature","language":[{"iso":"eng"}],"month":"10","date_published":"2023-10-01T00:00:00Z","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031442667"],"eissn":["1611-3349"]},"_id":"14454","quality_controlled":"1","oa_version":"Preprint","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"article_processing_charge":"No","volume":14245,"oa":1,"date_updated":"2023-10-31T11:48:20Z","abstract":[{"text":"As AI and machine-learned software are used increasingly for making decisions that affect humans, it is imperative that they remain fair and unbiased in their decisions. To complement design-time bias mitigation measures, runtime verification techniques have been introduced recently to monitor the algorithmic fairness of deployed systems. Previous monitoring techniques assume full observability of the states of the (unknown) monitored system. Moreover, they can monitor only fairness properties that are specified as arithmetic expressions over the probabilities of different events. In this work, we extend fairness monitoring to systems modeled as partially observed Markov chains (POMC), and to specifications containing arithmetic expressions over the expected values of numerical functions on event sequences. The only assumptions we make are that the underlying POMC is aperiodic and starts in the stationary distribution, with a bound on its mixing time being known. These assumptions enable us to estimate a given property for the entire distribution of possible executions of the monitored POMC, by observing only a single execution. Our monitors observe a long run of the system and, after each new observation, output updated PAC-estimates of how fair or biased the system is. The monitors are computationally lightweight and, using a prototype implementation, we demonstrate their effectiveness on several real-world examples.","lang":"eng"}],"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin","orcid":"0000-0001-8974-2542","last_name":"Kueffner","full_name":"Kueffner, Konstantin"},{"first_name":"Kaushik","last_name":"Mallik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"}],"citation":{"short":"T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference on Runtime Verification, Springer Nature, 2023, pp. 291–311.","ista":"Henzinger TA, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness under partial observations. 23rd International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 14245, 291–311.","mla":"Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness under Partial Observations.” <i>23rd International Conference on Runtime Verification</i>, vol. 14245, Springer Nature, 2023, pp. 291–311, doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_15\">10.1007/978-3-031-44267-4_15</a>.","ama":"Henzinger TA, Kueffner K, Mallik K. Monitoring algorithmic fairness under partial observations. In: <i>23rd International Conference on Runtime Verification</i>. Vol 14245. Springer Nature; 2023:291-311. doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_15\">10.1007/978-3-031-44267-4_15</a>","chicago":"Henzinger, Thomas A, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness under Partial Observations.” In <i>23rd International Conference on Runtime Verification</i>, 14245:291–311. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_15\">https://doi.org/10.1007/978-3-031-44267-4_15</a>.","apa":"Henzinger, T. A., Kueffner, K., &#38; Mallik, K. (2023). Monitoring algorithmic fairness under partial observations. In <i>23rd International Conference on Runtime Verification</i> (Vol. 14245, pp. 291–311). Thessaloniki, Greece: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_15\">https://doi.org/10.1007/978-3-031-44267-4_15</a>","ieee":"T. A. Henzinger, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness under partial observations,” in <i>23rd International Conference on Runtime Verification</i>, Thessaloniki, Greece, 2023, vol. 14245, pp. 291–311."},"publication_status":"published","alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2308.00341"}],"title":"Monitoring algorithmic fairness under partial observations","external_id":{"arxiv":["2308.00341"]},"doi":"10.1007/978-3-031-44267-4_15","year":"2023","ec_funded":1},{"publication":"35th International Conference on Computer Aided Verification","page":"3-15","file_date_updated":"2024-01-09T10:01:07Z","day":"16","type":"conference","intvolume":"     13966","status":"public","has_accepted_license":"1","department":[{"_id":"ToHe"}],"conference":{"end_date":"2023-07-22","name":"CAV: Computer Aided Verification","location":"Paris, France","start_date":"2023-07-17"},"file":[{"checksum":"1a361d83db0244fd32c03b544c294b5a","date_created":"2024-01-09T10:01:07Z","file_size":405147,"file_name":"2023_LNCSCAV_Majumdar.pdf","access_level":"open_access","date_updated":"2024-01-09T10:01:07Z","success":1,"creator":"dernst","file_id":"14765","relation":"main_file","content_type":"application/pdf"}],"date_created":"2024-01-08T13:18:00Z","month":"07","date_published":"2023-07-16T00:00:00Z","publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"volume":13966,"date_updated":"2024-02-27T07:39:51Z","oa":1,"article_processing_charge":"Yes (in subscription journal)","_id":"14758","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783031377099"],"isbn":["9783031377082"],"eissn":["1611-3349"]},"acknowledgement":"Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"oa_version":"Published Version","quality_controlled":"1","publication_status":"published","citation":{"mla":"Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” <i>35th International Conference on Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>.","ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In: <i>35th International Conference on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:3-15. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 3–15.","ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 3–15.","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties,” in <i>35th International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 3–15.","apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In <i>35th International Conference on Computer Aided Verification</i> (Vol. 13966, pp. 3–15). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>","chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” In <i>35th International Conference on Computer Aided Verification</i>, 13966:3–15. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>."},"abstract":[{"text":"We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-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.","lang":"eng"}],"author":[{"first_name":"Rupak","last_name":"Majumdar","full_name":"Majumdar, Rupak"},{"orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","last_name":"Mallik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"full_name":"Rychlicki, Mateusz","last_name":"Rychlicki","first_name":"Mateusz"},{"first_name":"Anne-Kathrin","last_name":"Schmuck","full_name":"Schmuck, Anne-Kathrin"},{"first_name":"Sadegh","last_name":"Soudjani","full_name":"Soudjani, Sadegh"}],"alternative_title":["LNCS"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"related_material":{"record":[{"status":"public","id":"14994","relation":"research_data"}]},"ddc":["000"],"doi":"10.1007/978-3-031-37709-9_1","year":"2023","ec_funded":1,"title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties"},{"volume":2,"date_updated":"2024-02-05T10:21:51Z","oa":1,"article_processing_charge":"Yes","arxiv":1,"acknowledgement":"A previous version of this paper has appeared in TACAS 2022. Authors ordered alphabetically. T. Banerjee was interning with MPI-SWS when this research was conducted. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"oa_version":"Published Version","_id":"14920","publication_identifier":{"issn":["2751-4838"]},"publication_status":"published","citation":{"ista":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2023. Fast symbolic algorithms for mega-regular games under strong transition fairness. TheoretiCS. 2, 4.","short":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS 2 (2023).","mla":"Banerjee, Tamajit, et al. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” <i>TheoretiCS</i>, vol. 2, 4, EPI Sciences, 2023, doi:<a href=\"https://doi.org/10.46298/theoretics.23.4\">10.46298/theoretics.23.4</a>.","ama":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. Fast symbolic algorithms for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. 2023;2. doi:<a href=\"https://doi.org/10.46298/theoretics.23.4\">10.46298/theoretics.23.4</a>","chicago":"Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, and Sadegh Soudjani. “Fast Symbolic Algorithms for Mega-Regular Games under Strong Transition Fairness.” <i>TheoretiCS</i>. EPI Sciences, 2023. <a href=\"https://doi.org/10.46298/theoretics.23.4\">https://doi.org/10.46298/theoretics.23.4</a>.","apa":"Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., &#38; Soudjani, S. (2023). Fast symbolic algorithms for mega-regular games under strong transition fairness. <i>TheoretiCS</i>. EPI Sciences. <a href=\"https://doi.org/10.46298/theoretics.23.4\">https://doi.org/10.46298/theoretics.23.4</a>","ieee":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “Fast symbolic algorithms for mega-regular games under strong transition fairness,” <i>TheoretiCS</i>, vol. 2. EPI Sciences, 2023."},"author":[{"full_name":"Banerjee, Tamajit","last_name":"Banerjee","first_name":"Tamajit"},{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"first_name":"Kaushik","last_name":"Mallik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck","first_name":"Anne-Kathrin"},{"last_name":"Soudjani","full_name":"Soudjani, Sadegh","first_name":"Sadegh"}],"abstract":[{"text":"We consider fixpoint algorithms for two-player games on graphs with $\\omega$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the\r\nsource vertex of a live edge is visited infinitely often along a play, the edge itself is traversed infinitely often along the play as well. We show that, surprisingly, strong transition fairness retains the algorithmic characteristics of the fixpoint algorithms for $\\omega$-regular games -- the new algorithms have the same alternation depth as the classical algorithms but invoke a new type of predecessor operator. For Rabin games with $k$ pairs, the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is independent of the number of live edges in the strong transition fairness assumption. Further, we show that GR(1) specifications with strong transition fairness assumptions can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm. In contrast, strong fairness necessarily requires increasing the alternation depth depending on the number of fairness assumptions. We get symbolic algorithms for (generalized) Rabin, parity and GR(1) objectives under strong transition fairness assumptions as well as a direct symbolic algorithm for qualitative winning in stochastic\r\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving the state of the art. Finally, we have implemented a BDD-based synthesis engine based on our algorithm. We show on a set of synthetic and real benchmarks that our algorithm is scalable, parallelizable, and outperforms previous algorithms by orders of magnitude.","lang":"eng"}],"article_number":"4","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["000"],"ec_funded":1,"year":"2023","doi":"10.46298/theoretics.23.4","title":"Fast symbolic algorithms for mega-regular games under strong transition fairness","external_id":{"arxiv":["2202.07480"]},"file_date_updated":"2024-02-05T10:19:35Z","publication":"TheoretiCS","type":"journal_article","day":"24","status":"public","intvolume":"         2","department":[{"_id":"ToHe"}],"has_accepted_license":"1","date_created":"2024-01-31T13:40:49Z","file":[{"file_id":"14940","creator":"dernst","content_type":"application/pdf","relation":"main_file","success":1,"date_updated":"2024-02-05T10:19:35Z","access_level":"open_access","date_created":"2024-02-05T10:19:35Z","checksum":"2972d531122a6f15727b396110fb3f5c","file_name":"2023_TheoretiCS_Banerjee.pdf","file_size":917076}],"article_type":"original","date_published":"2023-02-24T00:00:00Z","month":"02","language":[{"iso":"eng"}],"publisher":"EPI Sciences"},{"date_created":"2024-02-14T15:13:00Z","ddc":["000"],"related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"14758"}]},"department":[{"_id":"ToHe"}],"main_file_link":[{"url":"https://doi.org/10.5281/zenodo.7877790","open_access":"1"}],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"has_accepted_license":"1","publisher":"Zenodo","title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","date_published":"2023-04-28T00:00:00Z","year":"2023","doi":"10.5281/ZENODO.7877790","month":"04","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","_id":"14994","date_updated":"2024-02-27T07:39:51Z","oa":1,"article_processing_charge":"No","status":"public","author":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","last_name":"Mallik","full_name":"Mallik, Kaushik","first_name":"Kaushik"},{"full_name":"Rychlicki, Mateusz","last_name":"Rychlicki","first_name":"Mateusz"},{"last_name":"Schmuck","full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin"},{"first_name":"Sadegh","full_name":"Soudjani, Sadegh","last_name":"Soudjani"}],"abstract":[{"text":"This resource contains the artifacts for reproducing the experimental results presented in the paper titled \"A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties\" that has been submitted in CAV 2023.","lang":"eng"}],"type":"research_data_reference","day":"28","citation":{"apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.7877790\">https://doi.org/10.5281/ZENODO.7877790</a>","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties.” Zenodo, 2023.","chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.7877790\">https://doi.org/10.5281/ZENODO.7877790</a>.","mla":"Majumdar, Rupak, et al. <i>A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>.","ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>","ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.7877790\">10.5281/ZENODO.7877790</a>.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023)."}},{"alternative_title":["LNCS"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["000"],"doi":"10.1007/978-3-031-30820-8_15","year":"2023","title":"Computing adequately permissive assumptions for synthesis","oa":1,"date_updated":"2023-06-19T08:49:46Z","volume":13994,"article_processing_charge":"No","_id":"13141","publication_identifier":{"isbn":["9783031308192"],"issn":["0302-9743"],"eissn":["1611-3349"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","quality_controlled":"1","publication_status":"published","citation":{"ama":"Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions for synthesis. In: <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:211-228. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">10.1007/978-3-031-30820-8_15</a>","mla":"Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.” <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 211–28, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">10.1007/978-3-031-30820-8_15</a>.","short":"A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 211–228.","ista":"Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 211–228.","apa":"Anand, A., Mallik, K., Nayak, S. P., &#38; Schmuck, A. K. (2023). Computing adequately permissive assumptions for synthesis. In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 211–228). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">https://doi.org/10.1007/978-3-031-30820-8_15</a>","ieee":"A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately permissive assumptions for synthesis,” in <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13994, pp. 211–228.","chicago":"Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In <i>TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:211–28. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_15\">https://doi.org/10.1007/978-3-031-30820-8_15</a>."},"abstract":[{"text":"We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω\r\n-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.","lang":"eng"}],"author":[{"first_name":"Ashwani","last_name":"Anand","full_name":"Anand, Ashwani"},{"full_name":"Mallik, Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"last_name":"Nayak","full_name":"Nayak, Satya Prakash","first_name":"Satya Prakash"},{"first_name":"Anne Kathrin","full_name":"Schmuck, Anne Kathrin","last_name":"Schmuck"}],"has_accepted_license":"1","department":[{"_id":"ToHe"}],"conference":{"end_date":"2023-04-27","location":"Paris, France","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22"},"date_created":"2023-06-18T22:00:47Z","file":[{"file_size":521425,"file_name":"2023_LNCS_Anand.pdf","checksum":"60dcafc1b4f6f070be43bad3fe877974","date_created":"2023-06-19T08:43:21Z","access_level":"open_access","date_updated":"2023-06-19T08:43:21Z","success":1,"relation":"main_file","content_type":"application/pdf","creator":"dernst","file_id":"13151"}],"month":"04","date_published":"2023-04-20T00:00:00Z","publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","page":"211-228","file_date_updated":"2023-06-19T08:43:21Z","day":"20","type":"conference","intvolume":"     13994","status":"public"},{"citation":{"chicago":"Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Runtime Monitoring of Dynamic Fairness Properties.” In <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, 604–14. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3593013.3594028\">https://doi.org/10.1145/3593013.3594028</a>.","ieee":"T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Runtime monitoring of dynamic fairness properties,” in <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, Chicago, IL, United States, 2023, pp. 604–614.","apa":"Henzinger, T. A., Karimi, M., Kueffner, K., &#38; Mallik, K. (2023). Runtime monitoring of dynamic fairness properties. In <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i> (pp. 604–614). Chicago, IL, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3593013.3594028\">https://doi.org/10.1145/3593013.3594028</a>","short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency, Association for Computing Machinery, 2023, pp. 604–614.","ista":"Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Runtime monitoring of dynamic fairness properties. FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency. FAccT: Conference on Fairness, Accountability and Transparency, 604–614.","ama":"Henzinger TA, Karimi M, Kueffner K, Mallik K. Runtime monitoring of dynamic fairness properties. In: <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>. Association for Computing Machinery; 2023:604-614. doi:<a href=\"https://doi.org/10.1145/3593013.3594028\">10.1145/3593013.3594028</a>","mla":"Henzinger, Thomas A., et al. “Runtime Monitoring of Dynamic Fairness Properties.” <i>FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency</i>, Association for Computing Machinery, 2023, pp. 604–14, doi:<a href=\"https://doi.org/10.1145/3593013.3594028\">10.1145/3593013.3594028</a>."},"publication_status":"published","author":[{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mahyar","full_name":"Karimi, Mahyar","last_name":"Karimi"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin","last_name":"Kueffner"},{"orcid":"0000-0001-9864-7475","last_name":"Mallik","full_name":"Mallik, Kaushik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"}],"abstract":[{"text":"A machine-learned system that is fair in static decision-making tasks may have biased societal impacts in the long-run. This may happen when the system interacts with humans and feedback patterns emerge, reinforcing old biases in the system and creating new biases. While existing works try to identify and mitigate long-run biases through smart system design, we introduce techniques for monitoring fairness in real time. Our goal is to build and deploy a monitor that will continuously observe a long sequence of events generated by the system in the wild, and will output, with each event, a verdict on how fair the system is at the current point in time. The advantages of monitoring are two-fold. Firstly, fairness is evaluated at run-time, which is important because unfair behaviors may not be eliminated a priori, at design-time, due to partial knowledge about the system and the environment, as well as uncertainties and dynamic changes in the system and the environment, such as the unpredictability of human behavior. Secondly, monitors are by design oblivious to how the monitored system is constructed, which makes them suitable to be used as trusted third-party fairness watchdogs. They function as computationally lightweight statistical estimators, and their correctness proofs rely on the rigorous analysis of the stochastic process that models the assumptions about the underlying dynamics of the system. We show, both in theory and experiments, how monitors can warn us (1) if a bank’s credit policy over time has created an unfair distribution of credit scores among the population, and (2) if a resource allocator’s allocation policy over time has made unfair allocations. Our experiments demonstrate that the monitors introduce very low overhead. We believe that runtime monitoring is an important and mathematically rigorous new addition to the fairness toolbox.","lang":"eng"}],"article_processing_charge":"No","oa":1,"date_updated":"2023-12-13T11:30:31Z","arxiv":1,"quality_controlled":"1","oa_version":"Published Version","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"The authors would like to thank the anonymous reviewers for their valuable comments and helpful suggestions. This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","publication_identifier":{"isbn":["9781450372527"]},"_id":"13228","ec_funded":1,"doi":"10.1145/3593013.3594028","year":"2023","external_id":{"isi":["001062819300057"],"arxiv":["2305.04699"]},"title":"Runtime monitoring of dynamic fairness properties","isi":1,"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["000"],"type":"conference","day":"12","status":"public","file_date_updated":"2023-07-18T07:43:10Z","page":"604-614","publication":"FAccT '23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency","date_published":"2023-06-12T00:00:00Z","month":"06","language":[{"iso":"eng"}],"scopus_import":"1","publisher":"Association for Computing Machinery","department":[{"_id":"ToHe"}],"has_accepted_license":"1","file":[{"relation":"main_file","content_type":"application/pdf","creator":"dernst","file_id":"13245","success":1,"access_level":"open_access","date_updated":"2023-07-18T07:43:10Z","file_size":4100596,"file_name":"2023_ACM_HenzingerT.pdf","checksum":"96c759db9cdf94b81e37871a66a6ff48","date_created":"2023-07-18T07:43:10Z"}],"date_created":"2023-07-16T22:01:09Z","conference":{"start_date":"2023-06-12","location":"Chicago, IL, United States","end_date":"2023-06-15","name":"FAccT: Conference on Fairness, Accountability and Transparency"}},{"quality_controlled":"1","oa_version":"Published Version","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG101020093.","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031377037"],"isbn":["9783031377020"]},"_id":"13310","article_processing_charge":"Yes (in subscription journal)","date_updated":"2023-09-05T15:14:00Z","volume":13965,"oa":1,"arxiv":1,"author":[{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mahyar","orcid":"0009-0005-0820-1696","full_name":"Karimi, Mahyar","last_name":"Karimi","id":"f1dedef5-2f78-11ee-989a-c4c97bccf506"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542","first_name":"Konstantin"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","full_name":"Mallik, Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475"}],"abstract":[{"lang":"eng","text":"Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. Our monitors are of two types, and use, respectively, frequentist and Bayesian statistical inference techniques. While the frequentist monitors compute estimates that are objectively correct with respect to the ground truth, the Bayesian monitors compute estimates that are correct subject to a given prior belief about the system’s model. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. Although they exhibit different theoretical complexities in certain cases, in our experiments, both frequentist and Bayesian monitors took less than a millisecond to update their verdicts after each observation."}],"citation":{"ieee":"T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness,” in <i>Computer Aided Verification</i>, Paris, France, 2023, vol. 13965, pp. 358–382.","apa":"Henzinger, T. A., Karimi, M., Kueffner, K., &#38; Mallik, K. (2023). Monitoring algorithmic fairness. In <i>Computer Aided Verification</i> (Vol. 13965, pp. 358–382). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">https://doi.org/10.1007/978-3-031-37703-7_17</a>","chicago":"Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness.” In <i>Computer Aided Verification</i>, 13965:358–382. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">https://doi.org/10.1007/978-3-031-37703-7_17</a>.","ama":"Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness. In: <i>Computer Aided Verification</i>. Vol 13965. Springer Nature; 2023:358–382. doi:<a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">10.1007/978-3-031-37703-7_17</a>","mla":"Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” <i>Computer Aided Verification</i>, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:<a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">10.1007/978-3-031-37703-7_17</a>.","ista":"Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13965, 358–382.","short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification, Springer Nature, 2023, pp. 358–382."},"publication_status":"published","ddc":["000"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"alternative_title":["LNCS"],"title":"Monitoring algorithmic fairness","external_id":{"arxiv":["2305.15979"]},"ec_funded":1,"doi":"10.1007/978-3-031-37703-7_17","year":"2023","page":"358–382","file_date_updated":"2023-07-31T08:11:20Z","publication":"Computer Aided Verification","status":"public","intvolume":"     13965","type":"conference","day":"18","file":[{"file_id":"13327","creator":"dernst","relation":"main_file","content_type":"application/pdf","success":1,"access_level":"open_access","date_updated":"2023-07-31T08:11:20Z","checksum":"ccaf94bf7d658ba012c016e11869b54c","date_created":"2023-07-31T08:11:20Z","file_size":647760,"file_name":"2023_LNCS_CAV_HenzingerT.pdf"}],"date_created":"2023-07-25T18:32:40Z","conference":{"start_date":"2023-07-17","end_date":"2023-07-22","location":"Paris, France","name":"CAV: Computer Aided Verification"},"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"has_accepted_license":"1","language":[{"iso":"eng"}],"publisher":"Springer Nature","date_published":"2023-07-18T00:00:00Z","month":"07"},{"date_updated":"2023-02-09T08:58:48Z","oa":1,"volume":13244,"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","quality_controlled":"1","_id":"12529","publication_identifier":{"eisbn":["9783030995270"]},"extern":"1","publication_status":"published","citation":{"chicago":"Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Direct Symbolic Algorithm for Solving Stochastic Rabin Games.” In <i>28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 13244:81–98. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-99527-0_5\">https://doi.org/10.1007/978-3-030-99527-0_5</a>.","ieee":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “A direct symbolic algorithm for solving stochastic rabin games,” in <i>28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Munich, Germany, 2022, vol. 13244, pp. 81–98.","apa":"Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., &#38; Soudjani, S. (2022). A direct symbolic algorithm for solving stochastic rabin games. In <i>28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13244, pp. 81–98). Munich, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-99527-0_5\">https://doi.org/10.1007/978-3-030-99527-0_5</a>","short":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, in:, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2022, pp. 81–98.","ista":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2022. A direct symbolic algorithm for solving stochastic rabin games. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13244, 81–98.","ama":"Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. A direct symbolic algorithm for solving stochastic rabin games. In: <i>28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13244. Springer Nature; 2022:81-98. doi:<a href=\"https://doi.org/10.1007/978-3-030-99527-0_5\">10.1007/978-3-030-99527-0_5</a>","mla":"Banerjee, Tamajit, et al. “A Direct Symbolic Algorithm for Solving Stochastic Rabin Games.” <i>28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13244, Springer Nature, 2022, pp. 81–98, doi:<a href=\"https://doi.org/10.1007/978-3-030-99527-0_5\">10.1007/978-3-030-99527-0_5</a>."},"author":[{"first_name":"Tamajit","last_name":"Banerjee","full_name":"Banerjee, Tamajit"},{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","first_name":"Kaushik"},{"full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck","first_name":"Anne-Kathrin"},{"last_name":"Soudjani","full_name":"Soudjani, Sadegh","first_name":"Sadegh"}],"abstract":[{"text":"We consider turn-based stochastic 2-player games on graphs with ω-regular winning conditions. We provide a direct symbolic algorithm for solving such games when the winning condition is formulated as a Rabin condition. For a stochastic Rabin game with k pairs over a game graph with n vertices, our algorithm runs in O(nk+2k!) symbolic steps, which improves the state of the art.\r\nWe have implemented our symbolic algorithm, along with performance optimizations including parallellization and acceleration, in a BDD-based synthesis tool called Fairsyn. We demonstrate the superiority of Fairsyn compared to the state of the art on a set of synthetic benchmarks derived from the VLTS benchmark suite and on a control system benchmark from the literature. In our experiments, Fairsyn performed significantly faster with up to two orders of magnitude improvement in computation time.","lang":"eng"}],"main_file_link":[{"url":"https://doi.org/10.1007/978-3-030-99527-0_5","open_access":"1"}],"alternative_title":["LNCS"],"year":"2022","doi":"10.1007/978-3-030-99527-0_5","title":"A direct symbolic algorithm for solving stochastic rabin games","page":"81-98","publication":"28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","type":"conference","day":"29","status":"public","intvolume":"     13244","date_created":"2023-02-08T11:43:34Z","conference":{"start_date":"2022-04-02","location":"Munich, Germany","end_date":"2022-04-07","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"date_published":"2022-03-29T00:00:00Z","month":"03","language":[{"iso":"eng"}],"publisher":"Springer Nature","scopus_import":"1"},{"date_published":"2022-05-01T00:00:00Z","month":"05","doi":"10.1145/3501710.3519535","year":"2022","language":[{"iso":"eng"}],"scopus_import":"1","title":"BOCoSy: Small but powerful symbolic output-feedback control","publisher":"ACM","date_created":"2023-02-08T11:43:50Z","conference":{"start_date":"2022-05-04","end_date":"2022-05-06","location":"Milan, Italy","name":"HSCC: International Conference on Hybrid Systems Computation and Control"},"type":"conference","citation":{"ieee":"B. Finkbeiner, K. Mallik, N. Passing, M. Schledjewski, and A.-K. Schmuck, “BOCoSy: Small but powerful symbolic output-feedback control,” in <i>25th ACM International Conference on Hybrid Systems: Computation and Control</i>, Milan, Italy, 2022, p. 24:1-24:11.","apa":"Finkbeiner, B., Mallik, K., Passing, N., Schledjewski, M., &#38; Schmuck, A.-K. (2022). BOCoSy: Small but powerful symbolic output-feedback control. In <i>25th ACM International Conference on Hybrid Systems: Computation and Control</i> (p. 24:1-24:11). Milan, Italy: ACM. <a href=\"https://doi.org/10.1145/3501710.3519535\">https://doi.org/10.1145/3501710.3519535</a>","chicago":"Finkbeiner, Bernd, Kaushik Mallik, Noemi Passing, Malte Schledjewski, and Anne-Kathrin Schmuck. “BOCoSy: Small but Powerful Symbolic Output-Feedback Control.” In <i>25th ACM International Conference on Hybrid Systems: Computation and Control</i>, 24:1-24:11. ACM, 2022. <a href=\"https://doi.org/10.1145/3501710.3519535\">https://doi.org/10.1145/3501710.3519535</a>.","ama":"Finkbeiner B, Mallik K, Passing N, Schledjewski M, Schmuck A-K. BOCoSy: Small but powerful symbolic output-feedback control. In: <i>25th ACM International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2022:24:1-24:11. doi:<a href=\"https://doi.org/10.1145/3501710.3519535\">10.1145/3501710.3519535</a>","mla":"Finkbeiner, Bernd, et al. “BOCoSy: Small but Powerful Symbolic Output-Feedback Control.” <i>25th ACM International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2022, p. 24:1-24:11, doi:<a href=\"https://doi.org/10.1145/3501710.3519535\">10.1145/3501710.3519535</a>.","ista":"Finkbeiner B, Mallik K, Passing N, Schledjewski M, Schmuck A-K. 2022. BOCoSy: Small but powerful symbolic output-feedback control. 25th ACM International Conference on Hybrid Systems: Computation and Control. HSCC: International Conference on Hybrid Systems Computation and Control, 24:1-24:11.","short":"B. Finkbeiner, K. Mallik, N. Passing, M. Schledjewski, A.-K. Schmuck, in:, 25th ACM International Conference on Hybrid Systems: Computation and Control, ACM, 2022, p. 24:1-24:11."},"day":"01","publication_status":"published","author":[{"first_name":"Bernd","last_name":"Finkbeiner","full_name":"Finkbeiner, Bernd"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","first_name":"Kaushik"},{"first_name":"Noemi","last_name":"Passing","full_name":"Passing, Noemi"},{"last_name":"Schledjewski","full_name":"Schledjewski, Malte","first_name":"Malte"},{"first_name":"Anne-Kathrin","last_name":"Schmuck","full_name":"Schmuck, Anne-Kathrin"}],"status":"public","abstract":[{"text":"We present BOCoSy, a tool for Bounded symbolic Output-feedback Controller Synthesis. Given a specification, BOCoSy synthesizes symbolic output-feedback controllers which interact with a given plant via a pre-defined finite symbolic interface. BOCoSy solves this problem by a new lazy abstraction-refinement technique which starts with a very coarse abstraction of the external trace semantics of the given plant and iteratively removes non-admissible behavior from this abstract model until a controller is found. BOCoSy steers the search for controllers towards small and concise state space representations by utilizing ideas from bounded synthesis. As a result, BOCoSy returns small and explainable controllers that are still powerful enough to solve the given synthesis problem. We show that BOCoSy is able to synthesize small, human readable symbolic controllers quickly on a set of benchmarks.","lang":"eng"}],"page":"24:1-24:11","article_processing_charge":"No","date_updated":"2023-02-09T08:53:13Z","publication":"25th ACM International Conference on Hybrid Systems: Computation and Control","quality_controlled":"1","oa_version":"None","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","extern":"1","publication_identifier":{"isbn":["9781450391962"]},"_id":"12530"}]