[{"page":"237-257","type":"conference","publisher":"Springer Nature","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783032325181"]},"file":[{"date_updated":"2026-08-18T08:40:07Z","file_name":"2026_LNCS_Avni.pdf","file_id":"22730","date_created":"2026-08-18T08:40:07Z","content_type":"application/pdf","file_size":531980,"access_level":"open_access","success":1,"creator":"dernst","relation":"main_file","checksum":"f17ba3f82854fdb4eb69fd922965661a"}],"license":"https://creativecommons.org/licenses/by/4.0/","supplementarymaterial":"no","date_updated":"2026-08-18T08:41:44Z","oa":1,"date_created":"2026-08-16T22:01:44Z","ec_funded":1,"alternative_title":["LNCS"],"volume":16682,"publication":"38th International Conference on Computer Aided Verification","das_tickbox":"0","has_accepted_license":"1","acknowledgement":"This work is funded by the following grants: European Research Council under Grant No.: ERC-2020-AdG 101020093, ISF grant no. 1679/21, grant RYC2024-049116, MICIU/AEI/10.13039/501100011033, the ESF+, and Volkswagen Foundation within its Momentum framework under project no. 9C283.","intvolume":"     16682","doi":"10.1007/978-3-032-32519-8_13","_id":"22719","status":"public","quality_controlled":"1","author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"first_name":"Kaushik","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","last_name":"Mallik"},{"first_name":"Suman","full_name":"Sadhukhan, Suman","last_name":"Sadhukhan"},{"last_name":"Thejaswini","first_name":"K. S.","full_name":"Thejaswini, K. S."}],"oa_version":"Published Version","ddc":["000"],"fulldoi":"https://doi.org/10.1007/978-3-032-32519-8_13","conference":{"start_date":"2026-07-26","name":"CAV: Computer Aided Verification","end_date":"2026-07-29","location":"Lisbon, Portugal"},"external_id":{"arxiv":["2605.13185"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"OA_place":"publisher","article_processing_charge":"Yes (in subscription journal)","arxiv":1,"scopus_import":"1","language":[{"iso":"eng"}],"day":"24","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020"}],"OA_type":"hybrid","publication_status":"published","file_date_updated":"2026-08-18T08:40:07Z","department":[{"_id":"ToHe"}],"year":"2026","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2026-07-24T00:00:00Z","abstract":[{"text":"We study the problem of generating paths on a graph that satisfy a collection of w-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions—simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of w-regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.","lang":"eng"}],"researchdata_availability":"no","title":"Decoupled planning for multiple omega-regular objectives","month":"07","citation":{"ama":"Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. Decoupled planning for multiple omega-regular objectives. In: <i>38th International Conference on Computer Aided Verification</i>. Vol 16682. Springer Nature; 2026:237-257. doi:<a href=\"https://doi.org/10.1007/978-3-032-32519-8_13\">10.1007/978-3-032-32519-8_13</a>","chicago":"Avni, Guy, Thomas A Henzinger, Kaushik Mallik, Suman Sadhukhan, and K. S. Thejaswini. “Decoupled Planning for Multiple Omega-Regular Objectives.” In <i>38th International Conference on Computer Aided Verification</i>, 16682:237–57. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-32519-8_13\">https://doi.org/10.1007/978-3-032-32519-8_13</a>.","short":"G. Avni, T.A. Henzinger, K. Mallik, S. Sadhukhan, K.S. Thejaswini, in:, 38th International Conference on Computer Aided Verification, Springer Nature, 2026, pp. 237–257.","ieee":"G. Avni, T. A. Henzinger, K. Mallik, S. Sadhukhan, and K. S. Thejaswini, “Decoupled planning for multiple omega-regular objectives,” in <i>38th International Conference on Computer Aided Verification</i>, Lisbon, Portugal, 2026, vol. 16682, pp. 237–257.","apa":"Avni, G., Henzinger, T. A., Mallik, K., Sadhukhan, S., &#38; Thejaswini, K. S. (2026). Decoupled planning for multiple omega-regular objectives. In <i>38th International Conference on Computer Aided Verification</i> (Vol. 16682, pp. 237–257). Lisbon, Portugal: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-32519-8_13\">https://doi.org/10.1007/978-3-032-32519-8_13</a>","mla":"Avni, Guy, et al. “Decoupled Planning for Multiple Omega-Regular Objectives.” <i>38th International Conference on Computer Aided Verification</i>, vol. 16682, Springer Nature, 2026, pp. 237–57, doi:<a href=\"https://doi.org/10.1007/978-3-032-32519-8_13\">10.1007/978-3-032-32519-8_13</a>.","ista":"Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. 2026. Decoupled planning for multiple omega-regular objectives. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 16682, 237–257."}},{"date_updated":"2026-09-17T09:44:41Z","supplementarymaterial":"yes","file":[{"file_id":"22946","file_name":"2026_LIPIcsCONCUR_Asadi.pdf","date_updated":"2026-09-17T09:43:28Z","date_created":"2026-09-17T09:43:28Z","access_level":"open_access","success":1,"file_size":1175682,"content_type":"application/pdf","checksum":"de9af748d78fa42c173f68a71cbbd8d9","creator":"dernst","relation":"main_file"}],"publication_identifier":{"isbn":["9783959774475"],"eissn":["1868-8969"]},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","type":"conference","keyword":["Bidding Games","Stochastic Games"],"acknowledgement":"The research was partially supported by Austrian Science Fund (FWF) 10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), ERC-2020-AdG 101020093\r\n(VAMOS), and the RYC2024-049116-I grant funded by MICIU/AEI/10.13039/501100011033 and\r\nESF+.\r\n","has_accepted_license":"1","publication":"37th International Conference on Concurrency Theory","das_tickbox":"0","volume":391,"alternative_title":["LIPIcs"],"ec_funded":1,"date_created":"2026-09-13T22:01:53Z","oa":1,"scopus_import":"1","arxiv":1,"OA_place":"publisher","article_processing_charge":"Yes","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_number":"13:1-13:20","external_id":{"arxiv":["2606.29420"]},"conference":{"name":"CONCUR: Conference on Concurrency Theory","start_date":"2026-09-01","location":"Liverpool, United Kingdom","end_date":"2026-09-04"},"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13","ddc":["000"],"oa_version":"Published Version","corr_author":"1","_id":"22920","quality_controlled":"1","status":"public","author":[{"last_name":"Asadi","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","full_name":"Asadi, Ali","first_name":"Ali"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Kafshdar Goharshadi, Ehsan","first_name":"Ehsan","last_name":"Kafshdar Goharshadi","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587"},{"full_name":"Kebis, Pavol","first_name":"Pavol","last_name":"Kebis","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a"},{"full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475"}],"doi":"10.4230/LIPIcs.CONCUR.2026.13","intvolume":"       391","title":"Generalized bidding games: Where bidding and stochastic games meet","month":"08","citation":{"short":"A. Asadi, T.A. Henzinger, E. Goharshady, P. Kebis, K. Mallik, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","apa":"Asadi, A., Henzinger, T. A., Goharshady, E., Kebis, P., &#38; Mallik, K. (2026). Generalized bidding games: Where bidding and stochastic games meet. In <i>37th International Conference on Concurrency Theory</i> (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.13</a>","ieee":"A. Asadi, T. A. Henzinger, E. Goharshady, P. Kebis, and K. Mallik, “Generalized bidding games: Where bidding and stochastic games meet,” in <i>37th International Conference on Concurrency Theory</i>, Liverpool, United Kingdom, 2026, vol. 391.","chicago":"Asadi, Ali, Thomas A Henzinger, Ehsan Goharshady, Pavol Kebis, and Kaushik Mallik. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.” In <i>37th International Conference on Concurrency Theory</i>, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.13</a>.","ama":"Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. Generalized bidding games: Where bidding and stochastic games meet. In: <i>37th International Conference on Concurrency Theory</i>. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">10.4230/LIPIcs.CONCUR.2026.13</a>","mla":"Asadi, Ali, et al. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.” <i>37th International Conference on Concurrency Theory</i>, vol. 391, 13:1-13:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.13\">10.4230/LIPIcs.CONCUR.2026.13</a>.","ista":"Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. 2026. Generalized bidding games: Where bidding and stochastic games meet. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 13:1-13:20."},"abstract":[{"lang":"eng","text":"Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the right to move the token is determined by the current vertex. In traditional bidding games - referred to as pure bidding games - the right to move the token is determined at each step through bidding; here we consider Richman bidding, where the winning player of a bid pays the losing player. The winner is decided based on a temporal or quantitative specification evaluated over the resulting infinite play.\r\nIn this work, we combine turn-based games and pure bidding games into generalized bidding games, with player-1 vertices, player-2 vertices, and bidding vertices. This natural and simple generalization of bidding games has far-reaching consequences. First, we show that, as a model, generalized bidding games are more expressive than pure bidding games, and we provide several applications. Second, and most importantly, we show that generalized Richman bidding games are structurally equivalent to simple stochastic games, a well-studied model: they are linearly interreducible to each other. As was previously known, the special case of pure Richman bidding games corresponds to random-turn games. In other words, generalized bidding games extend pure bidding games in the same way that simple stochastic games extend random-turn games. We use this connection to solve generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff and discounted-sum) specifications. From a computational perspective, we establish that generalized bidding games with parity and mean-payoff specifications retain the best known upper bounds for turn-based games and pure bidding games, namely NP∩coNP.\r\nFinally, we study a repair problem that asks whether bidding vertices can be assigned \"owners\" so as to bring the threshold budget required to win the game below a given target. This problem has direct applications in compositional policy synthesis for multi-objective settings, and we show it to be NP-complete."}],"researchdata_availability":"no","date_published":"2026-08-24T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2026","department":[{"_id":"GradSch"},{"_id":"KrCh"},{"_id":"ToHe"}],"file_date_updated":"2026-09-17T09:43:28Z","publication_status":"published","OA_type":"gold","project":[{"name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"},{"grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy"},{"call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"language":[{"iso":"eng"}],"day":"24"},{"publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"page":"15659-15668","publisher":"Association for the Advancement of Artificial Intelligence","type":"conference","date_updated":"2026-02-16T12:24:30Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2412.11994","open_access":"1"}],"oa":1,"volume":39,"ec_funded":1,"acknowledgement":"This work is partly supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093. It is also partially supported by the State Government of Styria, Austria – Department Zukunftsfonds Steiermark.","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","issue":"15","date_created":"2025-05-11T22:02:39Z","fulldoi":"https://doi.org/10.1609/aaai.v39i15.33719","_id":"19665","status":"public","author":[{"first_name":"Filip","full_name":"Cano Cordoba, Filip","orcid":"0000-0002-0783-904X","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","last_name":"Cano Cordoba"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Könighofer","full_name":"Könighofer, Bettina","first_name":"Bettina"},{"first_name":"Konstantin","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner"},{"last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","first_name":"Kaushik"}],"quality_controlled":"1","intvolume":"        39","doi":"10.1609/aaai.v39i15.33719","oa_version":"Preprint","corr_author":"1","arxiv":1,"article_processing_charge":"No","OA_place":"repository","scopus_import":"1","conference":{"start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence","end_date":"2025-03-04","location":"Philadelphia, PA, United States"},"external_id":{"arxiv":["2412.11994"]},"publication_status":"published","department":[{"_id":"ToHe"}],"project":[{"call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"language":[{"iso":"eng"}],"day":"11","OA_type":"green","abstract":[{"lang":"eng","text":"As AI-based decision-makers increasingly influence human lives, it is a growing concern that their decisions may be unfair or biased with respect to people's protected attributes, such as gender and race. Most existing bias prevention measures provide probabilistic fairness guarantees in the long run, and it is possible that the decisions are biased on any decision sequence of fixed length. We introduce *fairness shielding*, where a symbolic decision-maker---the fairness shield---continuously monitors the sequence of decisions of another deployed black-box decision-maker, and makes interventions so that a given fairness criterion is met while the total intervention costs are minimized. We present four different algorithms for computing fairness shields, among which one guarantees fairness over fixed horizons, and three guarantee fairness periodically after fixed intervals. Given a distribution over future decisions and their intervention costs, our algorithms solve different instances of bounded-horizon optimal control problems with different levels of computational costs and optimality guarantees. Our empirical evaluation demonstrates the effectiveness of these shields in ensuring fairness while maintaining cost efficiency across various scenarios."}],"date_published":"2025-04-11T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"04","citation":{"apa":"Cano Cordoba, F., Henzinger, T. A., Könighofer, B., Kueffner, K., &#38; Mallik, K. (2025). Fairness shields: Safeguarding against biased decision makers. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 15659–15668). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">https://doi.org/10.1609/aaai.v39i15.33719</a>","ieee":"F. Cano Cordoba, T. A. Henzinger, B. Könighofer, K. Kueffner, and K. Mallik, “Fairness shields: Safeguarding against biased decision makers,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 15, pp. 15659–15668.","short":"F. Cano Cordoba, T.A. Henzinger, B. Könighofer, K. Kueffner, K. Mallik, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 15659–15668.","chicago":"Cano Cordoba, Filip, Thomas A Henzinger, Bettina Könighofer, Konstantin Kueffner, and Kaushik Mallik. “Fairness Shields: Safeguarding against Biased Decision Makers.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:15659–68. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">https://doi.org/10.1609/aaai.v39i15.33719</a>.","ama":"Cano Cordoba F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. Fairness shields: Safeguarding against biased decision makers. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:15659-15668. doi:<a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">10.1609/aaai.v39i15.33719</a>","mla":"Cano Cordoba, Filip, et al. “Fairness Shields: Safeguarding against Biased Decision Makers.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 15, Association for the Advancement of Artificial Intelligence, 2025, pp. 15659–68, doi:<a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">10.1609/aaai.v39i15.33719</a>.","ista":"Cano Cordoba F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. 2025. Fairness shields: Safeguarding against biased decision makers. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 15659–15668."},"title":"Fairness shields: Safeguarding against biased decision makers","year":"2025"},{"has_accepted_license":"1","acknowledgement":"This work was supported in part by the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SIS-SMU-100) and the ERC project ERC-2020-AdG 101020093.","publication":"37th International Conference on Computer Aided Verification","alternative_title":["LNCS"],"volume":15932,"ec_funded":1,"date_created":"2025-08-24T22:01:31Z","oa":1,"date_updated":"2025-12-01T12:34:41Z","file":[{"date_created":"2025-09-02T07:34:33Z","date_updated":"2025-09-02T07:34:33Z","file_name":"2025_CAV_HenzingerT.pdf","file_id":"20272","relation":"main_file","creator":"dernst","checksum":"beb1e2637de5b2268cc2262119439113","file_size":884831,"content_type":"application/pdf","success":1,"access_level":"open_access"}],"isi":1,"publication_identifier":{"isbn":["9783031986789"],"issn":["0302-9743"],"eissn":["1611-3349"]},"publisher":"Springer Nature","type":"conference","page":"29-55","title":"Supermartingale certificates for quantitative omega-regular verification and control","month":"07","citation":{"mla":"Henzinger, Thomas A., et al. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” <i>37th International Conference on Computer Aided Verification</i>, vol. 15932, Springer Nature, 2025, pp. 29–55, doi:<a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">10.1007/978-3-031-98679-6_2</a>.","ista":"Henzinger TA, Mallik K, Sadeghi P, Zikelic D. 2025. Supermartingale certificates for quantitative omega-regular verification and control. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15932, 29–55.","ieee":"T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates for quantitative omega-regular verification and control,” in <i>37th International Conference on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15932, pp. 29–55.","apa":"Henzinger, T. A., Mallik, K., Sadeghi, P., &#38; Zikelic, D. (2025). Supermartingale certificates for quantitative omega-regular verification and control. In <i>37th International Conference on Computer Aided Verification</i> (Vol. 15932, pp. 29–55). Zagreb, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">https://doi.org/10.1007/978-3-031-98679-6_2</a>","short":"T.A. Henzinger, K. Mallik, P. Sadeghi, D. Zikelic, in:, 37th International Conference on Computer Aided Verification, Springer Nature, 2025, pp. 29–55.","chicago":"Henzinger, Thomas A, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” In <i>37th International Conference on Computer Aided Verification</i>, 15932:29–55. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">https://doi.org/10.1007/978-3-031-98679-6_2</a>.","ama":"Henzinger TA, Mallik K, Sadeghi P, Zikelic D. Supermartingale certificates for quantitative omega-regular verification and control. In: <i>37th International Conference on Computer Aided Verification</i>. Vol 15932. Springer Nature; 2025:29-55. doi:<a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">10.1007/978-3-031-98679-6_2</a>"},"date_published":"2025-07-22T00:00:00Z","abstract":[{"lang":"eng","text":"We present the first supermartingale certificate for quantitative \r\n-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied only to quantitative reachability, safety, or reach-avoid properties, and to qualitative (i.e., probability 1) \r\n-regular properties.We also present fully automated algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic system dynamics and the controller can be represented in terms of polynomial inequalities. Our experiments demonstrate the ability of our method to solve verification and control tasks for stochastic systems that were beyond the reach of previous supermartingale-based approaches."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","file_date_updated":"2025-09-02T07:34:33Z","department":[{"_id":"ToHe"}],"publication_status":"published","OA_type":"hybrid","project":[{"call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"day":"22","language":[{"iso":"eng"}],"scopus_import":"1","arxiv":1,"article_processing_charge":"Yes (in subscription journal)","OA_place":"publisher","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"external_id":{"isi":["001562506600002"],"arxiv":["2505.18833"]},"conference":{"location":"Zagreb, Croatia","end_date":"2025-07-25","start_date":"2025-07-23","name":"CAV: Computer Aided Verification"},"fulldoi":"https://doi.org/10.1007/978-3-031-98679-6_2","ddc":["000"],"oa_version":"Published Version","_id":"20225","quality_controlled":"1","author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","first_name":"Kaushik"},{"first_name":"Pouya","full_name":"Sadeghi, Pouya","last_name":"Sadeghi"},{"first_name":"Dorde","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","last_name":"Zikelic"}],"status":"public","intvolume":"     15932","doi":"10.1007/978-3-031-98679-6_2"},{"conference":{"name":"L4DC: Learning for Dynamics & Control","start_date":"2025-06-04","location":"Ann Arbor, MI, United States","end_date":"2025-06-06"},"external_id":{"arxiv":["2412.16564"]},"article_processing_charge":"No","OA_place":"publisher","arxiv":1,"scopus_import":"1","intvolume":"       283","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"last_name":"Kresse","id":"faff3c84-23f6-11ef-9085-e5187b51c604","full_name":"Kresse, Fabian","first_name":"Fabian"},{"full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475"},{"last_name":"Yu","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi","first_name":"Zhengqi"},{"full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"_id":"20256","quality_controlled":"1","status":"public","corr_author":"1","oa_version":"Published Version","ddc":["000"],"year":"2025","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2025-06-01T00:00:00Z","abstract":[{"lang":"eng","text":"We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting future states of the system based on the states observed in the past. The numbers of past states and of predicted future states are parameters provided by the user. Our method is based on a combination of Taylor’s expansion and the backward difference operator for numerical differentiation. We also derive an upper bound on the prediction error under the assumption that the system dynamics and the controller are smooth. The predicted states are then used to predict safety violations ahead in time. Our experiments demonstrate practical applicability of our method for complex black-box systems, showing that it is computationally lightweight and yet significantly more accurate than the state-of-the-art predictive safety monitoring techniques."}],"citation":{"apa":"Henzinger, T. A., Kresse, F., Mallik, K., Yu, E., &#38; Zikelic, D. (2025). Predictive monitoring of black-box dynamical systems. In <i>7th Annual Learning for Dynamics &#38; Control Conference</i> (Vol. 283, pp. 804–816). Ann Arbor, MI, United States: ML Research Press.","short":"T.A. Henzinger, F. Kresse, K. Mallik, E. Yu, D. Zikelic, in:, 7th Annual Learning for Dynamics &#38; Control Conference, ML Research Press, 2025, pp. 804–816.","ieee":"T. A. Henzinger, F. Kresse, K. Mallik, E. Yu, and D. Zikelic, “Predictive monitoring of black-box dynamical systems,” in <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, Ann Arbor, MI, United States, 2025, vol. 283, pp. 804–816.","ama":"Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. Predictive monitoring of black-box dynamical systems. In: <i>7th Annual Learning for Dynamics &#38; Control Conference</i>. Vol 283. ML Research Press; 2025:804-816.","chicago":"Henzinger, Thomas A, Fabian Kresse, Kaushik Mallik, Emily Yu, and Dorde Zikelic. “Predictive Monitoring of Black-Box Dynamical Systems.” In <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, 283:804–16. ML Research Press, 2025.","ista":"Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. 2025. Predictive monitoring of black-box dynamical systems. 7th Annual Learning for Dynamics &#38; Control Conference. L4DC: Learning for Dynamics &#38; Control, PMLR, vol. 283, 804–816.","mla":"Henzinger, Thomas A., et al. “Predictive Monitoring of Black-Box Dynamical Systems.” <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, vol. 283, ML Research Press, 2025, pp. 804–16."},"month":"06","title":"Predictive monitoring of black-box dynamical systems","language":[{"iso":"eng"}],"day":"01","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020"}],"OA_type":"gold","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"ChLa"}],"file_date_updated":"2025-09-03T10:32:12Z","file":[{"date_created":"2025-09-03T10:32:12Z","file_name":"2025_L4DC_HenzingerT.pdf","file_id":"20283","date_updated":"2025-09-03T10:32:12Z","checksum":"d5236e561560635f5ae1d17de4903033","relation":"main_file","creator":"dernst","success":1,"access_level":"open_access","content_type":"application/pdf","file_size":489639}],"date_updated":"2025-09-03T10:37:59Z","page":"804-816","type":"conference","publisher":"ML Research Press","publication_identifier":{"eissn":["2640-3498"]},"date_created":"2025-08-31T22:01:32Z","ec_funded":1,"alternative_title":["PMLR"],"volume":283,"publication":"7th Annual Learning for Dynamics & Control Conference","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093.\r\n","has_accepted_license":"1","oa":1},{"oa":1,"ec_funded":1,"volume":2,"publication":"Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093 and the SBI Foundation Hub for Data Science &Analytics, IIT Bombay.","has_accepted_license":"1","date_created":"2025-09-07T22:01:33Z","publication_identifier":{"isbn":["9798400714542"],"issn":["2154-817X"]},"related_material":{"link":[{"url":"https://github.com/ariez-xyz/clemont","relation":"software"}],"record":[{"status":"public","id":"22808","relation":"dissertation_contains"}]},"page":"790-801","type":"conference","publisher":"Association for Computing Machinery","date_updated":"2026-09-18T07:41:29Z","file":[{"checksum":"81e18cdf9ca5f6dfa79425b326ea9725","creator":"dernst","relation":"main_file","access_level":"open_access","success":1,"content_type":"application/pdf","file_size":7745940,"date_created":"2025-09-08T08:46:31Z","file_id":"20310","file_name":"2025_KDD_Gupta.pdf","date_updated":"2025-09-08T08:46:31Z"}],"publication_status":"published","department":[{"_id":"ToHe"}],"file_date_updated":"2025-09-08T08:46:31Z","day":"03","language":[{"iso":"eng"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2025-08-03T00:00:00Z","abstract":[{"lang":"eng","text":"In automated decision-making, it is desirable that outputs of decision-makers be robust to slight perturbations in their inputs, a property that may be called input-output robustness. Input-output robustness appears in various different forms in the literature, such as robustness of AI models to adversarial or semantic perturbations and individual fairness of AI models that make decisions about humans. We propose runtime monitoring of input-output robustness of deployed, black-box AI models, where the goal is to design monitors that would observe one long execution sequence of the model, and would raise an alarm whenever it is detected that two similar inputs from the past led to dissimilar outputs. This way, monitoring will complement existing offline ''robustification'' approaches to increase the trustworthiness of AI decision-makers. We show that the monitoring problem can be cast as the fixed-radius nearest neighbor (FRNN) search problem, which, despite being well-studied, lacks suitable online solutions. We present our tool Clemont, which offers a number of lightweight monitors, some of which use upgraded online variants of existing FRNN algorithms, and one uses a novel algorithm based on binary decision diagrams--a data-structure commonly used in software and hardware verification. We have also developed an efficient parallelization technique that can substantially cut down the computation time of monitors for which the distance between input-output pairs is measured using the L∞norm. Using standard benchmarks from the literature of adversarial and semantic robustness and individual fairness, we perform a comparative study of different monitors in Clemont, and demonstrate their effectiveness in correctly detecting robustness violations at runtime."}],"citation":{"ieee":"A. Gupta, T. A. Henzinger, K. Kueffner, K. Mallik, and D. Pape, “Monitoring robustness and individual fairness,” in <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, Toronto, Canada, 2025, vol. 2, pp. 790–801.","apa":"Gupta, A., Henzinger, T. A., Kueffner, K., Mallik, K., &#38; Pape, D. (2025). Monitoring robustness and individual fairness. In <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i> (Vol. 2, pp. 790–801). Toronto, Canada: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3711896.3737054\">https://doi.org/10.1145/3711896.3737054</a>","short":"A. Gupta, T.A. Henzinger, K. Kueffner, K. Mallik, D. Pape, in:, Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining, Association for Computing Machinery, 2025, pp. 790–801.","ama":"Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. Monitoring robustness and individual fairness. In: <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>. Vol 2. Association for Computing Machinery; 2025:790-801. doi:<a href=\"https://doi.org/10.1145/3711896.3737054\">10.1145/3711896.3737054</a>","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Konstantin Kueffner, Kaushik Mallik, and David Pape. “Monitoring Robustness and Individual Fairness.” In <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, 2:790–801. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3711896.3737054\">https://doi.org/10.1145/3711896.3737054</a>.","ista":"Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. 2025. Monitoring robustness and individual fairness. Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining. KDD: Conference on Knowledge Discovery and Data Mining vol. 2, 790–801.","mla":"Gupta, Ashutosh, et al. “Monitoring Robustness and Individual Fairness.” <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, vol. 2, Association for Computing Machinery, 2025, pp. 790–801, doi:<a href=\"https://doi.org/10.1145/3711896.3737054\">10.1145/3711896.3737054</a>."},"month":"08","title":"Monitoring robustness and individual fairness","year":"2025","ddc":["000"],"fulldoi":"https://doi.org/10.1145/3711896.3737054","doi":"10.1145/3711896.3737054","intvolume":"         2","quality_controlled":"1","_id":"20292","status":"public","author":[{"first_name":"Ashutosh","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Kueffner, Konstantin","first_name":"Konstantin","last_name":"Kueffner","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","orcid":"0000-0001-8974-2542"},{"last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","first_name":"Kaushik"},{"last_name":"Pape","full_name":"Pape, David","first_name":"David"}],"corr_author":"1","oa_version":"Published Version","article_processing_charge":"No","OA_place":"publisher","arxiv":1,"scopus_import":"1","conference":{"start_date":"2025-08-03","name":"KDD: Conference on Knowledge Discovery and Data Mining","location":"Toronto, Canada","end_date":"2025-08-07"},"external_id":{"arxiv":["2506.00496"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"}},{"supplementarymaterial":"no","date_updated":"2026-10-21T12:02:55Z","file":[{"success":1,"access_level":"open_access","content_type":"application/pdf","file_size":1391381,"checksum":"cc6bb89be0eaa404a6ce019392cd293e","relation":"main_file","creator":"dernst","file_id":"17341","file_name":"2024_LIPICs_Cano.pdf","date_updated":"2024-07-29T11:15:59Z","date_created":"2024-07-29T11:15:59Z"}],"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773232"]},"isi":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","type":"conference","volume":299,"alternative_title":["LIPIcs"],"ec_funded":1,"has_accepted_license":"1","acknowledgement":"This work is partly supported by the European Research Council under Grant No.: ERC2020-AdG 101020093. It is also partially supported by the State Government of Styria, Austria –\r\nDepartment Zukunftsfonds Steiermark.","publication":"9th International Conference on Formal Structures for Computation and Deduction","das_tickbox":"0","date_created":"2024-07-28T22:01:09Z","oa":1,"article_processing_charge":"Yes","scopus_import":"1","conference":{"end_date":"2024-07-13","location":"Tallinn, Estonia","name":"FSCD: Conference on Formal Structures for Computation and Deduction","start_date":"2024-07-10"},"article_number":"2","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"external_id":{"isi":["001587746100002"]},"ddc":["000"],"fulldoi":"https://doi.org/10.4230/LIPIcs.FSCD.2024.2","author":[{"first_name":"Filip","full_name":"Cano, Filip","last_name":"Cano"},{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Könighofer, Bettina","first_name":"Bettina","last_name":"Könighofer"},{"last_name":"Kueffner","orcid":"0000-0001-8974-2542","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","full_name":"Kueffner, Konstantin","first_name":"Konstantin"},{"last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","first_name":"Kaushik"}],"_id":"17327","quality_controlled":"1","status":"public","intvolume":"       299","doi":"10.4230/LIPIcs.FSCD.2024.2","oa_version":"Published Version","corr_author":"1","researchdata_availability":"no","abstract":[{"text":"Sequential decision-making in probabilistic environments is a fundamental problem with many applications in AI and economics. In this paper, we present an algorithm for synthesizing sequential decision-making agents that optimize statistical properties such as maximum and average response times. In the general setting of sequential decision-making, the environment is modeled as a random process that generates inputs. The agent responds to each input, aiming to maximize rewards and minimize costs within a specified time horizon. The corresponding synthesis problem is known to be PSPACE-hard. We consider the special case where the input distribution, reward, and cost depend on input-output statistics specified by counter automata. For such problems, this paper presents the first PTIME synthesis algorithms. We introduce the notion of statistical abstraction, which clusters statistically indistinguishable input-output sequences into equivalence classes. This abstraction allows for a dynamic programming algorithm whose complexity grows polynomially with the considered horizon, making the statistical case exponentially more efficient than the general case. We evaluate our algorithm on three different application scenarios of a client-server protocol, where multiple clients compete via bidding to gain access to the service offered by the server. The synthesized policies optimize profit while guaranteeing that none of the server’s clients is disproportionately starved of the service.","lang":"eng"}],"date_published":"2024-07-01T00:00:00Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ieee":"F. Cano, T. A. Henzinger, B. Könighofer, K. Kueffner, and K. Mallik, “Abstraction-based decision making for statistical properties,” in <i>9th International Conference on Formal Structures for Computation and Deduction</i>, Tallinn, Estonia, 2024, vol. 299.","apa":"Cano, F., Henzinger, T. A., Könighofer, B., Kueffner, K., &#38; Mallik, K. (2024). Abstraction-based decision making for statistical properties. In <i>9th International Conference on Formal Structures for Computation and Deduction</i> (Vol. 299). Tallinn, Estonia: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSCD.2024.2\">https://doi.org/10.4230/LIPIcs.FSCD.2024.2</a>","short":"F. Cano, T.A. Henzinger, B. Könighofer, K. Kueffner, K. Mallik, in:, 9th International Conference on Formal Structures for Computation and Deduction, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","ama":"Cano F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. Abstraction-based decision making for statistical properties. In: <i>9th International Conference on Formal Structures for Computation and Deduction</i>. Vol 299. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSCD.2024.2\">10.4230/LIPIcs.FSCD.2024.2</a>","chicago":"Cano, Filip, Thomas A Henzinger, Bettina Könighofer, Konstantin Kueffner, and Kaushik Mallik. “Abstraction-Based Decision Making for Statistical Properties.” In <i>9th International Conference on Formal Structures for Computation and Deduction</i>, Vol. 299. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.FSCD.2024.2\">https://doi.org/10.4230/LIPIcs.FSCD.2024.2</a>.","mla":"Cano, Filip, et al. “Abstraction-Based Decision Making for Statistical Properties.” <i>9th International Conference on Formal Structures for Computation and Deduction</i>, vol. 299, 2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSCD.2024.2\">10.4230/LIPIcs.FSCD.2024.2</a>.","ista":"Cano F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. 2024. Abstraction-based decision making for statistical properties. 9th International Conference on Formal Structures for Computation and Deduction. FSCD: Conference on Formal Structures for Computation and Deduction, LIPIcs, vol. 299, 2."},"month":"07","title":"Abstraction-based decision making for statistical properties","year":"2024","publication_status":"published","department":[{"_id":"ToHe"}],"file_date_updated":"2024-07-29T11:15:59Z","project":[{"call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"day":"01","language":[{"iso":"eng"}]},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","researchdata_availability":"not applicable","date_published":"2024-02-01T00:00:00Z","abstract":[{"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.","lang":"eng"}],"citation":{"ama":"Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic systems via finite parity games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2024;51(2). doi:<a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">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, 2024. <a href=\"https://doi.org/10.1016/j.nahs.2023.101430\">https://doi.org/10.1016/j.nahs.2023.101430</a>.","short":"R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid Systems 51 (2024).","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, no. 2. Elsevier, 2024.","apa":"Majumdar, R., Mallik, K., Schmuck, A. K., &#38; Soudjani, S. (2024). 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>","mla":"Majumdar, Rupak, et al. “Symbolic Control for Stochastic Systems via Finite Parity Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 51, no. 2, 101430, Elsevier, 2024, 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. 2024. Symbolic control for stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems. 51(2), 101430."},"month":"02","title":"Symbolic control for stochastic systems via finite parity games","year":"2024","publication_status":"published","file_date_updated":"2024-07-16T10:26:41Z","department":[{"_id":"ToHe"}],"day":"01","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"article_processing_charge":"Yes (in subscription journal)","arxiv":1,"scopus_import":"1","external_id":{"isi":["001093188100001"],"arxiv":["2101.00834"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_number":"101430","ddc":["000"],"fulldoi":"https://doi.org/10.1016/j.nahs.2023.101430","intvolume":"        51","doi":"10.1016/j.nahs.2023.101430","status":"public","_id":"14400","quality_controlled":"1","author":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","first_name":"Kaushik"},{"last_name":"Schmuck","full_name":"Schmuck, Anne Kathrin","first_name":"Anne Kathrin"},{"full_name":"Soudjani, Sadegh","first_name":"Sadegh","last_name":"Soudjani"}],"corr_author":"1","oa_version":"Published Version","ec_funded":1,"volume":51,"publication":"Nonlinear Analysis: Hybrid Systems","das_tickbox":"1","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.","has_accepted_license":"1","date_created":"2023-10-08T22:01:15Z","issue":"2","oa":1,"dataavailabilitystatement":"No data was used for the research described in the article.\r\n","supplementarymaterial":"yes","date_updated":"2026-10-21T12:00:53Z","file":[{"file_id":"17258","file_name":"2024_NonlinearAnalysis_Majumdar.pdf","date_updated":"2024-07-16T10:26:41Z","date_created":"2024-07-16T10:26:41Z","success":1,"access_level":"open_access","file_size":1787569,"content_type":"application/pdf","checksum":"4eab70274d1004ea411f7f0e74c033ac","relation":"main_file","creator":"dernst"}],"article_type":"original","publication_identifier":{"issn":["1751-570X"]},"isi":1,"type":"journal_article","publisher":"Elsevier"},{"year":"2024","title":"Bidding games with charging","citation":{"ieee":"G. Avni, E. K. Goharshady, T. A. Henzinger, and K. Mallik, “Bidding games with charging,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311.","apa":"Avni, G., Goharshady, E. K., Henzinger, T. A., &#38; Mallik, K. (2024). Bidding games with charging. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.8</a>","short":"G. Avni, E.K. Goharshady, T.A. Henzinger, K. Mallik, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","chicago":"Avni, Guy, Ehsan Kafshdar Goharshady, Thomas A Henzinger, and Kaushik Mallik. “Bidding Games with Charging.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.8</a>.","ama":"Avni G, Goharshady EK, Henzinger TA, Mallik K. Bidding games with charging. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">10.4230/LIPIcs.CONCUR.2024.8</a>","ista":"Avni G, Goharshady EK, Henzinger TA, Mallik K. 2024. Bidding games with charging. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 8.","mla":"Avni, Guy, et al. “Bidding Games with Charging.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">10.4230/LIPIcs.CONCUR.2024.8</a>."},"month":"09","researchdata_availability":"no","abstract":[{"text":"Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules (turn-based, concurrent, etc.), and the winner is decided based on the infinite path (aka play) traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent monetary rewards, aka the \"charges.\" Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. For example, a reachability objective may require multiple detours to vertices with high charges to earn additional budget. We show that, nonetheless, the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied?","lang":"eng"}],"date_published":"2024-09-01T00:00:00Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"},{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"language":[{"iso":"eng"}],"day":"01","file_date_updated":"2024-09-17T09:35:03Z","department":[{"_id":"ToHe"}],"publication_status":"published","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_number":"8","external_id":{"arxiv":["2407.06288"],"isi":["001556847400008"]},"conference":{"end_date":"2024-09-13","location":"Calgary, Canada","start_date":"2024-09-09","name":"CONCUR: Conference on Concurrency Theory"},"scopus_import":"1","arxiv":1,"article_processing_charge":"Yes","oa_version":"Published Version","corr_author":"1","_id":"18066","status":"public","quality_controlled":"1","author":[{"full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Goharshady","full_name":"Goharshady, Ehsan Kafshdar","first_name":"Ehsan Kafshdar"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Kaushik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik"}],"intvolume":"       311","doi":"10.4230/LIPIcs.CONCUR.2024.8","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8","ddc":["000"],"date_created":"2024-09-15T22:01:39Z","has_accepted_license":"1","acknowledgement":"This work was supported in part by the ERC projects ERC-2020-AdG 101020093 and CoG 863818 (ForM-SMArt) and by ISF grant no. 1679/21.","das_tickbox":"0","publication":"35th International Conference on Concurrency Theory","volume":311,"alternative_title":["LIPIcs"],"ec_funded":1,"oa":1,"file":[{"access_level":"open_access","success":1,"content_type":"application/pdf","file_size":854430,"checksum":"cb6f2254b84922cd7bf224f550b73f4a","creator":"dernst","relation":"main_file","file_id":"18083","file_name":"2024_LIPICS_Avni.pdf","date_updated":"2024-09-17T09:35:03Z","date_created":"2024-09-17T09:35:03Z"}],"date_updated":"2026-10-21T12:17:18Z","supplementarymaterial":"no","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","type":"conference","isi":1,"publication_identifier":{"isbn":["9783959773393"],"issn":["1868-8969"]}},{"language":[{"iso":"eng"}],"day":"05","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093"}],"publication_status":"published","file_date_updated":"2024-05-22T07:09:24Z","department":[{"_id":"ToHe"}],"year":"2024","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","abstract":[{"lang":"eng","text":"Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory objectives. Existing approaches are monolithic, where a single policy fulfills all objectives. We present auction-based scheduling, a decentralized framework for multi-objective sequential decision making. Each objective is fulfilled using a separate and independent policy. Composition of policies is performed at runtime, where at each step, the policies simultaneously bid from pre-allocated budgets for the privilege of choosing the next action. The framework allows policies to be independently created, modified, and replaced. We study path planning problems on finite graphs with two temporal objectives and present algorithms to synthesize policies together with bidding policies in a decentralized manner. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other. We identify a class of assumptions called assume-admissible for which synthesis is always possible for graphs whose every vertex has at most two outgoing edges."}],"date_published":"2024-04-05T00:00:00Z","researchdata_availability":"no","title":"Auction-based scheduling","month":"04","citation":{"ista":"Avni G, Mallik K, Sadhukhan S. 2024. Auction-based scheduling. 30th 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. 14572, 153–172.","mla":"Avni, Guy, et al. “Auction-Based Scheduling.” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 153–72, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">10.1007/978-3-031-57256-2_8</a>.","chicago":"Avni, Guy, Kaushik Mallik, and Suman Sadhukhan. “Auction-Based Scheduling.” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:153–72. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">https://doi.org/10.1007/978-3-031-57256-2_8</a>.","ama":"Avni G, Mallik K, Sadhukhan S. Auction-based scheduling. In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:153-172. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">10.1007/978-3-031-57256-2_8</a>","apa":"Avni, G., Mallik, K., &#38; Sadhukhan, S. (2024). Auction-based scheduling. In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 153–172). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">https://doi.org/10.1007/978-3-031-57256-2_8</a>","short":"G. Avni, K. Mallik, S. Sadhukhan, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 153–172.","ieee":"G. Avni, K. Mallik, and S. Sadhukhan, “Auction-based scheduling,” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 153–172."},"intvolume":"     14572","doi":"10.1007/978-3-031-57256-2_8","quality_controlled":"1","_id":"15376","status":"public","author":[{"full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475"},{"last_name":"Sadhukhan","first_name":"Suman","full_name":"Sadhukhan, Suman"}],"corr_author":"1","oa_version":"Published Version","ddc":["000"],"fulldoi":"https://doi.org/10.1007/978-3-031-57256-2_8","conference":{"start_date":"2024-04-06","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2024-04-11","location":"Luxembourg City, Luxembourg"},"external_id":{"arxiv":["2310.11798"],"isi":["001284187100008"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"Yes (in subscription journal)","arxiv":1,"scopus_import":"1","oa":1,"date_created":"2024-05-12T22:01:02Z","ec_funded":1,"alternative_title":["LNCS"],"volume":14572,"publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","das_tickbox":"0","has_accepted_license":"1","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093 and by ISF grant no. 1679/21.","page":"153-172","type":"conference","publisher":"Springer Nature","isi":1,"publication_identifier":{"isbn":["9783031572555"],"issn":["0302-9743"],"eissn":["1611-3349"]},"file":[{"checksum":"dbeb123510997886d11925aedbf9c400","relation":"main_file","creator":"dernst","success":1,"access_level":"open_access","file_size":508191,"content_type":"application/pdf","date_created":"2024-05-22T07:09:24Z","file_name":"2024_LNCS_Avni.pdf","file_id":"15414","date_updated":"2024-05-22T07:09:24Z"}],"supplementarymaterial":"no","date_updated":"2026-10-21T12:16:28Z"},{"oa":1,"date_created":"2023-06-18T22:00:47Z","volume":13994,"alternative_title":["LNCS"],"publication":"TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems","has_accepted_license":"1","page":"211-228","type":"conference","publisher":"Springer Nature","publication_identifier":{"isbn":["9783031308192"],"issn":["0302-9743"],"eissn":["1611-3349"]},"isi":1,"file":[{"date_created":"2023-06-19T08:43:21Z","file_id":"13151","file_name":"2023_LNCS_Anand.pdf","date_updated":"2023-06-19T08:43:21Z","checksum":"60dcafc1b4f6f070be43bad3fe877974","relation":"main_file","creator":"dernst","success":1,"access_level":"open_access","file_size":521425,"content_type":"application/pdf"}],"date_updated":"2025-09-09T12:30:00Z","day":"20","language":[{"iso":"eng"}],"publication_status":"published","department":[{"_id":"ToHe"}],"file_date_updated":"2023-06-19T08:43:21Z","year":"2023","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","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"}],"date_published":"2023-04-20T00:00:00Z","title":"Computing adequately permissive assumptions for synthesis","month":"04","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>","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>.","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.","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.","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>","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>.","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."},"doi":"10.1007/978-3-031-30820-8_15","intvolume":"     13994","_id":"13141","status":"public","author":[{"full_name":"Anand, Ashwani","first_name":"Ashwani","last_name":"Anand"},{"last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","first_name":"Kaushik"},{"last_name":"Nayak","first_name":"Satya Prakash","full_name":"Nayak, Satya Prakash"},{"full_name":"Schmuck, Anne Kathrin","first_name":"Anne Kathrin","last_name":"Schmuck"}],"quality_controlled":"1","oa_version":"Published Version","ddc":["000"],"fulldoi":"https://doi.org/10.1007/978-3-031-30820-8_15","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22","location":"Paris, France","end_date":"2023-04-27"},"external_id":{"isi":["001288698100015"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"No","scopus_import":"1"},{"year":"2023","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2023-07-16T00:00:00Z","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"}],"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. 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>","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.","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.","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>","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>.","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.","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>."},"month":"07","title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","day":"16","language":[{"iso":"eng"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"}],"publication_status":"published","department":[{"_id":"ToHe"}],"file_date_updated":"2024-01-09T10:01:07Z","conference":{"end_date":"2023-07-22","location":"Paris, France","name":"CAV: Computer Aided Verification","start_date":"2023-07-17"},"external_id":{"isi":["001310805600001"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"Yes (in subscription journal)","scopus_import":"1","intvolume":"     13966","doi":"10.1007/978-3-031-37709-9_1","_id":"14758","author":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"full_name":"Rychlicki, Mateusz","first_name":"Mateusz","last_name":"Rychlicki"},{"full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin","last_name":"Schmuck"},{"last_name":"Soudjani","first_name":"Sadegh","full_name":"Soudjani, Sadegh"}],"quality_controlled":"1","status":"public","corr_author":"1","oa_version":"Published Version","ddc":["000"],"fulldoi":"https://doi.org/10.1007/978-3-031-37709-9_1","date_created":"2024-01-08T13:18:00Z","ec_funded":1,"volume":13966,"alternative_title":["LNCS"],"publication":"35th International Conference on Computer Aided Verification","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.","has_accepted_license":"1","oa":1,"file":[{"relation":"main_file","creator":"dernst","checksum":"1a361d83db0244fd32c03b544c294b5a","content_type":"application/pdf","file_size":405147,"success":1,"access_level":"open_access","date_created":"2024-01-09T10:01:07Z","date_updated":"2024-01-09T10:01:07Z","file_name":"2023_LNCSCAV_Majumdar.pdf","file_id":"14765"}],"date_updated":"2025-09-09T14:16:49Z","page":"3-15","related_material":{"record":[{"status":"public","id":"14994","relation":"research_data"}]},"type":"conference","publisher":"Springer Nature","publication_identifier":{"eisbn":["9783031377099"],"isbn":["9783031377082"],"issn":["0302-9743"],"eissn":["1611-3349"]},"isi":1},{"arxiv":1,"article_processing_charge":"Yes","article_number":"4","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"external_id":{"arxiv":["2202.07480"]},"fulldoi":"https://doi.org/10.46298/theoretics.23.4","ddc":["000"],"oa_version":"Published Version","corr_author":"1","quality_controlled":"1","_id":"14920","status":"public","author":[{"last_name":"Banerjee","first_name":"Tamajit","full_name":"Banerjee, Tamajit"},{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","first_name":"Kaushik"},{"last_name":"Schmuck","full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin"},{"last_name":"Soudjani","first_name":"Sadegh","full_name":"Soudjani, Sadegh"}],"doi":"10.46298/theoretics.23.4","intvolume":"         2","title":"Fast symbolic algorithms for mega-regular games under strong transition fairness","citation":{"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.","short":"T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS 2 (2023).","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>.","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>","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>.","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."},"month":"02","date_published":"2023-02-24T00:00:00Z","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"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2023","file_date_updated":"2024-02-05T10:19:35Z","department":[{"_id":"ToHe"}],"publication_status":"published","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020"}],"day":"24","language":[{"iso":"eng"}],"date_updated":"2025-04-14T07:55:57Z","article_type":"original","file":[{"checksum":"2972d531122a6f15727b396110fb3f5c","relation":"main_file","creator":"dernst","success":1,"access_level":"open_access","file_size":917076,"content_type":"application/pdf","date_created":"2024-02-05T10:19:35Z","file_name":"2023_TheoretiCS_Banerjee.pdf","file_id":"14940","date_updated":"2024-02-05T10:19:35Z"}],"publication_identifier":{"issn":["2751-4838"]},"publisher":"EPI Sciences","type":"journal_article","has_accepted_license":"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.","publication":"TheoretiCS","volume":2,"ec_funded":1,"date_created":"2024-01-31T13:40:49Z","oa":1},{"date_created":"2024-02-14T15:13:00Z","year":"2023","month":"04","title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","citation":{"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>.","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>.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023).","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.","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>","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>.","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>"},"has_accepted_license":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"}],"date_published":"2023-04-28T00:00:00Z","day":"28","oa":1,"main_file_link":[{"url":"https://doi.org/10.5281/zenodo.7877790","open_access":"1"}],"department":[{"_id":"ToHe"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_updated":"2025-09-09T14:16:48Z","article_processing_charge":"No","corr_author":"1","type":"research_data_reference","oa_version":"Published Version","publisher":"Zenodo","doi":"10.5281/ZENODO.7877790","author":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"first_name":"Kaushik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik"},{"full_name":"Rychlicki, Mateusz","first_name":"Mateusz","last_name":"Rychlicki"},{"first_name":"Anne-Kathrin","full_name":"Schmuck, Anne-Kathrin","last_name":"Schmuck"},{"first_name":"Sadegh","full_name":"Soudjani, Sadegh","last_name":"Soudjani"}],"_id":"14994","related_material":{"record":[{"relation":"used_in_publication","id":"14758","status":"public"}]},"status":"public","fulldoi":"https://doi.org/10.5281/ZENODO.7877790","ddc":["000"]},{"date_created":"2023-07-25T18:32:40Z","ec_funded":1,"volume":13965,"alternative_title":["LNCS"],"publication":"Computer Aided Verification","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG101020093.","has_accepted_license":"1","oa":1,"file":[{"file_name":"2023_LNCS_CAV_HenzingerT.pdf","file_id":"13327","date_updated":"2023-07-31T08:11:20Z","date_created":"2023-07-31T08:11:20Z","success":1,"access_level":"open_access","file_size":647760,"content_type":"application/pdf","checksum":"ccaf94bf7d658ba012c016e11869b54c","relation":"main_file","creator":"dernst"}],"date_updated":"2026-09-18T07:41:29Z","page":"358–382","related_material":{"record":[{"id":"22808","status":"public","relation":"dissertation_contains"}]},"type":"conference","publisher":"Springer Nature","isi":1,"publication_identifier":{"isbn":["9783031377020"],"eisbn":["9783031377037"],"issn":["0302-9743"],"eissn":["1611-3349"]},"year":"2023","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2023-07-18T00:00:00Z","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":{"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.","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.","short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification, Springer Nature, 2023, 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>","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>","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>."},"title":"Monitoring algorithmic fairness","month":"07","language":[{"iso":"eng"}],"day":"18","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"publication_status":"published","file_date_updated":"2023-07-31T08:11:20Z","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","location":"Paris, France","end_date":"2023-07-22"},"external_id":{"isi":["001310804800017"],"arxiv":["2305.15979"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"Yes (in subscription journal)","arxiv":1,"scopus_import":"1","doi":"10.1007/978-3-031-37703-7_17","intvolume":"     13965","author":[{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Karimi, Mahyar","first_name":"Mahyar","last_name":"Karimi","orcid":"0009-0005-0820-1696","id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b"},{"first_name":"Konstantin","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner"},{"first_name":"Kaushik","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","last_name":"Mallik"}],"_id":"13310","quality_controlled":"1","status":"public","corr_author":"1","oa_version":"Published Version","ddc":["000"],"fulldoi":"https://doi.org/10.1007/978-3-031-37703-7_17"},{"scopus_import":"1","article_processing_charge":"Yes (via OA deal)","arxiv":1,"external_id":{"arxiv":["2305.04699"],"isi":["001062819300057"]},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"conference":{"location":"Chicago, IL, United States","end_date":"2023-06-15","start_date":"2023-06-12","name":"FAccT: Conference on Fairness, Accountability and Transparency"},"fulldoi":"https://doi.org/10.1145/3593013.3594028","ddc":["000"],"corr_author":"1","oa_version":"Published Version","doi":"10.1145/3593013.3594028","status":"public","_id":"13228","author":[{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Karimi, Mahyar","first_name":"Mahyar","last_name":"Karimi","orcid":"0009-0005-0820-1696","id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b"},{"last_name":"Kueffner","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin","first_name":"Konstantin"},{"full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"}],"quality_controlled":"1","citation":{"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>.","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>","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."},"month":"06","title":"Runtime monitoring of dynamic fairness properties","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","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."}],"date_published":"2023-06-12T00:00:00Z","year":"2023","file_date_updated":"2023-07-18T07:43:10Z","department":[{"_id":"ToHe"}],"publication_status":"published","language":[{"iso":"eng"}],"day":"12","project":[{"call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"date_updated":"2026-09-18T07:41:29Z","file":[{"creator":"dernst","relation":"main_file","checksum":"96c759db9cdf94b81e37871a66a6ff48","content_type":"application/pdf","file_size":4100596,"access_level":"open_access","success":1,"date_created":"2023-07-18T07:43:10Z","date_updated":"2023-07-18T07:43:10Z","file_name":"2023_ACM_HenzingerT.pdf","file_id":"13245"}],"isi":1,"publication_identifier":{"isbn":["9781450372527"]},"type":"conference","publisher":"Association for Computing Machinery","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"22808"}]},"page":"604-614","publication":"FAccT '23: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency","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.","has_accepted_license":"1","ec_funded":1,"date_created":"2023-07-16T22:01:09Z","oa":1},{"year":"2023","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"}],"date_published":"2023-10-01T00:00:00Z","title":"Monitoring algorithmic fairness under partial observations","month":"10","citation":{"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>.","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.","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>.","short":"T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference on Runtime Verification, Springer Nature, 2023, pp. 291–311.","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."},"day":"01","language":[{"iso":"eng"}],"project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"publication_status":"published","department":[{"_id":"ToHe"}],"conference":{"end_date":"2023-10-06","location":"Thessaloniki, Greece","start_date":"2023-10-03","name":"RV: Conference on Runtime Verification"},"external_id":{"arxiv":["2308.00341"]},"article_processing_charge":"No","arxiv":1,"scopus_import":"1","intvolume":"     14245","doi":"10.1007/978-3-031-44267-4_15","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0001-8974-2542","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner","first_name":"Konstantin","full_name":"Kueffner, Konstantin"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik"}],"_id":"14454","quality_controlled":"1","status":"public","corr_author":"1","oa_version":"Preprint","fulldoi":"https://doi.org/10.1007/978-3-031-44267-4_15","date_created":"2023-10-29T23:01:15Z","ec_funded":1,"alternative_title":["LNCS"],"volume":14245,"publication":"23rd International Conference on Runtime Verification","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","oa":1,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2308.00341"}],"date_updated":"2026-09-18T07:41:29Z","related_material":{"record":[{"status":"public","id":"22808","relation":"dissertation_contains"}]},"page":"291-311","type":"conference","publisher":"Springer Nature","publication_identifier":{"isbn":["9783031442667"],"eissn":["1611-3349"],"issn":["0302-9743"]}},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2022-03-29T00:00:00Z","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"}],"citation":{"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>","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.","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>.","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."},"month":"03","title":"A direct symbolic algorithm for solving stochastic rabin games","year":"2022","publication_status":"published","day":"29","language":[{"iso":"eng"}],"article_processing_charge":"No","scopus_import":"1","conference":{"location":"Munich, Germany","end_date":"2022-04-07","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2022-04-02"},"fulldoi":"https://doi.org/10.1007/978-3-030-99527-0_5","doi":"10.1007/978-3-030-99527-0_5","intvolume":"     13244","_id":"12529","status":"public","quality_controlled":"1","author":[{"last_name":"Banerjee","first_name":"Tamajit","full_name":"Banerjee, Tamajit"},{"last_name":"Majumdar","full_name":"Majumdar, Rupak","first_name":"Rupak"},{"orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik"},{"last_name":"Schmuck","full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin"},{"last_name":"Soudjani","full_name":"Soudjani, Sadegh","first_name":"Sadegh"}],"corr_author":"1","oa_version":"Published Version","volume":13244,"alternative_title":["LNCS"],"publication":"28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","date_created":"2023-02-08T11:43:34Z","main_file_link":[{"url":"https://doi.org/10.1007/978-3-030-99527-0_5","open_access":"1"}],"extern":"1","oa":1,"date_updated":"2024-10-09T21:04:10Z","publication_identifier":{"eisbn":["9783030995270"]},"page":"81-98","type":"conference","publisher":"Springer Nature"},{"doi":"10.1145/3501710.3519535","_id":"12530","page":"24:1-24:11","author":[{"full_name":"Finkbeiner, Bernd","first_name":"Bernd","last_name":"Finkbeiner"},{"full_name":"Mallik, Kaushik","first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"full_name":"Passing, Noemi","first_name":"Noemi","last_name":"Passing"},{"last_name":"Schledjewski","full_name":"Schledjewski, Malte","first_name":"Malte"},{"full_name":"Schmuck, Anne-Kathrin","first_name":"Anne-Kathrin","last_name":"Schmuck"}],"quality_controlled":"1","status":"public","type":"conference","publisher":"ACM","oa_version":"None","fulldoi":"https://doi.org/10.1145/3501710.3519535","publication_identifier":{"isbn":["9781450391962"]},"conference":{"location":"Milan, Italy","end_date":"2022-05-06","start_date":"2022-05-04","name":"HSCC: International Conference on Hybrid Systems Computation and Control"},"article_processing_charge":"No","date_updated":"2023-02-09T08:53:13Z","scopus_import":"1","language":[{"iso":"eng"}],"day":"01","extern":"1","publication_status":"published","year":"2022","date_created":"2023-02-08T11:43:50Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2022-05-01T00:00:00Z","abstract":[{"lang":"eng","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."}],"month":"05","publication":"25th ACM International Conference on Hybrid Systems: Computation and Control","title":"BOCoSy: Small but powerful symbolic output-feedback control","citation":{"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.","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>.","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.","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>","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.","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>","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>."}}]