[{"alternative_title":["LNCS"],"title":"MDPs as distribution transformers: Affine invariant synthesis for safety objectives","publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"content_type":"application/pdf","relation":"main_file","success":1,"file_size":531745,"file_name":"2023_LNCS_Akshay.pdf","date_updated":"2023-09-20T08:46:43Z","date_created":"2023-09-20T08:46:43Z","file_id":"14349","checksum":"f143c8eedf609f20f2aad2eeb496d53f","creator":"dernst","access_level":"open_access"}],"project":[{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020"},{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"author":[{"full_name":"Akshay, S.","first_name":"S.","last_name":"Akshay"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-1712-2165","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde"}],"day":"17","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"acknowledgement":"This work was supported in part by the ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385 as well as DST/CEFIPRA/INRIA project EQuaVE and SERB Matrices grant MTR/2018/00074.","volume":13966,"quality_controlled":"1","article_processing_charge":"Yes (in subscription journal)","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"type":"conference","page":"86-112","date_created":"2023-09-10T22:01:12Z","publication":"International Conference on Computer Aided Verification","has_accepted_license":"1","ec_funded":1,"month":"07","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031377082"]},"oa":1,"status":"public","_id":"14317","year":"2023","date_updated":"2025-07-14T09:09:56Z","abstract":[{"lang":"eng","text":"Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization.\r\nIn light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples."}],"citation":{"chicago":"Akshay, S., Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.” In <i>International Conference on Computer Aided Verification</i>, 13966:86–112. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">https://doi.org/10.1007/978-3-031-37709-9_5</a>.","ista":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 86–112.","mla":"Akshay, S., et al. “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.” <i>International Conference on Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 86–112, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">10.1007/978-3-031-37709-9_5</a>.","apa":"Akshay, S., Chatterjee, K., Meggendorfer, T., &#38; Zikelic, D. (2023). MDPs as distribution transformers: Affine invariant synthesis for safety objectives. In <i>International Conference on Computer Aided Verification</i> (Vol. 13966, pp. 86–112). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">https://doi.org/10.1007/978-3-031-37709-9_5</a>","short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 86–112.","ama":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. In: <i>International Conference on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:86-112. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">10.1007/978-3-031-37709-9_5</a>","ieee":"S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “MDPs as distribution transformers: Affine invariant synthesis for safety objectives,” in <i>International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 86–112."},"intvolume":"     13966","ddc":["000"],"file_date_updated":"2023-09-20T08:46:43Z","scopus_import":"1","date_published":"2023-07-17T00:00:00Z","oa_version":"Published Version","publication_status":"published","conference":{"name":"CAV: Computer Aided Verification","start_date":"2023-07-17","location":"Paris, France","end_date":"2023-07-22"},"doi":"10.1007/978-3-031-37709-9_5"},{"type":"conference","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"has_accepted_license":"1","date_created":"2023-11-12T23:00:56Z","page":"141-148","publication":"Frontiers in Artificial Intelligence and Applications","external_id":{"arxiv":["2307.15218"]},"volume":372,"quality_controlled":"1","article_processing_charge":"No","project":[{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020"},{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"full_name":"Sadhukhan, Suman","first_name":"Suman","last_name":"Sadhukhan"},{"full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","first_name":"Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"file":[{"date_created":"2023-11-13T10:16:10Z","file_name":"2023_FAIA_Avni.pdf","date_updated":"2023-11-13T10:16:10Z","access_level":"open_access","checksum":"1390ca38480fa4cf286b0f1a42e8c12f","file_id":"14529","creator":"dernst","success":1,"file_size":501011,"relation":"main_file","content_type":"application/pdf"}],"acknowledgement":"This research was supported in part by ISF grant no. 1679/21, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie Grant Agreement No. 665385.","tmp":{"image":"/images/cc_by_nc.png","short":"CC BY-NC (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)"},"day":"28","publisher":"IOS Press","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Reachability poorman discrete-bidding games","oa_version":"Published Version","date_published":"2023-09-28T00:00:00Z","conference":{"end_date":"2023-10-04","location":"Krakow, Poland","start_date":"2023-09-30","name":"ECAI: European Conference on Artificial Intelligence"},"publication_status":"published","doi":"10.3233/FAIA230264","intvolume":"       372","citation":{"chicago":"Avni, Guy, Tobias Meggendorfer, Suman Sadhukhan, Josef Tkadlec, and Dorde Zikelic. “Reachability Poorman Discrete-Bidding Games.” In <i>Frontiers in Artificial Intelligence and Applications</i>, 372:141–48. IOS Press, 2023. <a href=\"https://doi.org/10.3233/FAIA230264\">https://doi.org/10.3233/FAIA230264</a>.","apa":"Avni, G., Meggendorfer, T., Sadhukhan, S., Tkadlec, J., &#38; Zikelic, D. (2023). Reachability poorman discrete-bidding games. In <i>Frontiers in Artificial Intelligence and Applications</i> (Vol. 372, pp. 141–148). Krakow, Poland: IOS Press. <a href=\"https://doi.org/10.3233/FAIA230264\">https://doi.org/10.3233/FAIA230264</a>","ista":"Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. 2023. Reachability poorman discrete-bidding games. Frontiers in Artificial Intelligence and Applications. ECAI: European Conference on Artificial Intelligence vol. 372, 141–148.","mla":"Avni, Guy, et al. “Reachability Poorman Discrete-Bidding Games.” <i>Frontiers in Artificial Intelligence and Applications</i>, vol. 372, IOS Press, 2023, pp. 141–48, doi:<a href=\"https://doi.org/10.3233/FAIA230264\">10.3233/FAIA230264</a>.","short":"G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, D. Zikelic, in:, Frontiers in Artificial Intelligence and Applications, IOS Press, 2023, pp. 141–148.","ama":"Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. Reachability poorman discrete-bidding games. In: <i>Frontiers in Artificial Intelligence and Applications</i>. Vol 372. IOS Press; 2023:141-148. doi:<a href=\"https://doi.org/10.3233/FAIA230264\">10.3233/FAIA230264</a>","ieee":"G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, and D. Zikelic, “Reachability poorman discrete-bidding games,” in <i>Frontiers in Artificial Intelligence and Applications</i>, Krakow, Poland, 2023, vol. 372, pp. 141–148."},"scopus_import":"1","file_date_updated":"2023-11-13T10:16:10Z","ddc":["000"],"_id":"14518","date_updated":"2025-07-14T09:09:57Z","abstract":[{"text":"We consider bidding games, a class of two-player zero-sum graph games. The game proceeds as follows. Both players have bounded budgets. A token is placed on a vertex of a graph, in each turn the players simultaneously submit bids, and the higher bidder moves the token, where we break bidding ties in favor of Player 1. Player 1 wins the game iff the token visits a designated target vertex. We consider, for the first time, poorman discrete-bidding in which the granularity of the bids is restricted and the higher bid is paid to the bank. Previous work either did not impose granularity restrictions or considered Richman bidding (bids are paid to the opponent). While the latter mechanisms are technically more accessible, the former is more appealing from a practical standpoint. Our study focuses on threshold budgets, which is the necessary and sufficient initial budget required for Player 1 to ensure winning against a given Player 2 budget. We first show existence of thresholds. In DAGs, we show that threshold budgets can be approximated with error bounds by thresholds under continuous-bidding and that they exhibit a periodic behavior. We identify closed-form solutions in special cases. We implement and experiment with an algorithm to find threshold budgets.","lang":"eng"}],"arxiv":1,"year":"2023","month":"09","ec_funded":1,"status":"public","publication_identifier":{"isbn":["9781643684369"],"issn":["0922-6389"]},"oa":1},{"doi":"10.15479/14539","publication_status":"published","date_published":"2023-11-15T00:00:00Z","oa_version":"Published Version","ddc":["000"],"file_date_updated":"2023-11-15T13:44:24Z","citation":{"chicago":"Zikelic, Dorde. “Automated Verification and Control of Infinite State Stochastic Systems.” Institute of Science and Technology Austria, 2023. <a href=\"https://doi.org/10.15479/14539\">https://doi.org/10.15479/14539</a>.","apa":"Zikelic, D. (2023). <i>Automated verification and control of infinite state stochastic systems</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/14539\">https://doi.org/10.15479/14539</a>","ista":"Zikelic D. 2023. Automated verification and control of infinite state stochastic systems. Institute of Science and Technology Austria.","mla":"Zikelic, Dorde. <i>Automated Verification and Control of Infinite State Stochastic Systems</i>. Institute of Science and Technology Austria, 2023, doi:<a href=\"https://doi.org/10.15479/14539\">10.15479/14539</a>.","short":"D. Zikelic, Automated Verification and Control of Infinite State Stochastic Systems, Institute of Science and Technology Austria, 2023.","ieee":"D. Zikelic, “Automated verification and control of infinite state stochastic systems,” Institute of Science and Technology Austria, 2023.","ama":"Zikelic D. Automated verification and control of infinite state stochastic systems. 2023. doi:<a href=\"https://doi.org/10.15479/14539\">10.15479/14539</a>"},"year":"2023","abstract":[{"lang":"eng","text":"Stochastic systems provide a formal framework for modelling and quantifying uncertainty in systems and have been widely adopted in many application domains. Formal\r\nverification and control of finite state stochastic systems, a subfield of formal methods\r\nalso known as probabilistic model checking, is well studied. In contrast, formal verification and control of infinite state stochastic systems have received comparatively\r\nless attention. However, infinite state stochastic systems commonly arise in practice.\r\nFor instance, probabilistic models that contain continuous probability distributions such\r\nas normal or uniform, or stochastic dynamical systems which are a classical model for\r\ncontrol under uncertainty, both give rise to infinite state systems.\r\nThe goal of this thesis is to contribute to laying theoretical and algorithmic foundations\r\nof fully automated formal verification and control of infinite state stochastic systems,\r\nwith a particular focus on systems that may be executed over a long or infinite time.\r\nWe consider formal verification of infinite state stochastic systems in the setting of\r\nstatic analysis of probabilistic programs and formal control in the setting of controller\r\nsynthesis in stochastic dynamical systems. For both problems, we present some of the\r\nfirst fully automated methods for probabilistic (a.k.a. quantitative) reachability and\r\nsafety analysis applicable to infinite time horizon systems. We also advance the state\r\nof the art of probability 1 (a.k.a. qualitative) reachability analysis for both problems.\r\nFinally, for formal controller synthesis in stochastic dynamical systems, we present a\r\nnovel framework for learning neural network control policies in stochastic dynamical\r\nsystems with formal guarantees on correctness with respect to quantitative reachability,\r\nsafety or reach-avoid specifications.\r\n"}],"date_updated":"2025-07-14T09:10:10Z","_id":"14539","oa":1,"publication_identifier":{"isbn":["978-3-99078-036-7"],"issn":["2663 - 337X"]},"status":"public","ec_funded":1,"month":"11","date_created":"2023-11-15T13:39:10Z","page":"256","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"language":[{"iso":"eng"}],"type":"dissertation","article_processing_charge":"No","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"1194"},{"relation":"part_of_dissertation","status":"public","id":"12000"},{"status":"public","relation":"part_of_dissertation","id":"12511"},{"relation":"part_of_dissertation","status":"public","id":"14600"},{"relation":"part_of_dissertation","status":"public","id":"14601"},{"id":"9644","status":"public","relation":"part_of_dissertation"},{"id":"10414","status":"public","relation":"part_of_dissertation"}]},"tmp":{"name":"Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode","short":"CC BY-NC-SA (4.0)","image":"/images/cc_by_nc_sa.png"},"day":"15","file":[{"relation":"main_file","content_type":"application/pdf","file_size":2116426,"success":1,"date_updated":"2023-11-15T13:43:28Z","file_name":"main.pdf","date_created":"2023-11-15T13:43:28Z","checksum":"f23e002b0059ca78e1fbb864da52dd7e","creator":"cchlebak","file_id":"14540","access_level":"open_access"},{"file_size":35884057,"relation":"source_file","content_type":"application/x-zip-compressed","date_created":"2023-11-15T13:44:24Z","file_name":"thesis_source.zip","date_updated":"2023-11-15T13:44:24Z","access_level":"closed","checksum":"80ca37618a3c7b59866875f8be9b15ed","file_id":"14541","creator":"cchlebak"}],"author":[{"first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","full_name":"Zikelic, Dorde"}],"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"title":"Automated verification and control of infinite state stochastic systems","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publisher":"Institute of Science and Technology Austria","supervisor":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"}],"degree_awarded":"PhD","alternative_title":["ISTA Thesis"]},{"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","day":"22","author":[{"last_name":"Ansaripour","first_name":"Matin","full_name":"Ansaripour, Matin"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","full_name":"Lechner, Mathias"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","orcid":"0000-0002-4681-1699","first_name":"Dorde"}],"project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","title":"Learning provably stabilizing neural controllers for discrete-time stochastic systems","alternative_title":["LNCS"],"publication":"21st International Symposium on Automated Technology for Verification and Analysis","date_created":"2023-11-19T23:00:56Z","page":"357-379","type":"conference","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"article_processing_charge":"No","quality_controlled":"1","volume":14215,"abstract":[{"text":"We consider the problem of learning control policies in discrete-time stochastic systems which guarantee that the system stabilizes within some specified stabilization region with probability 1. Our approach is based on the novel notion of stabilizing ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome the limitation of methods proposed in previous works whose applicability is restricted to systems in which the stabilizing region cannot be left once entered under any control policy. We present a learning procedure that learns a control policy together with an sRSM that formally certifies probability 1 stability, both learned as neural networks. We show that this procedure can also be adapted to formally verifying that, under a given Lipschitz continuous control policy, the stochastic system stabilizes within some stabilizing region with probability 1. Our experimental evaluation shows that our learning procedure can successfully learn provably stabilizing policies in practice.","lang":"eng"}],"date_updated":"2025-07-14T09:09:59Z","year":"2023","_id":"14559","status":"public","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031453281"]},"month":"10","ec_funded":1,"doi":"10.1007/978-3-031-45329-8_17","conference":{"end_date":"2023-10-27","location":"Singapore, Singapore","start_date":"2023-10-24","name":"ATVA: Automated Technology for Verification and Analysis"},"publication_status":"published","oa_version":"None","date_published":"2023-10-22T00:00:00Z","scopus_import":"1","citation":{"short":"M. Ansaripour, K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, 21st International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2023, pp. 357–379.","ama":"Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. Learning provably stabilizing neural controllers for discrete-time stochastic systems. In: <i>21st International Symposium on Automated Technology for Verification and Analysis</i>. Vol 14215. Springer Nature; 2023:357-379. doi:<a href=\"https://doi.org/10.1007/978-3-031-45329-8_17\">10.1007/978-3-031-45329-8_17</a>","ieee":"M. Ansaripour, K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “Learning provably stabilizing neural controllers for discrete-time stochastic systems,” in <i>21st International Symposium on Automated Technology for Verification and Analysis</i>, Singapore, Singapore, 2023, vol. 14215, pp. 357–379.","chicago":"Ansaripour, Matin, Krishnendu Chatterjee, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems.” In <i>21st International Symposium on Automated Technology for Verification and Analysis</i>, 14215:357–79. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-45329-8_17\">https://doi.org/10.1007/978-3-031-45329-8_17</a>.","mla":"Ansaripour, Matin, et al. “Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems.” <i>21st International Symposium on Automated Technology for Verification and Analysis</i>, vol. 14215, Springer Nature, 2023, pp. 357–79, doi:<a href=\"https://doi.org/10.1007/978-3-031-45329-8_17\">10.1007/978-3-031-45329-8_17</a>.","apa":"Ansaripour, M., Chatterjee, K., Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2023). Learning provably stabilizing neural controllers for discrete-time stochastic systems. In <i>21st International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 14215, pp. 357–379). Singapore, Singapore: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-45329-8_17\">https://doi.org/10.1007/978-3-031-45329-8_17</a>","ista":"Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning provably stabilizing neural controllers for discrete-time stochastic systems. 21st International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379."},"intvolume":"     14215"},{"year":"2023","date_updated":"2025-07-14T09:10:10Z","arxiv":1,"issue":"2","abstract":[{"lang":"eng","text":"We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in a LexRSM not existing even for simple terminating programs. Our contributions are twofold. First, we introduce a generalization of LexRSMs that allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs."}],"_id":"14778","article_number":"11","publication_identifier":{"eissn":["1433-299X"],"issn":["0934-5043"]},"oa":1,"status":"public","ec_funded":1,"month":"06","publication_status":"published","doi":"10.1145/3585391","date_published":"2023-06-23T00:00:00Z","oa_version":"Published Version","ddc":["000"],"file_date_updated":"2024-01-16T08:11:24Z","citation":{"short":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, Formal Aspects of Computing 35 (2023).","ama":"Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. <i>Formal Aspects of Computing</i>. 2023;35(2). doi:<a href=\"https://doi.org/10.1145/3585391\">10.1145/3585391</a>","ieee":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” <i>Formal Aspects of Computing</i>, vol. 35, no. 2. Association for Computing Machinery, 2023.","apa":"Chatterjee, K., Kafshdar Goharshady, E., Novotný, P., Zárevúcky, J., &#38; Zikelic, D. (2023). On lexicographic proof rules for probabilistic termination. <i>Formal Aspects of Computing</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3585391\">https://doi.org/10.1145/3585391</a>","mla":"Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>Formal Aspects of Computing</i>, vol. 35, no. 2, 11, Association for Computing Machinery, 2023, doi:<a href=\"https://doi.org/10.1145/3585391\">10.1145/3585391</a>.","ista":"Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023. On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. 35(2), 11.","chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>Formal Aspects of Computing</i>. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3585391\">https://doi.org/10.1145/3585391</a>."},"intvolume":"        35","day":"23","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"acknowledgement":"This research was partially supported by the ERC CoG (grant no. 863818; ForM-SMArt), the Czech Science Foundation (grant no. GA21-24711S), and the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie Grant Agreement No. 665385.","file":[{"file_size":502522,"success":1,"content_type":"application/pdf","relation":"main_file","date_created":"2024-01-16T08:11:24Z","file_name":"2023_FormalAspectsComputing_Chatterjee.pdf","date_updated":"2024-01-16T08:11:24Z","access_level":"open_access","creator":"dernst","file_id":"14804","checksum":"3bb133eeb27ec01649a9a36445d952d9"}],"project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020"}],"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Kafshdar Goharshady","first_name":"Ehsan","full_name":"Kafshdar Goharshady, Ehsan"},{"first_name":"Petr","last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"last_name":"Zárevúcky","first_name":"Jiří","full_name":"Zárevúcky, Jiří"},{"last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"title":"On lexicographic proof rules for probabilistic termination","publisher":"Association for Computing Machinery","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2024-01-10T09:27:43Z","publication":"Formal Aspects of Computing","has_accepted_license":"1","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"type":"journal_article","article_type":"original","article_processing_charge":"Yes (via OA deal)","related_material":{"record":[{"id":"10414","relation":"earlier_version","status":"public"}]},"external_id":{"arxiv":["2108.02188"]},"quality_controlled":"1","volume":35,"keyword":["Theoretical Computer Science","Software"]},{"title":"Learning control policies for stochastic systems with reach-avoid guarantees","publisher":"Association for the Advancement of Artificial Intelligence","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"26","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020"}],"author":[{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","full_name":"Lechner, Mathias"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"article_processing_charge":"No","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"14600"}]},"external_id":{"arxiv":["2210.05308"]},"quality_controlled":"1","volume":37,"keyword":["General Medicine"],"page":"11926-11935","date_created":"2024-01-18T07:44:31Z","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"type":"conference","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"status":"public","ec_funded":1,"month":"06","year":"2023","date_updated":"2025-07-14T09:10:02Z","issue":"10","abstract":[{"lang":"eng","text":"We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks."}],"arxiv":1,"_id":"14830","intvolume":"        37","citation":{"apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>.","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.","chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>.","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–11935.","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935.","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>"},"publication_status":"published","conference":{"location":"Washington, DC, United States","end_date":"2023-02-14","name":"AAAI: Conference on Artificial Intelligence","start_date":"2023-02-07"},"doi":"10.1609/aaai.v37i10.26407","date_published":"2023-06-26T00:00:00Z","oa_version":"Preprint"},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_published":"2023-12-15T00:00:00Z","language":[{"iso":"eng"}],"oa_version":"Preprint","type":"conference","publication":"37th Conference on Neural Information Processing Systems","date_created":"2024-02-25T09:23:24Z","publication_status":"epub_ahead","conference":{"location":"New Orleans, LO, United States","end_date":"2023-12-16","name":"NeurIPS: Neural Information Processing Systems","start_date":"2023-12-10"},"citation":{"short":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th Conference on Neural Information Processing Systems, 2023.","ama":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy learning in stochastic control systems with formal guarantees. In: <i>37th Conference on Neural Information Processing Systems</i>. ; 2023.","ieee":"D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional policy learning in stochastic control systems with formal guarantees,” in <i>37th Conference on Neural Information Processing Systems</i>, New Orleans, LO, United States, 2023.","apa":"Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., &#38; Henzinger, T. A. (2023). Compositional policy learning in stochastic control systems with formal guarantees. In <i>37th Conference on Neural Information Processing Systems</i>. New Orleans, LO, United States.","ista":"Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems.","mla":"Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” <i>37th Conference on Neural Information Processing Systems</i>, 2023.","chicago":"Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees.” In <i>37th Conference on Neural Information Processing Systems</i>, 2023."},"quality_controlled":"1","external_id":{"arxiv":["2312.01456"]},"article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2312.01456"}],"_id":"15023","author":[{"full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde"},{"full_name":"Lechner, Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias"},{"full_name":"Verma, Abhinav","first_name":"Abhinav","id":"a235593c-d7fa-11eb-a0c5-b22ca3c66ee6","last_name":"Verma"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"year":"2023","day":"15","arxiv":1,"abstract":[{"text":"Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.","lang":"eng"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt).","date_updated":"2025-07-14T09:10:04Z","ec_funded":1,"month":"12","oa":1,"title":"Compositional policy learning in stochastic control systems with formal guarantees","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public"},{"month":"04","ec_funded":1,"status":"public","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031308222"],"eissn":["1611-3349"]},"oa":1,"_id":"13142","date_updated":"2025-07-14T09:09:52Z","abstract":[{"text":"Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.","lang":"eng"}],"year":"2023","intvolume":"     13993","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” In <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, 13993:3–25. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">https://doi.org/10.1007/978-3-031-30823-9_1</a>.","mla":"Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems.” <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, vol. 13993, Springer Nature, 2023, pp. 3–25, doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">10.1007/978-3-031-30823-9_1</a>.","ista":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.","apa":"Chatterjee, K., Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2023). A learner-verifier framework for neural network controllers and certificates of stochastic systems. In <i>Tools and Algorithms for the Construction and Analysis of Systems </i> (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">https://doi.org/10.1007/978-3-031-30823-9_1</a>","ieee":"K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier framework for neural network controllers and certificates of stochastic systems,” in <i>Tools and Algorithms for the Construction and Analysis of Systems </i>, Paris, France, 2023, vol. 13993, pp. 3–25.","ama":"Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: <i>Tools and Algorithms for the Construction and Analysis of Systems </i>. Vol 13993. Springer Nature; 2023:3-25. doi:<a href=\"https://doi.org/10.1007/978-3-031-30823-9_1\">10.1007/978-3-031-30823-9_1</a>","short":"K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25."},"scopus_import":"1","file_date_updated":"2023-06-19T08:29:30Z","ddc":["000"],"oa_version":"Published Version","date_published":"2023-04-22T00:00:00Z","conference":{"start_date":"2023-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2023-04-27","location":"Paris, France"},"publication_status":"published","doi":"10.1007/978-3-031-30823-9_1","alternative_title":["LNCS"],"publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"A learner-verifier framework for neural network controllers and certificates of stochastic systems","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A"},{"full_name":"Lechner, Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias"},{"orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"file":[{"file_size":528455,"success":1,"content_type":"application/pdf","relation":"main_file","date_created":"2023-06-19T08:29:30Z","file_name":"2023_LNCS_Chatterjee.pdf","date_updated":"2023-06-19T08:29:30Z","access_level":"open_access","checksum":"3d8a8bb24d211bc83360dfc2fd744307","file_id":"13150","creator":"dernst"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","day":"22","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"quality_controlled":"1","volume":13993,"article_processing_charge":"No","type":"conference","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"has_accepted_license":"1","page":"3-25","date_created":"2023-06-18T22:00:47Z","publication":"Tools and Algorithms for the Construction and Analysis of Systems "},{"abstract":[{"lang":"eng","text":"We study the problem of training and certifying adversarially robust quantized neural networks (QNNs). Quantization is a technique for making neural networks more efficient by running them using low-bit integer arithmetic and is therefore commonly adopted in industry. Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization, and certification of the quantized representation is necessary to guarantee robustness. In this work, we present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs. Inspired by advances in robust learning of non-quantized networks, our training algorithm computes the gradient of an abstract representation of the actual network. Unlike existing approaches, our method can handle the discrete semantics of QNNs. Based on QA-IBP, we also develop a complete verification procedure for verifying the adversarial robustness of QNNs, which is guaranteed to terminate and produce a correct answer. Compared to existing approaches, the key advantage of our verification procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate experimentally that our approach significantly outperforms existing methods and establish the new state-of-the-art for training and certifying the robustness of QNNs."}],"arxiv":1,"issue":"12","date_updated":"2025-07-14T09:09:56Z","year":"2023","_id":"14242","status":"public","publication_identifier":{"isbn":["9781577358800"]},"oa":1,"month":"06","ec_funded":1,"doi":"10.1609/aaai.v37i12.26747","conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2023-02-07","location":"Washington, DC, United States","end_date":"2023-02-14"},"publication_status":"published","oa_version":"Preprint","date_published":"2023-06-26T00:00:00Z","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2211.16187"}],"citation":{"ista":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 14964–14973.","mla":"Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 12, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:<a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">10.1609/aaai.v37i12.26747</a>.","apa":"Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., &#38; Rus, D. (2023). Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 14964–14973). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">https://doi.org/10.1609/aaai.v37i12.26747</a>","chicago":"Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, Thomas A Henzinger, and Daniela Rus. “Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:14964–73. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">https://doi.org/10.1609/aaai.v37i12.26747</a>.","ama":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973. doi:<a href=\"https://doi.org/10.1609/aaai.v37i12.26747\">10.1609/aaai.v37i12.26747</a>","ieee":"M. Lechner, D. Zikelic, K. Chatterjee, T. A. Henzinger, and D. Rus, “Quantization-aware interval bound propagation for training certifiably robust quantized neural networks,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973.","short":"M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, D. Rus, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 14964–14973."},"intvolume":"        37","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. Research was sponsored by the United\r\nStates Air Force Research Laboratory and the United States Air Force Artificial Intelligence Accelerator and was accomplished under Cooperative Agreement Number FA8750-19-2-\r\n1000. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied,\r\nof the United States Air Force or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright\r\nnotation herein. The research was also funded in part by the AI2050 program at Schmidt Futures (Grant G-22-63172) and Capgemini SE.","day":"26","author":[{"last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","full_name":"Lechner, Mathias"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Rus","first_name":"Daniela","full_name":"Rus, Daniela"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Association for the Advancement of Artificial Intelligence","title":"Quantization-aware interval bound propagation for training certifiably robust quantized neural networks","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","date_created":"2023-08-27T22:01:17Z","page":"14964-14973","type":"conference","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"article_processing_charge":"No","volume":37,"quality_controlled":"1","external_id":{"arxiv":["2211.16187"]}},{"title":"Bidding graph games with partially-observable budgets","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"27","acknowledgement":"This research was supported in part by ISF grant no.1679/21, by the ERC CoG 863818 (ForM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","author":[{"full_name":"Avni, Guy","first_name":"Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jecker, Ismael R","first_name":"Ismael R","last_name":"Jecker","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425"},{"full_name":"Zikelic, Dorde","first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic"}],"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"article_processing_charge":"No","volume":37,"quality_controlled":"1","external_id":{"arxiv":["2211.13626"]},"publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","page":"5464-5471","date_created":"2023-08-27T22:01:18Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"type":"conference","publication_identifier":{"isbn":["9781577358800"]},"oa":1,"status":"public","ec_funded":1,"month":"06","year":"2023","abstract":[{"lang":"eng","text":"Two-player zero-sum \"graph games\" are central in logic, verification, and multi-agent systems. The game proceeds by placing a token on a vertex of a graph, and allowing the players to move it to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In \"bidding games\", however, the players have budgets and in each turn, an auction (bidding) determines which player moves the token. So far, bidding games have only been studied as full-information games. In this work we initiate the study of partial-information bidding games: we study bidding games in which a player's initial budget is drawn from a known probability distribution. We show that while for some bidding mechanisms and objectives, it is straightforward to adapt the results from the full-information setting to the partial-information setting, for others, the analysis is significantly more challenging, requires new techniques, and gives rise to interesting results. Specifically, we study games with \"mean-payoff\" objectives in combination with \"poorman\" bidding. We construct optimal strategies for a partially-informed player who plays against a fully-informed adversary. We show that, somewhat surprisingly, the \"value\" under pure strategies does not necessarily exist in such games."}],"arxiv":1,"issue":"5","date_updated":"2025-07-14T09:09:56Z","_id":"14243","main_file_link":[{"url":"https://doi.org/10.1609/aaai.v37i5.25679","open_access":"1"}],"scopus_import":"1","intvolume":"        37","citation":{"ama":"Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable budgets. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. ; 2023:5464-5471. doi:<a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">10.1609/aaai.v37i5.25679</a>","ieee":"G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable budgets,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471.","short":"G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, 2023, pp. 5464–5471.","chicago":"Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with Partially-Observable Budgets.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:5464–71, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">https://doi.org/10.1609/aaai.v37i5.25679</a>.","apa":"Avni, G., Jecker, I. R., &#38; Zikelic, D. (2023). Bidding graph games with partially-observable budgets. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 5464–5471). Washington, DC, United States. <a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">https://doi.org/10.1609/aaai.v37i5.25679</a>","mla":"Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 5, 2023, pp. 5464–71, doi:<a href=\"https://doi.org/10.1609/aaai.v37i5.25679\">10.1609/aaai.v37i5.25679</a>.","ista":"Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 5464–5471."},"doi":"10.1609/aaai.v37i5.25679","conference":{"start_date":"2023-02-07","name":"AAAI: Conference on Artificial Intelligence","end_date":"2023-02-14","location":"Washington, DC, United States"},"publication_status":"published","date_published":"2023-06-27T00:00:00Z","oa_version":"Published Version"},{"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"day":"09","acknowledgement":"We thank Shaun Willows, Thomas Lugnet, and the Living Room Application Vending team for suggesting threshold\r\nbounds as a developer-friendly way to interact with a differential cost analyzer, and we thank Jim Christy, Daniel\r\nSchoepe, and the Prime Video Automated Reasoning team for their support and helpful suggestions throughout the\r\nproject. We also thank Michael Emmi for feedback on an earlier version of this paper. And finally, we thank the anonymous reviewers for their useful feedback and Aws Albarghouthi for shepherding the final version of the paper. Ðorđe Žikelić was also partially supported by ERC CoG 863818 (FoRM-SMArt).","file":[{"content_type":"application/pdf","relation":"main_file","success":1,"file_size":318697,"date_updated":"2022-06-27T07:38:21Z","file_name":"2022_PLDI_Zikelic.pdf","date_created":"2022-06-27T07:38:21Z","creator":"dernst","checksum":"7eb915a2ca5b5ce4729321f33b2e16e1","file_id":"11466","access_level":"open_access"}],"isi":1,"author":[{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic"},{"last_name":"Chang","first_name":"Bor-Yuh Evan","full_name":"Chang, Bor-Yuh Evan"},{"last_name":"Bolignano","first_name":"Pauline","full_name":"Bolignano, Pauline"},{"full_name":"Raimondi, Franco","first_name":"Franco","last_name":"Raimondi"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"title":"Differential cost analysis with simultaneous potentials and anti-potentials","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publisher":"Association for Computing Machinery","publication":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","page":"442-457","date_created":"2022-06-21T09:26:15Z","has_accepted_license":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"type":"conference","article_processing_charge":"No","quality_controlled":"1","external_id":{"arxiv":["2204.00870"],"isi":["000850435600030"]},"year":"2022","arxiv":1,"abstract":[{"text":"We present a novel approach to differential cost analysis that, given a program revision, attempts to statically bound the difference in resource usage, or cost, between the two program versions. Differential cost analysis is particularly interesting because of the many compelling applications for it, such as detecting resource-use regressions at code-review time or proving the absence of certain side-channel vulnerabilities. One prior approach to differential cost analysis is to apply relational reasoning that conceptually constructs a product program on which one can over-approximate the difference in costs between the two program versions. However, a significant challenge in any relational approach is effectively aligning the program versions to get precise results. In this paper, our key insight is that we can avoid the need for and the limitations of program alignment if, instead, we bound the difference of two cost-bound summaries rather than directly bounding the concrete cost difference. In particular, our method computes a threshold value for the maximal difference in cost between two program versions simultaneously using two kinds of cost-bound summaries---a potential function that evaluates to an upper bound for the cost incurred in the first program and an anti-potential function that evaluates to a lower bound for the cost incurred in the second. Our method has a number of desirable properties: it can be fully automated, it allows optimizing the threshold value on relative cost, it is suitable for programs that are not syntactically similar, and it supports non-determinism. We have evaluated an implementation of our approach on a number of program pairs collected from the literature, and we find that our method computes tight threshold values on relative cost in most examples.","lang":"eng"}],"date_updated":"2025-07-14T09:09:54Z","_id":"11459","oa":1,"publication_identifier":{"isbn":["9781450392655"]},"status":"public","ec_funded":1,"month":"06","doi":"10.1145/3519939.3523435","publication_status":"published","conference":{"end_date":"2022-06-17","location":"San Diego, CA, United States","start_date":"2022-06-13","name":"PLDI: Programming Language Design and Implementation"},"date_published":"2022-06-09T00:00:00Z","oa_version":"Published Version","ddc":["000"],"file_date_updated":"2022-06-27T07:38:21Z","scopus_import":"1","citation":{"chicago":"Zikelic, Dorde, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi. “Differential Cost Analysis with Simultaneous Potentials and Anti-Potentials.” In <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 442–57. Association for Computing Machinery, 2022. <a href=\"https://doi.org/10.1145/3519939.3523435\">https://doi.org/10.1145/3519939.3523435</a>.","ista":"Zikelic D, Chang B-YE, Bolignano P, Raimondi F. 2022. Differential cost analysis with simultaneous potentials and anti-potentials. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 442–457.","mla":"Zikelic, Dorde, et al. “Differential Cost Analysis with Simultaneous Potentials and Anti-Potentials.” <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2022, pp. 442–57, doi:<a href=\"https://doi.org/10.1145/3519939.3523435\">10.1145/3519939.3523435</a>.","apa":"Zikelic, D., Chang, B.-Y. E., Bolignano, P., &#38; Raimondi, F. (2022). Differential cost analysis with simultaneous potentials and anti-potentials. In <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 442–457). San Diego, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3519939.3523435\">https://doi.org/10.1145/3519939.3523435</a>","short":"D. Zikelic, B.-Y.E. Chang, P. Bolignano, F. Raimondi, in:, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022, pp. 442–457.","ama":"Zikelic D, Chang B-YE, Bolignano P, Raimondi F. Differential cost analysis with simultaneous potentials and anti-potentials. In: <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2022:442-457. doi:<a href=\"https://doi.org/10.1145/3519939.3523435\">10.1145/3519939.3523435</a>","ieee":"D. Zikelic, B.-Y. E. Chang, P. Bolignano, and F. Raimondi, “Differential cost analysis with simultaneous potentials and anti-potentials,” in <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, San Diego, CA, United States, 2022, pp. 442–457."}},{"date_created":"2023-11-24T13:10:09Z","publication":"arXiv","publication_status":"submitted","doi":"10.48550/ARXIV.2210.05308","language":[{"iso":"eng"}],"date_published":"2022-11-29T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"type":"preprint","oa_version":"Preprint","main_file_link":[{"url":"https://arxiv.org/abs/2210.05308","open_access":"1"}],"article_processing_charge":"No","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"14539"},{"id":"14830","status":"public","relation":"later_version"}]},"external_id":{"arxiv":["2210.05308"]},"citation":{"chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">https://doi.org/10.48550/ARXIV.2210.05308</a>.","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. arXiv, <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>.","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>ArXiv</i>, doi:<a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>.","apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (n.d.). Learning control policies for stochastic systems with reach-avoid guarantees. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">https://doi.org/10.48550/ARXIV.2210.05308</a>","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">10.48550/ARXIV.2210.05308</a>","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” <i>arXiv</i>. .","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, ArXiv (n.d.)."},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-sa/4.0/legalcode","name":"Creative Commons Attribution-ShareAlike 4.0 International Public License (CC BY-SA 4.0)","image":"/images/cc_by_sa.png","short":"CC BY-SA (4.0)"},"day":"29","year":"2022","date_updated":"2025-07-14T09:10:02Z","arxiv":1,"abstract":[{"lang":"eng","text":"We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold $p\\in[0,1]$ over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on $3$ stochastic non-linear reinforcement learning tasks."}],"_id":"14600","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","call_identifier":"H2020"}],"author":[{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"},{"first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"title":"Learning control policies for stochastic systems with reach-avoid guarantees","oa":1,"status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","ec_funded":1,"license":"https://creativecommons.org/licenses/by-sa/4.0/","month":"11"},{"oa_version":"Preprint","type":"preprint","language":[{"iso":"eng"}],"date_published":"2022-05-24T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"submitted","doi":"10.48550/arXiv.2205.11991","date_created":"2023-11-24T13:22:30Z","publication":"arXiv","external_id":{"arxiv":["2205.11991"]},"citation":{"short":"D. Zikelic, M. Lechner, K. Chatterjee, T.A. Henzinger, ArXiv (n.d.).","ama":"Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>","ieee":"D. Zikelic, M. Lechner, K. Chatterjee, and T. A. Henzinger, “Learning stabilizing policies in stochastic control systems,” <i>arXiv</i>. .","mla":"Zikelic, Dorde, et al. “Learning Stabilizing Policies in Stochastic Control Systems.” <i>ArXiv</i>, doi:<a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>.","ista":"Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. arXiv, <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>.","apa":"Zikelic, D., Lechner, M., Chatterjee, K., &#38; Henzinger, T. A. (n.d.). Learning stabilizing policies in stochastic control systems. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">https://doi.org/10.48550/arXiv.2205.11991</a>","chicago":"Zikelic, Dorde, Mathias Lechner, Krishnendu Chatterjee, and Thomas A Henzinger. “Learning Stabilizing Policies in Stochastic Control Systems.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2205.11991\">https://doi.org/10.48550/arXiv.2205.11991</a>."},"related_material":{"record":[{"id":"14539","relation":"dissertation_contains","status":"public"}]},"main_file_link":[{"url":"https://arxiv.org/abs/2205.11991","open_access":"1"}],"article_processing_charge":"No","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"},{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"author":[{"first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","full_name":"Zikelic, Dorde"},{"first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"}],"_id":"14601","date_updated":"2025-07-14T09:10:00Z","arxiv":1,"abstract":[{"lang":"eng","text":"In this work, we address the problem of learning provably stable neural\r\nnetwork policies for stochastic control systems. While recent work has\r\ndemonstrated the feasibility of certifying given policies using martingale\r\ntheory, the problem of how to learn such policies is little explored. Here, we\r\nstudy the effectiveness of jointly learning a policy together with a martingale\r\ncertificate that proves its stability using a single learning algorithm. We\r\nobserve that the joint optimization problem becomes easily stuck in local\r\nminima when starting from a randomly initialized policy. Our results suggest\r\nthat some form of pre-training of the policy is required for the joint\r\noptimization to repair and verify the policy successfully."}],"day":"24","year":"2022","month":"05","ec_funded":1,"status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","title":"Learning stabilizing policies in stochastic control systems","oa":1},{"article_processing_charge":"Yes (in subscription journal)","external_id":{"isi":["000870304500004"]},"quality_controlled":"1","volume":13371,"related_material":{"record":[{"id":"14539","relation":"dissertation_contains","status":"public"}]},"has_accepted_license":"1","date_created":"2022-08-28T22:02:02Z","page":"55-78","publication":"Proceedings of the 34th International Conference on Computer Aided Verification","type":"conference","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"publisher":"Springer","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","title":"Sound and complete certificates for auantitative termination analysis of probabilistic programs","alternative_title":["LNCS"],"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055, the HKUST Startup Grant R9272 and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","day":"07","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","call_identifier":"H2020"}],"isi":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"file":[{"file_size":505094,"success":1,"relation":"main_file","content_type":"application/pdf","date_created":"2022-08-29T09:17:01Z","file_name":"2022_LNCS_Chatterjee.pdf","date_updated":"2022-08-29T09:17:01Z","access_level":"open_access","file_id":"12003","creator":"alisjak","checksum":"24e0f810ec52735a90ade95198bc641d"}],"file_date_updated":"2022-08-29T09:17:01Z","scopus_import":"1","ddc":["000"],"citation":{"ama":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Sound and complete certificates for auantitative termination analysis of probabilistic programs. In: <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>. Vol 13371. Springer; 2022:55-78. doi:<a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">10.1007/978-3-031-13185-1_4</a>","ieee":"K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Sound and complete certificates for auantitative termination analysis of probabilistic programs,” in <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, Haifa, Israel, 2022, vol. 13371, pp. 55–78.","short":"K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, in:, Proceedings of the 34th International Conference on Computer Aided Verification, Springer, 2022, pp. 55–78.","ista":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2022. Sound and complete certificates for auantitative termination analysis of probabilistic programs. Proceedings of the 34th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13371, 55–78.","apa":"Chatterjee, K., Goharshady, A. K., Meggendorfer, T., &#38; Zikelic, D. (2022). Sound and complete certificates for auantitative termination analysis of probabilistic programs. In <i>Proceedings of the 34th International Conference on Computer Aided Verification</i> (Vol. 13371, pp. 55–78). Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">https://doi.org/10.1007/978-3-031-13185-1_4</a>","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Certificates for Auantitative Termination Analysis of Probabilistic Programs.” <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, vol. 13371, Springer, 2022, pp. 55–78, doi:<a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">10.1007/978-3-031-13185-1_4</a>.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. “Sound and Complete Certificates for Auantitative Termination Analysis of Probabilistic Programs.” In <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, 13371:55–78. Springer, 2022. <a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">https://doi.org/10.1007/978-3-031-13185-1_4</a>."},"intvolume":"     13371","publication_status":"published","conference":{"name":"CAV: Computer Aided Verification","start_date":"2022-08-07","location":"Haifa, Israel","end_date":"2022-08-10"},"doi":"10.1007/978-3-031-13185-1_4","oa_version":"Published Version","date_published":"2022-08-07T00:00:00Z","status":"public","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031131844"]},"oa":1,"month":"08","ec_funded":1,"date_updated":"2025-07-14T09:09:58Z","abstract":[{"text":"We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p∈[0,1], we aim for certificates proving that the program terminates with probability at least 1−p. The basic idea of our approach is to find a terminating stochastic invariant, i.e. a subset SI of program states such that (i) the probability of the program ever leaving SI is no more than p, and (ii) almost-surely, the program either leaves SI or terminates.\r\n\r\nWhile stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for qualitative termination analysis, we obtain the first automated, sound, and relatively complete algorithm for quantitative termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant.\r\n\r\nOur prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods.","lang":"eng"}],"year":"2022","_id":"12000"},{"has_accepted_license":"1","publication":"42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","date_created":"2023-01-01T23:00:50Z","type":"conference","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"language":[{"iso":"eng"}],"article_processing_charge":"No","volume":250,"quality_controlled":"1","acknowledgement":"The research was partially supported by the Hong Kong Research Grants Council ECS\r\nProject No. 26208122, ERC CoG 863818 (FoRM-SMArt), the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385, HKUST– Kaisa Joint Research Institute Project Grant HKJRI3A-055 and HKUST Startup Grant R9272. Ali Ahmadi and Roodabeh Safavi were interns at HKUST.","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"day":"14","author":[{"full_name":"Ahmadi, Ali","last_name":"Ahmadi","first_name":"Ali"},{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","first_name":"Tobias","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias"},{"first_name":"Roodabeh","last_name":"Safavi Hemami","id":"72ed2640-8972-11ed-ae7b-f9c81ec75154","full_name":"Safavi Hemami, Roodabeh"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde"}],"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"call_identifier":"H2020","name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"file":[{"success":1,"file_size":872534,"relation":"main_file","content_type":"application/pdf","access_level":"open_access","creator":"dernst","checksum":"6660c802489013f034c9e8bd57f4d46e","file_id":"12324","date_created":"2023-01-20T10:39:44Z","date_updated":"2023-01-20T10:39:44Z","file_name":"2022_LIPICs_Ahmadi.pdf"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","title":"Algorithms and hardness results for computing cores of Markov chains","doi":"10.4230/LIPIcs.FSTTCS.2022.29","publication_status":"published","conference":{"name":"FSTTC: Foundations of Software Technology and Theoretical Computer Science","start_date":"2022-12-18","location":"Madras, India","end_date":"2022-12-20"},"oa_version":"Published Version","date_published":"2022-12-14T00:00:00Z","scopus_import":"1","file_date_updated":"2023-01-20T10:39:44Z","ddc":["000"],"intvolume":"       250","citation":{"ista":"Ahmadi A, Chatterjee K, Goharshady AK, Meggendorfer T, Safavi Hemami R, Zikelic D. 2022. Algorithms and hardness results for computing cores of Markov chains. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTC: Foundations of Software Technology and Theoretical Computer Science vol. 250, 29.","mla":"Ahmadi, Ali, et al. “Algorithms and Hardness Results for Computing Cores of Markov Chains.” <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 250, 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29\">10.4230/LIPIcs.FSTTCS.2022.29</a>.","apa":"Ahmadi, A., Chatterjee, K., Goharshady, A. K., Meggendorfer, T., Safavi Hemami, R., &#38; Zikelic, D. (2022). Algorithms and hardness results for computing cores of Markov chains. In <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 250). Madras, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29\">https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29</a>","chicago":"Ahmadi, Ali, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Roodabeh Safavi Hemami, and Dorde Zikelic. “Algorithms and Hardness Results for Computing Cores of Markov Chains.” In <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Vol. 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29\">https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29</a>.","ama":"Ahmadi A, Chatterjee K, Goharshady AK, Meggendorfer T, Safavi Hemami R, Zikelic D. Algorithms and hardness results for computing cores of Markov chains. In: <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 250. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.29\">10.4230/LIPIcs.FSTTCS.2022.29</a>","ieee":"A. Ahmadi, K. Chatterjee, A. K. Goharshady, T. Meggendorfer, R. Safavi Hemami, and D. Zikelic, “Algorithms and hardness results for computing cores of Markov chains,” in <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Madras, India, 2022, vol. 250.","short":"A. Ahmadi, K. Chatterjee, A.K. Goharshady, T. Meggendorfer, R. Safavi Hemami, D. Zikelic, in:, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022."},"abstract":[{"lang":"eng","text":"Given a Markov chain M = (V, v_0, δ), with state space V and a starting state v_0, and a probability threshold ε, an ε-core is a subset C of states that is left with probability at most ε. More formally, C ⊆ V is an ε-core, iff ℙ[reach (V\\C)] ≤ ε. Cores have been applied in a wide variety of verification problems over Markov chains, Markov decision processes, and probabilistic programs, as a means of discarding uninteresting and low-probability parts of a probabilistic system and instead being able to focus on the states that are likely to be encountered in a real-world run. In this work, we focus on the problem of computing a minimal ε-core in a Markov chain. Our contributions include both negative and positive results: (i) We show that the decision problem on the existence of an ε-core of a given size is NP-complete. This solves an open problem posed in [Jan Kretínský and Tobias Meggendorfer, 2020]. We additionally show that the problem remains NP-complete even when limited to acyclic Markov chains with bounded maximal vertex degree; (ii) We provide a polynomial time algorithm for computing a minimal ε-core on Markov chains over control-flow graphs of structured programs. A straightforward combination of our algorithm with standard branch prediction techniques allows one to apply the idea of cores to find a subset of program lines that are left with low probability and then focus any desired static analysis on this core subset."}],"date_updated":"2025-07-14T09:09:55Z","year":"2022","article_number":"29","_id":"12102","status":"public","oa":1,"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959772617"]},"month":"12","ec_funded":1},{"acknowledgement":"K.C. acknowledges support from ERC Start Grant No. (279307: Graph Games), ERC Consolidator Grant No. (863818: ForM-SMart), and Austrian Science Fund (FWF)\r\nGrants No. P23499-N23 and No. S11407-N23 (RiSE). This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie\r\nSkłodowska-Curie Grant Agreement No. 665385.","day":"29","isi":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda"},{"first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas","full_name":"Pavlogiannis, Andreas"},{"full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec"}],"project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publisher":"American Physical Society","title":"Social balance on networks: Local minima and best-edge dynamics","publication":"Physical Review E","date_created":"2023-01-16T09:57:57Z","type":"journal_article","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"article_processing_charge":"No","article_type":"original","quality_controlled":"1","volume":106,"external_id":{"isi":["000870243100001"],"arxiv":["2210.02394"]},"abstract":[{"lang":"eng","text":"Structural balance theory is an established framework for studying social relationships of friendship and enmity. These relationships are modeled by a signed network whose energy potential measures the level of imbalance, while stochastic dynamics drives the network toward a state of minimum energy that captures social balance. It is known that this energy landscape has local minima that can trap socially aware dynamics, preventing it from reaching balance. Here we first study the robustness and attractor properties of these local minima. We show that a stochastic process can reach them from an abundance of initial states and that some local minima cannot be escaped by mild perturbations of the network. Motivated by these anomalies, we introduce best-edge dynamics (BED), a new plausible stochastic process. We prove that BED always reaches balance and that it does so fast in various interesting settings."}],"issue":"3","arxiv":1,"date_updated":"2025-07-14T09:09:49Z","year":"2022","article_number":"034321","_id":"12257","status":"public","oa":1,"publication_identifier":{"issn":["2470-0045"],"eissn":["2470-0053"]},"month":"09","ec_funded":1,"doi":"10.1103/physreve.106.034321","publication_status":"published","oa_version":"Preprint","date_published":"2022-09-29T00:00:00Z","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2210.02394"}],"citation":{"ama":"Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. Social balance on networks: Local minima and best-edge dynamics. <i>Physical Review E</i>. 2022;106(3). doi:<a href=\"https://doi.org/10.1103/physreve.106.034321\">10.1103/physreve.106.034321</a>","ieee":"K. Chatterjee, J. Svoboda, D. Zikelic, A. Pavlogiannis, and J. Tkadlec, “Social balance on networks: Local minima and best-edge dynamics,” <i>Physical Review E</i>, vol. 106, no. 3. American Physical Society, 2022.","short":"K. Chatterjee, J. Svoboda, D. Zikelic, A. Pavlogiannis, J. Tkadlec, Physical Review E 106 (2022).","chicago":"Chatterjee, Krishnendu, Jakub Svoboda, Dorde Zikelic, Andreas Pavlogiannis, and Josef Tkadlec. “Social Balance on Networks: Local Minima and Best-Edge Dynamics.” <i>Physical Review E</i>. American Physical Society, 2022. <a href=\"https://doi.org/10.1103/physreve.106.034321\">https://doi.org/10.1103/physreve.106.034321</a>.","apa":"Chatterjee, K., Svoboda, J., Zikelic, D., Pavlogiannis, A., &#38; Tkadlec, J. (2022). Social balance on networks: Local minima and best-edge dynamics. <i>Physical Review E</i>. American Physical Society. <a href=\"https://doi.org/10.1103/physreve.106.034321\">https://doi.org/10.1103/physreve.106.034321</a>","ista":"Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. 2022. Social balance on networks: Local minima and best-edge dynamics. Physical Review E. 106(3), 034321.","mla":"Chatterjee, Krishnendu, et al. “Social Balance on Networks: Local Minima and Best-Edge Dynamics.” <i>Physical Review E</i>, vol. 106, no. 3, 034321, American Physical Society, 2022, doi:<a href=\"https://doi.org/10.1103/physreve.106.034321\">10.1103/physreve.106.034321</a>."},"intvolume":"       106"},{"page":"7326-7336","date_created":"2023-02-05T17:29:50Z","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"type":"journal_article","article_type":"original","article_processing_charge":"No","related_material":{"record":[{"id":"14539","relation":"dissertation_contains","status":"public"}]},"external_id":{"arxiv":["2112.09495"]},"volume":36,"quality_controlled":"1","keyword":["General Medicine"],"day":"28","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme\r\nunder the Marie Skłodowska-Curie Grant Agreement No. 665385.","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"author":[{"last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","full_name":"Lechner, Mathias"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"}],"title":"Stability verification in stochastic control systems via neural network supermartingales","publisher":"Association for the Advancement of Artificial Intelligence","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","doi":"10.1609/aaai.v36i7.20695","date_published":"2022-06-28T00:00:00Z","oa_version":"Preprint","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2112.09495"}],"intvolume":"        36","citation":{"short":"M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022) 7326–7336.","ieee":"M. Lechner, D. Zikelic, K. Chatterjee, and T. A. Henzinger, “Stability verification in stochastic control systems via neural network supermartingales,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 7. Association for the Advancement of Artificial Intelligence, pp. 7326–7336, 2022.","ama":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA. Stability verification in stochastic control systems via neural network supermartingales. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2022;36(7):7326-7336. doi:<a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">10.1609/aaai.v36i7.20695</a>","mla":"Lechner, Mathias, et al. “Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 7, Association for the Advancement of Artificial Intelligence, 2022, pp. 7326–36, doi:<a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">10.1609/aaai.v36i7.20695</a>.","apa":"Lechner, M., Zikelic, D., Chatterjee, K., &#38; Henzinger, T. A. (2022). Stability verification in stochastic control systems via neural network supermartingales. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">https://doi.org/10.1609/aaai.v36i7.20695</a>","ista":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA. 2022. Stability verification in stochastic control systems via neural network supermartingales. Proceedings of the AAAI Conference on Artificial Intelligence. 36(7), 7326–7336.","chicago":"Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A Henzinger. “Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2022. <a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">https://doi.org/10.1609/aaai.v36i7.20695</a>."},"year":"2022","date_updated":"2025-07-14T09:09:58Z","abstract":[{"lang":"eng","text":"We consider the problem of formally verifying almost-sure (a.s.) asymptotic stability in discrete-time nonlinear stochastic control systems. While verifying stability in deterministic control systems is extensively studied in the literature, verifying stability in stochastic control systems is an open problem. The few existing works on this topic either consider only specialized forms of stochasticity or make restrictive assumptions on the system, rendering them inapplicable to learning algorithms with neural network policies. \r\n In this work, we present an approach for general nonlinear stochastic control problems with two novel aspects: (a) instead of classical stochastic extensions of Lyapunov functions, we use ranking supermartingales (RSMs) to certify a.s. asymptotic stability, and (b) we present a method for learning neural network RSMs. \r\n We prove that our approach guarantees a.s. asymptotic stability of the system and\r\n provides the first method to obtain bounds on the stabilization time, which stochastic Lyapunov functions do not.\r\n Finally, we validate our approach experimentally on a set of nonlinear stochastic reinforcement learning environments with neural network policies."}],"arxiv":1,"issue":"7","_id":"12511","oa":1,"publication_identifier":{"eissn":["2374-3468"],"isbn":["9781577358350"],"issn":["2159-5399"]},"status":"public","ec_funded":1,"month":"06"},{"file_date_updated":"2022-01-26T07:41:16Z","main_file_link":[{"url":"https://ojs.aaai.org/index.php/AAAI/article/view/16496","open_access":"1"}],"scopus_import":"1","ddc":["000"],"citation":{"ieee":"T. A. Henzinger, M. Lechner, and D. Zikelic, “Scalable verification of quantized neural networks,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Virtual, 2021, vol. 35, no. 5A, pp. 3787–3795.","ama":"Henzinger TA, Lechner M, Zikelic D. Scalable verification of quantized neural networks. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 35. AAAI Press; 2021:3787-3795.","short":"T.A. Henzinger, M. Lechner, D. Zikelic, in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 3787–3795.","apa":"Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2021). Scalable verification of quantized neural networks. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 35, pp. 3787–3795). Virtual: AAAI Press.","mla":"Henzinger, Thomas A., et al. “Scalable Verification of Quantized Neural Networks.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 35, no. 5A, AAAI Press, 2021, pp. 3787–95.","ista":"Henzinger TA, Lechner M, Zikelic D. 2021. Scalable verification of quantized neural networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 3787–3795.","chicago":"Henzinger, Thomas A, Mathias Lechner, and Dorde Zikelic. “Scalable Verification of Quantized Neural Networks.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 35:3787–95. AAAI Press, 2021."},"intvolume":"        35","conference":{"name":"AAAI: Association for the Advancement of Artificial Intelligence","start_date":"2021-02-02","location":"Virtual","end_date":"2021-02-09"},"publication_status":"published","oa_version":"Published Version","date_published":"2021-05-28T00:00:00Z","status":"public","oa":1,"publication_identifier":{"isbn":["978-1-57735-866-4"],"eissn":["2374-3468"],"issn":["2159-5399"]},"month":"05","ec_funded":1,"arxiv":1,"abstract":[{"lang":"eng","text":"Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for verification of an idealized model of the actual network which works over real arithmetic and ignores rounding imprecisions. This idealization is in stark contrast to network quantization, which is a technique that trades numerical precision for computational efficiency and is, therefore, often applied in practice. Neglecting rounding errors of such low-bit quantized neural networks has been shown to lead to wrong conclusions about the network’s correctness. Thus, the desired approach for verifying quantized neural networks would be one that takes these rounding errors\r\ninto account. In this paper, we show that verifying the bitexact implementation of quantized neural networks with bitvector specifications is PSPACE-hard, even though verifying idealized real-valued networks and satisfiability of bit-vector specifications alone are each in NP. Furthermore, we explore several practical heuristics toward closing the complexity gap between idealized and bit-exact verification. In particular, we propose three techniques for making SMT-based verification of quantized neural networks more scalable. Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches."}],"issue":"5A","date_updated":"2025-07-14T09:10:11Z","year":"2021","_id":"10665","article_processing_charge":"No","volume":35,"quality_controlled":"1","external_id":{"arxiv":["2012.08185"]},"related_material":{"record":[{"id":"11362","relation":"dissertation_contains","status":"public"}]},"has_accepted_license":"1","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","date_created":"2022-01-25T15:15:02Z","page":"3787-3795","type":"conference","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"AAAI Press","title":"Scalable verification of quantized neural networks","alternative_title":["Technical Tracks"],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein\r\nAward), ERC CoG 863818 (FoRM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.\r\n","day":"28","author":[{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","first_name":"Mathias","full_name":"Lechner, Mathias"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699"}],"project":[{"call_identifier":"H2020","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"file":[{"date_created":"2022-01-26T07:41:16Z","file_name":"16496-Article Text-19990-1-2-20210518 (1).pdf","date_updated":"2022-01-26T07:41:16Z","access_level":"open_access","file_id":"10684","creator":"mlechner","checksum":"2bc8155b2526a70fba5b7301bc89dbd1","success":1,"file_size":137235,"content_type":"application/pdf","relation":"main_file"}]},{"_id":"10694","year":"2021","abstract":[{"text":"In a two-player zero-sum graph game the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In bidding games, however, the players have budgets, and in each turn, we hold an “auction” (bidding) to determine which player moves the token: both players simultaneously submit bids and the higher bidder moves the token. The bidding mechanisms differ in their payment schemes. Bidding games were largely studied with variants of first-price bidding in which only the higher bidder pays his bid. We focus on all-pay bidding, where both players pay their bids. Finite-duration all-pay bidding games were studied and shown to be technically more challenging than their first-price counterparts. We study for the first time, infinite-duration all-pay bidding games. Our most interesting results are for mean-payoff objectives: we portray a complete picture for games played on strongly-connected graphs. We study both pure (deterministic) and mixed (probabilistic) strategies and completely characterize the optimal and almost-sure (with probability 1) payoffs the players can respectively guarantee. We show that mean-payoff games under all-pay bidding exhibit the intriguing mathematical properties of their first-price counterparts; namely, an equivalence with random-turn games in which in each turn, the player who moves is selected according to a (biased) coin toss. The equivalences for all-pay bidding are more intricate and unexpected than for first-price bidding.","lang":"eng"}],"arxiv":1,"date_updated":"2025-07-14T09:10:12Z","ec_funded":1,"month":"01","oa":1,"publication_identifier":{"isbn":["978-1-61197-646-5"]},"status":"public","date_published":"2021-01-01T00:00:00Z","oa_version":"Preprint","doi":"10.1137/1.9781611976465.38","publication_status":"published","conference":{"start_date":"2021-01-10","name":"SODA: Symposium on Discrete Algorithms","end_date":"2021-01-13","location":"Virtual"},"citation":{"chicago":"Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Infinite-Duration All-Pay Bidding Games.” In <i>Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms</i>, edited by Dániel Marx, 617–36. Society for Industrial and Applied Mathematics, 2021. <a href=\"https://doi.org/10.1137/1.9781611976465.38\">https://doi.org/10.1137/1.9781611976465.38</a>.","apa":"Avni, G., Jecker, I. R., &#38; Zikelic, D. (2021). Infinite-duration all-pay bidding games. In D. Marx (Ed.), <i>Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms</i> (pp. 617–636). Virtual: Society for Industrial and Applied Mathematics. <a href=\"https://doi.org/10.1137/1.9781611976465.38\">https://doi.org/10.1137/1.9781611976465.38</a>","ista":"Avni G, Jecker IR, Zikelic D. 2021. Infinite-duration all-pay bidding games. Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 617–636.","mla":"Avni, Guy, et al. “Infinite-Duration All-Pay Bidding Games.” <i>Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms</i>, edited by Dániel Marx, Society for Industrial and Applied Mathematics, 2021, pp. 617–36, doi:<a href=\"https://doi.org/10.1137/1.9781611976465.38\">10.1137/1.9781611976465.38</a>.","short":"G. Avni, I.R. Jecker, D. Zikelic, in:, D. Marx (Ed.), Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial and Applied Mathematics, 2021, pp. 617–636.","ama":"Avni G, Jecker IR, Zikelic D. Infinite-duration all-pay bidding games. In: Marx D, ed. <i>Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms</i>. Society for Industrial and Applied Mathematics; 2021:617-636. doi:<a href=\"https://doi.org/10.1137/1.9781611976465.38\">10.1137/1.9781611976465.38</a>","ieee":"G. Avni, I. R. Jecker, and D. Zikelic, “Infinite-duration all-pay bidding games,” in <i>Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms</i>, Virtual, 2021, pp. 617–636."},"scopus_import":"1","main_file_link":[{"url":"https://arxiv.org/abs/2005.06636","open_access":"1"}],"author":[{"first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","full_name":"Avni, Guy"},{"full_name":"Jecker, Ismael R","first_name":"Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","last_name":"Jecker"},{"first_name":"Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"International IST Doctoral Program","call_identifier":"H2020","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"day":"01","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and by the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","title":"Infinite-duration all-pay bidding games","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publisher":"Society for Industrial and Applied Mathematics","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"language":[{"iso":"eng"}],"type":"conference","publication":"Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms","date_created":"2022-01-27T12:11:23Z","page":"617-636","quality_controlled":"1","editor":[{"first_name":"Dániel","last_name":"Marx","full_name":"Marx, Dániel"}],"external_id":{"arxiv":["2005.06636"]},"article_processing_charge":"No"},{"doi":"10.1145/3453483.3454093","publication_status":"published","conference":{"name":"PLDI: Programming Language Design and Implementation","start_date":"2021-06-20","location":"Online","end_date":"2021-06-26"},"oa_version":"Preprint","date_published":"2021-06-01T00:00:00Z","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2104.01189"}],"citation":{"chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. “Proving Non-Termination by Program Reversal.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 1033–48. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3453483.3454093\">https://doi.org/10.1145/3453483.3454093</a>.","apa":"Chatterjee, K., Goharshady, E. K., Novotný, P., &#38; Zikelic, D. (2021). Proving non-termination by program reversal. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 1033–1048). Online: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3453483.3454093\">https://doi.org/10.1145/3453483.3454093</a>","mla":"Chatterjee, Krishnendu, et al. “Proving Non-Termination by Program Reversal.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 1033–48, doi:<a href=\"https://doi.org/10.1145/3453483.3454093\">10.1145/3453483.3454093</a>.","ista":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. Proving non-termination by program reversal. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1033–1048.","short":"K. Chatterjee, E.K. Goharshady, P. Novotný, D. Zikelic, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1033–1048.","ama":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. Proving non-termination by program reversal. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:1033-1048. doi:<a href=\"https://doi.org/10.1145/3453483.3454093\">10.1145/3453483.3454093</a>","ieee":"K. Chatterjee, E. K. Goharshady, P. Novotný, and D. Zikelic, “Proving non-termination by program reversal,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Online, 2021, pp. 1033–1048."},"arxiv":1,"abstract":[{"lang":"eng","text":"We present a new approach to proving non-termination of non-deterministic integer programs. Our technique is rather simple but efficient. It relies on a purely syntactic reversal of the program's transition system followed by a constraint-based invariant synthesis with constraints coming from both the original and the reversed transition system. The latter task is performed by a simple call to an off-the-shelf SMT-solver, which allows us to leverage the latest advances in SMT-solving. Moreover, our method offers a combination of features not present (as a whole) in previous approaches: it handles programs with non-determinism, provides relative completeness guarantees and supports programs with polynomial arithmetic. The experiments performed with our prototype tool RevTerm show that our approach, despite its simplicity and stronger theoretical guarantees, is at least on par with the state-of-the-art tools, often achieving a non-trivial improvement under a proper configuration of its parameters."}],"date_updated":"2025-07-14T09:10:06Z","year":"2021","_id":"9644","status":"public","oa":1,"publication_identifier":{"isbn":["9781450383912"]},"month":"06","ec_funded":1,"publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","page":"1033-1048","date_created":"2021-07-11T22:01:17Z","type":"conference","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"article_processing_charge":"No","quality_controlled":"1","external_id":{"isi":["000723661700067"],"arxiv":["2104.01189"]},"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"14539"}]},"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This research was partially supported by the ERCCoG 863818 (ForM-SMArt) and the Czech Science Foundation grant No. GJ19-15134Y.","day":"01","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Goharshady, Ehsan Kafshdar","last_name":"Goharshady","first_name":"Ehsan Kafshdar"},{"full_name":"Novotný, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","orcid":"0000-0002-4681-1699","first_name":"Dorde","full_name":"Zikelic, Dorde"}],"isi":1,"project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publisher":"Association for Computing Machinery","title":"Proving non-termination by program reversal"}]