[{"_id":"9640","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","oa_version":"Published Version","quality_controlled":"1","article_number":"4009","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"date_updated":"2026-04-02T14:04:10Z","status":"public","volume":12,"month":"06","publication_status":"published","isi":1,"department":[{"_id":"KrCh"}],"type":"journal_article","scopus_import":"1","ec_funded":1,"project":[{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"},{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"}],"publication":"Nature Communications","language":[{"iso":"eng"}],"ddc":["510"],"file_date_updated":"2021-07-19T13:02:20Z","article_processing_charge":"No","publisher":"Springer Nature","file":[{"access_level":"open_access","checksum":"5767418926a7f7fb76151de29473dae0","relation":"main_file","file_id":"9692","date_created":"2021-07-19T13:02:20Z","file_size":628992,"date_updated":"2021-07-19T13:02:20Z","content_type":"application/pdf","success":1,"file_name":"2021_NatCoom_Tkadlec.pdf","creator":"cziletti"}],"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.","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>","short":"J. Tkadlec, A. Pavlogiannis, K. Chatterjee, M.A. Nowak, Nature Communications 12 (2021)."},"has_accepted_license":"1","title":"Fast and strong amplifiers of natural selection","pmid":1,"publication_identifier":{"eissn":["2041-1723"]},"external_id":{"pmid":["34188036"],"isi":["000671752100003"]},"intvolume":"        12","date_created":"2021-07-11T22:01:15Z","year":"2021","issue":"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.","article_type":"original","doi":"10.1038/s41467-021-24271-w","day":"29","abstract":[{"lang":"eng","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."}],"oa":1,"author":[{"orcid":"0000-0002-1097-9684","first_name":"Josef","full_name":"Tkadlec, Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","full_name":"Nowak, Martin A.","first_name":"Martin A."}],"date_published":"2021-06-29T00:00:00Z"},{"department":[{"_id":"KrCh"}],"type":"conference","scopus_import":"1","ec_funded":1,"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"}],"publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","language":[{"iso":"eng"}],"page":"1033-1048","_id":"9644","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa_version":"Preprint","related_material":{"record":[{"relation":"research_data","status":"public","id":"15284"},{"relation":"dissertation_contains","status":"public","id":"14539"}]},"quality_controlled":"1","main_file_link":[{"url":"https://arxiv.org/abs/2104.01189","open_access":"1"}],"status":"public","date_updated":"2026-04-07T13:27:55Z","month":"06","publication_status":"published","isi":1,"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.","doi":"10.1145/3453483.3454093","day":"01","abstract":[{"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.","lang":"eng"}],"conference":{"name":"PLDI: Programming Language Design and Implementation","end_date":"2021-06-26","start_date":"2021-06-20","location":"Online"},"oa":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Goharshady","full_name":"Goharshady, Ehsan Kafshdar","first_name":"Ehsan Kafshdar"},{"full_name":"Novotný, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný"},{"last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","full_name":"Zikelic, Dorde"}],"arxiv":1,"date_published":"2021-06-01T00:00:00Z","publisher":"Association for Computing Machinery","article_processing_charge":"No","citation":{"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.","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.","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>","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>.","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.","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>.","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>"},"title":"Proving non-termination by program reversal","publication_identifier":{"isbn":["9781450383912"]},"external_id":{"isi":["000723661700067"],"arxiv":["2104.01189"]},"year":"2021","date_created":"2021-07-11T22:01:17Z"},{"ec_funded":1,"scopus_import":"1","type":"conference","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies"}],"quality_controlled":"1","oa_version":"Submitted Version","_id":"9645","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"772-787","publication_status":"published","month":"06","isi":1,"status":"public","date_updated":"2025-07-10T12:02:00Z","main_file_link":[{"open_access":"1","url":"https://hal.archives-ouvertes.fr/hal-03183862/"}],"doi":"10.1145/3453483.3454076","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).","date_published":"2021-06-01T00:00:00Z","oa":1,"author":[{"last_name":"Asadi","first_name":"Ali","full_name":"Asadi, Ali"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Fu, Hongfei","first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584"},{"full_name":"Mahdavi, Mohammad","first_name":"Mohammad","last_name":"Mahdavi"}],"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."}],"conference":{"start_date":"2021-06-20","location":"Online","end_date":"2021-06-26","name":"PLDI: Programming Language Design and Implementation"},"day":"01","citation":{"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.","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>","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.","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.","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>.","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>"},"publisher":"Association for Computing Machinery","article_processing_charge":"No","date_created":"2021-07-11T22:01:17Z","year":"2021","publication_identifier":{"isbn":["9781450383912"]},"external_id":{"isi":["000723661700050"]},"title":"Polynomial reachability witnesses via Stellensätze"},{"isi":1,"month":"06","publication_status":"published","status":"public","date_updated":"2025-04-15T07:55:05Z","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2011.14617"}],"quality_controlled":"1","_id":"9646","oa_version":"Preprint","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","page":"1171-1186","language":[{"iso":"eng"}],"publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","project":[{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies"}],"ec_funded":1,"scopus_import":"1","type":"conference","department":[{"_id":"KrCh"}],"year":"2021","date_created":"2021-07-11T22:01:18Z","external_id":{"isi":["000723661700076"],"arxiv":["2011.14617"]},"publication_identifier":{"isbn":["9781450383912"]},"title":"Quantitative analysis of assertion violations in probabilistic programs","citation":{"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>","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>.","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.","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.","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>","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>.","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."},"article_processing_charge":"No","publisher":"Association for Computing Machinery","date_published":"2021-06-01T00:00:00Z","arxiv":1,"author":[{"last_name":"Wang","first_name":"Jinyi","full_name":"Wang, Jinyi"},{"last_name":"Sun","full_name":"Sun, Yican","first_name":"Yican"},{"full_name":"Fu, Hongfei","first_name":"Hongfei","last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"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."}],"conference":{"location":"Online","start_date":"2021-06-20","end_date":"2021-06-26","name":"PLDI: Programming Language Design and Implementation"},"day":"01","doi":"10.1145/3453483.3454102","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)."},{"citation":{"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>","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.","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.","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>","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>.","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."},"file":[{"creator":"dernst","success":1,"file_name":"2021_LNCS_Agarwal.pdf","content_type":"application/pdf","date_updated":"2022-05-13T07:00:20Z","file_size":1516756,"date_created":"2022-05-13T07:00:20Z","file_id":"11368","relation":"main_file","checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","access_level":"open_access"}],"publisher":"Springer Nature","article_processing_charge":"Yes","file_date_updated":"2022-05-13T07:00:20Z","ddc":["000"],"year":"2021","date_created":"2021-09-05T22:01:24Z","publication_identifier":{"issn":["0302-9743"],"eisbn":["978-3-030-81685-8"],"eissn":["1611-3349"],"isbn":["978-3-030-81684-1"]},"external_id":{"isi":["000698732400016"],"arxiv":["2105.06424"]},"title":"Stateless model checking under a reads-value-from equivalence","has_accepted_license":"1","doi":"10.1007/978-3-030-81685-8_16","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.","date_published":"2021-07-15T00:00:00Z","oa":1,"author":[{"last_name":"Agarwal","full_name":"Agarwal, Pratyush","first_name":"Pratyush"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Pathak","full_name":"Pathak, Shreya","first_name":"Shreya"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","first_name":"Viktor","full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X"}],"arxiv":1,"abstract":[{"lang":"eng","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."}],"conference":{"location":"Virtual","start_date":"2021-07-20","name":"CAV: Computer Aided Verification ","end_date":"2021-07-23"},"day":"15","quality_controlled":"1","related_material":{"record":[{"relation":"dissertation_contains","id":"10199","status":"public"}]},"_id":"9987","oa_version":"Published Version","page":"341-366","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication_status":"published","volume":"12759 ","month":"07","isi":1,"status":"public","date_updated":"2026-04-08T07:00:30Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ec_funded":1,"alternative_title":["LNCS"],"scopus_import":"1","corr_author":"1","type":"conference","department":[{"_id":"KrCh"}],"language":[{"iso":"eng"}],"publication":"33rd International Conference on Computer-Aided Verification ","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}]},{"date_created":"2021-11-15T17:12:57Z","year":"2021","publication_identifier":{"issn":["2663-337X"]},"title":"Evolution of cooperation via (in)direct reciprocity under imperfect information","has_accepted_license":"1","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>","short":"L. Schmid, Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information, Institute of Science and Technology Austria, 2021.","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>","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>.","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."},"file":[{"file_id":"10305","access_level":"closed","checksum":"86a05b430756ca12ae8107b6e6f3c1e5","relation":"source_file","date_updated":"2022-12-20T23:30:08Z","file_size":29703124,"content_type":"application/zip","creator":"lschmid","file_name":"submission_new.zip","date_created":"2021-11-18T12:41:46Z","embargo_to":"open_access"},{"checksum":"d940af042e94660c6b6a7b4f0b184d47","access_level":"open_access","relation":"main_file","file_id":"10306","date_created":"2021-11-18T12:59:15Z","file_size":8320985,"date_updated":"2022-12-20T23:30:08Z","embargo":"2022-10-18","content_type":"application/pdf","creator":"lschmid","file_name":"thesis_new_upload.pdf"}],"publisher":"Institute of Science and Technology Austria","article_processing_charge":"No","file_date_updated":"2022-12-20T23:30:08Z","ddc":["519","576"],"date_published":"2021-11-17T00:00:00Z","oa":1,"author":[{"orcid":"0000-0002-6978-7329","first_name":"Laura","full_name":"Schmid, Laura","last_name":"Schmid","id":"38B437DE-F248-11E8-B48F-1D18A9856A87"}],"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"}],"day":"17","doi":"10.15479/at:ista:10293","degree_awarded":"PhD","month":"11","publication_status":"published","status":"public","date_updated":"2026-04-08T07:11:20Z","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"9997"},{"relation":"part_of_dissertation","id":"9402","status":"public"},{"relation":"part_of_dissertation","id":"2","status":"public"}]},"oa_version":"Published Version","_id":"10293","page":"171","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","language":[{"iso":"eng"}],"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"}],"alternative_title":["ISTA Thesis"],"ec_funded":1,"supervisor":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"corr_author":"1","OA_place":"publisher","type":"dissertation","department":[{"_id":"GradSch"},{"_id":"KrCh"}]},{"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).","issue":"1","article_type":"original","doi":"10.1038/s41598-021-96932-1","day":"31","abstract":[{"lang":"eng","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."}],"author":[{"id":"38B437DE-F248-11E8-B48F-1D18A9856A87","last_name":"Schmid","full_name":"Schmid, Laura","first_name":"Laura","orcid":"0000-0002-6978-7329"},{"full_name":"Shati, Pouya","first_name":"Pouya","last_name":"Shati"},{"last_name":"Hilbe","full_name":"Hilbe, Christian","first_name":"Christian"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"}],"oa":1,"date_published":"2021-08-31T00:00:00Z","file_date_updated":"2021-09-13T10:31:21Z","ddc":["003"],"file":[{"file_id":"10006","relation":"main_file","access_level":"open_access","checksum":"19df8816cf958b272b85841565c73182","date_updated":"2021-09-13T10:31:21Z","file_size":2424943,"success":1,"creator":"cchlebak","file_name":"2021_ScientificReports_Schmid.pdf","content_type":"application/pdf","date_created":"2021-09-13T10:31:21Z"}],"publisher":"Springer Nature","article_processing_charge":"Yes","citation":{"short":"L. Schmid, P. Shati, C. Hilbe, K. Chatterjee, Scientific Reports 11 (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>","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.","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.","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>.","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>"},"has_accepted_license":"1","pmid":1,"title":"The evolution of indirect reciprocity under action and assessment generosity","external_id":{"isi":["000692406400018"],"pmid":["34465830"]},"publication_identifier":{"eissn":["2045-2322"]},"date_created":"2021-09-11T16:22:02Z","year":"2021","intvolume":"        11","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"type":"journal_article","corr_author":"1","scopus_import":"1","ec_funded":1,"project":[{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"Z211","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"keyword":["Multidisciplinary"],"publication":"Scientific Reports","language":[{"iso":"eng"}],"_id":"9997","oa_version":"Published Version","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","related_material":{"record":[{"status":"public","id":"10293","relation":"dissertation_contains"}]},"article_number":"17443","quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2026-07-03T22:33:34Z","isi":1,"volume":11,"month":"08","publication_status":"published"},{"file_date_updated":"2023-11-07T08:27:23Z","ddc":["000"],"citation":{"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>.","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>","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.","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>.","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>","short":"L. Schmid, K. Chatterjee, C. Hilbe, M.A. Nowak, Nature Human Behaviour 5 (2021) 1292–1302."},"file":[{"file_id":"14496","access_level":"open_access","checksum":"34f55e173f90dc1dab731063458ac780","relation":"main_file","content_type":"application/pdf","creator":"dernst","success":1,"file_name":"2021_NatureHumanBehaviour_Schmid_accepted.pdf","date_updated":"2023-11-07T08:27:23Z","file_size":5232761,"date_created":"2023-11-07T08:27:23Z"}],"article_processing_charge":"No","publisher":"Springer Nature","title":"A unified framework of direct and indirect reciprocity","pmid":1,"has_accepted_license":"1","intvolume":"         5","date_created":"2021-05-18T16:56:57Z","year":"2021","publication_identifier":{"eissn":["2397-3374"]},"external_id":{"pmid":["33986519"],"isi":["000650304000002"]},"article_type":"original","issue":"10","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.","doi":"10.1038/s41562-021-01114-8","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."}],"day":"13","date_published":"2021-05-13T00:00:00Z","oa":1,"author":[{"id":"38B437DE-F248-11E8-B48F-1D18A9856A87","last_name":"Schmid","first_name":"Laura","full_name":"Schmid, Laura","orcid":"0000-0002-6978-7329"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","last_name":"Hilbe","full_name":"Hilbe, Christian","first_name":"Christian","orcid":"0000-0001-5116-955X"},{"full_name":"Nowak, Martin A.","first_name":"Martin A.","last_name":"Nowak"}],"_id":"9402","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","page":"1292–1302","quality_controlled":"1","related_material":{"record":[{"relation":"dissertation_contains","id":"10293","status":"public"}],"link":[{"url":"https://ist.ac.at/en/news/the-emergence-of-cooperation/","description":"News on IST Homepage","relation":"press_release"}]},"status":"public","date_updated":"2026-07-03T22:33:34Z","volume":5,"month":"05","publication_status":"published","isi":1,"type":"journal_article","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"ec_funded":1,"corr_author":"1","scopus_import":"1","publication":"Nature Human Behaviour","project":[{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"}],"language":[{"iso":"eng"}]},{"language":[{"iso":"eng"}],"project":[{"name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies","_id":"267066CE-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"alternative_title":["ISTA Thesis"],"supervisor":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"corr_author":"1","OA_place":"publisher","type":"dissertation","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"degree_awarded":"PhD","month":"01","publication_status":"published","date_updated":"2026-04-16T10:07:18Z","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","name":"Creative Commons Public Domain Dedication (CC0 1.0)","image":"/images/cc_0.png","short":"CC0 (1.0)"},"related_material":{"record":[{"id":"6490","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"6780","status":"public"},{"relation":"part_of_dissertation","id":"7158","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"66"},{"relation":"part_of_dissertation","id":"6378","status":"public"},{"status":"public","id":"311","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"6175","status":"public"},{"relation":"part_of_dissertation","id":"6340","status":"public"},{"id":"7014","status":"public","relation":"part_of_dissertation"},{"status":"public","id":"6009","relation":"part_of_dissertation"},{"id":"1437","status":"public","relation":"part_of_dissertation"},{"id":"8728","status":"public","relation":"part_of_dissertation"},{"id":"8089","status":"public","relation":"part_of_dissertation"},{"id":"6380","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"5977","status":"public"},{"id":"6056","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"639","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"1386"},{"status":"public","id":"6918","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"7810","status":"public"},{"relation":"part_of_dissertation","id":"949","status":"public"}]},"_id":"8934","page":"278","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","oa_version":"Published Version","date_published":"2021-01-01T00:00:00Z","oa":1,"author":[{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584"}],"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"}],"day":"01","doi":"10.15479/AT:ISTA:8934","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).","date_created":"2020-12-10T12:17:07Z","year":"2021","publication_identifier":{"issn":["2663-337X"]},"title":"Parameterized and algebro-geometric advances in static program analysis","has_accepted_license":"1","citation":{"ieee":"A. K. Goharshady, “Parameterized and algebro-geometric advances in static program analysis,” Institute of Science and Technology Austria, 2021.","ista":"Goharshady AK. 2021. Parameterized and algebro-geometric advances in static program analysis. Institute of Science and Technology Austria.","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>","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>.","short":"A.K. Goharshady, Parameterized and Algebro-Geometric Advances in Static Program Analysis, Institute of Science and Technology Austria, 2021.","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>"},"publisher":"Institute of Science and Technology Austria","article_processing_charge":"No","file":[{"creator":"akafshda","file_name":"Thesis-pdfa.pdf","content_type":"application/pdf","embargo":"2021-12-22","date_updated":"2021-12-23T23:30:04Z","file_size":5251507,"date_created":"2020-12-22T20:08:44Z","file_id":"8969","relation":"main_file","access_level":"open_access","checksum":"d1b9db3725aed34dadd81274aeb9426c"},{"relation":"source_file","access_level":"closed","checksum":"1661df7b393e6866d2460eba3c905130","file_id":"8970","date_created":"2020-12-22T20:08:50Z","embargo_to":"open_access","file_size":10636756,"date_updated":"2021-03-04T23:30:04Z","creator":"akafshda","file_name":"source.zip","content_type":"application/zip"}],"ddc":["005"],"file_date_updated":"2021-12-23T23:30:04Z"},{"date_published":"2020-12-19T00:00:00Z","author":[{"orcid":"0000-0002-8214-4758","full_name":"Milutinovic, Barbara","first_name":"Barbara","last_name":"Milutinovic","id":"2CDC32B8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Miriam","full_name":"Stock, Miriam","id":"42462816-F248-11E8-B48F-1D18A9856A87","last_name":"Stock"},{"full_name":"Grasse, Anna V","first_name":"Anna V","last_name":"Grasse","id":"406F989C-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Elisabeth","full_name":"Naderlinger, Elisabeth","id":"31757262-F248-11E8-B48F-1D18A9856A87","last_name":"Naderlinger"},{"orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","first_name":"Christian","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Cremer","id":"2F64EC8C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2193-3868","full_name":"Cremer, Sylvia","first_name":"Sylvia"}],"oa":1,"abstract":[{"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.","lang":"eng"}],"day":"19","doi":"10.5061/DRYAD.CRJDFN318","corr_author":"1","type":"research_data_reference","department":[{"_id":"SyCr"},{"_id":"KrCh"}],"date_created":"2023-05-23T16:11:22Z","year":"2020","month":"12","status":"public","date_updated":"2025-06-12T07:32:35Z","title":"Social immunity modulates competition between coinfecting pathogens","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5061/dryad.crjdfn318"}],"tmp":{"legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","name":"Creative Commons Public Domain Dedication (CC0 1.0)","image":"/images/cc_0.png","short":"CC0 (1.0)"},"citation":{"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>.","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>","short":"B. Milutinovic, M. Stock, A.V. Grasse, E. Naderlinger, C. Hilbe, S. Cremer, (2020).","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>","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>."},"related_material":{"record":[{"relation":"used_in_publication","status":"public","id":"7343"}]},"article_processing_charge":"No","publisher":"Dryad","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"13060","oa_version":"Published Version","ddc":["570"]},{"article_processing_charge":"No","publisher":"Association for the Advancement of Artificial Intelligence","citation":{"short":"T. Brázdil, K. Chatterjee, P. Novotný, J. Vahala, Proceedings of the 34th AAAI Conference on Artificial Intelligence 34 (2020) 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>.","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.","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.","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>."},"title":"Reinforcement learning of risk-constrained policies in Markov decision processes","external_id":{"arxiv":["2002.12086"]},"publication_identifier":{"issn":["2374-3468"]},"year":"2020","date_created":"2024-03-04T08:07:22Z","intvolume":"        34","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.","issue":"06","article_type":"original","doi":"10.1609/aaai.v34i06.6531","day":"03","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"}],"conference":{"start_date":"2020-02-07","location":"New York, NY, United States","end_date":"2020-02-12","name":"AAAI: Conference on Artificial Intelligence"},"author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Petr","full_name":"Novotný, Petr","last_name":"Novotný"},{"full_name":"Vahala, Jiří","first_name":"Jiří","last_name":"Vahala"}],"arxiv":1,"oa":1,"date_published":"2020-04-03T00:00:00Z","oa_version":"Preprint","_id":"15055","page":"9794-9801","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2002.12086","open_access":"1"}],"date_updated":"2025-04-15T06:30:08Z","status":"public","month":"04","publication_status":"published","volume":34,"department":[{"_id":"KrCh"}],"type":"journal_article","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"}],"publication":"Proceedings of the 34th AAAI Conference on Artificial Intelligence","keyword":["General Medicine"],"language":[{"iso":"eng"}]},{"conference":{"name":"EuroCG: European Workshop on Computational Geometry","end_date":"2020-03-18","start_date":"2020-03-16","location":"Würzburg, Germany, Virtual"},"publication":"36th European Workshop on Computational Geometry","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."}],"day":"01","date_published":"2020-04-01T00:00:00Z","oa":1,"author":[{"last_name":"Aichholzer","first_name":"Oswin","full_name":"Aichholzer, Oswin"},{"first_name":"Julia","full_name":"Obmann, Julia","last_name":"Obmann"},{"last_name":"Patak","id":"B593B804-1035-11EA-B4F1-947645A5BB83","full_name":"Patak, Pavel","first_name":"Pavel"},{"last_name":"Perz","first_name":"Daniel","full_name":"Perz, Daniel"},{"last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","first_name":"Josef","full_name":"Tkadlec, Josef"}],"language":[{"iso":"eng"}],"type":"conference","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.","corr_author":"1","title":"Disjoint tree-compatible plane perfect matchings","date_updated":"2026-06-18T17:45:52Z","status":"public","main_file_link":[{"open_access":"1","url":"https://www1.pub.informatik.uni-wuerzburg.de/eurocg2020/data/uploads/papers/eurocg20_paper_56.pdf"}],"date_created":"2024-03-05T08:57:17Z","year":"2020","month":"04","publication_status":"published","oa_version":"Published Version","_id":"15082","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"quality_controlled":"1","citation":{"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.","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.","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.","mla":"Aichholzer, Oswin, et al. “Disjoint Tree-Compatible Plane Perfect Matchings.” <i>36th European Workshop on Computational Geometry</i>, 56, 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.","short":"O. Aichholzer, J. Obmann, P. Patak, D. Perz, J. Tkadlec, in:, 36th European Workshop on Computational Geometry, 2020."},"article_number":"56","article_processing_charge":"No"},{"corr_author":"1","department":[{"_id":"KrCh"}],"type":"book_chapter","OA_place":"publisher","language":[{"iso":"eng"}],"project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"}],"publication":"Foundations of Probabilistic Programming","quality_controlled":"1","oa_version":"Published Version","_id":"19986","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"221-258","publication_status":"published","month":"11","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2025-09-23T12:10:25Z","doi":"10.1017/9781108770750.008","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.","oa":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Hongfei","full_name":"Fu, Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu"},{"first_name":"Petr","full_name":"Novotný, Petr","last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2020-11-18T00:00:00Z","day":"18","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"}],"publisher":"Cambridge University Press","article_processing_charge":"No","file":[{"relation":"main_file","checksum":"28ece115e8d2d9263e253a598e7caef2","access_level":"open_access","file_id":"20380","date_created":"2025-09-23T12:03:09Z","success":1,"file_name":"2020_ProbProgramming_Chatterjee.pdf","creator":"dernst","content_type":"application/pdf","date_updated":"2025-09-23T12:03:09Z","file_size":316681}],"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>","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.","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>.","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>","short":"K. Chatterjee, H. Fu, P. Novotný, in:, Foundations of Probabilistic Programming, Cambridge University Press, 2020, pp. 221–258."},"ddc":["000"],"file_date_updated":"2025-09-23T12:03:09Z","publication_identifier":{"eisbn":["9781108770750"],"isbn":["9781108488518"]},"date_created":"2025-07-10T13:28:51Z","year":"2020","has_accepted_license":"1","title":"Termination Analysis of Probabilistic Programs with Martingales"},{"ddc":["000"],"file_date_updated":"2020-11-25T09:38:14Z","article_processing_charge":"No","publisher":"Association for Computing Machinery","file":[{"file_name":"2020_LICS_Ashok.pdf","creator":"dernst","success":1,"content_type":"application/pdf","date_updated":"2020-11-25T09:38:14Z","file_size":1001395,"date_created":"2020-11-25T09:38:14Z","file_id":"8804","relation":"main_file","access_level":"open_access","checksum":"d0d0288fe991dd16cf5f02598b794240"}],"citation":{"short":"P. Ashok, K. Chatterjee, J. Kretinsky, M. Weininger, T. Winkler, in:, Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , Association for Computing Machinery, 2020, pp. 102–115.","ama":"Ashok P, Chatterjee K, Kretinsky J, Weininger M, Winkler T. Approximating values of generalized-reachability stochastic games. In: <i>Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science </i>. Association for Computing Machinery; 2020:102-115. doi:<a href=\"https://doi.org/10.1145/3373718.3394761\">10.1145/3373718.3394761</a>","mla":"Ashok, Pranav, et al. “Approximating Values of Generalized-Reachability Stochastic Games.” <i>Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science </i>, Association for Computing Machinery, 2020, pp. 102–15, doi:<a href=\"https://doi.org/10.1145/3373718.3394761\">10.1145/3373718.3394761</a>.","ieee":"P. Ashok, K. Chatterjee, J. Kretinsky, M. Weininger, and T. Winkler, “Approximating values of generalized-reachability stochastic games,” in <i>Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science </i>, Saarbrücken, Germany, 2020, pp. 102–115.","ista":"Ashok P, Chatterjee K, Kretinsky J, Weininger M, Winkler T. 2020. Approximating values of generalized-reachability stochastic games. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science . LICS: Logic in Computer Science, 102–115.","apa":"Ashok, P., Chatterjee, K., Kretinsky, J., Weininger, M., &#38; Winkler, T. (2020). Approximating values of generalized-reachability stochastic games. In <i>Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science </i> (pp. 102–115). Saarbrücken, Germany: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3373718.3394761\">https://doi.org/10.1145/3373718.3394761</a>","chicago":"Ashok, Pranav, Krishnendu Chatterjee, Jan Kretinsky, Maximilian Weininger, and Tobias Winkler. “Approximating Values of Generalized-Reachability Stochastic Games.” In <i>Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science </i>, 102–15. Association for Computing Machinery, 2020. <a href=\"https://doi.org/10.1145/3373718.3394761\">https://doi.org/10.1145/3373718.3394761</a>."},"has_accepted_license":"1","title":"Approximating values of generalized-reachability stochastic games","external_id":{"isi":["000665014900010"],"arxiv":["1908.05106"]},"publication_identifier":{"isbn":["9781450371049"]},"date_created":"2020-06-14T22:00:48Z","year":"2020","acknowledgement":"Pranav Ashok, Jan Křetínský and Maximilian Weininger were funded in part by TUM IGSSE Grant 10.06 (PARSEC) and the German Research Foundation (DFG) project KR 4890/2-1\r\n“Statistical Unbounded Verification”. Krishnendu Chatterjee was supported by the ERC CoG 863818 (ForM-SMArt) and Vienna Science and Technology Fund (WWTF) Project ICT15-\r\n003. Tobias Winkler was supported by the RTG 2236 UnRAVe.","doi":"10.1145/3373718.3394761","day":"08","abstract":[{"lang":"eng","text":"Simple stochastic games are turn-based 2½-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. In this paper, we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound."}],"conference":{"name":"LICS: Logic in Computer Science","end_date":"2020-07-11","start_date":"2020-07-08","location":"Saarbrücken, Germany"},"author":[{"last_name":"Ashok","first_name":"Pranav","full_name":"Ashok, Pranav"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"last_name":"Weininger","full_name":"Weininger, Maximilian","first_name":"Maximilian"},{"last_name":"Winkler","full_name":"Winkler, Tobias","first_name":"Tobias"}],"arxiv":1,"oa":1,"date_published":"2020-07-08T00:00:00Z","oa_version":"Published Version","_id":"7955","page":"102-115","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","date_updated":"2025-07-10T11:54:53Z","status":"public","isi":1,"month":"07","publication_status":"published","department":[{"_id":"KrCh"}],"type":"conference","scopus_import":"1","ec_funded":1,"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"publication":"Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science ","language":[{"iso":"eng"}]},{"publication_identifier":{"issn":["2334-0835"],"eissn":["2334-0843"]},"date_created":"2020-08-02T22:00:58Z","year":"2020","intvolume":"        30","title":"Multiple-environment Markov decision processes: Efficient analysis and applications","publisher":"Association for the Advancement of Artificial Intelligence","article_processing_charge":"No","citation":{"ama":"Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. Multiple-environment Markov decision processes: Efficient analysis and applications. In: <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>. Vol 30. Association for the Advancement of Artificial Intelligence; 2020:48-56.","mla":"Chatterjee, Krishnendu, et al. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, vol. 30, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56.","short":"K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, A. Royer, in:, Proceedings of the 30th International Conference on Automated Planning and Scheduling, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Deep Karkhanis, Petr Novotný, and Amélie Royer. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” In <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, 30:48–56. Association for the Advancement of Artificial Intelligence, 2020.","apa":"Chatterjee, K., Chmelik, M., Karkhanis, D., Novotný, P., &#38; Royer, A. (2020). Multiple-environment Markov decision processes: Efficient analysis and applications. In <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i> (Vol. 30, pp. 48–56). Nancy, France: Association for the Advancement of Artificial Intelligence.","ieee":"K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, and A. Royer, “Multiple-environment Markov decision processes: Efficient analysis and applications,” in <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, Nancy, France, 2020, vol. 30, pp. 48–56.","ista":"Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. 2020. Multiple-environment Markov decision processes: Efficient analysis and applications. Proceedings of the 30th International Conference on Automated Planning and Scheduling. ICAPS: International Conference on Automated Planning and Scheduling vol. 30, 48–56."},"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin"},{"first_name":"Deep","full_name":"Karkhanis, Deep","last_name":"Karkhanis"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný","full_name":"Novotný, Petr","first_name":"Petr"},{"last_name":"Royer","id":"3811D890-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8407-0705","first_name":"Amélie","full_name":"Royer, Amélie"}],"date_published":"2020-06-01T00:00:00Z","day":"01","abstract":[{"lang":"eng","text":"Multiple-environment Markov decision processes (MEMDPs) are MDPs equipped with not one, but multiple probabilistic transition functions, which represent the various possible unknown environments. While the previous research on MEMDPs focused on theoretical properties for long-run average payoff, we study them with discounted-sum payoff and focus on their practical advantages and applications. MEMDPs can be viewed as a special case of Partially observable and Mixed observability MDPs: the state of the system is perfectly observable, but not the environment. We show that the specific structure of MEMDPs allows for more efficient algorithmic analysis, in particular for faster belief updates. We demonstrate the applicability of MEMDPs in several domains. In particular, we formalize the sequential decision-making approach to contextual recommendation systems as MEMDPs and substantially improve over the previous MDP approach."}],"conference":{"end_date":"2020-10-30","name":"ICAPS: International Conference on Automated Planning and Scheduling","location":"Nancy, France","start_date":"2020-10-26"},"acknowledgement":"Krishnendu Chatterjee is supported by the Austrian ScienceFund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE),and COST Action GAMENET. Petr Novotn ́y is supported bythe Czech Science Foundation grant No. GJ19-15134Y.","publication_status":"published","volume":30,"month":"06","status":"public","date_updated":"2026-04-08T07:26:44Z","related_material":{"record":[{"id":"8390","status":"public","relation":"dissertation_contains"}]},"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"8193","page":"48-56","oa_version":"None","language":[{"iso":"eng"}],"project":[{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"}],"publication":"Proceedings of the 30th International Conference on Automated Planning and Scheduling","scopus_import":"1","department":[{"_id":"KrCh"}],"type":"conference"},{"type":"conference","department":[{"_id":"KrCh"}],"alternative_title":["LNCS"],"ec_funded":1,"scopus_import":"1","publication":"International Conference on Computer Aided Verification","project":[{"call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"language":[{"iso":"eng"}],"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","_id":"8272","page":"398-420","oa_version":"Published Version","quality_controlled":"1","related_material":{"record":[{"status":"public","id":"12738","relation":"later_version"}]},"date_updated":"2026-04-16T09:31:14Z","status":"public","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"isi":1,"volume":12225,"publication_status":"published","month":"07","doi":"10.1007/978-3-030-53291-8_21","abstract":[{"lang":"eng","text":"We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in   NP∩coNP , matching the current known bound for single objectives; and in general the decision problem is   PSPACE -hard and can be solved in   NEXPTIME∩coNEXPTIME . We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies."}],"conference":{"name":"CAV: Computer Aided Verification"},"day":"14","date_published":"2020-07-14T00:00:00Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Joost P","full_name":"Katoen, Joost P","orcid":"0000-0002-6143-1926","id":"4524F760-F248-11E8-B48F-1D18A9856A87","last_name":"Katoen"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"},{"last_name":"Winkler","full_name":"Winkler, Tobias","first_name":"Tobias"}],"arxiv":1,"oa":1,"ddc":["000"],"file_date_updated":"2020-08-17T11:32:44Z","citation":{"short":"K. Chatterjee, J.P. Katoen, M. Weininger, T. Winkler, in:, International Conference on Computer Aided Verification, Springer Nature, 2020, pp. 398–420.","ama":"Chatterjee K, Katoen JP, Weininger M, Winkler T. Stochastic games with lexicographic reachability-safety objectives. In: <i>International Conference on Computer Aided Verification</i>. Vol 12225. Springer Nature; 2020:398-420. doi:<a href=\"https://doi.org/10.1007/978-3-030-53291-8_21\">10.1007/978-3-030-53291-8_21</a>","mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Reachability-Safety Objectives.” <i>International Conference on Computer Aided Verification</i>, vol. 12225, Springer Nature, 2020, pp. 398–420, doi:<a href=\"https://doi.org/10.1007/978-3-030-53291-8_21\">10.1007/978-3-030-53291-8_21</a>.","ieee":"K. Chatterjee, J. P. Katoen, M. Weininger, and T. Winkler, “Stochastic games with lexicographic reachability-safety objectives,” in <i>International Conference on Computer Aided Verification</i>, 2020, vol. 12225, pp. 398–420.","ista":"Chatterjee K, Katoen JP, Weininger M, Winkler T. 2020. Stochastic games with lexicographic reachability-safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 12225, 398–420.","chicago":"Chatterjee, Krishnendu, Joost P Katoen, Maximilian Weininger, and Tobias Winkler. “Stochastic Games with Lexicographic Reachability-Safety Objectives.” In <i>International Conference on Computer Aided Verification</i>, 12225:398–420. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-53291-8_21\">https://doi.org/10.1007/978-3-030-53291-8_21</a>.","apa":"Chatterjee, K., Katoen, J. P., Weininger, M., &#38; Winkler, T. (2020). Stochastic games with lexicographic reachability-safety objectives. In <i>International Conference on Computer Aided Verification</i> (Vol. 12225, pp. 398–420). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-53291-8_21\">https://doi.org/10.1007/978-3-030-53291-8_21</a>"},"article_processing_charge":"No","file":[{"file_name":"2020_LNCS_CAV_Chatterjee.pdf","creator":"dernst","success":1,"content_type":"application/pdf","date_updated":"2020-08-17T11:32:44Z","file_size":625056,"date_created":"2020-08-17T11:32:44Z","file_id":"8276","relation":"main_file","checksum":"093d4788d7d5b2ce0ffe64fbe7820043","access_level":"open_access"}],"publisher":"Springer Nature","title":"Stochastic games with lexicographic reachability-safety objectives","has_accepted_license":"1","year":"2020","date_created":"2020-08-16T22:00:58Z","intvolume":"     12225","external_id":{"arxiv":["2005.04018"],"isi":["000695272500021"]},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783030532901"]}},{"day":"01","abstract":[{"text":"The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.","lang":"eng"}],"oa":1,"author":[{"first_name":"Peixin","full_name":"Wang, Peixin","last_name":"Wang"},{"first_name":"Hongfei","full_name":"Fu, Hongfei","last_name":"Fu"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Yuxin","full_name":"Deng, Yuxin","last_name":"Deng"},{"full_name":"Xu, Ming","first_name":"Ming","last_name":"Xu"}],"arxiv":1,"date_published":"2020-01-01T00:00:00Z","issue":"POPL","acknowledgement":"We thank anonymous reviewers for helpful comments, especially for pointing to us a scenario of piecewise-linear approximation (Remark5). The research was partially supported by the National Natural Science Foundation of China (NSFC) under Grant No. 61802254, 61672229, 61832015,61772336,11871221 and Austrian Science Fund (FWF) NFN under Grant No. S11407-N23 (RiSE/SHiNE). We thank Prof. Yuxi Fu, director of the BASICS Lab at Shanghai Jiao Tong University, for his support.","doi":"10.1145/3371093","has_accepted_license":"1","title":"Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time","publication_identifier":{"eissn":["2475-1421"]},"external_id":{"arxiv":["1902.04744"]},"intvolume":"         4","year":"2020","date_created":"2020-08-30T22:01:12Z","file_date_updated":"2020-09-01T11:12:58Z","ddc":["004"],"file":[{"relation":"main_file","access_level":"open_access","checksum":"c6193d109ff4ecb17e7a6513d8eb34c0","file_id":"8328","date_created":"2020-09-01T11:12:58Z","date_updated":"2020-09-01T11:12:58Z","file_size":564151,"file_name":"2019_ACM_POPL_Wang.pdf","creator":"cziletti","success":1,"content_type":"application/pdf"}],"article_processing_charge":"No","publisher":"ACM","citation":{"chicago":"Wang, Peixin, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” In <i>Proceedings of the ACM on Programming Languages</i>, Vol. 4. ACM, 2020. <a href=\"https://doi.org/10.1145/3371093\">https://doi.org/10.1145/3371093</a>.","apa":"Wang, P., Fu, H., Chatterjee, K., Deng, Y., &#38; Xu, M. (2020). Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In <i>Proceedings of the ACM on Programming Languages</i> (Vol. 4). ACM. <a href=\"https://doi.org/10.1145/3371093\">https://doi.org/10.1145/3371093</a>","ieee":"P. Wang, H. Fu, K. Chatterjee, Y. Deng, and M. Xu, “Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time,” in <i>Proceedings of the ACM on Programming Languages</i>, 2020, vol. 4, no. POPL.","ista":"Wang P, Fu H, Chatterjee K, Deng Y, Xu M. 2020. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. Proceedings of the ACM on Programming Languages. vol. 4, 25.","ama":"Wang P, Fu H, Chatterjee K, Deng Y, Xu M. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In: <i>Proceedings of the ACM on Programming Languages</i>. Vol 4. ACM; 2020. doi:<a href=\"https://doi.org/10.1145/3371093\">10.1145/3371093</a>","mla":"Wang, Peixin, et al. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 4, no. POPL, 25, ACM, 2020, doi:<a href=\"https://doi.org/10.1145/3371093\">10.1145/3371093</a>.","short":"P. Wang, H. Fu, K. Chatterjee, Y. Deng, M. Xu, in:, Proceedings of the ACM on Programming Languages, ACM, 2020."},"project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"}],"publication":"Proceedings of the ACM on Programming Languages","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"type":"conference","scopus_import":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","date_updated":"2025-04-15T06:30:10Z","publication_status":"published","month":"01","volume":4,"_id":"8324","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","related_material":{"link":[{"relation":"software","url":"https://doi.org/10.5281/zenodo.3533633"}]},"quality_controlled":"1","article_number":"25"},{"external_id":{"arxiv":["2007.02894"]},"publication_identifier":{"isbn":["9783959771597"],"issn":["1868-8969"]},"date_created":"2020-09-20T22:01:36Z","year":"2020","intvolume":"       170","has_accepted_license":"1","title":"Simplified game of life: Algorithms and complexity","article_processing_charge":"No","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"content_type":"application/pdf","creator":"dernst","file_name":"2020_LIPIcs_Chatterjee.pdf","success":1,"date_updated":"2020-09-21T13:57:34Z","file_size":491374,"date_created":"2020-09-21T13:57:34Z","file_id":"8550","access_level":"open_access","checksum":"bbd7c4f55d45f2ff2a0a4ef0e10a77b1","relation":"main_file"}],"citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Simplified game of life: Algorithms and complexity. In: <i>45th International Symposium on Mathematical Foundations of Computer Science</i>. Vol 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.22\">10.4230/LIPIcs.MFCS.2020.22</a>","mla":"Chatterjee, Krishnendu, et al. “Simplified Game of Life: Algorithms and Complexity.” <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, vol. 170, 22:1-22:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.22\">10.4230/LIPIcs.MFCS.2020.22</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, I.R. Jecker, J. Svoboda, in:, 45th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Simplified Game of Life: Algorithms and Complexity.” In <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, Vol. 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.22\">https://doi.org/10.4230/LIPIcs.MFCS.2020.22</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., &#38; Svoboda, J. (2020). Simplified game of life: Algorithms and complexity. In <i>45th International Symposium on Mathematical Foundations of Computer Science</i> (Vol. 170). Prague, Czech Republic: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.22\">https://doi.org/10.4230/LIPIcs.MFCS.2020.22</a>","ista":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. 2020. Simplified game of life: Algorithms and complexity. 45th International Symposium on Mathematical Foundations of Computer Science. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 170, 22:1-22:13.","ieee":"K. Chatterjee, R. Ibsen-Jensen, I. R. Jecker, and J. Svoboda, “Simplified game of life: Algorithms and complexity,” in <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, Prague, Czech Republic, 2020, vol. 170."},"ddc":["000"],"file_date_updated":"2020-09-21T13:57:34Z","arxiv":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Jecker, Ismael R","first_name":"Ismael R","last_name":"Jecker","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","last_name":"Svoboda","first_name":"Jakub","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267"}],"oa":1,"date_published":"2020-08-18T00:00:00Z","day":"18","abstract":[{"text":"Game of Life is a simple and elegant model to study dynamical system over networks. The model consists of a graph where every vertex has one of two types, namely, dead or alive. A configuration is a mapping of the vertices to the types. An update rule describes how the type of a vertex is updated given the types of its neighbors. In every round, all vertices are updated synchronously, which leads to a configuration update. While in general, Game of Life allows a broad range of update rules, we focus on two simple families of update rules, namely, underpopulation and overpopulation, that model several interesting dynamics studied in the literature. In both settings, a dead vertex requires at least a desired number of live neighbors to become alive. For underpopulation (resp., overpopulation), a live vertex requires at least (resp. at most) a desired number of live neighbors to remain alive. We study the basic computation problems, e.g., configuration reachability, for these two families of rules. For underpopulation rules, we show that these problems can be solved in polynomial time, whereas for overpopulation rules they are PSPACE-complete.","lang":"eng"}],"conference":{"end_date":"2020-08-28","name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2020-08-24","location":"Prague, Czech Republic"},"doi":"10.4230/LIPIcs.MFCS.2020.22","acknowledgement":"Krishnendu Chatterjee: The research was partially supported by the Vienna Science and\r\nTechnology Fund (WWTF) Project ICT15-003.\r\nIsmaël Jecker: This project has received funding from the European Union’s Horizon 2020 research\r\nand innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 754411.","month":"08","publication_status":"published","volume":170,"tmp":{"image":"/images/cc_by.png","short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"status":"public","date_updated":"2025-07-10T11:57:06Z","article_number":"22:1-22:13","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"8533","oa_version":"Published Version","language":[{"iso":"eng"}],"project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"754411","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships"}],"publication":"45th International Symposium on Mathematical Foundations of Computer Science","scopus_import":"1","alternative_title":["LIPIcs"],"ec_funded":1,"department":[{"_id":"KrCh"}],"type":"conference"},{"language":[{"iso":"eng"}],"publication":"45th International Symposium on Mathematical Foundations of Computer Science","project":[{"grant_number":"754411","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships"}],"ec_funded":1,"alternative_title":["LIPIcs"],"corr_author":"1","scopus_import":"1","type":"conference","department":[{"_id":"KrCh"}],"volume":170,"publication_status":"published","month":"08","date_updated":"2025-07-10T11:57:07Z","status":"public","tmp":{"image":"/images/cc_by.png","short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"quality_controlled":"1","article_number":"51:1-51:12","_id":"8534","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","date_published":"2020-08-18T00:00:00Z","oa":1,"author":[{"full_name":"Jecker, Ismael R","first_name":"Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","last_name":"Jecker"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"},{"first_name":"Nicolas","full_name":"Mazzocchi, Nicolas","last_name":"Mazzocchi"}],"conference":{"start_date":"2020-08-24","location":"Prague, Czech Republic","end_date":"2020-08-28","name":"MFCS: Mathematical Foundations of Computer Science"},"abstract":[{"lang":"eng","text":"A regular language L of finite words is composite if there are regular languages L₁,L₂,…,L_t such that L = ⋂_{i = 1}^t L_i and the index (number of states in a minimal DFA) of every language L_i is strictly smaller than the index of L. Otherwise, L is prime. Primality of regular languages was introduced and studied in [O. Kupferman and J. Mosheiff, 2015], where the complexity of deciding the primality of the language of a given DFA was left open, with a doubly-exponential gap between the upper and lower bounds. We study primality for unary regular languages, namely regular languages with a singleton alphabet. A unary language corresponds to a subset of ℕ, making the study of unary prime languages closer to that of primality in number theory. We show that the setting of languages is richer. In particular, while every composite number is the product of two smaller numbers, the number t of languages necessary to decompose a composite unary language induces a strict hierarchy. In addition, a primality witness for a unary language L, namely a word that is not in L but is in all products of languages that contain L and have an index smaller than L’s, may be of exponential length. Still, we are able to characterize compositionality by structural properties of a DFA for L, leading to a LogSpace algorithm for primality checking of unary DFAs."}],"day":"18","doi":"10.4230/LIPIcs.MFCS.2020.51","acknowledgement":"Ismaël Jecker: This project has received funding from the European Union’s Horizon\r\n2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No.\r\n754411. Nicolas Mazzocchi: PhD fellowship FRIA from the F.R.S.-FNRS.","intvolume":"       170","year":"2020","date_created":"2020-09-20T22:01:36Z","publication_identifier":{"isbn":["9783959771597"],"issn":["1868-8969"]},"title":"Unary prime languages","has_accepted_license":"1","citation":{"ama":"Jecker IR, Kupferman O, Mazzocchi N. Unary prime languages. In: <i>45th International Symposium on Mathematical Foundations of Computer Science</i>. Vol 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.51\">10.4230/LIPIcs.MFCS.2020.51</a>","mla":"Jecker, Ismael R., et al. “Unary Prime Languages.” <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, vol. 170, 51:1-51:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.51\">10.4230/LIPIcs.MFCS.2020.51</a>.","short":"I.R. Jecker, O. Kupferman, N. Mazzocchi, in:, 45th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","chicago":"Jecker, Ismael R, Orna Kupferman, and Nicolas Mazzocchi. “Unary Prime Languages.” In <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, Vol. 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.51\">https://doi.org/10.4230/LIPIcs.MFCS.2020.51</a>.","apa":"Jecker, I. R., Kupferman, O., &#38; Mazzocchi, N. (2020). Unary prime languages. In <i>45th International Symposium on Mathematical Foundations of Computer Science</i> (Vol. 170). Prague, Czech Republic: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2020.51\">https://doi.org/10.4230/LIPIcs.MFCS.2020.51</a>","ieee":"I. R. Jecker, O. Kupferman, and N. Mazzocchi, “Unary prime languages,” in <i>45th International Symposium on Mathematical Foundations of Computer Science</i>, Prague, Czech Republic, 2020, vol. 170.","ista":"Jecker IR, Kupferman O, Mazzocchi N. 2020. Unary prime languages. 45th International Symposium on Mathematical Foundations of Computer Science. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 170, 51:1-51:12."},"file":[{"file_id":"8552","relation":"main_file","checksum":"2dc9e2fad6becd4563aef3e27a473f70","access_level":"open_access","file_size":597977,"date_updated":"2020-09-21T14:17:08Z","creator":"dernst","file_name":"2020_LIPIcsMFCS_Jecker.pdf","success":1,"content_type":"application/pdf","date_created":"2020-09-21T14:17:08Z"}],"article_processing_charge":"No","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","ddc":["000"],"file_date_updated":"2020-09-21T14:17:08Z"},{"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959771603"]},"external_id":{"arxiv":["2007.08917"]},"intvolume":"       171","date_created":"2020-10-04T22:01:36Z","year":"2020","has_accepted_license":"1","title":"Multi-dimensional long-run average problems for vector addition systems with states","file":[{"date_created":"2020-10-05T14:04:25Z","content_type":"application/pdf","success":1,"file_name":"2020_LIPIcsCONCUR_Chatterjee.pdf","creator":"dernst","date_updated":"2020-10-05T14:04:25Z","file_size":601231,"access_level":"open_access","checksum":"5039752f644c4b72b9361d21a5e31baf","relation":"main_file","file_id":"8610"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","article_processing_charge":"No","citation":{"ista":"Chatterjee K, Henzinger TA, Otop J. 2020. Multi-dimensional long-run average problems for vector addition systems with states. 31st International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 171, 23.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Multi-dimensional long-run average problems for vector addition systems with states,” in <i>31st International Conference on Concurrency Theory</i>, Virtual, 2020, vol. 171.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” In <i>31st International Conference on Concurrency Theory</i>, Vol. 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">https://doi.org/10.4230/LIPIcs.CONCUR.2020.23</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2020). Multi-dimensional long-run average problems for vector addition systems with states. In <i>31st International Conference on Concurrency Theory</i> (Vol. 171). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">https://doi.org/10.4230/LIPIcs.CONCUR.2020.23</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, 31st International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","mla":"Chatterjee, Krishnendu, et al. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” <i>31st International Conference on Concurrency Theory</i>, vol. 171, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">10.4230/LIPIcs.CONCUR.2020.23</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Multi-dimensional long-run average problems for vector addition systems with states. In: <i>31st International Conference on Concurrency Theory</i>. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">10.4230/LIPIcs.CONCUR.2020.23</a>"},"ddc":["000"],"file_date_updated":"2020-10-05T14:04:25Z","oa":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"}],"arxiv":1,"date_published":"2020-08-06T00:00:00Z","day":"06","abstract":[{"lang":"eng","text":"A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating."}],"conference":{"name":"CONCUR: Conference on Concurrency Theory","end_date":"2020-09-04","start_date":"2020-09-01","location":"Virtual"},"doi":"10.4230/LIPIcs.CONCUR.2020.23","publication_status":"published","volume":171,"month":"08","tmp":{"image":"/images/cc_by.png","short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"date_updated":"2025-07-10T11:57:10Z","status":"public","quality_controlled":"1","article_number":"23","oa_version":"Published Version","_id":"8600","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF"},{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems"}],"publication":"31st International Conference on Concurrency Theory","scopus_import":"1","corr_author":"1","alternative_title":["LIPIcs"],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"type":"conference"}]