[{"language":[{"iso":"eng"}],"scopus_import":"1","issue":"4","publication":"PLoS Computational Biology","ec_funded":1,"publication_identifier":{"eissn":["1553-7358"],"issn":["1553-734X"]},"acknowledgement":"Authors would like to thank Christian Hilbe and Martin Nowak for their inspiring and very helpful feedback on the manuscript.","citation":{"ista":"Kleshnina M, Streipert SS, Filar JA, Chatterjee K. 2021. Mistakes can stabilise the dynamics of rock-paper-scissors games. PLoS Computational Biology. 17(4), e1008523.","ieee":"M. Kleshnina, S. S. Streipert, J. A. Filar, and K. Chatterjee, “Mistakes can stabilise the dynamics of rock-paper-scissors games,” <i>PLoS Computational Biology</i>, vol. 17, no. 4. Public Library of Science, 2021.","short":"M. Kleshnina, S.S. Streipert, J.A. Filar, K. Chatterjee, PLoS Computational Biology 17 (2021).","ama":"Kleshnina M, Streipert SS, Filar JA, Chatterjee K. Mistakes can stabilise the dynamics of rock-paper-scissors games. <i>PLoS Computational Biology</i>. 2021;17(4). doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1008523\">10.1371/journal.pcbi.1008523</a>","mla":"Kleshnina, Maria, et al. “Mistakes Can Stabilise the Dynamics of Rock-Paper-Scissors Games.” <i>PLoS Computational Biology</i>, vol. 17, no. 4, e1008523, Public Library of Science, 2021, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1008523\">10.1371/journal.pcbi.1008523</a>.","apa":"Kleshnina, M., Streipert, S. S., Filar, J. A., &#38; Chatterjee, K. (2021). Mistakes can stabilise the dynamics of rock-paper-scissors games. <i>PLoS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.1008523\">https://doi.org/10.1371/journal.pcbi.1008523</a>","chicago":"Kleshnina, Maria, Sabrina S. Streipert, Jerzy A. Filar, and Krishnendu Chatterjee. “Mistakes Can Stabilise the Dynamics of Rock-Paper-Scissors Games.” <i>PLoS Computational Biology</i>. Public Library of Science, 2021. <a href=\"https://doi.org/10.1371/journal.pcbi.1008523\">https://doi.org/10.1371/journal.pcbi.1008523</a>."},"project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"date_updated":"2025-06-12T06:40:39Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Kleshnina","first_name":"Maria","id":"4E21749C-F248-11E8-B48F-1D18A9856A87","full_name":"Kleshnina, Maria"},{"last_name":"Streipert","first_name":"Sabrina S.","full_name":"Streipert, Sabrina S."},{"full_name":"Filar, Jerzy A.","last_name":"Filar","first_name":"Jerzy A."},{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"status":"public","date_created":"2021-05-09T22:01:38Z","title":"Mistakes can stabilise the dynamics of rock-paper-scissors games","_id":"9381","abstract":[{"text":"A game of rock-paper-scissors is an interesting example of an interaction where none of the pure strategies strictly dominates all others, leading to a cyclic pattern. In this work, we consider an unstable version of rock-paper-scissors dynamics and allow individuals to make behavioural mistakes during the strategy execution. We show that such an assumption can break a cyclic relationship leading to a stable equilibrium emerging with only one strategy surviving. We consider two cases: completely random mistakes when individuals have no bias towards any strategy and a general form of mistakes. Then, we determine conditions for a strategy to dominate all other strategies. However, given that individuals who adopt a dominating strategy are still prone to behavioural mistakes in the observed behaviour, we may still observe extinct strategies. That is, behavioural mistakes in strategy execution stabilise evolutionary dynamics leading to an evolutionary stable and, potentially, mixed co-existence equilibrium.","lang":"eng"}],"oa_version":"Published Version","type":"journal_article","article_type":"original","isi":1,"article_number":"e1008523","doi":"10.1371/journal.pcbi.1008523","file":[{"access_level":"open_access","creator":"kschuh","relation":"main_file","success":1,"checksum":"a94ebe0c4116f5047eaa6029e54d2dac","date_created":"2021-05-11T13:50:06Z","date_updated":"2021-05-11T13:50:06Z","content_type":"application/pdf","file_name":"2021_pcbi_Kleshnina.pdf","file_size":1323820,"file_id":"9385"}],"volume":17,"oa":1,"day":"01","publisher":"Public Library of Science","department":[{"_id":"KrCh"}],"month":"04","external_id":{"pmid":["33844680"],"isi":["000639711200001"]},"article_processing_charge":"No","has_accepted_license":"1","date_published":"2021-04-01T00:00:00Z","file_date_updated":"2021-05-11T13:50:06Z","fulldoi":"https://doi.org/10.1371/journal.pcbi.1008523","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"intvolume":"        17","publication_status":"published","pmid":1,"year":"2021","quality_controlled":"1"},{"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"page":"401-428","citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>. Springer, 2021. <a href=\"https://doi.org/10.1007/s10703-021-00373-5\">https://doi.org/10.1007/s10703-021-00373-5</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 57, 401–428.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System Design 57 (2021) 401–428.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in bounded treewidth graphs,” <i>Formal Methods in System Design</i>, vol. 57. Springer, pp. 401–428, 2021.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>, vol. 57, Springer, 2021, pp. 401–28, doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>. 2021;57:401-428. doi:<a href=\"https://doi.org/10.1007/s10703-021-00373-5\">10.1007/s10703-021-00373-5</a>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-04-15T07:23:30Z","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas"}],"status":"public","date_created":"2021-05-16T22:01:47Z","_id":"9393","title":"Faster algorithms for quantitative verification in bounded treewidth graphs","abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"article_type":"original","oa_version":"Preprint","type":"journal_article","language":[{"iso":"eng"}],"scopus_import":"1","publication":"Formal Methods in System Design","ec_funded":1,"publication_identifier":{"issn":["0925-9856"],"eissn":["1572-8102"]},"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant (279307: Graph Games), and Microsoft faculty fellows award.","article_processing_charge":"No","date_published":"2021-09-01T00:00:00Z","arxiv":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.07384"}],"fulldoi":"https://doi.org/10.1007/s10703-021-00373-5","intvolume":"        57","year":"2021","quality_controlled":"1","publication_status":"published","isi":1,"doi":"10.1007/s10703-021-00373-5","volume":57,"oa":1,"day":"01","month":"09","department":[{"_id":"KrCh"}],"publisher":"Springer","external_id":{"arxiv":["1504.07384"],"isi":["000645490300001"]}},{"intvolume":"        29","abstract":[{"lang":"eng","text":"Optimal decision making requires individuals to know their available options and to anticipate correctly what consequences these options have. In many social interactions, however, we refrain from gathering all relevant information, even if this information would help us make better decisions and is costless to obtain. This chapter examines several examples of “deliberate ignorance.” Two simple models are proposed to illustrate how ignorance can evolve among self-interested and payoff - maximizing individuals, and open problems are highlighted that lie ahead for future research to explore."}],"type":"book_chapter","oa_version":"Published Version","quality_controlled":"1","year":"2021","ddc":["000"],"date_created":"2021-05-19T12:25:42Z","author":[{"orcid":"0000-0002-6978-7329","full_name":"Schmid, Laura","first_name":"Laura","last_name":"Schmid","id":"38B437DE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Hilbe, Christian","first_name":"Christian","last_name":"Hilbe"}],"status":"public","title":"The evolution of strategic ignorance in strategic interaction","editor":[{"full_name":"Hertwig, Ralph","last_name":"Hertwig","first_name":"Ralph"},{"first_name":"Christoph","last_name":"Engel","full_name":"Engel, Christoph"}],"_id":"9403","main_file_link":[{"url":"https://esforum.de/publications/PDFs/sfr29/SFR29_09_Hilbe%20and%20Schmid.pdf","open_access":"1"}],"date_updated":"2026-06-18T19:49:35Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"139-152","article_processing_charge":"No","citation":{"apa":"Schmid, L., &#38; Hilbe, C. (2021). The evolution of strategic ignorance in strategic interaction. In R. Hertwig &#38; C. Engel (Eds.), <i>Deliberate Ignorance: Choosing Not To Know</i> (Vol. 29, pp. 139–152). MIT Press.","chicago":"Schmid, Laura, and Christian Hilbe. “The Evolution of Strategic Ignorance in Strategic Interaction.” In <i>Deliberate Ignorance: Choosing Not To Know</i>, edited by Ralph Hertwig and Christoph Engel, 29:139–52. Strüngmann Forum Reports. MIT Press, 2021.","ieee":"L. Schmid and C. Hilbe, “The evolution of strategic ignorance in strategic interaction,” in <i>Deliberate Ignorance: Choosing Not To Know</i>, vol. 29, R. Hertwig and C. Engel, Eds. MIT Press, 2021, pp. 139–152.","ista":"Schmid L, Hilbe C. 2021.The evolution of strategic ignorance in strategic interaction. In: Deliberate Ignorance: Choosing Not To Know. vol. 29, 139–152.","short":"L. Schmid, C. Hilbe, in:, R. Hertwig, C. Engel (Eds.), Deliberate Ignorance: Choosing Not To Know, MIT Press, 2021, pp. 139–152.","mla":"Schmid, Laura, and Christian Hilbe. “The Evolution of Strategic Ignorance in Strategic Interaction.” <i>Deliberate Ignorance: Choosing Not To Know</i>, edited by Ralph Hertwig and Christoph Engel, vol. 29, MIT Press, 2021, pp. 139–52.","ama":"Schmid L, Hilbe C. The evolution of strategic ignorance in strategic interaction. In: Hertwig R, Engel C, eds. <i>Deliberate Ignorance: Choosing Not To Know</i>. Vol 29. Strüngmann Forum Reports. MIT Press; 2021:139-152."},"date_published":"2021-03-01T00:00:00Z","publisher":"MIT Press","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"month":"03","publication_identifier":{"isbn":["978-0-262-04559-9"]},"oa":1,"day":"01","publication":"Deliberate Ignorance: Choosing Not To Know","volume":29,"language":[{"iso":"eng"}],"series_title":"Strüngmann Forum Reports"},{"volume":12,"doi":"10.1038/s41467-021-24271-w","file":[{"success":1,"checksum":"5767418926a7f7fb76151de29473dae0","date_created":"2021-07-19T13:02:20Z","access_level":"open_access","creator":"cziletti","relation":"main_file","file_id":"9692","file_name":"2021_NatCoom_Tkadlec.pdf","date_updated":"2021-07-19T13:02:20Z","content_type":"application/pdf","file_size":628992}],"isi":1,"article_number":"4009","external_id":{"isi":["000671752100003"],"pmid":["34188036"]},"publisher":"Springer Nature","month":"06","department":[{"_id":"KrCh"}],"day":"29","oa":1,"fulldoi":"https://doi.org/10.1038/s41467-021-24271-w","has_accepted_license":"1","date_published":"2021-06-29T00:00:00Z","file_date_updated":"2021-07-19T13:02:20Z","article_processing_charge":"No","publication_status":"published","year":"2021","quality_controlled":"1","pmid":1,"intvolume":"        12","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["510"],"language":[{"iso":"eng"}],"ec_funded":1,"acknowledgement":"K.C. acknowledges support from ERC Start grant no. (279307: Graph Games), ERC Consolidator grant no. (863818: ForM-SMart), Austrian Science Fund (FWF) grant no. P23499-N23 and S11407-N23 (RiSE). M.A.N. acknowledges support from Office of Naval Research grant N00014-16-1-2914 and from the John Templeton Foundation.","publication_identifier":{"eissn":["2041-1723"]},"publication":"Nature Communications","scopus_import":"1","issue":"1","date_updated":"2026-04-02T14:04:10Z","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","citation":{"apa":"Tkadlec, J., Pavlogiannis, A., Chatterjee, K., &#38; Nowak, M. A. (2021). Fast and strong amplifiers of natural selection. <i>Nature Communications</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41467-021-24271-w\">https://doi.org/10.1038/s41467-021-24271-w</a>","chicago":"Tkadlec, Josef, Andreas Pavlogiannis, Krishnendu Chatterjee, and Martin A. Nowak. “Fast and Strong Amplifiers of Natural Selection.” <i>Nature Communications</i>. Springer Nature, 2021. <a href=\"https://doi.org/10.1038/s41467-021-24271-w\">https://doi.org/10.1038/s41467-021-24271-w</a>.","ieee":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, and M. A. Nowak, “Fast and strong amplifiers of natural selection,” <i>Nature Communications</i>, vol. 12, no. 1. Springer Nature, 2021.","ista":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. 2021. Fast and strong amplifiers of natural selection. Nature Communications. 12(1), 4009.","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Nature Communications 12 (2021).","mla":"Tkadlec, Josef, et al. “Fast and Strong Amplifiers of Natural Selection.” <i>Nature Communications</i>, vol. 12, no. 1, 4009, Springer Nature, 2021, doi:<a href=\"https://doi.org/10.1038/s41467-021-24271-w\">10.1038/s41467-021-24271-w</a>.","ama":"Tkadlec J, Pavlogiannis A, Chatterjee K, Nowak MA. Fast and strong amplifiers of natural selection. <i>Nature Communications</i>. 2021;12(1). doi:<a href=\"https://doi.org/10.1038/s41467-021-24271-w\">10.1038/s41467-021-24271-w</a>"},"project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"oa_version":"Published Version","type":"journal_article","article_type":"original","abstract":[{"text":"Selection and random drift determine the probability that novel mutations fixate in a population. Population structure is known to affect the dynamics of the evolutionary process. Amplifiers of selection are population structures that increase the fixation probability of beneficial mutants compared to well-mixed populations. Over the past 15 years, extensive research has produced remarkable structures called strong amplifiers which guarantee that every beneficial mutation fixates with high probability. But strong amplification has come at the cost of considerably delaying the fixation event, which can slow down the overall rate of evolution. However, the precise relationship between fixation probability and time has remained elusive. Here we characterize the slowdown effect of strong amplification. First, we prove that all strong amplifiers must delay the fixation event at least to some extent. Second, we construct strong amplifiers that delay the fixation event only marginally as compared to the well-mixed populations. Our results thus establish a tight relationship between fixation probability and time: Strong amplification always comes at a cost of a slowdown, but more than a marginal slowdown is not needed.","lang":"eng"}],"title":"Fast and strong amplifiers of natural selection","_id":"9640","status":"public","author":[{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","first_name":"Josef","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Nowak, Martin A.","last_name":"Nowak","first_name":"Martin A."}],"date_created":"2021-07-11T22:01:15Z"},{"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781450383912"]},"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This research was partially supported by the ERCCoG 863818 (ForM-SMArt) and the Czech Science Foundation grant No. GJ19-15134Y.","ec_funded":1,"scopus_import":"1","publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","date_updated":"2026-04-07T13:27:55Z","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. “Proving Non-Termination by Program Reversal.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 1033–48. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3453483.3454093\">https://doi.org/10.1145/3453483.3454093</a>.","apa":"Chatterjee, K., Goharshady, E. K., Novotný, P., &#38; Zikelic, D. (2021). Proving non-termination by program reversal. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 1033–1048). Online: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3453483.3454093\">https://doi.org/10.1145/3453483.3454093</a>","ama":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. Proving non-termination by program reversal. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:1033-1048. doi:<a href=\"https://doi.org/10.1145/3453483.3454093\">10.1145/3453483.3454093</a>","mla":"Chatterjee, Krishnendu, et al. “Proving Non-Termination by Program Reversal.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 1033–48, doi:<a href=\"https://doi.org/10.1145/3453483.3454093\">10.1145/3453483.3454093</a>.","ieee":"K. Chatterjee, E. K. Goharshady, P. Novotný, and D. Zikelic, “Proving non-termination by program reversal,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Online, 2021, pp. 1033–1048.","ista":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. Proving non-termination by program reversal. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1033–1048.","short":"K. Chatterjee, E.K. Goharshady, P. Novotný, D. Zikelic, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1033–1048."},"page":"1033-1048","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"related_material":{"record":[{"id":"15284","relation":"research_data","status":"public"},{"status":"public","relation":"dissertation_contains","id":"14539"}]},"abstract":[{"lang":"eng","text":"We present a new approach to proving non-termination of non-deterministic integer programs. Our technique is rather simple but efficient. It relies on a purely syntactic reversal of the program's transition system followed by a constraint-based invariant synthesis with constraints coming from both the original and the reversed transition system. The latter task is performed by a simple call to an off-the-shelf SMT-solver, which allows us to leverage the latest advances in SMT-solving. Moreover, our method offers a combination of features not present (as a whole) in previous approaches: it handles programs with non-determinism, provides relative completeness guarantees and supports programs with polynomial arithmetic. The experiments performed with our prototype tool RevTerm show that our approach, despite its simplicity and stronger theoretical guarantees, is at least on par with the state-of-the-art tools, often achieving a non-trivial improvement under a proper configuration of its parameters."}],"type":"conference","oa_version":"Preprint","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Ehsan Kafshdar","last_name":"Goharshady","full_name":"Goharshady, Ehsan Kafshdar"},{"full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotný"},{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic"}],"status":"public","date_created":"2021-07-11T22:01:17Z","title":"Proving non-termination by program reversal","_id":"9644","doi":"10.1145/3453483.3454093","isi":1,"publisher":"Association for Computing Machinery","department":[{"_id":"KrCh"}],"month":"06","external_id":{"arxiv":["2104.01189"],"isi":["000723661700067"]},"oa":1,"day":"01","main_file_link":[{"url":"https://arxiv.org/abs/2104.01189","open_access":"1"}],"arxiv":1,"fulldoi":"https://doi.org/10.1145/3453483.3454093","article_processing_charge":"No","conference":{"name":"PLDI: Programming Language Design and Implementation","start_date":"2021-06-20","end_date":"2021-06-26","location":"Online"},"date_published":"2021-06-01T00:00:00Z","publication_status":"published","quality_controlled":"1","year":"2021"},{"article_processing_charge":"No","conference":{"location":"Online","name":"PLDI: Programming Language Design and Implementation","end_date":"2021-06-26","start_date":"2021-06-20"},"date_published":"2021-06-01T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://hal.archives-ouvertes.fr/hal-03183862/"}],"fulldoi":"https://doi.org/10.1145/3453483.3454076","publication_status":"published","quality_controlled":"1","year":"2021","isi":1,"doi":"10.1145/3453483.3454076","oa":1,"day":"01","publisher":"Association for Computing Machinery","department":[{"_id":"KrCh"}],"month":"06","external_id":{"isi":["000723661700050"]},"page":"772-787","citation":{"apa":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A. K., &#38; Mahdavi, M. (2021). Polynomial reachability witnesses via Stellensätze. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 772–787). Online: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3453483.3454076\">https://doi.org/10.1145/3453483.3454076</a>","chicago":"Asadi, Ali, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. “Polynomial Reachability Witnesses via Stellensätze.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 772–87. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3453483.3454076\">https://doi.org/10.1145/3453483.3454076</a>.","ista":"Asadi A, Chatterjee K, Fu H, Goharshady AK, Mahdavi M. 2021. Polynomial reachability witnesses via Stellensätze. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 772–787.","short":"A. Asadi, K. Chatterjee, H. Fu, A.K. Goharshady, M. Mahdavi, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 772–787.","ieee":"A. Asadi, K. Chatterjee, H. Fu, A. K. Goharshady, and M. Mahdavi, “Polynomial reachability witnesses via Stellensätze,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Online, 2021, pp. 772–787.","mla":"Asadi, Ali, et al. “Polynomial Reachability Witnesses via Stellensätze.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 772–87, doi:<a href=\"https://doi.org/10.1145/3453483.3454076\">10.1145/3453483.3454076</a>.","ama":"Asadi A, Chatterjee K, Fu H, Goharshady AK, Mahdavi M. Polynomial reachability witnesses via Stellensätze. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:772-787. doi:<a href=\"https://doi.org/10.1145/3453483.3454076\">10.1145/3453483.3454076</a>"},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies"}],"date_updated":"2025-07-10T12:02:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2021-07-11T22:01:17Z","author":[{"full_name":"Asadi, Ali","first_name":"Ali","last_name":"Asadi"},{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Fu, Hongfei","first_name":"Hongfei","last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","last_name":"Goharshady"},{"full_name":"Mahdavi, Mohammad","first_name":"Mohammad","last_name":"Mahdavi"}],"status":"public","title":"Polynomial reachability witnesses via Stellensätze","_id":"9645","abstract":[{"lang":"eng","text":"We consider the fundamental problem of reachability analysis over imperative programs with real variables. Previous works that tackle reachability are either unable to handle programs consisting of general loops (e.g. symbolic execution), or lack completeness guarantees (e.g. abstract interpretation), or are not automated (e.g. incorrectness logic). In contrast, we propose a novel approach for reachability analysis that can handle general and complex loops, is complete, and can be entirely automated for a wide family of programs. Through the notion of Inductive Reachability Witnesses (IRWs), our approach extends ideas from both invariant generation and termination to reachability analysis.\r\n\r\nWe first show that our IRW-based approach is sound and complete for reachability analysis of imperative programs. Then, we focus on linear and polynomial programs and develop automated methods for synthesizing linear and polynomial IRWs. In the linear case, we follow the well-known approaches using Farkas' Lemma. Our main contribution is in the polynomial case, where we present a push-button semi-complete algorithm. We achieve this using a novel combination of classical theorems in real algebraic geometry, such as Putinar's Positivstellensatz and Hilbert's Strong Nullstellensatz. Finally, our experimental results show we can prove complex reachability objectives over various benchmarks that were beyond the reach of previous methods."}],"oa_version":"Submitted Version","type":"conference","language":[{"iso":"eng"}],"scopus_import":"1","publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the National Natural Science Foundation of China (NSFC) Grant No. 61802254, the Huawei Innovation Research Program, the Facebook PhD Fellowship Program, and DOC Fellowship No. 24956 of the Austrian Academy of Sciences (ÖAW).","publication_identifier":{"isbn":["9781450383912"]},"ec_funded":1},{"_id":"9646","title":"Quantitative analysis of assertion violations in probabilistic programs","author":[{"full_name":"Wang, Jinyi","last_name":"Wang","first_name":"Jinyi"},{"first_name":"Yican","last_name":"Sun","full_name":"Sun, Yican"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Goharshady","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar"}],"date_created":"2021-07-11T22:01:18Z","status":"public","type":"conference","oa_version":"Preprint","abstract":[{"lang":"eng","text":"We consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide automated algorithms that obtain both lower and upper bounds on the assertion violation probability. The main novelty of our approach is that we prove new and dedicated fixed-point theorems which serve as the theoretical basis of our algorithms and enable us to reason about assertion violation bounds in terms of pre and post fixed-point functions. To synthesize such fixed-points, we devise algorithms that utilize a wide range of mathematical tools, including repulsing ranking supermartingales, Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization. On the theoretical side, we provide (i) the first automated algorithm for lower-bounds on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds of exponential form in affine programs, and (iii) provably and significantly tighter upper-bounds than the previous approaches. On the practical side, we show our algorithms can handle a wide variety of programs from the literature and synthesize bounds that are remarkably tighter than previous results, in some cases by thousands of orders of magnitude."}],"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"}],"citation":{"chicago":"Wang, Jinyi, Yican Sun, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 1171–86. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3453483.3454102\">https://doi.org/10.1145/3453483.3454102</a>.","apa":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2021). Quantitative analysis of assertion violations in probabilistic programs. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 1171–1186). Online: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3453483.3454102\">https://doi.org/10.1145/3453483.3454102</a>","mla":"Wang, Jinyi, et al. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 1171–86, doi:<a href=\"https://doi.org/10.1145/3453483.3454102\">10.1145/3453483.3454102</a>.","ama":"Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. Quantitative analysis of assertion violations in probabilistic programs. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:1171-1186. doi:<a href=\"https://doi.org/10.1145/3453483.3454102\">10.1145/3453483.3454102</a>","ieee":"J. Wang, Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Quantitative analysis of assertion violations in probabilistic programs,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Online, 2021, pp. 1171–1186.","ista":"Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. 2021. Quantitative analysis of assertion violations in probabilistic programs. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1171–1186.","short":"J. Wang, Y. Sun, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1171–1186."},"page":"1171-1186","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","date_updated":"2025-04-15T07:55:05Z","publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","scopus_import":"1","acknowledgement":"We are very thankful to the anonymous reviewers for the helpful and valuable comments. The work was partially supported by the National Natural Science Foundation of China (NSFC) Grant No. 61802254, the Huawei Innovation Research Program, the ERC CoG 863818 (ForM-SMArt), the Facebook PhD Fellowship Program and DOC Fellowship #24956 of the Austrian Academy of Sciences (ÖAW).","ec_funded":1,"publication_identifier":{"isbn":["9781450383912"]},"language":[{"iso":"eng"}],"quality_controlled":"1","year":"2021","publication_status":"published","date_published":"2021-06-01T00:00:00Z","conference":{"name":"PLDI: Programming Language Design and Implementation","start_date":"2021-06-20","end_date":"2021-06-26","location":"Online"},"article_processing_charge":"No","fulldoi":"https://doi.org/10.1145/3453483.3454102","arxiv":1,"main_file_link":[{"url":"https://arxiv.org/abs/2011.14617","open_access":"1"}],"day":"01","oa":1,"external_id":{"isi":["000723661700076"],"arxiv":["2011.14617"]},"department":[{"_id":"KrCh"}],"month":"06","publisher":"Association for Computing Machinery","isi":1,"doi":"10.1145/3453483.3454102"},{"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"quality_controlled":"1","year":"2021","publication_status":"published","date_published":"2021-07-15T00:00:00Z","alternative_title":["LNCS"],"file_date_updated":"2022-05-13T07:00:20Z","conference":{"end_date":"2021-07-23","start_date":"2021-07-20","name":"CAV: Computer Aided Verification ","location":"Virtual"},"has_accepted_license":"1","article_processing_charge":"Yes","fulldoi":"https://doi.org/10.1007/978-3-030-81685-8_16","arxiv":1,"day":"15","oa":1,"corr_author":"1","external_id":{"isi":["000698732400016"],"arxiv":["2105.06424"]},"month":"07","department":[{"_id":"KrCh"}],"publisher":"Springer Nature","isi":1,"volume":"12759 ","file":[{"file_id":"11368","file_size":1516756,"content_type":"application/pdf","date_updated":"2022-05-13T07:00:20Z","file_name":"2021_LNCS_Agarwal.pdf","date_created":"2022-05-13T07:00:20Z","checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","success":1,"creator":"dernst","relation":"main_file","access_level":"open_access"}],"doi":"10.1007/978-3-030-81685-8_16","_id":"9987","title":"Stateless model checking under a reads-value-from equivalence","date_created":"2021-09-05T22:01:24Z","author":[{"full_name":"Agarwal, Pratyush","first_name":"Pratyush","last_name":"Agarwal"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Shreya","last_name":"Pathak","full_name":"Pathak, Shreya"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"first_name":"Viktor","last_name":"Toman","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor"}],"status":"public","type":"conference","oa_version":"Published Version","abstract":[{"text":"Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present   RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover,   RVF-SMC  generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.","lang":"eng"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"10199","status":"public"}]},"project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"page":"341-366","citation":{"mla":"Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” <i>33rd International Conference on Computer-Aided Verification </i>, vol. 12759, Springer Nature, 2021, pp. 341–66, doi:<a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">10.1007/978-3-030-81685-8_16</a>.","ama":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. Stateless model checking under a reads-value-from equivalence. In: <i>33rd International Conference on Computer-Aided Verification </i>. Vol 12759. Springer Nature; 2021:341-366. doi:<a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">10.1007/978-3-030-81685-8_16</a>","ista":"Agarwal P, Chatterjee K, Pathak S, Pavlogiannis A, Toman V. 2021. Stateless model checking under a reads-value-from equivalence. 33rd International Conference on Computer-Aided Verification . CAV: Computer Aided Verification , LNCS, vol. 12759, 341–366.","ieee":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in <i>33rd International Conference on Computer-Aided Verification </i>, Virtual, 2021, vol. 12759, pp. 341–366.","short":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, V. Toman, in:, 33rd International Conference on Computer-Aided Verification , Springer Nature, 2021, pp. 341–366.","chicago":"Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In <i>33rd International Conference on Computer-Aided Verification </i>, 12759:341–66. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">https://doi.org/10.1007/978-3-030-81685-8_16</a>.","apa":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., &#38; Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In <i>33rd International Conference on Computer-Aided Verification </i> (Vol. 12759, pp. 341–366). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-81685-8_16\">https://doi.org/10.1007/978-3-030-81685-8_16</a>"},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","date_updated":"2026-04-08T07:00:30Z","publication":"33rd International Conference on Computer-Aided Verification ","scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["978-3-030-81684-1"],"eisbn":["978-3-030-81685-8"],"eissn":["1611-3349"]},"ec_funded":1,"acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) through project ICT15-003.","language":[{"iso":"eng"}]},{"project":[{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","call_identifier":"H2020"},{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"citation":{"mla":"Lechner, Mathias, et al. “Infinite Time Horizon Safety of Bayesian Neural Networks.” <i>35th Conference on Neural Information Processing Systems</i>, Neural Information Processing Systems Foundation, 2021, doi:<a href=\"https://doi.org/10.48550/arXiv.2111.03165\">10.48550/arXiv.2111.03165</a>.","ama":"Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. Infinite time horizon safety of Bayesian neural networks. In: <i>35th Conference on Neural Information Processing Systems</i>. Neural Information Processing Systems Foundation; 2021. doi:<a href=\"https://doi.org/10.48550/arXiv.2111.03165\">10.48550/arXiv.2111.03165</a>","ista":"Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. 2021. Infinite time horizon safety of Bayesian neural networks. 35th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems,  Advances in Neural Information Processing Systems, .","short":"M. Lechner, Ð. Žikelić, K. Chatterjee, T.A. Henzinger, in:, 35th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2021.","ieee":"M. Lechner, Ð. Žikelić, K. Chatterjee, and T. A. Henzinger, “Infinite time horizon safety of Bayesian neural networks,” in <i>35th Conference on Neural Information Processing Systems</i>, Virtual, 2021.","chicago":"Lechner, Mathias, Ðorđe Žikelić, Krishnendu Chatterjee, and Thomas A Henzinger. “Infinite Time Horizon Safety of Bayesian Neural Networks.” In <i>35th Conference on Neural Information Processing Systems</i>. Neural Information Processing Systems Foundation, 2021. <a href=\"https://doi.org/10.48550/arXiv.2111.03165\">https://doi.org/10.48550/arXiv.2111.03165</a>.","apa":"Lechner, M., Žikelić, Ð., Chatterjee, K., &#38; Henzinger, T. A. (2021). Infinite time horizon safety of Bayesian neural networks. In <i>35th Conference on Neural Information Processing Systems</i>. Virtual: Neural Information Processing Systems Foundation. <a href=\"https://doi.org/10.48550/arXiv.2111.03165\">https://doi.org/10.48550/arXiv.2111.03165</a>"},"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"11362"}]},"license":"https://creativecommons.org/licenses/by-nc-nd/3.0/","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-07-07T06:49:10Z","author":[{"first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"first_name":"Ðorđe","last_name":"Žikelić","full_name":"Žikelić, Ðorđe"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2022-01-25T15:45:58Z","status":"public","_id":"10667","title":"Infinite time horizon safety of Bayesian neural networks","abstract":[{"text":"Bayesian neural networks (BNNs) place distributions over the weights of a neural network to model uncertainty in the data and the network's prediction. We consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with infinite time horizon systems. Compared to the existing sampling-based approaches, which are inapplicable to the infinite time horizon setting, we train a separate deterministic neural network that serves as an infinite time horizon safety certificate. In particular, we show that the certificate network guarantees the safety of the system over a subset of the BNN weight posterior's support. Our method first computes a safe weight set and then alters the BNN's weight posterior to reject samples outside this set. Moreover, we show how to extend our approach to a safe-exploration reinforcement learning setting, in order to avoid unsafe trajectories during the training of the policy. We evaluate our approach on a series of reinforcement learning benchmarks, including non-Lyapunovian safety specifications.","lang":"eng"}],"oa_version":"Published Version","type":"conference","language":[{"iso":"eng"}],"publication":"35th Conference on Neural Information Processing Systems","publication_identifier":{"issn":["1049-5258"]},"ec_funded":1,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","article_processing_charge":"No","alternative_title":[" Advances in Neural Information Processing Systems"],"file_date_updated":"2022-01-26T07:39:59Z","date_published":"2021-12-01T00:00:00Z","conference":{"start_date":"2021-12-06","end_date":"2021-12-10","name":"NeurIPS: Neural Information Processing Systems","location":"Virtual"},"has_accepted_license":"1","arxiv":1,"main_file_link":[{"open_access":"1","url":"https://proceedings.neurips.cc/paper/2021/hash/544defa9fddff50c53b71c43e0da72be-Abstract.html"}],"fulldoi":"https://doi.org/10.48550/arXiv.2111.03165","das_tickbox":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","short":"CC BY-NC-ND (3.0)","image":"/images/cc_by_nc_nd.png"},"ddc":["000"],"quality_controlled":"1","year":"2021","publication_status":"published","file":[{"file_size":452492,"file_name":"infinite_time_horizon_safety_o.pdf","date_updated":"2022-01-26T07:39:59Z","content_type":"application/pdf","file_id":"10682","relation":"main_file","creator":"mlechner","access_level":"open_access","checksum":"0fc0f852525c10dda9cc9ffea07fb4e4","date_created":"2022-01-26T07:39:59Z","success":1}],"doi":"10.48550/arXiv.2111.03165","corr_author":"1","oa":1,"day":"01","department":[{"_id":"GradSch"},{"_id":"ToHe"},{"_id":"KrCh"}],"month":"12","publisher":"Neural Information Processing Systems Foundation","external_id":{"arxiv":["2111.03165"]}},{"date_published":"2021-03-16T00:00:00Z","article_processing_charge":"No","fulldoi":"https://doi.org/10.1016/j.artint.2021.103499","arxiv":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.07031"}],"quality_controlled":"1","year":"2021","publication_status":"published","intvolume":"       297","article_number":"103499","isi":1,"volume":297,"doi":"10.1016/j.artint.2021.103499","day":"16","oa":1,"corr_author":"1","external_id":{"isi":["000657537500003"],"arxiv":["1804.07031"]},"department":[{"_id":"KrCh"}],"month":"03","publisher":"Elsevier","related_material":{"record":[{"id":"35","relation":"earlier_version","status":"public"}]},"citation":{"ista":"Chatterjee K, Dvořák W, Henzinger M, Svozil A. 2021. Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. 297(8), 103499.","ieee":"K. Chatterjee, W. Dvořák, M. Henzinger, and A. Svozil, “Algorithms and conditional lower bounds for planning problems,” <i>Artificial Intelligence</i>, vol. 297, no. 8. Elsevier, 2021.","short":"K. Chatterjee, W. Dvořák, M. Henzinger, A. Svozil, Artificial Intelligence 297 (2021).","ama":"Chatterjee K, Dvořák W, Henzinger M, Svozil A. Algorithms and conditional lower bounds for planning problems. <i>Artificial Intelligence</i>. 2021;297(8). doi:<a href=\"https://doi.org/10.1016/j.artint.2021.103499\">10.1016/j.artint.2021.103499</a>","mla":"Chatterjee, Krishnendu, et al. “Algorithms and Conditional Lower Bounds for Planning Problems.” <i>Artificial Intelligence</i>, vol. 297, no. 8, 103499, Elsevier, 2021, doi:<a href=\"https://doi.org/10.1016/j.artint.2021.103499\">10.1016/j.artint.2021.103499</a>.","apa":"Chatterjee, K., Dvořák, W., Henzinger, M., &#38; Svozil, A. (2021). Algorithms and conditional lower bounds for planning problems. <i>Artificial Intelligence</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.artint.2021.103499\">https://doi.org/10.1016/j.artint.2021.103499</a>","chicago":"Chatterjee, Krishnendu, Wolfgang Dvořák, Monika Henzinger, and Alexander Svozil. “Algorithms and Conditional Lower Bounds for Planning Problems.” <i>Artificial Intelligence</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.artint.2021.103499\">https://doi.org/10.1016/j.artint.2021.103499</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-07-07T13:36:04Z","_id":"9293","title":"Algorithms and conditional lower bounds for planning problems","date_created":"2021-03-28T22:01:40Z","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Dvořák, Wolfgang","first_name":"Wolfgang","last_name":"Dvořák"},{"full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"Svozil","first_name":"Alexander","full_name":"Svozil, Alexander"}],"status":"public","article_type":"original","oa_version":"Preprint","type":"journal_article","abstract":[{"text":"We consider planning problems for graphs, Markov Decision Processes (MDPs), and games on graphs in an explicit state space. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems with k different target sets: (a) the coverage problem asks whether there is a plan for each individual target set; and (b) the sequential target reachability problem asks whether the targets can be reached in a given sequence. For the coverage problem, we present a linear-time algorithm for graphs, and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds, based on the boolean matrix multiplication (BMM) conjecture and strong exponential time hypothesis (SETH), establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs, and for the sequential reachability problem games on graphs are harder than MDPs and graphs; and (ii) problem-separation results showing that for MDPs the coverage problem is harder than the sequential target problem.","lang":"eng"}],"language":[{"iso":"eng"}],"publication":"Artificial Intelligence","issue":"8","scopus_import":"1","publication_identifier":{"issn":["0004-3702"]}},{"publication_status":"published","year":"2021","quality_controlled":"1","fulldoi":"https://doi.org/10.1109/LICS52264.2021.9470739","main_file_link":[{"url":"https://arxiv.org/abs/2104.07466","open_access":"1"}],"arxiv":1,"conference":{"start_date":"2021-06-29","end_date":"2021-07-02","name":"LICS: Logic in Computer Science","location":"Rome, Italy"},"date_published":"2021-07-07T00:00:00Z","article_processing_charge":"No","keyword":["Computer science","Computational modeling","Markov processes","Probabilistic logic","Formal verification","Game Theory"],"external_id":{"isi":["000947350400089"],"arxiv":["2104.07466"]},"publisher":"IEEE","month":"07","department":[{"_id":"KrCh"}],"day":"07","oa":1,"doi":"10.1109/LICS52264.2021.9470739","isi":1,"oa_version":"Preprint","type":"conference","abstract":[{"text":"We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with  n  vertices and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of  ω -regular objectives for MDPs. We consider the canonical parity objectives for  ω -regular objectives, and for parity objectives with  d -priorities we present an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 .","lang":"eng"}],"title":"Symbolic time and space tradeoffs for probabilistic verification","_id":"10002","date_created":"2021-09-12T22:01:24Z","status":"public","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Dvorak","first_name":"Wolfgang","full_name":"Dvorak, Wolfgang"},{"orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","last_name":"Henzinger","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Svozil, Alexander","last_name":"Svozil","first_name":"Alexander"}],"date_updated":"2026-08-12T06:39:42Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"short":"K. Chatterjee, W. Dvorak, M. Henzinger, A. Svozil, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2021, pp. 1–13.","ista":"Chatterjee K, Dvorak W, Henzinger M, Svozil A. 2021. Symbolic time and space tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 1–13.","ieee":"K. Chatterjee, W. Dvorak, M. Henzinger, and A. Svozil, “Symbolic time and space tradeoffs for probabilistic verification,” in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021, pp. 1–13.","mla":"Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2021, pp. 1–13, doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>.","ama":"Chatterjee K, Dvorak W, Henzinger M, Svozil A. Symbolic time and space tradeoffs for probabilistic verification. In: <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2021:1-13. doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>","apa":"Chatterjee, K., Dvorak, W., Henzinger, M., &#38; Svozil, A. (2021). Symbolic time and space tradeoffs for probabilistic verification. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13). Rome, Italy: IEEE. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorak, Monika Henzinger, and Alexander Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 1–13. IEEE, 2021. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>."},"page":"1-13","project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"publication_identifier":{"issn":["1043-6871"],"eisbn":["978-1-6654-4895-6"],"isbn":["978-1-6654-4896-3"]},"ec_funded":1,"acknowledgement":"The authors are grateful to the anonymous referees for their valuable comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For M. H. the research leading to these results has received funding from the European Research Council under the European Unions Seventh Framework Programme (FP/2007–2013) / ERC Grant Agreement no. 340506.","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","scopus_import":"1","language":[{"iso":"eng"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-10-16T07:57:38Z","project":[{"grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"citation":{"apa":"Chatterjee, K., &#38; Doyen, L. (2021). Stochastic processes with expected stopping time. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13). Rome, Italy: IEEE. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470595\">https://doi.org/10.1109/LICS52264.2021.9470595</a>","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 1–13. IEEE, 2021. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470595\">https://doi.org/10.1109/LICS52264.2021.9470595</a>.","ieee":"K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,” in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021, pp. 1–13.","ista":"Chatterjee K, Doyen L. 2021. Stochastic processes with expected stopping time. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 1–13.","short":"K. Chatterjee, L. Doyen, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2021, pp. 1–13.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2021, pp. 1–13, doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470595\">10.1109/LICS52264.2021.9470595</a>.","ama":"Chatterjee K, Doyen L. Stochastic processes with expected stopping time. In: <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2021:1-13. doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470595\">10.1109/LICS52264.2021.9470595</a>"},"page":"1-13","related_material":{"record":[{"status":"public","relation":"later_version","id":"18630"}]},"abstract":[{"lang":"eng","text":"Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs."}],"oa_version":"Preprint","type":"conference","date_created":"2021-09-12T22:01:25Z","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"}],"status":"public","_id":"10004","title":"Stochastic processes with expected stopping time","language":[{"iso":"eng"}],"acknowledgement":"We are grateful to the anonymous reviewers of LICS 2021 and of a previous version of this paper for insightful comments that helped improving the presentation. This research was partially supported by the grant ERC CoG 863818 (ForM-SMArt).","publication_identifier":{"eisbn":["978-1-6654-4895-6"],"isbn":["978-1-6654-4896-3"],"issn":["1043-6871"]},"ec_funded":1,"scopus_import":"1","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","arxiv":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2104.07278"}],"fulldoi":"https://doi.org/10.1109/LICS52264.2021.9470595","keyword":["Computer science","Heuristic algorithms","Memory management","Automata","Markov processes","Probability distribution","Complexity theory"],"article_processing_charge":"No","date_published":"2021-07-07T00:00:00Z","conference":{"name":"LICS: Logic in Computer Science","end_date":"2021-07-02","start_date":"2021-06-29","location":"Rome, Italy"},"year":"2021","quality_controlled":"1","publication_status":"published","doi":"10.1109/LICS52264.2021.9470595","isi":1,"department":[{"_id":"KrCh"}],"month":"07","publisher":"IEEE","external_id":{"arxiv":["2104.07278"],"isi":["000947350400036"]},"oa":1,"day":"07"},{"doi":"10.15479/at:ista:10293","file":[{"embargo_to":"open_access","file_id":"10305","content_type":"application/zip","date_updated":"2022-12-20T23:30:08Z","file_name":"submission_new.zip","file_size":29703124,"date_created":"2021-11-18T12:41:46Z","checksum":"86a05b430756ca12ae8107b6e6f3c1e5","access_level":"closed","relation":"source_file","creator":"lschmid"},{"access_level":"open_access","creator":"lschmid","relation":"main_file","checksum":"d940af042e94660c6b6a7b4f0b184d47","date_created":"2021-11-18T12:59:15Z","file_name":"thesis_new_upload.pdf","date_updated":"2022-12-20T23:30:08Z","embargo":"2022-10-18","content_type":"application/pdf","file_size":8320985,"file_id":"10306"}],"publisher":"Institute of Science and Technology Austria","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"month":"11","oa":1,"corr_author":"1","day":"17","degree_awarded":"PhD","fulldoi":"https://doi.org/10.15479/at:ista:10293","article_processing_charge":"No","has_accepted_license":"1","alternative_title":["ISTA Thesis"],"date_published":"2021-11-17T00:00:00Z","file_date_updated":"2022-12-20T23:30:08Z","publication_status":"published","year":"2021","ddc":["519","576"],"language":[{"iso":"eng"}],"OA_place":"publisher","ec_funded":1,"publication_identifier":{"issn":["2663-337X"]},"date_updated":"2026-04-08T07:11:20Z","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","citation":{"mla":"Schmid, Laura. <i>Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information</i>. Institute of Science and Technology Austria, 2021, doi:<a href=\"https://doi.org/10.15479/at:ista:10293\">10.15479/at:ista:10293</a>.","ama":"Schmid L. Evolution of cooperation via (in)direct reciprocity under imperfect information. 2021. doi:<a href=\"https://doi.org/10.15479/at:ista:10293\">10.15479/at:ista:10293</a>","ista":"Schmid L. 2021. Evolution of cooperation via (in)direct reciprocity under imperfect information. Institute of Science and Technology Austria.","ieee":"L. Schmid, “Evolution of cooperation via (in)direct reciprocity under imperfect information,” Institute of Science and Technology Austria, 2021.","short":"L. Schmid, Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information, Institute of Science and Technology Austria, 2021.","chicago":"Schmid, Laura. “Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information.” Institute of Science and Technology Austria, 2021. <a href=\"https://doi.org/10.15479/at:ista:10293\">https://doi.org/10.15479/at:ista:10293</a>.","apa":"Schmid, L. (2021). <i>Evolution of cooperation via (in)direct reciprocity under imperfect information</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:10293\">https://doi.org/10.15479/at:ista:10293</a>"},"page":"171","project":[{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"id":"9997","relation":"part_of_dissertation","status":"public"},{"relation":"part_of_dissertation","id":"9402","status":"public"},{"relation":"part_of_dissertation","id":"2","status":"public"}]},"abstract":[{"text":"Indirect reciprocity in evolutionary game theory is a prominent mechanism for explaining the evolution of cooperation among unrelated individuals. In contrast to direct reciprocity, which is based on individuals meeting repeatedly, and conditionally cooperating by using their own experiences, indirect reciprocity is based on individuals’ reputations. If a player helps another, this increases the helper’s public standing, benefitting them in the future. This lets cooperation in the population emerge without individuals having to meet more than once. While the two modes of reciprocity are intertwined, they are difficult to compare. Thus, they are usually studied in isolation. Direct reciprocity can maintain cooperation with simple strategies, and is robust against noise even when players do not remember more\r\nthan their partner’s last action. Meanwhile, indirect reciprocity requires its successful strategies, or social norms, to be more complex. Exhaustive search previously identified eight such norms, called the “leading eight”, which excel at maintaining cooperation. However, as the first result of this thesis, we show that the leading eight break down once we remove the fundamental assumption that information is synchronized and public, such that everyone agrees on reputations. Once we consider a more realistic scenario of imperfect information, where reputations are private, and individuals occasionally misinterpret or miss observations, the leading eight do not promote cooperation anymore. Instead, minor initial disagreements can proliferate, fragmenting populations into subgroups. In a next step, we consider ways to mitigate this issue. We first explore whether introducing “generosity” can stabilize cooperation when players use the leading eight strategies in noisy environments. This approach of modifying strategies to include probabilistic elements for coping with errors is known to work well in direct reciprocity. However, as we show here, it fails for the more complex norms of indirect reciprocity. Imperfect information still prevents cooperation from evolving. On the other hand, we succeeded to show in this thesis that modifying the leading eight to use “quantitative assessment”, i.e. tracking reputation scores on a scale beyond good and bad, and making overall judgments of others based on a threshold, is highly successful, even when noise increases in the environment. Cooperation can flourish when reputations\r\nare more nuanced, and players have a broader understanding what it means to be “good.” Finally, we present a single theoretical framework that unites the two modes of reciprocity despite their differences. Within this framework, we identify a novel simple and successful strategy for indirect reciprocity, which can cope with noisy environments and has an analogue in direct reciprocity. We can also analyze decision making when different sources of information are available. Our results help highlight that for sustaining cooperation, already the most simple rules of reciprocity can be sufficient.","lang":"eng"}],"supervisor":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"}],"type":"dissertation","oa_version":"Published Version","date_created":"2021-11-15T17:12:57Z","status":"public","author":[{"full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329","first_name":"Laura","last_name":"Schmid","id":"38B437DE-F248-11E8-B48F-1D18A9856A87"}],"title":"Evolution of cooperation via (in)direct reciprocity under imperfect information","_id":"10293"},{"abstract":[{"text":"Indirect reciprocity is a mechanism for the evolution of cooperation based on social norms. This mechanism requires that individuals in a population observe and judge each other’s behaviors. Individuals with a good reputation are more likely to receive help from others. Previous work suggests that indirect reciprocity is only effective when all relevant information is reliable and publicly available. Otherwise, individuals may disagree on how to assess others, even if they all apply the same social norm. Such disagreements can lead to a breakdown of cooperation. Here we explore whether the predominantly studied ‘leading eight’ social norms of indirect reciprocity can be made more robust by equipping them with an element of generosity. To this end, we distinguish between two kinds of generosity. According to assessment generosity, individuals occasionally assign a good reputation to group members who would usually be regarded as bad. According to action generosity, individuals occasionally cooperate with group members with whom they would usually defect. Using individual-based simulations, we show that the two kinds of generosity have a very different effect on the resulting reputation dynamics. Assessment generosity tends to add to the overall noise and allows defectors to invade. In contrast, a limited amount of action generosity can be beneficial in a few cases. However, even when action generosity is beneficial, the respective simulations do not result in full cooperation. Our results suggest that while generosity can favor cooperation when individuals use the most simple strategies of reciprocity, it is disadvantageous when individuals use more complex social norms.","lang":"eng"}],"type":"journal_article","oa_version":"Published Version","article_type":"original","status":"public","author":[{"full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","last_name":"Schmid","first_name":"Laura"},{"first_name":"Pouya","last_name":"Shati","full_name":"Shati, Pouya"},{"full_name":"Hilbe, Christian","first_name":"Christian","last_name":"Hilbe"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"date_created":"2021-09-11T16:22:02Z","title":"The evolution of indirect reciprocity under action and assessment generosity","_id":"9997","date_updated":"2026-10-22T22:30:45Z","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"apa":"Schmid, L., Shati, P., Hilbe, C., &#38; Chatterjee, K. (2021). The evolution of indirect reciprocity under action and assessment generosity. <i>Scientific Reports</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41598-021-96932-1\">https://doi.org/10.1038/s41598-021-96932-1</a>","chicago":"Schmid, Laura, Pouya Shati, Christian Hilbe, and Krishnendu Chatterjee. “The Evolution of Indirect Reciprocity under Action and Assessment Generosity.” <i>Scientific Reports</i>. Springer Nature, 2021. <a href=\"https://doi.org/10.1038/s41598-021-96932-1\">https://doi.org/10.1038/s41598-021-96932-1</a>.","short":"L. Schmid, P. Shati, C. Hilbe, K. Chatterjee, Scientific Reports 11 (2021).","ista":"Schmid L, Shati P, Hilbe C, Chatterjee K. 2021. The evolution of indirect reciprocity under action and assessment generosity. Scientific Reports. 11(1), 17443.","ieee":"L. Schmid, P. Shati, C. Hilbe, and K. Chatterjee, “The evolution of indirect reciprocity under action and assessment generosity,” <i>Scientific Reports</i>, vol. 11, no. 1. Springer Nature, 2021.","mla":"Schmid, Laura, et al. “The Evolution of Indirect Reciprocity under Action and Assessment Generosity.” <i>Scientific Reports</i>, vol. 11, no. 1, 17443, Springer Nature, 2021, doi:<a href=\"https://doi.org/10.1038/s41598-021-96932-1\">10.1038/s41598-021-96932-1</a>.","ama":"Schmid L, Shati P, Hilbe C, Chatterjee K. The evolution of indirect reciprocity under action and assessment generosity. <i>Scientific Reports</i>. 2021;11(1). doi:<a href=\"https://doi.org/10.1038/s41598-021-96932-1\">10.1038/s41598-021-96932-1</a>"},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"}],"related_material":{"record":[{"status":"public","id":"10293","relation":"dissertation_contains"}]},"acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.). L.S. received additional partial support by the Austrian Science Fund (FWF) under Grant Z211-N23 (Wittgenstein Award).","publication_identifier":{"eissn":["2045-2322"]},"ec_funded":1,"scopus_import":"1","issue":"1","publication":"Scientific Reports","language":[{"iso":"eng"}],"intvolume":"        11","publication_status":"published","year":"2021","quality_controlled":"1","pmid":1,"ddc":["003"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"fulldoi":"https://doi.org/10.1038/s41598-021-96932-1","article_processing_charge":"Yes","keyword":["Multidisciplinary"],"has_accepted_license":"1","date_published":"2021-08-31T00:00:00Z","file_date_updated":"2021-09-13T10:31:21Z","publisher":"Springer Nature","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"month":"08","external_id":{"isi":["000692406400018"],"pmid":["34465830"]},"corr_author":"1","oa":1,"day":"31","doi":"10.1038/s41598-021-96932-1","file":[{"creator":"cchlebak","relation":"main_file","access_level":"open_access","date_created":"2021-09-13T10:31:21Z","checksum":"19df8816cf958b272b85841565c73182","success":1,"file_size":2424943,"date_updated":"2021-09-13T10:31:21Z","content_type":"application/pdf","file_name":"2021_ScientificReports_Schmid.pdf","file_id":"10006"}],"volume":11,"isi":1,"article_number":"17443"},{"intvolume":"         5","pmid":1,"quality_controlled":"1","year":"2021","publication_status":"published","ddc":["000"],"fulldoi":"https://doi.org/10.1038/s41562-021-01114-8","article_processing_charge":"No","file_date_updated":"2023-11-07T08:27:23Z","date_published":"2021-05-13T00:00:00Z","has_accepted_license":"1","month":"05","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"publisher":"Springer Nature","external_id":{"isi":["000650304000002"],"pmid":["33986519"]},"corr_author":"1","oa":1,"day":"13","file":[{"content_type":"application/pdf","date_updated":"2023-11-07T08:27:23Z","file_name":"2021_NatureHumanBehaviour_Schmid_accepted.pdf","file_size":5232761,"file_id":"14496","access_level":"open_access","creator":"dernst","relation":"main_file","success":1,"date_created":"2023-11-07T08:27:23Z","checksum":"34f55e173f90dc1dab731063458ac780"}],"doi":"10.1038/s41562-021-01114-8","volume":5,"isi":1,"abstract":[{"lang":"eng","text":"Direct and indirect reciprocity are key mechanisms for the evolution of cooperation. Direct reciprocity means that individuals use their own experience to decide whether to cooperate with another person. Indirect reciprocity means that they also consider the experiences of others. Although these two mechanisms are intertwined, they are typically studied in isolation. Here, we introduce a mathematical framework that allows us to explore both kinds of reciprocity simultaneously. We show that the well-known ‘generous tit-for-tat’ strategy of direct reciprocity has a natural analogue in indirect reciprocity, which we call ‘generous scoring’. Using an equilibrium analysis, we characterize under which conditions either of the two strategies can maintain cooperation. With simulations, we additionally explore which kind of reciprocity evolves when members of a population engage in social learning to adapt to their environment. Our results draw unexpected connections between direct and indirect reciprocity while highlighting important differences regarding their evolvability."}],"article_type":"original","oa_version":"Submitted Version","type":"journal_article","date_created":"2021-05-18T16:56:57Z","status":"public","author":[{"full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329","first_name":"Laura","last_name":"Schmid","id":"38B437DE-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","first_name":"Christian","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"_id":"9402","title":"A unified framework of direct and indirect reciprocity","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-10-22T22:30:45Z","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"citation":{"apa":"Schmid, L., Chatterjee, K., Hilbe, C., &#38; Nowak, M. A. (2021). A unified framework of direct and indirect reciprocity. <i>Nature Human Behaviour</i>. Springer Nature. <a href=\"https://doi.org/10.1038/s41562-021-01114-8\">https://doi.org/10.1038/s41562-021-01114-8</a>","chicago":"Schmid, Laura, Krishnendu Chatterjee, Christian Hilbe, and Martin A. Nowak. “A Unified Framework of Direct and Indirect Reciprocity.” <i>Nature Human Behaviour</i>. Springer Nature, 2021. <a href=\"https://doi.org/10.1038/s41562-021-01114-8\">https://doi.org/10.1038/s41562-021-01114-8</a>.","ieee":"L. Schmid, K. Chatterjee, C. Hilbe, and M. A. Nowak, “A unified framework of direct and indirect reciprocity,” <i>Nature Human Behaviour</i>, vol. 5, no. 10. Springer Nature, pp. 1292–1302, 2021.","ista":"Schmid L, Chatterjee K, Hilbe C, Nowak MA. 2021. A unified framework of direct and indirect reciprocity. Nature Human Behaviour. 5(10), 1292–1302.","short":"L. Schmid, K. Chatterjee, C. Hilbe, M.A. Nowak, Nature Human Behaviour 5 (2021) 1292–1302.","ama":"Schmid L, Chatterjee K, Hilbe C, Nowak MA. A unified framework of direct and indirect reciprocity. <i>Nature Human Behaviour</i>. 2021;5(10):1292–1302. doi:<a href=\"https://doi.org/10.1038/s41562-021-01114-8\">10.1038/s41562-021-01114-8</a>","mla":"Schmid, Laura, et al. “A Unified Framework of Direct and Indirect Reciprocity.” <i>Nature Human Behaviour</i>, vol. 5, no. 10, Springer Nature, 2021, pp. 1292–1302, doi:<a href=\"https://doi.org/10.1038/s41562-021-01114-8\">10.1038/s41562-021-01114-8</a>."},"page":"1292–1302","related_material":{"link":[{"relation":"press_release","description":"News on IST Homepage","url":"https://ist.ac.at/en/news/the-emergence-of-cooperation/"}],"record":[{"relation":"dissertation_contains","id":"10293","status":"public"}]},"acknowledgement":"This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.), the European Research Council Start Grant 279307: Graph Games (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.","ec_funded":1,"publication_identifier":{"eissn":["2397-3374"]},"issue":"10","scopus_import":"1","publication":"Nature Human Behaviour","language":[{"iso":"eng"}]},{"tmp":{"legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","name":"Creative Commons Public Domain Dedication (CC0 1.0)","short":"CC0 (1.0)","image":"/images/cc_0.png"},"ddc":["005"],"year":"2021","publication_status":"published","file_date_updated":"2021-12-23T23:30:04Z","alternative_title":["ISTA Thesis"],"date_published":"2021-01-01T00:00:00Z","has_accepted_license":"1","article_processing_charge":"No","fulldoi":"https://doi.org/10.15479/AT:ISTA:8934","degree_awarded":"PhD","day":"01","oa":1,"corr_author":"1","month":"01","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"publisher":"Institute of Science and Technology Austria","file":[{"file_size":5251507,"embargo":"2021-12-22","date_updated":"2021-12-23T23:30:04Z","content_type":"application/pdf","file_name":"Thesis-pdfa.pdf","file_id":"8969","creator":"akafshda","relation":"main_file","access_level":"open_access","date_created":"2020-12-22T20:08:44Z","checksum":"d1b9db3725aed34dadd81274aeb9426c"},{"file_id":"8970","embargo_to":"open_access","file_size":10636756,"file_name":"source.zip","date_updated":"2021-03-04T23:30:04Z","content_type":"application/zip","date_created":"2020-12-22T20:08:50Z","checksum":"1661df7b393e6866d2460eba3c905130","creator":"akafshda","relation":"source_file","access_level":"closed"}],"doi":"10.15479/AT:ISTA:8934","_id":"8934","title":"Parameterized and algebro-geometric advances in static program analysis","author":[{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","last_name":"Goharshady"}],"status":"public","date_created":"2020-12-10T12:17:07Z","oa_version":"Published Version","type":"dissertation","supervisor":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"text":"In this thesis, we consider several of the most classical and fundamental problems in static analysis and formal verification, including invariant generation, reachability analysis, termination analysis of probabilistic programs, data-flow analysis, quantitative analysis of Markov chains and Markov decision processes, and the problem of data packing in cache management.\r\nWe use techniques from parameterized complexity theory, polyhedral geometry, and real algebraic geometry to significantly improve the state-of-the-art, in terms of both scalability and completeness guarantees, for the mentioned problems. In some cases, our results are the first theoretical improvements for the respective problems in two or three decades.","lang":"eng"}],"related_material":{"record":[{"relation":"part_of_dissertation","id":"6490","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"6780"},{"status":"public","relation":"part_of_dissertation","id":"7158"},{"status":"public","id":"66","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"6378","status":"public"},{"status":"public","id":"311","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"6175"},{"status":"public","relation":"part_of_dissertation","id":"6340"},{"status":"public","id":"7014","relation":"part_of_dissertation"},{"status":"public","id":"6009","relation":"part_of_dissertation"},{"status":"public","id":"1437","relation":"part_of_dissertation"},{"status":"public","id":"8728","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"8089","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"6380"},{"status":"public","relation":"part_of_dissertation","id":"5977"},{"status":"public","id":"6056","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"639"},{"status":"public","relation":"part_of_dissertation","id":"1386"},{"relation":"part_of_dissertation","id":"6918","status":"public"},{"status":"public","relation":"part_of_dissertation","id":"7810"},{"relation":"part_of_dissertation","id":"949","status":"public"}]},"license":"https://creativecommons.org/publicdomain/zero/1.0/","project":[{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"page":"278","citation":{"chicago":"Goharshady, Amir Kafshdar. “Parameterized and Algebro-Geometric Advances in Static Program Analysis.” Institute of Science and Technology Austria, 2021. <a href=\"https://doi.org/10.15479/AT:ISTA:8934\">https://doi.org/10.15479/AT:ISTA:8934</a>.","apa":"Goharshady, A. K. (2021). <i>Parameterized and algebro-geometric advances in static program analysis</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:8934\">https://doi.org/10.15479/AT:ISTA:8934</a>","mla":"Goharshady, Amir Kafshdar. <i>Parameterized and Algebro-Geometric Advances in Static Program Analysis</i>. Institute of Science and Technology Austria, 2021, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:8934\">10.15479/AT:ISTA:8934</a>.","ama":"Goharshady AK. Parameterized and algebro-geometric advances in static program analysis. 2021. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:8934\">10.15479/AT:ISTA:8934</a>","ista":"Goharshady AK. 2021. Parameterized and algebro-geometric advances in static program analysis. Institute of Science and Technology Austria.","ieee":"A. K. Goharshady, “Parameterized and algebro-geometric advances in static program analysis,” Institute of Science and Technology Austria, 2021.","short":"A.K. Goharshady, Parameterized and Algebro-Geometric Advances in Static Program Analysis, Institute of Science and Technology Austria, 2021."},"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","date_updated":"2026-04-16T10:07:18Z","publication_identifier":{"issn":["2663-337X"]},"acknowledgement":"The research was partially supported by an IBM PhD fellowship, a Facebook PhD fellowship, and DOC fellowship #24956 of the Austrian Academy of Sciences (OeAW).","OA_place":"publisher","language":[{"iso":"eng"}]},{"article_processing_charge":"No","citation":{"mla":"Milutinovic, Barbara, et al. <i>Social Immunity Modulates Competition between Coinfecting Pathogens</i>. Dryad, 2020, doi:<a href=\"https://doi.org/10.5061/DRYAD.CRJDFN318\">10.5061/DRYAD.CRJDFN318</a>.","ama":"Milutinovic B, Stock M, Grasse AV, Naderlinger E, Hilbe C, Cremer S. Social immunity modulates competition between coinfecting pathogens. 2020. doi:<a href=\"https://doi.org/10.5061/DRYAD.CRJDFN318\">10.5061/DRYAD.CRJDFN318</a>","ieee":"B. Milutinovic, M. Stock, A. V. Grasse, E. Naderlinger, C. Hilbe, and S. Cremer, “Social immunity modulates competition between coinfecting pathogens.” Dryad, 2020.","ista":"Milutinovic B, Stock M, Grasse AV, Naderlinger E, Hilbe C, Cremer S. 2020. Social immunity modulates competition between coinfecting pathogens, Dryad, <a href=\"https://doi.org/10.5061/DRYAD.CRJDFN318\">10.5061/DRYAD.CRJDFN318</a>.","short":"B. Milutinovic, M. Stock, A.V. Grasse, E. Naderlinger, C. Hilbe, S. Cremer, (2020).","chicago":"Milutinovic, Barbara, Miriam Stock, Anna V Grasse, Elisabeth Naderlinger, Christian Hilbe, and Sylvia Cremer. “Social Immunity Modulates Competition between Coinfecting Pathogens.” Dryad, 2020. <a href=\"https://doi.org/10.5061/DRYAD.CRJDFN318\">https://doi.org/10.5061/DRYAD.CRJDFN318</a>.","apa":"Milutinovic, B., Stock, M., Grasse, A. V., Naderlinger, E., Hilbe, C., &#38; Cremer, S. (2020). Social immunity modulates competition between coinfecting pathogens. Dryad. <a href=\"https://doi.org/10.5061/DRYAD.CRJDFN318\">https://doi.org/10.5061/DRYAD.CRJDFN318</a>"},"related_material":{"record":[{"id":"7343","relation":"used_in_publication","status":"public"}]},"date_published":"2020-12-19T00:00:00Z","main_file_link":[{"url":"https://doi.org/10.5061/dryad.crjdfn318","open_access":"1"}],"date_updated":"2025-06-12T07:32:35Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","fulldoi":"https://doi.org/10.5061/DRYAD.CRJDFN318","ddc":["570"],"tmp":{"legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","name":"Creative Commons Public Domain Dedication (CC0 1.0)","short":"CC0 (1.0)","image":"/images/cc_0.png"},"date_created":"2023-05-23T16:11:22Z","author":[{"orcid":"0000-0002-8214-4758","full_name":"Milutinovic, Barbara","id":"2CDC32B8-F248-11E8-B48F-1D18A9856A87","first_name":"Barbara","last_name":"Milutinovic"},{"id":"42462816-F248-11E8-B48F-1D18A9856A87","last_name":"Stock","first_name":"Miriam","full_name":"Stock, Miriam"},{"last_name":"Grasse","first_name":"Anna V","id":"406F989C-F248-11E8-B48F-1D18A9856A87","full_name":"Grasse, Anna V"},{"id":"31757262-F248-11E8-B48F-1D18A9856A87","first_name":"Elisabeth","last_name":"Naderlinger","full_name":"Naderlinger, Elisabeth"},{"orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Hilbe"},{"id":"2F64EC8C-F248-11E8-B48F-1D18A9856A87","last_name":"Cremer","first_name":"Sylvia","full_name":"Cremer, Sylvia","orcid":"0000-0002-2193-3868"}],"status":"public","title":"Social immunity modulates competition between coinfecting pathogens","_id":"13060","abstract":[{"lang":"eng","text":"Coinfections with multiple pathogens can result in complex within-host dynamics affecting virulence and transmission. Whilst multiple infections are intensively studied in solitary hosts, it is so far unresolved how social host interactions interfere with pathogen competition, and if this depends on coinfection diversity. We studied how the collective disease defenses of ants – their social immunity ­– influence pathogen competition in coinfections of same or different fungal pathogen species. Social immunity reduced virulence for all pathogen combinations, but interfered with spore production only in different-species coinfections. Here, it decreased overall pathogen sporulation success, whilst simultaneously increasing co-sporulation on individual cadavers and maintaining a higher pathogen diversity at the community-level. Mathematical modeling revealed that host sanitary care alone can modulate competitive outcomes between pathogens, giving advantage to fast-germinating, thus less grooming-sensitive ones. Host social interactions can hence modulate infection dynamics in coinfected group members, thereby altering pathogen communities at the host- and population-level."}],"oa_version":"Published Version","type":"research_data_reference","year":"2020","doi":"10.5061/DRYAD.CRJDFN318","oa":1,"corr_author":"1","day":"19","publisher":"Dryad","department":[{"_id":"SyCr"},{"_id":"KrCh"}],"month":"12"},{"fulldoi":"https://doi.org/10.1609/aaai.v34i06.6531","arxiv":1,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2002.12086"}],"date_published":"2020-04-03T00:00:00Z","conference":{"name":"AAAI: Conference on Artificial Intelligence","start_date":"2020-02-07","end_date":"2020-02-12","location":"New York, NY, United States"},"keyword":["General Medicine"],"article_processing_charge":"No","quality_controlled":"1","year":"2020","publication_status":"published","intvolume":"        34","volume":34,"doi":"10.1609/aaai.v34i06.6531","external_id":{"arxiv":["2002.12086"]},"month":"04","department":[{"_id":"KrCh"}],"publisher":"Association for the Advancement of Artificial Intelligence","day":"03","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-04-15T06:30:08Z","project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"}],"page":"9794-9801","citation":{"apa":"Brázdil, T., Chatterjee, K., Novotný, P., &#38; Vahala, J. (2020). Reinforcement learning of risk-constrained policies in Markov decision processes. <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>. New York, NY, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v34i06.6531\">https://doi.org/10.1609/aaai.v34i06.6531</a>","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Petr Novotný, and Jiří Vahala. “Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes.” <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2020. <a href=\"https://doi.org/10.1609/aaai.v34i06.6531\">https://doi.org/10.1609/aaai.v34i06.6531</a>.","ieee":"T. Brázdil, K. Chatterjee, P. Novotný, and J. Vahala, “Reinforcement learning of risk-constrained policies in Markov decision processes,” <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 06. Association for the Advancement of Artificial Intelligence, pp. 9794–9801, 2020.","short":"T. Brázdil, K. Chatterjee, P. Novotný, J. Vahala, Proceedings of the 34th AAAI Conference on Artificial Intelligence 34 (2020) 9794–9801.","ista":"Brázdil T, Chatterjee K, Novotný P, Vahala J. 2020. Reinforcement learning of risk-constrained policies in Markov decision processes. Proceedings of the 34th AAAI Conference on Artificial Intelligence. 34(06), 9794–9801.","ama":"Brázdil T, Chatterjee K, Novotný P, Vahala J. Reinforcement learning of risk-constrained policies in Markov decision processes. <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>. 2020;34(06):9794-9801. doi:<a href=\"https://doi.org/10.1609/aaai.v34i06.6531\">10.1609/aaai.v34i06.6531</a>","mla":"Brázdil, Tomáš, et al. “Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes.” <i>Proceedings of the 34th AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 06, Association for the Advancement of Artificial Intelligence, 2020, pp. 9794–801, doi:<a href=\"https://doi.org/10.1609/aaai.v34i06.6531\">10.1609/aaai.v34i06.6531</a>."},"article_type":"original","oa_version":"Preprint","type":"journal_article","abstract":[{"text":"<jats:p>Markov decision processes (MDPs) are the defacto framework for sequential decision making in the presence of stochastic uncertainty. A classical optimization criterion for MDPs is to maximize the expected discounted-sum payoff, which ignores low probability catastrophic events with highly negative impact on the system. On the other hand, risk-averse policies require the probability of undesirable events to be below a given threshold, but they do not account for optimization of the expected payoff. We consider MDPs with discounted-sum payoff with failure states which represent catastrophic outcomes. The objective of risk-constrained planning is to maximize the expected discounted-sum payoff among risk-averse policies that ensure the probability to encounter a failure state is below a desired threshold. Our main contribution is an efficient risk-constrained planning algorithm that combines UCT-like search with a predictor learned through interaction with the MDP (in the style of AlphaZero) and with a risk-constrained action selection via linear programming. We demonstrate the effectiveness of our approach with experiments on classical MDPs from the literature, including benchmarks with an order of 106 states.</jats:p>","lang":"eng"}],"_id":"15055","title":"Reinforcement learning of risk-constrained policies in Markov decision processes","status":"public","author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Novotný, Petr","first_name":"Petr","last_name":"Novotný"},{"full_name":"Vahala, Jiří","first_name":"Jiří","last_name":"Vahala"}],"date_created":"2024-03-04T08:07:22Z","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2374-3468"]},"acknowledgement":"Krishnendu Chatterjee is supported by the Austrian Science Fund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE), and COST Action GAMENET. Tomas Brazdil is supported by the Grant Agency of Masaryk University grant no. MUNI/G/0739/2017 and by the Czech Science Foundation grant No. 18-11193S. Petr Novotny and Jirı Vahala are supported by the Czech Science Foundation grant No. GJ19-15134Y.","publication":"Proceedings of the 34th AAAI Conference on Artificial Intelligence","issue":"06"},{"_id":"15082","title":"Disjoint tree-compatible plane perfect matchings","author":[{"full_name":"Aichholzer, Oswin","first_name":"Oswin","last_name":"Aichholzer"},{"first_name":"Julia","last_name":"Obmann","full_name":"Obmann, Julia"},{"full_name":"Patak, Pavel","id":"B593B804-1035-11EA-B4F1-947645A5BB83","last_name":"Patak","first_name":"Pavel"},{"full_name":"Perz, Daniel","last_name":"Perz","first_name":"Daniel"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","first_name":"Josef","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684"}],"status":"public","date_created":"2024-03-05T08:57:17Z","ddc":["000"],"year":"2020","quality_controlled":"1","oa_version":"Published Version","type":"conference","publication_status":"published","abstract":[{"lang":"eng","text":"Two plane drawings of geometric graphs on the same set of points are called disjoint compatible if their union is plane and they do not have an edge in common. For a given set S of 2n points two plane drawings of perfect matchings M1 and M2 (which do not need to be disjoint nor compatible) are disjoint tree-compatible if there exists a plane drawing of a spanning tree T on S which is disjoint compatible to both M1 and M2.\r\nWe show that the graph of all disjoint tree-compatible perfect geometric matchings on 2n points in convex position is connected if and only if 2n ≥ 10. Moreover, in that case the diameter\r\nof this graph is either 4 or 5, independent of n."}],"date_published":"2020-04-01T00:00:00Z","conference":{"location":"Würzburg, Germany, Virtual","name":"EuroCG: European Workshop on Computational Geometry","start_date":"2020-03-16","end_date":"2020-03-18"},"article_processing_charge":"No","citation":{"ista":"Aichholzer O, Obmann J, Patak P, Perz D, Tkadlec J. 2020. Disjoint tree-compatible plane perfect matchings. 36th European Workshop on Computational Geometry. EuroCG: European Workshop on Computational Geometry, 56.","ieee":"O. Aichholzer, J. Obmann, P. Patak, D. Perz, and J. Tkadlec, “Disjoint tree-compatible plane perfect matchings,” in <i>36th European Workshop on Computational Geometry</i>, Würzburg, Germany, Virtual, 2020.","short":"O. Aichholzer, J. Obmann, P. Patak, D. Perz, J. Tkadlec, in:, 36th European Workshop on Computational Geometry, 2020.","ama":"Aichholzer O, Obmann J, Patak P, Perz D, Tkadlec J. Disjoint tree-compatible plane perfect matchings. In: <i>36th European Workshop on Computational Geometry</i>. ; 2020.","mla":"Aichholzer, Oswin, et al. “Disjoint Tree-Compatible Plane Perfect Matchings.” <i>36th European Workshop on Computational Geometry</i>, 56, 2020.","apa":"Aichholzer, O., Obmann, J., Patak, P., Perz, D., &#38; Tkadlec, J. (2020). Disjoint tree-compatible plane perfect matchings. In <i>36th European Workshop on Computational Geometry</i>. Würzburg, Germany, Virtual.","chicago":"Aichholzer, Oswin, Julia Obmann, Pavel Patak, Daniel Perz, and Josef Tkadlec. “Disjoint Tree-Compatible Plane Perfect Matchings.” In <i>36th European Workshop on Computational Geometry</i>, 2020."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-06-18T17:45:52Z","main_file_link":[{"open_access":"1","url":"https://www1.pub.informatik.uni-wuerzburg.de/eurocg2020/data/uploads/papers/eurocg20_paper_56.pdf"}],"day":"01","publication":"36th European Workshop on Computational Geometry","corr_author":"1","oa":1,"month":"04","department":[{"_id":"KrCh"},{"_id":"UlWa"}],"acknowledgement":"Research on this work was initiated at the 6th Austrian-Japanese-Mexican-Spanish Workshop on Discrete Geometry and continued during the 16th European Geometric Graph-Week, both held near Strobl, Austria. We are grateful to the participants for the inspiring atmosphere. We especially thank Alexander Pilz for bringing this class of problems to our attention and Birgit Vogtenhuber for inspiring discussions. D.P. is partially supported by the FWF grant I 3340-N35 (Collaborative DACH project Arrangements and Drawings). The research stay of P.P. at IST Austria is funded by the project CZ.02.2.69/0.0/0.0/17_050/0008466 Improvement of internationalization in the field of research and development at Charles University, through the support of quality projects MSCA-IF. This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 734922.","article_number":"56","language":[{"iso":"eng"}]},{"corr_author":"1","oa":1,"day":"18","publisher":"Cambridge University Press","department":[{"_id":"KrCh"}],"month":"11","doi":"10.1017/9781108770750.008","file":[{"relation":"main_file","creator":"dernst","access_level":"open_access","date_created":"2025-09-23T12:03:09Z","checksum":"28ece115e8d2d9263e253a598e7caef2","success":1,"file_size":316681,"file_name":"2020_ProbProgramming_Chatterjee.pdf","content_type":"application/pdf","date_updated":"2025-09-23T12:03:09Z","file_id":"20380"}],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"publication_status":"published","year":"2020","quality_controlled":"1","article_processing_charge":"No","has_accepted_license":"1","file_date_updated":"2025-09-23T12:03:09Z","date_published":"2020-11-18T00:00:00Z","fulldoi":"https://doi.org/10.1017/9781108770750.008","publication":"Foundations of Probabilistic Programming","acknowledgement":"Krishnendu Chatterjee is supported by the Austrian Science Fund (FWF) NFN\r\nGrant No. S11407-N23 (RiSE/SHiNE), and COST Action GAMENET. Hongfei Fu\r\nis supported by the National Natural Science Foundation of China (NSFC) Grant\r\nNo. 61802254. Petr Novotný is supported by the Czech Science Foundation grant\r\nNo. GJ19-15134Y.","publication_identifier":{"isbn":["9781108488518"],"eisbn":["9781108770750"]},"OA_place":"publisher","language":[{"iso":"eng"}],"date_created":"2025-07-10T13:28:51Z","status":"public","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"full_name":"Novotný, Petr","last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"title":"Termination Analysis of Probabilistic Programs with Martingales","_id":"19986","abstract":[{"text":"For non-probabilistic programs, a key question in static analysis is termination, which asks whether a given program terminates under a given initial condition. In the presence of probabilistic behaviour, there are two fundamental extensions of the termination question: (a) the almost-sure termination question, which asks whether the termination probability is 1; and (b) the bounded-time termination question, which asks whether the expected termination time is bounded. There are many active research directions to address these two questions; one important such direction is the use of martingale theory for termination analysis. In this chapter, we survey the main techniques of the martingale-based approach to the termination analysis of probabilistic programs.","lang":"eng"}],"oa_version":"Published Version","type":"book_chapter","page":"221-258","citation":{"chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Petr Novotný. “Termination Analysis of Probabilistic Programs with Martingales.” In <i>Foundations of Probabilistic Programming</i>, 221–58. Cambridge University Press, 2020. <a href=\"https://doi.org/10.1017/9781108770750.008\">https://doi.org/10.1017/9781108770750.008</a>.","apa":"Chatterjee, K., Fu, H., &#38; Novotný, P. (2020). Termination Analysis of Probabilistic Programs with Martingales. In <i>Foundations of Probabilistic Programming</i> (pp. 221–258). Cambridge University Press. <a href=\"https://doi.org/10.1017/9781108770750.008\">https://doi.org/10.1017/9781108770750.008</a>","ama":"Chatterjee K, Fu H, Novotný P. Termination Analysis of Probabilistic Programs with Martingales. In: <i>Foundations of Probabilistic Programming</i>. Cambridge University Press; 2020:221-258. doi:<a href=\"https://doi.org/10.1017/9781108770750.008\">10.1017/9781108770750.008</a>","mla":"Chatterjee, Krishnendu, et al. “Termination Analysis of Probabilistic Programs with Martingales.” <i>Foundations of Probabilistic Programming</i>, Cambridge University Press, 2020, pp. 221–58, doi:<a href=\"https://doi.org/10.1017/9781108770750.008\">10.1017/9781108770750.008</a>.","short":"K. Chatterjee, H. Fu, P. Novotný, in:, Foundations of Probabilistic Programming, Cambridge University Press, 2020, pp. 221–258.","ieee":"K. Chatterjee, H. Fu, and P. Novotný, “Termination Analysis of Probabilistic Programs with Martingales,” in <i>Foundations of Probabilistic Programming</i>, Cambridge University Press, 2020, pp. 221–258.","ista":"Chatterjee K, Fu H, Novotný P. 2020.Termination Analysis of Probabilistic Programs with Martingales. In: Foundations of Probabilistic Programming. , 221–258."},"project":[{"grant_number":"S11407","call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"date_updated":"2025-09-23T12:10:25Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"}]