[{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"isi":1,"publisher":"Association for Computing Machinery","has_accepted_license":"1","publication_identifier":{"isbn":["9781450392655"]},"date_published":"2022-06-09T00:00:00Z","external_id":{"arxiv":["2204.00870"],"isi":["000850435600030"]},"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_date_updated":"2022-06-27T07:38:21Z","publication":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","corr_author":"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"}],"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>.","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.","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>","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.","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.","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>","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>."},"author":[{"full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chang, Bor-Yuh Evan","first_name":"Bor-Yuh Evan","last_name":"Chang"},{"last_name":"Bolignano","first_name":"Pauline","full_name":"Bolignano, Pauline"},{"full_name":"Raimondi, Franco","first_name":"Franco","last_name":"Raimondi"}],"quality_controlled":"1","month":"06","oa":1,"year":"2022","day":"09","date_created":"2022-06-21T09:26:15Z","file":[{"relation":"main_file","file_size":318697,"file_id":"11466","creator":"dernst","content_type":"application/pdf","date_created":"2022-06-27T07:38:21Z","success":1,"file_name":"2022_PLDI_Zikelic.pdf","checksum":"7eb915a2ca5b5ce4729321f33b2e16e1","access_level":"open_access","date_updated":"2022-06-27T07:38:21Z"}],"_id":"11459","ddc":["000"],"language":[{"iso":"eng"}],"article_processing_charge":"No","scopus_import":"1","doi":"10.1145/3519939.3523435","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","date_updated":"2025-04-14T07:52:47Z","conference":{"start_date":"2022-06-13","location":"San Diego, CA, United States","name":"PLDI: Programming Language Design and Implementation","end_date":"2022-06-17"},"publication_status":"published","status":"public","page":"442-457","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","arxiv":1,"ec_funded":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"oa_version":"Published Version","type":"conference","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"title":"Differential cost analysis with simultaneous potentials and anti-potentials"},{"article_type":"original","oa_version":"Published Version","type":"journal_article","department":[{"_id":"UlWa"},{"_id":"HeEd"},{"_id":"KrCh"}],"title":"On compatible matchings","page":"225-240","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"ec_funded":1,"project":[{"call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425"},{"_id":"268116B8-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Mathematics, Computer Science","grant_number":"Z00342"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"scopus_import":"1","doi":"10.7155/jgaa.00591","intvolume":"        26","license":"https://creativecommons.org/licenses/by/4.0/","date_updated":"2026-04-16T09:18:20Z","issue":"2","publication_status":"published","status":"public","_id":"11938","file":[{"file_id":"11940","creator":"dernst","relation":"main_file","file_size":694538,"date_updated":"2022-08-22T06:42:42Z","access_level":"open_access","checksum":"dc6e255e3558faff924fd9e370886c11","file_name":"2022_JourGraphAlgorithmsApplic_Aichholzer.pdf","success":1,"date_created":"2022-08-22T06:42:42Z","content_type":"application/pdf"}],"ddc":["000"],"language":[{"iso":"eng"}],"article_processing_charge":"No","year":"2022","day":"01","date_created":"2022-08-21T22:01:56Z","volume":26,"author":[{"full_name":"Aichholzer, Oswin","first_name":"Oswin","last_name":"Aichholzer"},{"first_name":"Alan M","last_name":"Arroyo Guevara","id":"3207FDC6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2401-8670","full_name":"Arroyo Guevara, Alan M"},{"id":"45CFE238-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6660-1322","last_name":"Masárová","first_name":"Zuzana","full_name":"Masárová, Zuzana"},{"full_name":"Parada, Irene","last_name":"Parada","first_name":"Irene"},{"first_name":"Daniel","last_name":"Perz","full_name":"Perz, Daniel"},{"last_name":"Pilz","first_name":"Alexander","full_name":"Pilz, Alexander"},{"last_name":"Tkadlec","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef"},{"last_name":"Vogtenhuber","first_name":"Birgit","full_name":"Vogtenhuber, Birgit"}],"related_material":{"record":[{"id":"9296","status":"public","relation":"earlier_version"}]},"quality_controlled":"1","month":"06","oa":1,"publication":"Journal of Graph Algorithms and Applications","corr_author":"1","abstract":[{"lang":"eng","text":"A matching is compatible to two or more labeled point sets of size n with labels {1, . . . , n} if its straight-line drawing on each of these point sets is crossing-free. We study the maximum number of edges in a matching compatible to two or more labeled point sets in general position in the plane. We show that for any two labeled sets of n points in convex position there exists a compatible matching with ⌊√2n + 1 − 1⌋ edges. More generally, for any ℓ labeled point sets we construct compatible matchings of size Ω(n1/ℓ). As a corresponding upper bound, we use probabilistic arguments to show that for any ℓ given sets of n points there exists a labeling of each set such that the largest compatible matching has O(n2/(ℓ+1)) edges. Finally, we show that Θ(log n) copies of any set of n points are necessary and sufficient for the existence of labelings of these point sets such that any compatible matching consists only of a single edge."}],"citation":{"apa":"Aichholzer, O., Arroyo Guevara, A. M., Masárová, Z., Parada, I., Perz, D., Pilz, A., … Vogtenhuber, B. (2022). On compatible matchings. <i>Journal of Graph Algorithms and Applications</i>. Brown University. <a href=\"https://doi.org/10.7155/jgaa.00591\">https://doi.org/10.7155/jgaa.00591</a>","short":"O. Aichholzer, A.M. Arroyo Guevara, Z. Masárová, I. Parada, D. Perz, A. Pilz, J. Tkadlec, B. Vogtenhuber, Journal of Graph Algorithms and Applications 26 (2022) 225–240.","chicago":"Aichholzer, Oswin, Alan M Arroyo Guevara, Zuzana Masárová, Irene Parada, Daniel Perz, Alexander Pilz, Josef Tkadlec, and Birgit Vogtenhuber. “On Compatible Matchings.” <i>Journal of Graph Algorithms and Applications</i>. Brown University, 2022. <a href=\"https://doi.org/10.7155/jgaa.00591\">https://doi.org/10.7155/jgaa.00591</a>.","ieee":"O. Aichholzer <i>et al.</i>, “On compatible matchings,” <i>Journal of Graph Algorithms and Applications</i>, vol. 26, no. 2. Brown University, pp. 225–240, 2022.","ista":"Aichholzer O, Arroyo Guevara AM, Masárová Z, Parada I, Perz D, Pilz A, Tkadlec J, Vogtenhuber B. 2022. On compatible matchings. Journal of Graph Algorithms and Applications. 26(2), 225–240.","mla":"Aichholzer, Oswin, et al. “On Compatible Matchings.” <i>Journal of Graph Algorithms and Applications</i>, vol. 26, no. 2, Brown University, 2022, pp. 225–40, doi:<a href=\"https://doi.org/10.7155/jgaa.00591\">10.7155/jgaa.00591</a>.","ama":"Aichholzer O, Arroyo Guevara AM, Masárová Z, et al. On compatible matchings. <i>Journal of Graph Algorithms and Applications</i>. 2022;26(2):225-240. doi:<a href=\"https://doi.org/10.7155/jgaa.00591\">10.7155/jgaa.00591</a>"},"tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publisher":"Brown University","has_accepted_license":"1","publication_identifier":{"issn":["1526-1719"]},"date_published":"2022-06-01T00:00:00Z","external_id":{"arxiv":["2101.03928"]},"acknowledgement":"A.A. funded by the Marie Sklodowska-Curie grant agreement No 754411. Z.M. partially funded by Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z 342-N31. I.P., D.P., and B.V. partially supported by FWF within the collaborative DACH project Arrangements and Drawings as FWF project I 3340-N35. A.P. supported by a Schrödinger fellowship of the FWF: J-3847-N35. J.T. partially supported by ERC Start grant no. (279307: Graph Games), FWF grant no. P23499-N23 and S11407-N23 (RiSE).","file_date_updated":"2022-08-22T06:42:42Z"},{"title":"Sound and complete certificates for auantitative termination analysis of probabilistic programs","department":[{"_id":"KrCh"}],"oa_version":"Published Version","type":"conference","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","page":"55-78","publication_status":"published","status":"public","date_updated":"2026-04-07T13:27:55Z","conference":{"start_date":"2022-08-07","location":"Haifa, Israel","name":"CAV: Computer Aided Verification","end_date":"2022-08-10"},"intvolume":"     13371","scopus_import":"1","doi":"10.1007/978-3-031-13185-1_4","article_processing_charge":"Yes (in subscription journal)","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","date_created":"2022-08-29T09:17:01Z","success":1,"file_name":"2022_LNCS_Chatterjee.pdf","checksum":"24e0f810ec52735a90ade95198bc641d","access_level":"open_access","date_updated":"2022-08-29T09:17:01Z","file_size":505094,"relation":"main_file","creator":"alisjak","file_id":"12003"}],"_id":"12000","ddc":["000"],"volume":13371,"date_created":"2022-08-28T22:02:02Z","alternative_title":["LNCS"],"year":"2022","day":"07","oa":1,"month":"08","related_material":{"record":[{"status":"public","id":"14539","relation":"dissertation_contains"}]},"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","first_name":"Amir Kafshdar"},{"orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","last_name":"Meggendorfer","full_name":"Meggendorfer, Tobias"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic"}],"quality_controlled":"1","citation":{"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.","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>","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>.","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.","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>","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."},"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"}],"publication":"Proceedings of the 34th International Conference on Computer Aided Verification","publication_identifier":{"isbn":["9783031131844"],"issn":["0302-9743"],"eissn":["1611-3349"]},"file_date_updated":"2022-08-29T09:17:01Z","external_id":{"isi":["000870304500004"]},"date_published":"2022-08-07T00:00:00Z","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.","has_accepted_license":"1","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publisher":"Springer","isi":1},{"file":[{"file_size":657396,"relation":"main_file","file_id":"12323","creator":"dernst","content_type":"application/pdf","date_created":"2023-01-20T10:19:19Z","success":1,"file_name":"2022_LIPICs_Chatterjee.pdf","checksum":"a21e3ba2421e2c4a06aa2cb6d530ede1","access_level":"open_access","date_updated":"2023-01-20T10:19:19Z"}],"_id":"12101","ddc":["000"],"article_processing_charge":"No","language":[{"iso":"eng"}],"scopus_import":"1","doi":"10.4230/LIPIcs.FSTTCS.2022.11","intvolume":"       250","date_updated":"2026-04-07T11:49:11Z","conference":{"location":"Madras, India","start_date":"2022-12-18","end_date":"2022-12-20","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science"},"publication_status":"published","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"oa_version":"Published Version","type":"conference","department":[{"_id":"KrCh"}],"title":"Complexity of spatial games","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","has_accepted_license":"1","publication_identifier":{"isbn":["9783959772617"],"issn":["1868-8969"]},"file_date_updated":"2023-01-20T10:19:19Z","date_published":"2022-12-14T00:00:00Z","acknowledgement":"Krishnendu Chatterjee: The research was partially supported by the ERC CoG 863818\r\n(ForM-SMArt).\r\nIsmaël Jecker: The research was partially supported by the ERC grant 950398 (INFSYS).\r\nJakub Svoboda: The research was partially supported by the ERC CoG 863818 (ForM-SMArt)","publication":"42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","corr_author":"1","abstract":[{"text":"Spatial games form a widely-studied class of games from biology and physics modeling the evolution of social behavior. Formally, such a game is defined by a square (d by d) payoff matrix M and an undirected graph G. Each vertex of G represents an individual, that initially follows some strategy i ∈ {1,2,…,d}. In each round of the game, every individual plays the matrix game with each of its neighbors: An individual following strategy i meeting a neighbor following strategy j receives a payoff equal to the entry (i,j) of M. Then, each individual updates its strategy to its neighbors' strategy with the highest sum of payoffs, and the next round starts. The basic computational problems consist of reachability between configurations and the average frequency of a strategy. For general spatial games and graphs, these problems are in PSPACE. In this paper, we examine restricted setting: the game is a prisoner’s dilemma; and G is a subgraph of grid. We prove that basic computational problems for spatial games with prisoner’s dilemma on a subgraph of a grid are PSPACE-hard.","lang":"eng"}],"citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2022. Complexity of spatial games. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Foundations of Software Technology and Theoretical Computer Science vol. 250, 11:1-11:14.","ama":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Complexity of spatial games. 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.11\">10.4230/LIPIcs.FSTTCS.2022.11</a>","mla":"Chatterjee, Krishnendu, et al. “Complexity of Spatial Games.” <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 250, 11:1-11:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11\">10.4230/LIPIcs.FSTTCS.2022.11</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Complexity of Spatial Games.” 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.11\">https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.","apa":"Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., &#38; Svoboda, J. (2022). Complexity of spatial games. 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.11\">https://doi.org/10.4230/LIPIcs.FSTTCS.2022.11</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Complexity of spatial games,” in <i>42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Madras, India, 2022, vol. 250."},"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"first_name":"Ismael R","last_name":"Jecker","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","full_name":"Jecker, Ismael R"},{"full_name":"Svoboda, Jakub","last_name":"Svoboda","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"20138","status":"public"}]},"quality_controlled":"1","month":"12","oa":1,"year":"2022","day":"14","article_number":"11:1-11:14","date_created":"2023-01-01T23:00:50Z","volume":250},{"article_processing_charge":"No","language":[{"iso":"eng"}],"file":[{"success":1,"content_type":"application/pdf","date_created":"2023-01-20T10:39:44Z","access_level":"open_access","date_updated":"2023-01-20T10:39:44Z","file_name":"2022_LIPICs_Ahmadi.pdf","checksum":"6660c802489013f034c9e8bd57f4d46e","file_size":872534,"relation":"main_file","file_id":"12324","creator":"dernst"}],"_id":"12102","ddc":["000"],"publication_status":"published","status":"public","date_updated":"2025-07-10T11:50:23Z","conference":{"end_date":"2022-12-20","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","location":"Madras, India","start_date":"2022-12-18"},"intvolume":"       250","doi":"10.4230/LIPIcs.FSTTCS.2022.29","scopus_import":"1","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Algorithms and hardness results for computing cores of Markov chains","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"oa_version":"Published Version","type":"conference","publication_identifier":{"isbn":["9783959772617"],"issn":["1868-8969"]},"file_date_updated":"2023-01-20T10:39:44Z","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.","date_published":"2022-12-14T00:00:00Z","has_accepted_license":"1","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","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. FSTTCS: Foundations of Software Technology and Theoretical Computer Science vol. 250, 29.","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>","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>.","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>.","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.","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>","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."},"corr_author":"1","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."}],"publication":"42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","oa":1,"month":"12","author":[{"full_name":"Ahmadi, Ali","first_name":"Ali","last_name":"Ahmadi"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias"},{"last_name":"Safavi Hemami","first_name":"Roodabeh","id":"72ed2640-8972-11ed-ae7b-f9c81ec75154","full_name":"Safavi Hemami, Roodabeh"},{"last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"quality_controlled":"1","volume":250,"date_created":"2023-01-01T23:00:50Z","year":"2022","article_number":"29","day":"14"},{"_id":"12170","language":[{"iso":"eng"}],"article_processing_charge":"No","date_updated":"2025-09-10T09:49:29Z","conference":{"location":"Virtual","start_date":"2022-10-25","end_date":"2022-10-28","name":"ATVA: Automated Technology for Verification and Analysis"},"publication_status":"published","status":"public","scopus_import":"1","doi":"10.1007/978-3-031-19992-9_20","intvolume":"     13505","page":"320-326","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"title":"PET – A partial exploration tool for probabilistic verification","oa_version":"None","type":"conference","publication_identifier":{"isbn":["9783031199912"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031199929"]},"external_id":{"isi":["001456146500020"]},"acknowledgement":"We thank Pranav Ashok and Maximilian Weininger for their contributions to spiritual predecessors of PET as well as motivating the initial development of this tool.","date_published":"2022-10-21T00:00:00Z","publisher":"Springer Nature","isi":1,"corr_author":"1","abstract":[{"lang":"eng","text":"We present PET, a specialized and highly optimized framework for partial exploration on probabilistic systems. Over the last decade, several significant advances in the analysis of Markov decision processes employed partial exploration. In a nutshell, this idea allows to focus computation on specific parts of the system, guided by heuristics, while maintaining correctness. In particular, only relevant parts of the system are constructed on demand, which in turn potentially allows to omit constructing large parts of the system. Depending on the model, this leads to dramatic speed-ups, in extreme cases even up to an arbitrary factor. PET unifies several previous implementations and provides a flexible framework to easily implement partial exploration for many further problems. Our experimental evaluation shows significant improvements compared to the previous implementations while vastly reducing the overhead required to add support for additional properties."}],"citation":{"ieee":"T. Meggendorfer, “PET – A partial exploration tool for probabilistic verification,” in <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 320–326.","short":"T. Meggendorfer, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 320–326.","chicago":"Meggendorfer, Tobias. “PET – A Partial Exploration Tool for Probabilistic Verification.” In <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, 13505:320–26. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">https://doi.org/10.1007/978-3-031-19992-9_20</a>.","apa":"Meggendorfer, T. (2022). PET – A partial exploration tool for probabilistic verification. In <i>20th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 13505, pp. 320–326). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">https://doi.org/10.1007/978-3-031-19992-9_20</a>","ama":"Meggendorfer T. PET – A partial exploration tool for probabilistic verification. In: <i>20th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:320-326. doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">10.1007/978-3-031-19992-9_20</a>","mla":"Meggendorfer, Tobias. “PET – A Partial Exploration Tool for Probabilistic Verification.” <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 320–26, doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">10.1007/978-3-031-19992-9_20</a>.","ista":"Meggendorfer T. 2022. PET – A partial exploration tool for probabilistic verification. 20th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 13505, 320–326."},"publication":"20th International Symposium on Automated Technology for Verification and Analysis","author":[{"first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias"}],"quality_controlled":"1","month":"10","volume":13505,"year":"2022","day":"21","date_created":"2023-01-12T12:11:07Z","alternative_title":["LNCS"]},{"oa":1,"month":"09","quality_controlled":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Svoboda, Jakub","last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas"},{"full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"20138"}]},"volume":106,"date_created":"2023-01-16T09:57:57Z","article_number":"034321","day":"29","year":"2022","external_id":{"isi":["000870243100001"],"arxiv":["2210.02394"]},"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.","date_published":"2022-09-29T00:00:00Z","publication_identifier":{"eissn":["2470-0053"],"issn":["2470-0045"]},"publisher":"American Physical Society","isi":1,"citation":{"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>.","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>","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>","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>.","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."},"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."}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2210.02394","open_access":"1"}],"publication":"Physical Review E","project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020"}],"ec_funded":1,"arxiv":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","title":"Social balance on networks: Local minima and best-edge dynamics","department":[{"_id":"KrCh"}],"type":"journal_article","oa_version":"Preprint","article_type":"original","article_processing_charge":"No","language":[{"iso":"eng"}],"_id":"12257","status":"public","publication_status":"published","issue":"3","date_updated":"2026-04-07T11:49:11Z","intvolume":"       106","scopus_import":"1","doi":"10.1103/physreve.106.034321"},{"oa":1,"month":"06","quality_controlled":"1","author":[{"full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","last_name":"Schmid","first_name":"Laura"},{"full_name":"Hilbe, Christian","last_name":"Hilbe","first_name":"Christian","orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"volume":18,"date_created":"2023-01-16T10:02:51Z","article_number":"e1010149","day":"14","year":"2022","acknowledgement":"This work was supported by the European Research Council (https://erc.europa.eu/)\r\nCoG 863818 (ForM-SMArt) (to K.C.), and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.). The funders had no role in study design, data collection and analysis, decision to publish, or preparation of the manuscript.","date_published":"2022-06-14T00:00:00Z","file_date_updated":"2023-01-30T11:28:13Z","external_id":{"isi":["000843626800031"],"pmid":["35700167"]},"publication_identifier":{"eissn":["1553-7358"]},"pmid":1,"has_accepted_license":"1","isi":1,"publisher":"Public Library of Science","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"citation":{"ama":"Schmid L, Hilbe C, Chatterjee K, Nowak M. Direct reciprocity between individuals that use different strategy spaces. <i>PLOS Computational Biology</i>. 2022;18(6). doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1010149\">10.1371/journal.pcbi.1010149</a>","mla":"Schmid, Laura, et al. “Direct Reciprocity between Individuals That Use Different Strategy Spaces.” <i>PLOS Computational Biology</i>, vol. 18, no. 6, e1010149, Public Library of Science, 2022, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1010149\">10.1371/journal.pcbi.1010149</a>.","ista":"Schmid L, Hilbe C, Chatterjee K, Nowak M. 2022. Direct reciprocity between individuals that use different strategy spaces. PLOS Computational Biology. 18(6), e1010149.","ieee":"L. Schmid, C. Hilbe, K. Chatterjee, and M. Nowak, “Direct reciprocity between individuals that use different strategy spaces,” <i>PLOS Computational Biology</i>, vol. 18, no. 6. Public Library of Science, 2022.","chicago":"Schmid, Laura, Christian Hilbe, Krishnendu Chatterjee, and Martin Nowak. “Direct Reciprocity between Individuals That Use Different Strategy Spaces.” <i>PLOS Computational Biology</i>. Public Library of Science, 2022. <a href=\"https://doi.org/10.1371/journal.pcbi.1010149\">https://doi.org/10.1371/journal.pcbi.1010149</a>.","short":"L. Schmid, C. Hilbe, K. Chatterjee, M. Nowak, PLOS Computational Biology 18 (2022).","apa":"Schmid, L., Hilbe, C., Chatterjee, K., &#38; Nowak, M. (2022). Direct reciprocity between individuals that use different strategy spaces. <i>PLOS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.1010149\">https://doi.org/10.1371/journal.pcbi.1010149</a>"},"abstract":[{"text":"In repeated interactions, players can use strategies that respond to the outcome of previous rounds. Much of the existing literature on direct reciprocity assumes that all competing individuals use the same strategy space. Here, we study both learning and evolutionary dynamics of players that differ in the strategy space they explore. We focus on the infinitely repeated donation game and compare three natural strategy spaces: memory-1 strategies, which consider the last moves of both players, reactive strategies, which respond to the last move of the co-player, and unconditional strategies. These three strategy spaces differ in the memory capacity that is needed. We compute the long term average payoff that is achieved in a pairwise learning process. We find that smaller strategy spaces can dominate larger ones. For weak selection, unconditional players dominate both reactive and memory-1 players. For intermediate selection, reactive players dominate memory-1 players. Only for strong selection and low cost-to-benefit ratio, memory-1 players dominate the others. We observe that the supergame between strategy spaces can be a social dilemma: maximum payoff is achieved if both players explore a larger strategy space, but smaller strategy spaces dominate.","lang":"eng"}],"corr_author":"1","publication":"PLOS Computational Biology","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"ec_funded":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","title":"Direct reciprocity between individuals that use different strategy spaces","department":[{"_id":"KrCh"}],"type":"journal_article","oa_version":"Published Version","keyword":["Computational Theory and Mathematics","Cellular and Molecular Neuroscience","Genetics","Molecular Biology","Ecology","Modeling and Simulation","Ecology","Evolution","Behavior and Systematics"],"article_type":"original","article_processing_charge":"No","language":[{"iso":"eng"}],"ddc":["000","570"],"file":[{"file_id":"12460","creator":"dernst","relation":"main_file","file_size":3143222,"checksum":"31b6b311b6731f1658277a9dfff6632c","file_name":"2022_PlosCompBio_Schmid.pdf","date_updated":"2023-01-30T11:28:13Z","access_level":"open_access","date_created":"2023-01-30T11:28:13Z","content_type":"application/pdf","success":1}],"_id":"12280","status":"public","issue":"6","publication_status":"published","date_updated":"2025-04-14T07:52:47Z","intvolume":"        18","scopus_import":"1","doi":"10.1371/journal.pcbi.1010149"},{"oa":1,"month":"06","quality_controlled":"1","related_material":{"record":[{"id":"14539","status":"public","relation":"dissertation_contains"}]},"author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner","full_name":"Lechner, Mathias"},{"orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","full_name":"Zikelic, Dorde"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"}],"volume":36,"date_created":"2023-02-05T17:29:50Z","day":"28","year":"2022","date_published":"2022-06-28T00:00:00Z","external_id":{"arxiv":["2112.09495"]},"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.","publication_identifier":{"isbn":["9781577358350"],"issn":["2159-5399"],"eissn":["2374-3468"]},"publisher":"Association for the Advancement of Artificial Intelligence","citation":{"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.","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>","short":"M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022) 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>.","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>.","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>","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."},"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."}],"corr_author":"1","main_file_link":[{"url":"https://arxiv.org/abs/2112.09495","open_access":"1"}],"publication":"Proceedings of the AAAI Conference on Artificial Intelligence","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020"}],"ec_funded":1,"arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"7326-7336","title":"Stability verification in stochastic control systems via neural network supermartingales","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"type":"journal_article","oa_version":"Preprint","article_type":"original","keyword":["General Medicine"],"language":[{"iso":"eng"}],"article_processing_charge":"No","_id":"12511","status":"public","issue":"7","publication_status":"published","date_updated":"2026-04-07T13:27:55Z","intvolume":"        36","doi":"10.1609/aaai.v36i7.20695","scopus_import":"1"},{"date_published":"2022-06-28T00:00:00Z","external_id":{"arxiv":["2203.01640"]},"publication_identifier":{"isbn":["1577358767"],"eissn":["2374-3468"]},"publisher":"Association for the Advancement of Artificial Intelligence","abstract":[{"lang":"eng","text":"We treat the problem of risk-aware control for stochastic shortest path (SSP) on Markov decision processes (MDP). Typically, expectation is considered for SSP, which however is oblivious to the incurred risk. We present an alternative view, instead optimizing conditional value-at-risk (CVaR), an established risk measure. We treat both Markov chains as well as MDP and introduce, through novel insights, two algorithms, based on linear programming and value iteration, respectively. Both algorithms offer precise and provably correct solutions. Evaluation of our prototype implementation shows that risk-aware control is feasible on several moderately sized models."}],"corr_author":"1","citation":{"mla":"Meggendorfer, Tobias. “Risk-Aware Stochastic Shortest Path.” <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i>, vol. 36, no. 9, Association for the Advancement of Artificial Intelligence, 2022, pp. 9858–67, doi:<a href=\"https://doi.org/10.1609/aaai.v36i9.21222\">10.1609/aaai.v36i9.21222</a>.","ama":"Meggendorfer T. Risk-aware stochastic shortest path. In: <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i>. Vol 36. Association for the Advancement of Artificial Intelligence; 2022:9858-9867. doi:<a href=\"https://doi.org/10.1609/aaai.v36i9.21222\">10.1609/aaai.v36i9.21222</a>","ista":"Meggendorfer T. 2022. Risk-aware stochastic shortest path. Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022. Conference on Artificial Intelligence vol. 36, 9858–9867.","ieee":"T. Meggendorfer, “Risk-aware stochastic shortest path,” in <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i>, Virtual, 2022, vol. 36, no. 9, pp. 9858–9867.","apa":"Meggendorfer, T. (2022). Risk-aware stochastic shortest path. In <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i> (Vol. 36, pp. 9858–9867). Virtual: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v36i9.21222\">https://doi.org/10.1609/aaai.v36i9.21222</a>","chicago":"Meggendorfer, Tobias. “Risk-Aware Stochastic Shortest Path.” In <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i>, 36:9858–67. Association for the Advancement of Artificial Intelligence, 2022. <a href=\"https://doi.org/10.1609/aaai.v36i9.21222\">https://doi.org/10.1609/aaai.v36i9.21222</a>.","short":"T. Meggendorfer, in:, Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022, Association for the Advancement of Artificial Intelligence, 2022, pp. 9858–9867."},"main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.2203.01640"}],"publication":"Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022","oa":1,"quality_controlled":"1","author":[{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"}],"month":"06","volume":36,"day":"28","year":"2022","date_created":"2023-02-19T23:00:56Z","_id":"12568","article_processing_charge":"No","language":[{"iso":"eng"}],"conference":{"start_date":"2022-02-22","location":"Virtual","end_date":"2022-03-01","name":"Conference on Artificial Intelligence"},"date_updated":"2024-10-09T21:04:32Z","status":"public","publication_status":"published","issue":"9","scopus_import":"1","doi":"10.1609/aaai.v36i9.21222","intvolume":"        36","page":"9858-9867","arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"title":"Risk-aware stochastic shortest path","type":"conference","oa_version":"Preprint"},{"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Mohammadi, Mona","last_name":"Mohammadi","first_name":"Mona","id":"4363614d-b686-11ed-a7d5-ac9e4a24bc2e"},{"last_name":"Saona Urmeneta","first_name":"Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","orcid":"0000-0001-5103-038X","full_name":"Saona Urmeneta, Raimundo J"}],"arxiv":1,"month":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"oa":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"day":"28","article_number":"2209.14368","year":"2022","type":"preprint","date_created":"2023-02-24T12:21:40Z","oa_version":"Preprint","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"title":"Repeated prophet inequality with near-optimal bounds","_id":"12677","article_processing_charge":"No","language":[{"iso":"eng"}],"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant.","date_published":"2022-09-28T00:00:00Z","external_id":{"arxiv":["2209.14368"]},"main_file_link":[{"url":" https://doi.org/10.48550/arXiv.2209.14368","open_access":"1"}],"doi":"10.48550/ARXIV.2209.14368","publication":"arXiv","abstract":[{"lang":"eng","text":"In modern sample-driven Prophet Inequality, an adversary chooses a sequence of n items with values v1,v2,…,vn to be presented to a decision maker (DM). The process follows in two phases. In the first phase (sampling phase), some items, possibly selected at random, are revealed to the DM, but she can never accept them. In the second phase, the DM is presented with the other items in a random order and online fashion. For each item, she must make an irrevocable decision to either accept the item and stop the process or reject the item forever and proceed to the next item. The goal of the DM is to maximize the expected value as compared to a Prophet (or offline algorithm) that has access to all information. In this setting, the sampling phase has no cost and is not part of the optimization process. However, in many scenarios, the samples are obtained as part of the decision-making process.\r\nWe model this aspect as a two-phase Prophet Inequality where an adversary chooses a sequence of 2n items with values v1,v2,…,v2n and the items are randomly ordered. Finally, there are two phases of the Prophet Inequality problem with the first n-items and the rest of the items, respectively. We show that some basic algorithms achieve a ratio of at most 0.450. We present an algorithm that achieves a ratio of at least 0.495. Finally, we show that for every algorithm the ratio it can achieve is at most 0.502. Hence our algorithm is near-optimal."}],"corr_author":"1","date_updated":"2025-04-14T07:52:48Z","citation":{"ama":"Chatterjee K, Mohammadi M, Saona Urmeneta RJ. Repeated prophet inequality with near-optimal bounds. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/ARXIV.2209.14368\">10.48550/ARXIV.2209.14368</a>","mla":"Chatterjee, Krishnendu, et al. “Repeated Prophet Inequality with Near-Optimal Bounds.” <i>ArXiv</i>, 2209.14368, doi:<a href=\"https://doi.org/10.48550/ARXIV.2209.14368\">10.48550/ARXIV.2209.14368</a>.","ista":"Chatterjee K, Mohammadi M, Saona Urmeneta RJ. Repeated prophet inequality with near-optimal bounds. arXiv, 2209.14368.","ieee":"K. Chatterjee, M. Mohammadi, and R. J. Saona Urmeneta, “Repeated prophet inequality with near-optimal bounds,” <i>arXiv</i>. .","chicago":"Chatterjee, Krishnendu, Mona Mohammadi, and Raimundo J Saona Urmeneta. “Repeated Prophet Inequality with Near-Optimal Bounds.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/ARXIV.2209.14368\">https://doi.org/10.48550/ARXIV.2209.14368</a>.","short":"K. Chatterjee, M. Mohammadi, R.J. Saona Urmeneta, ArXiv (n.d.).","apa":"Chatterjee, K., Mohammadi, M., &#38; Saona Urmeneta, R. J. (n.d.). Repeated prophet inequality with near-optimal bounds. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/ARXIV.2209.14368\">https://doi.org/10.48550/ARXIV.2209.14368</a>"},"status":"public","publication_status":"submitted"},{"oa":1,"author":[{"orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","full_name":"Zikelic, Dorde"},{"full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"}],"related_material":{"record":[{"status":"public","id":"14830","relation":"later_version"},{"relation":"dissertation_contains","id":"14539","status":"public"}]},"month":"11","year":"2022","article_number":"2210.05308","day":"29","date_created":"2023-11-24T13:10:09Z","OA_place":"repository","external_id":{"arxiv":["2210.05308"]},"date_published":"2022-11-29T00:00:00Z","tmp":{"name":"Creative Commons Attribution-ShareAlike 4.0 International Public License (CC BY-SA 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-sa/4.0/legalcode","short":"CC BY-SA (4.0)","image":"/images/cc_by_sa.png"},"corr_author":"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."}],"citation":{"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>","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>ArXiv</i>, 2210.05308, doi:<a href=\"https://doi.org/10.48550/ARXIV.2210.05308\">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, 2210.05308.","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” <i>arXiv</i>. .","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>.","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, ArXiv (n.d.).","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>"},"publication":"arXiv","main_file_link":[{"url":"https://arxiv.org/abs/2210.05308","open_access":"1"}],"ec_funded":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"call_identifier":"H2020","grant_number":"665385","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Learning control policies for stochastic systems with reach-avoid guarantees","oa_version":"Preprint","type":"preprint","_id":"14600","language":[{"iso":"eng"}],"article_processing_charge":"No","date_updated":"2026-04-07T13:27:56Z","publication_status":"draft","status":"public","doi":"10.48550/ARXIV.2210.05308","license":"https://creativecommons.org/licenses/by-sa/4.0/"},{"author":[{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic"},{"first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"14539","status":"public"}]},"month":"05","oa":1,"article_number":"2205.11991","day":"24","year":"2022","date_created":"2023-11-24T13:22:30Z","external_id":{"arxiv":["2205.11991"]},"date_published":"2022-05-24T00:00:00Z","OA_place":"repository","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2205.11991"}],"publication":"arXiv","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."}],"corr_author":"1","citation":{"ista":"Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. arXiv, 2205.11991.","mla":"Zikelic, Dorde, et al. “Learning Stabilizing Policies in Stochastic Control Systems.” <i>ArXiv</i>, 2205.11991, doi:<a href=\"https://doi.org/10.48550/arXiv.2205.11991\">10.48550/arXiv.2205.11991</a>.","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>","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>.","short":"D. Zikelic, M. Lechner, K. Chatterjee, T.A. Henzinger, ArXiv (n.d.).","ieee":"D. Zikelic, M. Lechner, K. Chatterjee, and T. A. Henzinger, “Learning stabilizing policies in stochastic control systems,” <i>arXiv</i>. ."},"arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"type":"preprint","oa_version":"Preprint","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"Learning stabilizing policies in stochastic control systems","_id":"14601","article_processing_charge":"No","language":[{"iso":"eng"}],"doi":"10.48550/arXiv.2205.11991","date_updated":"2026-04-07T13:27:56Z","status":"public","publication_status":"draft"},{"oa":1,"related_material":{"link":[{"url":"https://github.com/alexmcavoy/fmtl/","relation":"software"}]},"author":[{"full_name":"McAvoy, Alex","last_name":"McAvoy","first_name":"Alex"},{"full_name":"Kates-Harbeck, Julian","last_name":"Kates-Harbeck","first_name":"Julian"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Hilbe","first_name":"Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian"}],"quality_controlled":"1","month":"09","volume":1,"year":"2022","day":"01","article_number":"pgac141","date_created":"2024-05-28T14:23:12Z","pmid":1,"publication_identifier":{"issn":["2752-6542"]},"file_date_updated":"2024-08-06T07:33:30Z","acknowledgement":"The authors are grateful to Jörg Oechssler for many helpful comments. A.M. was supported by a Simons Postdoctoral Fellowship (Math+X) at the University of Pennsylvania; K.C. was supported by the European Research Council Consolidator Grant 863818 (ForM-SMArt); and C.H. was supported by the European Research Council Starting Grant 850529 (E-DIRECT).","date_published":"2022-09-01T00:00:00Z","external_id":{"arxiv":["2105.06199"],"pmid":["36714856"]},"tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publisher":"Oxford University Press","has_accepted_license":"1","abstract":[{"text":"Across many domains of interaction, both natural and artificial, individuals use past experience to shape future behaviors. The results of such learning processes depend on what individuals wish to maximize. A natural objective is one’s own success. However, when two such “selfish” learners interact with each other, the outcome can be detrimental to both, especially when there are conflicts of interest. Here, we explore how a learner can align incentives with a selfish opponent. Moreover, we consider the dynamics that arise when learning rules themselves are subject to evolutionary pressure. By combining extensive simulations and analytical techniques, we demonstrate that selfish learning is unstable in most classical two-player repeated games. If evolution operates on the level of long-run payoffs, selection instead favors learning rules that incorporate social (other-regarding) preferences. To further corroborate these results, we analyze data from a repeated prisoner’s dilemma experiment. We find that selfish learning is insufficient to explain human behavior when there is a trade-off between payoff maximization and fairness.","lang":"eng"}],"citation":{"mla":"McAvoy, Alex, et al. “Evolutionary Instability of Selfish Learning in Repeated Games.” <i>PNAS Nexus</i>, vol. 1, no. 4, pgac141, Oxford University Press, 2022, doi:<a href=\"https://doi.org/10.1093/pnasnexus/pgac141\">10.1093/pnasnexus/pgac141</a>.","ama":"McAvoy A, Kates-Harbeck J, Chatterjee K, Hilbe C. Evolutionary instability of selfish learning in repeated games. <i>PNAS Nexus</i>. 2022;1(4). doi:<a href=\"https://doi.org/10.1093/pnasnexus/pgac141\">10.1093/pnasnexus/pgac141</a>","ista":"McAvoy A, Kates-Harbeck J, Chatterjee K, Hilbe C. 2022. Evolutionary instability of selfish learning in repeated games. PNAS Nexus. 1(4), pgac141.","ieee":"A. McAvoy, J. Kates-Harbeck, K. Chatterjee, and C. Hilbe, “Evolutionary instability of selfish learning in repeated games,” <i>PNAS Nexus</i>, vol. 1, no. 4. Oxford University Press, 2022.","apa":"McAvoy, A., Kates-Harbeck, J., Chatterjee, K., &#38; Hilbe, C. (2022). Evolutionary instability of selfish learning in repeated games. <i>PNAS Nexus</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/pnasnexus/pgac141\">https://doi.org/10.1093/pnasnexus/pgac141</a>","short":"A. McAvoy, J. Kates-Harbeck, K. Chatterjee, C. Hilbe, PNAS Nexus 1 (2022).","chicago":"McAvoy, Alex, Julian Kates-Harbeck, Krishnendu Chatterjee, and Christian Hilbe. “Evolutionary Instability of Selfish Learning in Repeated Games.” <i>PNAS Nexus</i>. Oxford University Press, 2022. <a href=\"https://doi.org/10.1093/pnasnexus/pgac141\">https://doi.org/10.1093/pnasnexus/pgac141</a>."},"publication":"PNAS Nexus","ec_funded":1,"project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"department":[{"_id":"KrCh"}],"title":"Evolutionary instability of selfish learning in repeated games","article_type":"original","oa_version":"Published Version","type":"journal_article","file":[{"creator":"dernst","file_id":"17400","relation":"main_file","file_size":2410962,"date_updated":"2024-08-06T07:33:30Z","access_level":"open_access","checksum":"79a8e3e4be7e8a2b407b4efddd65f3f3","file_name":"2022_PNASNexus_McAvoy.pdf","success":1,"date_created":"2024-08-06T07:33:30Z","content_type":"application/pdf"}],"_id":"17061","ddc":["000"],"article_processing_charge":"Yes","language":[{"iso":"eng"}],"date_updated":"2025-06-11T13:54:20Z","publication_status":"published","issue":"4","status":"public","doi":"10.1093/pnasnexus/pgac141","scopus_import":"1","intvolume":"         1"},{"title":"Index appearance record with preorders","department":[{"_id":"KrCh"}],"oa_version":"Published Version","type":"journal_article","keyword":["computer networks and communications","information systems","software"],"article_type":"original","project":[{"_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854","name":"IST Austria Open Access Fund"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","page":"585-618","publication_status":"published","status":"public","date_updated":"2025-04-15T06:53:08Z","intvolume":"        59","scopus_import":"1","doi":"10.1007/s00236-021-00412-y","language":[{"iso":"eng"}],"article_processing_charge":"Yes (via OA deal)","_id":"10602","file":[{"relation":"main_file","file_size":1066082,"creator":"cchlebak","file_id":"10603","success":1,"date_created":"2022-01-07T07:50:31Z","content_type":"application/pdf","date_updated":"2022-01-07T07:50:31Z","access_level":"open_access","checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","file_name":"2021_ActaInfor_Křetínský.pdf"}],"ddc":["000"],"volume":59,"date_created":"2022-01-06T12:37:27Z","year":"2022","day":"01","oa":1,"month":"10","author":[{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","first_name":"Jan","last_name":"Kretinsky"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"first_name":"Clara","last_name":"Waldmann","full_name":"Waldmann, Clara"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"}],"quality_controlled":"1","citation":{"mla":"Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>, vol. 59, Springer Nature, 2022, pp. 585–618, doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. <i>Acta Informatica</i>. 2022;59:585-618. doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618.","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” <i>Acta Informatica</i>, vol. 59. Springer Nature, pp. 585–618, 2022.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2022). Index appearance record with preorders. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>.","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618."},"corr_author":"1","abstract":[{"lang":"eng","text":"Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches."}],"publication":"Acta Informatica","publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"external_id":{"isi":["000735765500001"]},"date_published":"2022-10-01T00:00:00Z","file_date_updated":"2022-01-07T07:50:31Z","acknowledgement":"This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art.","has_accepted_license":"1","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"isi":1,"publisher":"Springer Nature"},{"title":"Infection dynamics of COVID-19 virus under lockdown and reopening","department":[{"_id":"KrCh"}],"oa_version":"Published Version","type":"journal_article","article_type":"original","project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"ec_funded":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","arxiv":1,"issue":"1","publication_status":"published","status":"public","date_updated":"2025-04-14T07:52:45Z","intvolume":"        12","doi":"10.1038/s41598-022-05333-5","scopus_import":"1","article_processing_charge":"No","language":[{"iso":"eng"}],"_id":"10731","file":[{"relation":"main_file","file_size":2971922,"file_id":"10744","creator":"alisjak","content_type":"application/pdf","date_created":"2022-02-07T14:57:59Z","success":1,"file_name":"2022_ScientificReports_Svoboda.pdf","checksum":"247afd30c173390940f099ead35a28ed","access_level":"open_access","date_updated":"2022-02-07T14:57:59Z"}],"ddc":["570"],"volume":12,"date_created":"2022-02-06T23:01:30Z","year":"2022","day":"27","article_number":"1526","oa":1,"month":"01","author":[{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","orcid":"0000-0002-1419-3267","last_name":"Svoboda","first_name":"Jakub"},{"full_name":"Tkadlec, Josef","last_name":"Tkadlec","first_name":"Josef"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Nowak, Martin A.","last_name":"Nowak","first_name":"Martin A."}],"quality_controlled":"1","citation":{"ieee":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Infection dynamics of COVID-19 virus under lockdown and reopening,” <i>Scientific Reports</i>, vol. 12, no. 1. Springer Nature, 2022.","apa":"Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening. <i>Scientific Reports</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41598-022-05333-5\">https://doi.org/10.1038/s41598-022-05333-5</a>","short":"J. Svoboda, J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Scientific Reports 12 (2022).","chicago":"Svoboda, Jakub, Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” <i>Scientific Reports</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1038/s41598-022-05333-5\">https://doi.org/10.1038/s41598-022-05333-5</a>.","mla":"Svoboda, Jakub, et al. “Infection Dynamics of COVID-19 Virus under Lockdown and Reopening.” <i>Scientific Reports</i>, vol. 12, no. 1, 1526, Springer Nature, 2022, doi:<a href=\"https://doi.org/10.1038/s41598-022-05333-5\">10.1038/s41598-022-05333-5</a>.","ama":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Infection dynamics of COVID-19 virus under lockdown and reopening. <i>Scientific Reports</i>. 2022;12(1). doi:<a href=\"https://doi.org/10.1038/s41598-022-05333-5\">10.1038/s41598-022-05333-5</a>","ista":"Svoboda J, Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2022. Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports. 12(1), 1526."},"abstract":[{"text":"Motivated by COVID-19, we develop and analyze a simple stochastic model for the spread of disease in human population. We track how the number of infected and critically ill people develops over time in order to estimate the demand that is imposed on the hospital system. To keep this demand under control, we consider a class of simple policies for slowing down and reopening society and we compare their efficiency in mitigating the spread of the virus from several different points of view. We find that in order to avoid overwhelming of the hospital system, a policy must impose a harsh lockdown or it must react swiftly (or both). While reacting swiftly is universally beneficial, being harsh pays off only when the country is patient about reopening and when the neighboring countries coordinate their mitigation efforts. Our work highlights the importance of acting decisively when closing down and the importance of patience and coordination between neighboring countries when reopening.","lang":"eng"}],"publication":"Scientific Reports","publication_identifier":{"eissn":["2045-2322"]},"file_date_updated":"2022-02-07T14:57:59Z","external_id":{"arxiv":["2012.15155"],"isi":["000749198000039"]},"date_published":"2022-01-27T00:00:00Z","acknowledgement":"K.C. acknowledges support from ERC Consolidator Grant No. (863818: ForM-SMart). A.P. acknowledges support from FWF Grant No. J-4220. M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.","has_accepted_license":"1","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"isi":1,"publisher":"Springer Nature"},{"abstract":[{"lang":"eng","text":"Partially observable Markov decision processes (POMDPs) are standard models for dynamic systems with probabilistic and nondeterministic behaviour in uncertain environments. We prove that in POMDPs with long-run average objective, the decision maker has approximately optimal strategies with finite memory. This implies notably that approximating the long-run value is recursively enumerable, as well as a weak continuity property of the value with respect to the transition function. "}],"citation":{"chicago":"Chatterjee, Krishnendu, Raimundo J Saona Urmeneta, and Bruno Ziliotto. “Finite-Memory Strategies in POMDPs with Long-Run Average Objectives.” <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences, 2022. <a href=\"https://doi.org/10.1287/moor.2020.1116\">https://doi.org/10.1287/moor.2020.1116</a>.","short":"K. Chatterjee, R.J. Saona Urmeneta, B. Ziliotto, Mathematics of Operations Research 47 (2022) 100–119.","apa":"Chatterjee, K., Saona Urmeneta, R. J., &#38; Ziliotto, B. (2022). Finite-memory strategies in POMDPs with long-run average objectives. <i>Mathematics of Operations Research</i>. Institute for Operations Research and the Management Sciences. <a href=\"https://doi.org/10.1287/moor.2020.1116\">https://doi.org/10.1287/moor.2020.1116</a>","ieee":"K. Chatterjee, R. J. Saona Urmeneta, and B. Ziliotto, “Finite-memory strategies in POMDPs with long-run average objectives,” <i>Mathematics of Operations Research</i>, vol. 47, no. 1. Institute for Operations Research and the Management Sciences, pp. 100–119, 2022.","ista":"Chatterjee K, Saona Urmeneta RJ, Ziliotto B. 2022. Finite-memory strategies in POMDPs with long-run average objectives. Mathematics of Operations Research. 47(1), 100–119.","ama":"Chatterjee K, Saona Urmeneta RJ, Ziliotto B. Finite-memory strategies in POMDPs with long-run average objectives. <i>Mathematics of Operations Research</i>. 2022;47(1):100-119. doi:<a href=\"https://doi.org/10.1287/moor.2020.1116\">10.1287/moor.2020.1116</a>","mla":"Chatterjee, Krishnendu, et al. “Finite-Memory Strategies in POMDPs with Long-Run Average Objectives.” <i>Mathematics of Operations Research</i>, vol. 47, no. 1, Institute for Operations Research and the Management Sciences, 2022, pp. 100–19, doi:<a href=\"https://doi.org/10.1287/moor.2020.1116\">10.1287/moor.2020.1116</a>."},"publication":"Mathematics of Operations Research","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1904.13360"}],"publication_identifier":{"issn":["0364-765X"],"eissn":["1526-5471"]},"date_published":"2022-02-01T00:00:00Z","external_id":{"arxiv":["1904.13360"],"isi":["000731918100001"]},"acknowledgement":"Partially supported by Austrian Science Fund (FWF) NFN Grant No RiSE/SHiNE S11407, by CONICYT Chile through grant PII 20150140, and by ECOS-CONICYT through grant C15E03.\r\n","isi":1,"publisher":"Institute for Operations Research and the Management Sciences","volume":47,"year":"2022","day":"01","date_created":"2021-04-08T09:33:31Z","oa":1,"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Saona Urmeneta, Raimundo J","last_name":"Saona Urmeneta","first_name":"Raimundo J","orcid":"0000-0001-5103-038X","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"last_name":"Ziliotto","first_name":"Bruno","full_name":"Ziliotto, Bruno"}],"related_material":{"record":[{"id":"20234","status":"public","relation":"dissertation_contains"}]},"quality_controlled":"1","month":"02","date_updated":"2026-04-07T12:31:21Z","publication_status":"published","issue":"1","status":"public","scopus_import":"1","doi":"10.1287/moor.2020.1116","intvolume":"        47","_id":"9311","article_processing_charge":"No","language":[{"iso":"eng"}],"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"title":"Finite-memory strategies in POMDPs with long-run average objectives","article_type":"original","keyword":["Management Science and Operations Research","General Mathematics","Computer Science Applications"],"oa_version":"Preprint","type":"journal_article","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"}],"page":"100-119","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","arxiv":1},{"article_processing_charge":"No","language":[{"iso":"eng"}],"file":[{"relation":"main_file","file_size":960036,"file_id":"14372","creator":"dernst","content_type":"application/pdf","date_created":"2023-09-26T10:43:15Z","success":1,"file_name":"2022_LIPIcS_Grover.pdf","checksum":"e282e43d3ae0ba6e067b72f4583e13c0","access_level":"open_access","date_updated":"2023-09-26T10:43:15Z"}],"_id":"12775","ddc":["000"],"intvolume":"       243","scopus_import":"1","doi":"10.4230/LIPIcs.CONCUR.2022.11","publication_status":"published","status":"public","date_updated":"2026-07-07T13:37:58Z","conference":{"location":"Warsaw, Poland","start_date":"2022-09-13","name":"CONCUR: Conference on Concurrency Theory","end_date":"2022-09-16"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"oa_version":"Published Version","type":"conference","title":"Anytime guarantees for reachability in uncountable Markov decision processes","department":[{"_id":"KrCh"}],"has_accepted_license":"1","das_tickbox":"1","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_identifier":{"issn":["1868-8969"]},"file_date_updated":"2023-09-26T10:43:15Z","acknowledgement":"Kush Grover: The author has been supported by the DFG research training group GRK\r\n2428 ConVeY.\r\nMaximilian Weininger: The author has been partially supported by DFG projects 383882557\r\nStatistical Unbounded Verification (SUV) and 427755713 Group-By Objectives in Probabilistic\r\nVerification (GOPro)","external_id":{"arxiv":["2008.04824"]},"date_published":"2022-09-15T00:00:00Z","publication":"33rd International Conference on Concurrency Theory","citation":{"ama":"Grover K, Kretinsky J, Meggendorfer T, Weininger M. Anytime guarantees for reachability in uncountable Markov decision processes. In: <i>33rd International Conference on Concurrency Theory</i>. Vol 243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2022.11\">10.4230/LIPIcs.CONCUR.2022.11</a>","mla":"Grover, Kush, et al. “Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.” <i>33rd International Conference on Concurrency Theory</i>, vol. 243, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2022.11\">10.4230/LIPIcs.CONCUR.2022.11</a>.","ista":"Grover K, Kretinsky J, Meggendorfer T, Weininger M. 2022. Anytime guarantees for reachability in uncountable Markov decision processes. 33rd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 243, 11.","ieee":"K. Grover, J. Kretinsky, T. Meggendorfer, and M. Weininger, “Anytime guarantees for reachability in uncountable Markov decision processes,” in <i>33rd International Conference on Concurrency Theory</i>, Warsaw, Poland, 2022, vol. 243.","short":"K. Grover, J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 33rd International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.","chicago":"Grover, Kush, Jan Kretinsky, Tobias Meggendorfer, and Maimilian Weininger. “Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.” In <i>33rd International Conference on Concurrency Theory</i>, Vol. 243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2022.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2022.11</a>.","apa":"Grover, K., Kretinsky, J., Meggendorfer, T., &#38; Weininger, M. (2022). Anytime guarantees for reachability in uncountable Markov decision processes. In <i>33rd International Conference on Concurrency Theory</i> (Vol. 243). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2022.11\">https://doi.org/10.4230/LIPIcs.CONCUR.2022.11</a>"},"corr_author":"1","abstract":[{"text":"We consider the problem of approximating the reachability probabilities in Markov decision processes (MDP) with uncountable (continuous) state and action spaces. While there are algorithms that, for special classes of such MDP, provide a sequence of approximations converging to the true value in the limit, our aim is to obtain an algorithm with guarantees on the precision of the approximation.\r\nAs this problem is undecidable in general, assumptions on the MDP are necessary. Our main contribution is to identify sufficient assumptions that are as weak as possible, thus approaching the \"boundary\" of which systems can be correctly and reliably analyzed. To this end, we also argue why each of our assumptions is necessary for algorithms based on processing finitely many observations.\r\nWe present two solution variants. The first one provides converging lower bounds under weaker assumptions than typical ones from previous works concerned with guarantees. The second one then utilizes stronger assumptions to additionally provide converging upper bounds. Altogether, we obtain an anytime algorithm, i.e. yielding a sequence of approximants with known and iteratively improving precision, converging to the true value in the limit. Besides, due to the generality of our assumptions, our algorithms are very general templates, readily allowing for various heuristics from literature in contrast to, e.g., a specific discretization algorithm. Our theoretical contribution thus paves the way for future practical improvements without sacrificing correctness guarantees.","lang":"eng"}],"month":"09","author":[{"full_name":"Grover, Kush","first_name":"Kush","last_name":"Grover"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan"},{"last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias"},{"first_name":"Maimilian","last_name":"Weininger","full_name":"Weininger, Maimilian"}],"quality_controlled":"1","oa":1,"date_created":"2023-03-28T08:09:32Z","alternative_title":["LIPIcs"],"year":"2022","article_number":"11","day":"15","volume":243},{"publication_identifier":{"issn":["1045-0823"],"isbn":["9780999241196"]},"acknowledgement":"This research was supported by the Czech Science Foundation (no. 19-24384Y), by the OP VVV MEYS funded project CZ.02.1.01/0.0/0.0/16 019/0000765 “Research Center for Informatics”, by the ERC CoG 863818 (ForM-SMArt), and by the Combat Capabilities Development Command Army Research Laboratory and was accomplished under Cooperative\r\nAgreement Number W911NF-13-2-0045 (ARL Cyber Security CRA). The views and conclusions contained in this document are those of the authors and should not be interpreted as\r\nrepresenting the official policies, either expressed or implied, of the Combat Capabilities Development Command Army Research Laboratory or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes not withstanding any copyright notation here on. ","date_published":"2021-09-01T00:00:00Z","publisher":"International Joint Conferences on Artificial Intelligence","citation":{"apa":"Tomášek, P., Horák, K., Aradhye, A., Bošanský, B., &#38; Chatterjee, K. (2021). Solving partially observable stochastic shortest-path games. In <i>30th International Joint Conference on Artificial Intelligence</i> (pp. 4182–4189). Virtual, Online: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2021/575\">https://doi.org/10.24963/ijcai.2021/575</a>","short":"P. Tomášek, K. Horák, A. Aradhye, B. Bošanský, K. Chatterjee, in:, 30th International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2021, pp. 4182–4189.","chicago":"Tomášek, Petr, Karel Horák, Aditya Aradhye, Branislav Bošanský, and Krishnendu Chatterjee. “Solving Partially Observable Stochastic Shortest-Path Games.” In <i>30th International Joint Conference on Artificial Intelligence</i>, 4182–89. International Joint Conferences on Artificial Intelligence, 2021. <a href=\"https://doi.org/10.24963/ijcai.2021/575\">https://doi.org/10.24963/ijcai.2021/575</a>.","ieee":"P. Tomášek, K. Horák, A. Aradhye, B. Bošanský, and K. Chatterjee, “Solving partially observable stochastic shortest-path games,” in <i>30th International Joint Conference on Artificial Intelligence</i>, Virtual, Online, 2021, pp. 4182–4189.","ista":"Tomášek P, Horák K, Aradhye A, Bošanský B, Chatterjee K. 2021. Solving partially observable stochastic shortest-path games. 30th International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conferences on Artificial Intelligence, 4182–4189.","mla":"Tomášek, Petr, et al. “Solving Partially Observable Stochastic Shortest-Path Games.” <i>30th International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2021, pp. 4182–89, doi:<a href=\"https://doi.org/10.24963/ijcai.2021/575\">10.24963/ijcai.2021/575</a>.","ama":"Tomášek P, Horák K, Aradhye A, Bošanský B, Chatterjee K. Solving partially observable stochastic shortest-path games. In: <i>30th International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2021:4182-4189. doi:<a href=\"https://doi.org/10.24963/ijcai.2021/575\">10.24963/ijcai.2021/575</a>"},"abstract":[{"text":"We study the two-player zero-sum extension of the partially observable stochastic shortest-path problem where one agent has only partial information about the environment. We formulate this problem as a partially observable stochastic game (POSG): given a set of target states and negative rewards for each transition, the player with imperfect information maximizes the expected undiscounted total reward until a target state is reached. The second player with the perfect information aims for the opposite. We base our formalism on POSGs with one-sided observability (OS-POSGs) and give the following contributions: (1) we introduce a novel heuristic search value iteration algorithm that iteratively solves depth-limited variants of the game, (2) we derive the bound on the depth guaranteeing an arbitrary precision, (3) we propose a novel upper-bound estimation that allows early terminations, and (4) we experimentally evaluate the algorithm on a pursuit-evasion game.","lang":"eng"}],"publication":"30th International Joint Conference on Artificial Intelligence","main_file_link":[{"open_access":"1","url":"https://doi.org/10.24963/ijcai.2021/575"}],"oa":1,"month":"09","author":[{"first_name":"Petr","last_name":"Tomášek","full_name":"Tomášek, Petr"},{"full_name":"Horák, Karel","first_name":"Karel","last_name":"Horák"},{"full_name":"Aradhye, Aditya","first_name":"Aditya","last_name":"Aradhye"},{"full_name":"Bošanský, Branislav","last_name":"Bošanský","first_name":"Branislav"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"}],"quality_controlled":"1","date_created":"2022-03-13T23:01:47Z","year":"2021","day":"01","language":[{"iso":"eng"}],"article_processing_charge":"No","_id":"10847","ddc":["000"],"publication_status":"published","status":"public","date_updated":"2026-06-18T10:41:02Z","conference":{"location":"Virtual, Online","start_date":"2021-08-19","end_date":"2021-08-27","name":"IJCAI: International Joint Conferences on Artificial Intelligence"},"doi":"10.24963/ijcai.2021/575","scopus_import":"1","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"4182-4189","title":"Solving partially observable stochastic shortest-path games","department":[{"_id":"KrCh"}],"oa_version":"Published Version","type":"conference"},{"citation":{"ista":"Bansal S, Chatterjee K, Vardi MY. 2021. On satisficing in quantitative games. 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 12651, 20–37.","mla":"Bansal, Suguman, et al. “On Satisficing in Quantitative Games.” <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 12651, Springer Nature, 2021, pp. 20–37, doi:<a href=\"https://doi.org/10.1007/978-3-030-72016-2_2\">10.1007/978-3-030-72016-2_2</a>.","ama":"Bansal S, Chatterjee K, Vardi MY. On satisficing in quantitative games. In: <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 12651. Springer Nature; 2021:20-37. doi:<a href=\"https://doi.org/10.1007/978-3-030-72016-2_2\">10.1007/978-3-030-72016-2_2</a>","apa":"Bansal, S., Chatterjee, K., &#38; Vardi, M. Y. (2021). On satisficing in quantitative games. In <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 12651, pp. 20–37). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-72016-2_2\">https://doi.org/10.1007/978-3-030-72016-2_2</a>","chicago":"Bansal, Suguman, Krishnendu Chatterjee, and Moshe Y. Vardi. “On Satisficing in Quantitative Games.” In <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 12651:20–37. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-72016-2_2\">https://doi.org/10.1007/978-3-030-72016-2_2</a>.","short":"S. Bansal, K. Chatterjee, M.Y. Vardi, in:, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2021, pp. 20–37.","ieee":"S. Bansal, K. Chatterjee, and M. Y. Vardi, “On satisficing in quantitative games,” in <i>27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2021, vol. 12651, pp. 20–37."},"abstract":[{"lang":"eng","text":"Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games. Optimization is one form of analysis. We argue that in many cases it may be better to replace the optimization problem with the satisficing problem, where instead of searching for optimal solutions, the goal is to search for solutions that adhere to a given threshold bound.\r\nThis work defines and investigates the satisficing problem on a two-player graph game with the discounted-sum cost model. We show that while the satisficing problem can be solved using numerical methods just like the optimization problem, this approach does not render compelling benefits over optimization. When the discount factor is, however, an integer, we present another approach to satisficing, which is purely based on automata methods. We show that this approach is algorithmically more performant – both theoretically and empirically – and demonstrates the broader applicability of satisficing over optimization."}],"publication":"27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","publication_identifier":{"isbn":["9783030720155"],"issn":["0302-9743"],"eissn":["1611-3349"]},"external_id":{"arxiv":["2101.02594"]},"acknowledgement":"We thank anonymous reviewers for valuable inputs. This work is supported in part by NSF grant 2030859 to the CRA for the CIFellows Project, NSF grants IIS-1527668, CCF-1704883, IIS-1830549, the ERC CoG 863818 (ForM-SMArt), and an award from the Maryland Procurement Office.","date_published":"2021-03-21T00:00:00Z","file_date_updated":"2023-03-28T11:00:33Z","has_accepted_license":"1","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publisher":"Springer Nature","volume":12651,"date_created":"2023-03-26T22:01:09Z","alternative_title":["LNCS"],"year":"2021","day":"21","oa":1,"month":"03","author":[{"first_name":"Suguman","last_name":"Bansal","full_name":"Bansal, Suguman"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Moshe Y.","last_name":"Vardi","full_name":"Vardi, Moshe Y."}],"quality_controlled":"1","publication_status":"published","status":"public","date_updated":"2025-07-10T13:18:02Z","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2021-04-01","start_date":"2021-03-27","location":"Luxembourg City, Luxembourg"},"intvolume":"     12651","doi":"10.1007/978-3-030-72016-2_2","scopus_import":"1","language":[{"iso":"eng"}],"article_processing_charge":"No","_id":"12767","file":[{"file_id":"12777","creator":"dernst","file_size":747418,"relation":"main_file","checksum":"b020b78b23587ce7610b1aafb4e63438","file_name":"2021_LNCS_Bansal.pdf","date_updated":"2023-03-28T11:00:33Z","access_level":"open_access","date_created":"2023-03-28T11:00:33Z","content_type":"application/pdf","success":1}],"ddc":["000"],"title":"On satisficing in quantitative games","department":[{"_id":"KrCh"}],"oa_version":"Published Version","type":"conference","project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"page":"20-37"}]