[{"publisher":"Association for Computing Machinery","isi":1,"acknowledgement":"We are very thankful to the anonymous reviewers for the helpful and valuable comments. The work was partially supported by the National Natural Science Foundation of China (NSFC) Grant No. 61802254, the Huawei Innovation Research Program, the ERC CoG 863818 (ForM-SMArt), the Facebook PhD Fellowship Program and DOC Fellowship #24956 of the Austrian Academy of Sciences (ÖAW).","doi":"10.1145/3453483.3454102","conference":{"name":"PLDI: Programming Language Design and Implementation","end_date":"2021-06-26","location":"Online","start_date":"2021-06-20"},"_id":"9646","date_published":"2021-06-01T00:00:00Z","quality_controlled":"1","department":[{"_id":"KrCh"}],"day":"01","title":"Quantitative analysis of assertion violations in probabilistic programs","oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication_identifier":{"isbn":["9781450383912"]},"article_processing_charge":"No","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies"}],"arxiv":1,"date_updated":"2025-04-15T07:55:05Z","language":[{"iso":"eng"}],"citation":{"chicago":"Wang, Jinyi, Yican Sun, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.” In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 1171–86. Association for Computing Machinery, 2021. https://doi.org/10.1145/3453483.3454102.","apa":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., & Goharshady, A. K. (2021). Quantitative analysis of assertion violations in probabilistic programs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 1171–1186). Online: Association for Computing Machinery. https://doi.org/10.1145/3453483.3454102","ieee":"J. Wang, Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Quantitative analysis of assertion violations in probabilistic programs,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Online, 2021, pp. 1171–1186.","ista":"Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. 2021. Quantitative analysis of assertion violations in probabilistic programs. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1171–1186.","ama":"Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. Quantitative analysis of assertion violations in probabilistic programs. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2021:1171-1186. doi:10.1145/3453483.3454102","mla":"Wang, Jinyi, et al. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.” Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1171–86, doi:10.1145/3453483.3454102.","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."},"ec_funded":1,"status":"public","external_id":{"arxiv":["2011.14617"],"isi":["000723661700076"]},"abstract":[{"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.","lang":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2011.14617"}],"type":"conference","date_created":"2021-07-11T22:01:18Z","scopus_import":"1","publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","oa_version":"Preprint","month":"06","publication_status":"published","year":"2021","page":"1171-1186","author":[{"full_name":"Wang, Jinyi","first_name":"Jinyi","last_name":"Wang"},{"full_name":"Sun, Yican","first_name":"Yican","last_name":"Sun"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","full_name":"Fu, Hongfei","first_name":"Hongfei","last_name":"Fu"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584"}]},{"arxiv":1,"ddc":["000"],"date_updated":"2026-04-08T07:00:30Z","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"has_accepted_license":"1","status":"public","external_id":{"arxiv":["2105.06424"],"isi":["000698732400016"]},"abstract":[{"text":"Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover, RVF-SMC generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.","lang":"eng"}],"type":"conference","corr_author":"1","scopus_import":"1","publication":"33rd International Conference on Computer-Aided Verification ","oa_version":"Published Version","date_created":"2021-09-05T22:01:24Z","language":[{"iso":"eng"}],"citation":{"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.","mla":"Agarwal, Pratyush, et al. “Stateless Model Checking under a Reads-Value-from Equivalence.” 33rd International Conference on Computer-Aided Verification , vol. 12759, Springer Nature, 2021, pp. 341–66, doi:10.1007/978-3-030-81685-8_16.","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: 33rd International Conference on Computer-Aided Verification . Vol 12759. Springer Nature; 2021:341-366. doi:10.1007/978-3-030-81685-8_16","ieee":"P. Agarwal, K. Chatterjee, S. Pathak, A. Pavlogiannis, and V. Toman, “Stateless model checking under a reads-value-from equivalence,” in 33rd International Conference on Computer-Aided Verification , Virtual, 2021, vol. 12759, pp. 341–366.","apa":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., & Toman, V. (2021). Stateless model checking under a reads-value-from equivalence. In 33rd International Conference on Computer-Aided Verification (Vol. 12759, pp. 341–366). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-81685-8_16","chicago":"Agarwal, Pratyush, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. “Stateless Model Checking under a Reads-Value-from Equivalence.” In 33rd International Conference on Computer-Aided Verification , 12759:341–66. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-81685-8_16."},"ec_funded":1,"file_date_updated":"2022-05-13T07:00:20Z","publication_status":"published","year":"2021","month":"07","volume":"12759 ","related_material":{"record":[{"relation":"dissertation_contains","id":"10199","status":"public"}]},"author":[{"first_name":"Pratyush","last_name":"Agarwal","full_name":"Agarwal, Pratyush"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Shreya","last_name":"Pathak","full_name":"Pathak, Shreya"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"orcid":"0000-0001-9036-063X","first_name":"Viktor","last_name":"Toman","full_name":"Toman, Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"alternative_title":["LNCS"],"page":"341-366","conference":{"end_date":"2021-07-23","start_date":"2021-07-20","location":"Virtual","name":"CAV: Computer Aided Verification "},"publisher":"Springer Nature","isi":1,"acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) through project ICT15-003.","file":[{"date_created":"2022-05-13T07:00:20Z","content_type":"application/pdf","access_level":"open_access","relation":"main_file","creator":"dernst","date_updated":"2022-05-13T07:00:20Z","file_name":"2021_LNCS_Agarwal.pdf","file_id":"11368","success":1,"checksum":"4b346e5fbaa8b9bdf107819c7b2aadee","file_size":1516756}],"doi":"10.1007/978-3-030-81685-8_16","quality_controlled":"1","_id":"9987","date_published":"2021-07-15T00:00:00Z","title":"Stateless model checking under a reads-value-from equivalence","oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","department":[{"_id":"KrCh"}],"day":"15","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publication_identifier":{"eisbn":["978-3-030-81685-8"],"issn":["0302-9743"],"isbn":["978-3-030-81684-1"],"eissn":["1611-3349"]},"article_processing_charge":"Yes"},{"article_processing_charge":"No","publication_identifier":{"issn":["1049-5258"]},"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (3.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode"},"license":"https://creativecommons.org/licenses/by-nc-nd/3.0/","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"title":"Infinite time horizon safety of Bayesian neural networks","day":"01","department":[{"_id":"GradSch"},{"_id":"ToHe"},{"_id":"KrCh"}],"das_tickbox":"1","_id":"10667","quality_controlled":"1","date_published":"2021-12-01T00:00:00Z","conference":{"end_date":"2021-12-10","location":"Virtual","start_date":"2021-12-06","name":"NeurIPS: Neural Information Processing Systems"},"file":[{"checksum":"0fc0f852525c10dda9cc9ffea07fb4e4","success":1,"file_name":"infinite_time_horizon_safety_o.pdf","file_id":"10682","date_updated":"2022-01-26T07:39:59Z","file_size":452492,"date_created":"2022-01-26T07:39:59Z","content_type":"application/pdf","creator":"mlechner","relation":"main_file","access_level":"open_access"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","doi":"10.48550/arXiv.2111.03165","publisher":"Neural Information Processing Systems Foundation","alternative_title":[" Advances in Neural Information Processing Systems"],"author":[{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"first_name":"Ðorđe","last_name":"Žikelić","full_name":"Žikelić, Ðorđe"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724"}],"year":"2021","publication_status":"published","file_date_updated":"2022-01-26T07:39:59Z","related_material":{"record":[{"relation":"dissertation_contains","id":"11362","status":"public"}]},"month":"12","publication":"35th Conference on Neural Information Processing Systems","date_created":"2022-01-25T15:45:58Z","oa_version":"Published Version","main_file_link":[{"url":"https://proceedings.neurips.cc/paper/2021/hash/544defa9fddff50c53b71c43e0da72be-Abstract.html","open_access":"1"}],"corr_author":"1","type":"conference","abstract":[{"text":"Bayesian neural networks (BNNs) place distributions over the weights of a neural network to model uncertainty in the data and the network's prediction. We consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with infinite time horizon systems. Compared to the existing sampling-based approaches, which are inapplicable to the infinite time horizon setting, we train a separate deterministic neural network that serves as an infinite time horizon safety certificate. In particular, we show that the certificate network guarantees the safety of the system over a subset of the BNN weight posterior's support. Our method first computes a safe weight set and then alters the BNN's weight posterior to reject samples outside this set. Moreover, we show how to extend our approach to a safe-exploration reinforcement learning setting, in order to avoid unsafe trajectories during the training of the policy. We evaluate our approach on a series of reinforcement learning benchmarks, including non-Lyapunovian safety specifications.","lang":"eng"}],"status":"public","external_id":{"arxiv":["2111.03165"]},"has_accepted_license":"1","citation":{"ista":"Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. 2021. Infinite time horizon safety of Bayesian neural networks. 35th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, .","ieee":"M. Lechner, Ð. Žikelić, K. Chatterjee, and T. A. Henzinger, “Infinite time horizon safety of Bayesian neural networks,” in 35th Conference on Neural Information Processing Systems, Virtual, 2021.","ama":"Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. Infinite time horizon safety of Bayesian neural networks. In: 35th Conference on Neural Information Processing Systems. Neural Information Processing Systems Foundation; 2021. doi:10.48550/arXiv.2111.03165","apa":"Lechner, M., Žikelić, Ð., Chatterjee, K., & Henzinger, T. A. (2021). Infinite time horizon safety of Bayesian neural networks. In 35th Conference on Neural Information Processing Systems. Virtual: Neural Information Processing Systems Foundation. https://doi.org/10.48550/arXiv.2111.03165","short":"M. Lechner, Ð. Žikelić, K. Chatterjee, T.A. Henzinger, in:, 35th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2021.","mla":"Lechner, Mathias, et al. “Infinite Time Horizon Safety of Bayesian Neural Networks.” 35th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2021, doi:10.48550/arXiv.2111.03165.","chicago":"Lechner, Mathias, Ðorđe Žikelić, Krishnendu Chatterjee, and Thomas A Henzinger. “Infinite Time Horizon Safety of Bayesian Neural Networks.” In 35th Conference on Neural Information Processing Systems. Neural Information Processing Systems Foundation, 2021. https://doi.org/10.48550/arXiv.2111.03165."},"ec_funded":1,"language":[{"iso":"eng"}],"date_updated":"2026-07-07T06:49:10Z","ddc":["000"],"arxiv":1,"project":[{"name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"665385"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}]},{"publisher":"Elsevier","isi":1,"doi":"10.1016/j.artint.2021.103499","article_number":"103499","quality_controlled":"1","_id":"9293","date_published":"2021-03-16T00:00:00Z","oa":1,"title":"Algorithms and conditional lower bounds for planning problems","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"day":"16","publication_identifier":{"issn":["0004-3702"]},"article_processing_charge":"No","date_updated":"2026-07-07T13:36:04Z","arxiv":1,"intvolume":" 297","abstract":[{"lang":"eng","text":"We consider planning problems for graphs, Markov Decision Processes (MDPs), and games on graphs in an explicit state space. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems with k different target sets: (a) the coverage problem asks whether there is a plan for each individual target set; and (b) the sequential target reachability problem asks whether the targets can be reached in a given sequence. For the coverage problem, we present a linear-time algorithm for graphs, and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds, based on the boolean matrix multiplication (BMM) conjecture and strong exponential time hypothesis (SETH), establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs, and for the sequential reachability problem games on graphs are harder than MDPs and graphs; and (ii) problem-separation results showing that for MDPs the coverage problem is harder than the sequential target problem."}],"status":"public","external_id":{"arxiv":["1804.07031"],"isi":["000657537500003"]},"oa_version":"Preprint","date_created":"2021-03-28T22:01:40Z","publication":"Artificial Intelligence","scopus_import":"1","corr_author":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.07031"}],"type":"journal_article","citation":{"short":"K. Chatterjee, W. Dvořák, M. Henzinger, A. Svozil, Artificial Intelligence 297 (2021).","mla":"Chatterjee, Krishnendu, et al. “Algorithms and Conditional Lower Bounds for Planning Problems.” Artificial Intelligence, vol. 297, no. 8, 103499, Elsevier, 2021, doi:10.1016/j.artint.2021.103499.","ama":"Chatterjee K, Dvořák W, Henzinger M, Svozil A. Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. 2021;297(8). doi:10.1016/j.artint.2021.103499","ista":"Chatterjee K, Dvořák W, Henzinger M, Svozil A. 2021. Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. 297(8), 103499.","ieee":"K. Chatterjee, W. Dvořák, M. Henzinger, and A. Svozil, “Algorithms and conditional lower bounds for planning problems,” Artificial Intelligence, vol. 297, no. 8. Elsevier, 2021.","apa":"Chatterjee, K., Dvořák, W., Henzinger, M., & Svozil, A. (2021). Algorithms and conditional lower bounds for planning problems. Artificial Intelligence. Elsevier. https://doi.org/10.1016/j.artint.2021.103499","chicago":"Chatterjee, Krishnendu, Wolfgang Dvořák, Monika Henzinger, and Alexander Svozil. “Algorithms and Conditional Lower Bounds for Planning Problems.” Artificial Intelligence. Elsevier, 2021. https://doi.org/10.1016/j.artint.2021.103499."},"article_type":"original","language":[{"iso":"eng"}],"publication_status":"published","year":"2021","month":"03","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"35"}]},"issue":"8","volume":297,"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Dvořák, Wolfgang","last_name":"Dvořák","first_name":"Wolfgang"},{"last_name":"Henzinger","first_name":"Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H"},{"last_name":"Svozil","first_name":"Alexander","full_name":"Svozil, Alexander"}]},{"abstract":[{"lang":"eng","text":"We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with n vertices and m edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires O(n2) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(nm−−√) symbolic operations and O(m−−√) symbolic space. A main open question is whether the worst-case O(n2) bound for symbolic operations can be beaten. We present a symbolic algorithm that requires O˜(n1.5) symbolic operations and O˜(n−−√) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all 0<ϵ≤1/2 the symbolic algorithm requires O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space ( O˜ hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of ω -regular objectives for MDPs. We consider the canonical parity objectives for ω -regular objectives, and for parity objectives with d -priorities we present an algorithm that computes the almost-sure winning region with O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space, for all 0<ϵ≤1/2 ."}],"external_id":{"isi":["000947350400089"],"arxiv":["2104.07466"]},"status":"public","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","scopus_import":"1","oa_version":"Preprint","date_created":"2021-09-12T22:01:24Z","type":"conference","main_file_link":[{"url":"https://arxiv.org/abs/2104.07466","open_access":"1"}],"citation":{"chicago":"Chatterjee, Krishnendu, Wolfgang Dvorak, Monika Henzinger, and Alexander Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 1–13. IEEE, 2021. https://doi.org/10.1109/LICS52264.2021.9470739.","ama":"Chatterjee K, Dvorak W, Henzinger M, Svozil A. Symbolic time and space tradeoffs for probabilistic verification. In: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2021:1-13. doi:10.1109/LICS52264.2021.9470739","ista":"Chatterjee K, Dvorak W, Henzinger M, Svozil A. 2021. Symbolic time and space tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 1–13.","ieee":"K. Chatterjee, W. Dvorak, M. Henzinger, and A. Svozil, “Symbolic time and space tradeoffs for probabilistic verification,” in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Rome, Italy, 2021, pp. 1–13.","apa":"Chatterjee, K., Dvorak, W., Henzinger, M., & Svozil, A. (2021). Symbolic time and space tradeoffs for probabilistic verification. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 1–13). Rome, Italy: IEEE. https://doi.org/10.1109/LICS52264.2021.9470739","short":"K. Chatterjee, W. Dvorak, M. Henzinger, A. Svozil, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2021, pp. 1–13.","mla":"Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2021, pp. 1–13, doi:10.1109/LICS52264.2021.9470739."},"ec_funded":1,"language":[{"iso":"eng"}],"date_updated":"2026-08-12T06:39:42Z","arxiv":1,"project":[{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Dvorak, Wolfgang","first_name":"Wolfgang","last_name":"Dvorak"},{"last_name":"Henzinger","first_name":"Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H"},{"last_name":"Svozil","first_name":"Alexander","full_name":"Svozil, Alexander"}],"page":"1-13","publication_status":"published","year":"2021","month":"07","quality_controlled":"1","_id":"10002","date_published":"2021-07-07T00:00:00Z","conference":{"end_date":"2021-07-02","location":"Rome, Italy","start_date":"2021-06-29","name":"LICS: Logic in Computer Science"},"publisher":"IEEE","doi":"10.1109/LICS52264.2021.9470739","isi":1,"acknowledgement":"The authors are grateful to the anonymous referees for their valuable comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For M. H. the research leading to these results has received funding from the European Research Council under the European Unions Seventh Framework Programme (FP/2007–2013) / ERC Grant Agreement no. 340506.","publication_identifier":{"isbn":["978-1-6654-4896-3"],"eisbn":["978-1-6654-4895-6"],"issn":["1043-6871"]},"article_processing_charge":"No","oa":1,"title":"Symbolic time and space tradeoffs for probabilistic verification","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"keyword":["Computer science","Computational modeling","Markov processes","Probabilistic logic","Formal verification","Game Theory"],"day":"07"},{"title":"Stochastic processes with expected stopping time","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"keyword":["Computer science","Heuristic algorithms","Memory management","Automata","Markov processes","Probability distribution","Complexity theory"],"day":"07","publication_identifier":{"eisbn":["978-1-6654-4895-6"],"issn":["1043-6871"],"isbn":["978-1-6654-4896-3"]},"article_processing_charge":"No","conference":{"location":"Rome, Italy","start_date":"2021-06-29","end_date":"2021-07-02","name":"LICS: Logic in Computer Science"},"publisher":"IEEE","isi":1,"acknowledgement":"We are grateful to the anonymous reviewers of LICS 2021 and of a previous version of this paper for insightful comments that helped improving the presentation. This research was partially supported by the grant ERC CoG 863818 (ForM-SMArt).","doi":"10.1109/LICS52264.2021.9470595","date_published":"2021-07-07T00:00:00Z","_id":"10004","quality_controlled":"1","publication_status":"published","year":"2021","month":"07","related_material":{"record":[{"status":"public","id":"18630","relation":"later_version"}]},"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"page":"1-13","arxiv":1,"date_updated":"2026-08-12T06:39:27Z","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"status":"public","external_id":{"arxiv":["2104.07278"],"isi":["000947350400036"]},"abstract":[{"text":"Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs.","lang":"eng"}],"type":"conference","main_file_link":[{"url":"https://arxiv.org/abs/2104.07278","open_access":"1"}],"scopus_import":"1","oa_version":"Preprint","date_created":"2021-09-12T22:01:25Z","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","language":[{"iso":"eng"}],"citation":{"chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 1–13. IEEE, 2021. https://doi.org/10.1109/LICS52264.2021.9470595.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2021, pp. 1–13, doi:10.1109/LICS52264.2021.9470595.","short":"K. Chatterjee, L. Doyen, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2021, pp. 1–13.","apa":"Chatterjee, K., & Doyen, L. (2021). Stochastic processes with expected stopping time. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 1–13). Rome, Italy: IEEE. https://doi.org/10.1109/LICS52264.2021.9470595","ieee":"K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,” in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Rome, Italy, 2021, pp. 1–13.","ama":"Chatterjee K, Doyen L. Stochastic processes with expected stopping time. In: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2021:1-13. doi:10.1109/LICS52264.2021.9470595","ista":"Chatterjee K, Doyen L. 2021. Stochastic processes with expected stopping time. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 1–13."},"ec_funded":1},{"language":[{"iso":"eng"}],"citation":{"chicago":"Schmid, Laura. “Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information.” Institute of Science and Technology Austria, 2021. https://doi.org/10.15479/at:ista:10293.","ista":"Schmid L. 2021. Evolution of cooperation via (in)direct reciprocity under imperfect information. Institute of Science and Technology Austria.","ama":"Schmid L. Evolution of cooperation via (in)direct reciprocity under imperfect information. 2021. doi:10.15479/at:ista:10293","ieee":"L. Schmid, “Evolution of cooperation via (in)direct reciprocity under imperfect information,” Institute of Science and Technology Austria, 2021.","apa":"Schmid, L. (2021). Evolution of cooperation via (in)direct reciprocity under imperfect information. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:10293","short":"L. Schmid, Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information, Institute of Science and Technology Austria, 2021.","mla":"Schmid, Laura. Evolution of Cooperation via (in)Direct Reciprocity under Imperfect Information. Institute of Science and Technology Austria, 2021, doi:10.15479/at:ista:10293."},"ec_funded":1,"status":"public","has_accepted_license":"1","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"}],"corr_author":"1","type":"dissertation","oa_version":"Published Version","date_created":"2021-11-15T17:12:57Z","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"ddc":["519","576"],"date_updated":"2026-04-08T07:11:20Z","OA_place":"publisher","page":"171","author":[{"full_name":"Schmid, Laura","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6978-7329","first_name":"Laura","last_name":"Schmid"}],"alternative_title":["ISTA Thesis"],"month":"11","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"9997"},{"relation":"part_of_dissertation","id":"9402","status":"public"},{"status":"public","id":"2","relation":"part_of_dissertation"}]},"file_date_updated":"2022-12-20T23:30:08Z","publication_status":"published","year":"2021","date_published":"2021-11-17T00:00:00Z","_id":"10293","supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"}],"publisher":"Institute of Science and Technology Austria","degree_awarded":"PhD","doi":"10.15479/at:ista:10293","file":[{"relation":"source_file","creator":"lschmid","access_level":"closed","date_created":"2021-11-18T12:41:46Z","content_type":"application/zip","file_size":29703124,"embargo_to":"open_access","checksum":"86a05b430756ca12ae8107b6e6f3c1e5","date_updated":"2022-12-20T23:30:08Z","file_name":"submission_new.zip","file_id":"10305"},{"content_type":"application/pdf","date_created":"2021-11-18T12:59:15Z","relation":"main_file","creator":"lschmid","access_level":"open_access","checksum":"d940af042e94660c6b6a7b4f0b184d47","date_updated":"2022-12-20T23:30:08Z","embargo":"2022-10-18","file_name":"thesis_new_upload.pdf","file_id":"10306","file_size":8320985}],"publication_identifier":{"issn":["2663-337X"]},"article_processing_charge":"No","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"day":"17","title":"Evolution of cooperation via (in)direct reciprocity under imperfect information","oa":1,"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd"},{"language":[{"iso":"eng"}],"citation":{"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.","ama":"Schmid L, Shati P, Hilbe C, Chatterjee K. The evolution of indirect reciprocity under action and assessment generosity. Scientific Reports. 2021;11(1). doi:10.1038/s41598-021-96932-1","ieee":"L. Schmid, P. Shati, C. Hilbe, and K. Chatterjee, “The evolution of indirect reciprocity under action and assessment generosity,” Scientific Reports, vol. 11, no. 1. Springer Nature, 2021.","apa":"Schmid, L., Shati, P., Hilbe, C., & Chatterjee, K. (2021). The evolution of indirect reciprocity under action and assessment generosity. Scientific Reports. Springer Nature. https://doi.org/10.1038/s41598-021-96932-1","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.” Scientific Reports, vol. 11, no. 1, 17443, Springer Nature, 2021, doi:10.1038/s41598-021-96932-1.","chicago":"Schmid, Laura, Pouya Shati, Christian Hilbe, and Krishnendu Chatterjee. “The Evolution of Indirect Reciprocity under Action and Assessment Generosity.” Scientific Reports. Springer Nature, 2021. https://doi.org/10.1038/s41598-021-96932-1."},"ec_funded":1,"article_type":"original","type":"journal_article","corr_author":"1","oa_version":"Published Version","date_created":"2021-09-11T16:22:02Z","publication":"Scientific Reports","scopus_import":"1","status":"public","external_id":{"pmid":["34465830"],"isi":["000692406400018"]},"has_accepted_license":"1","abstract":[{"text":"Indirect reciprocity is a mechanism for the evolution of cooperation based on social norms. This mechanism requires that individuals in a population observe and judge each other’s behaviors. Individuals with a good reputation are more likely to receive help from others. Previous work suggests that indirect reciprocity is only effective when all relevant information is reliable and publicly available. Otherwise, individuals may disagree on how to assess others, even if they all apply the same social norm. Such disagreements can lead to a breakdown of cooperation. Here we explore whether the predominantly studied ‘leading eight’ social norms of indirect reciprocity can be made more robust by equipping them with an element of generosity. To this end, we distinguish between two kinds of generosity. According to assessment generosity, individuals occasionally assign a good reputation to group members who would usually be regarded as bad. According to action generosity, individuals occasionally cooperate with group members with whom they would usually defect. Using individual-based simulations, we show that the two kinds of generosity have a very different effect on the resulting reputation dynamics. Assessment generosity tends to add to the overall noise and allows defectors to invade. In contrast, a limited amount of action generosity can be beneficial in a few cases. However, even when action generosity is beneficial, the respective simulations do not result in full cooperation. Our results suggest that while generosity can favor cooperation when individuals use the most simple strategies of reciprocity, it is disadvantageous when individuals use more complex social norms.","lang":"eng"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"intvolume":" 11","ddc":["003"],"date_updated":"2026-09-03T22:30:50Z","pmid":1,"author":[{"id":"38B437DE-F248-11E8-B48F-1D18A9856A87","full_name":"Schmid, Laura","first_name":"Laura","orcid":"0000-0002-6978-7329","last_name":"Schmid"},{"first_name":"Pouya","last_name":"Shati","full_name":"Shati, Pouya"},{"first_name":"Christian","last_name":"Hilbe","full_name":"Hilbe, Christian"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"}],"volume":11,"related_material":{"record":[{"status":"public","id":"10293","relation":"dissertation_contains"}]},"issue":"1","month":"08","year":"2021","publication_status":"published","file_date_updated":"2021-09-13T10:31:21Z","date_published":"2021-08-31T00:00:00Z","_id":"9997","quality_controlled":"1","article_number":"17443","file":[{"content_type":"application/pdf","date_created":"2021-09-13T10:31:21Z","access_level":"open_access","relation":"main_file","creator":"cchlebak","date_updated":"2021-09-13T10:31:21Z","file_name":"2021_ScientificReports_Schmid.pdf","file_id":"10006","checksum":"19df8816cf958b272b85841565c73182","success":1,"file_size":2424943}],"isi":1,"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).","doi":"10.1038/s41598-021-96932-1","publisher":"Springer Nature","article_processing_charge":"Yes","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publication_identifier":{"eissn":["2045-2322"]},"day":"31","keyword":["Multidisciplinary"],"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","title":"The evolution of indirect reciprocity under action and assessment generosity","oa":1},{"publication_identifier":{"eissn":["2397-3374"]},"article_processing_charge":"No","title":"A unified framework of direct and indirect reciprocity","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"day":"13","quality_controlled":"1","_id":"9402","date_published":"2021-05-13T00:00:00Z","publisher":"Springer Nature","isi":1,"file":[{"date_created":"2023-11-07T08:27:23Z","content_type":"application/pdf","relation":"main_file","creator":"dernst","access_level":"open_access","success":1,"checksum":"34f55e173f90dc1dab731063458ac780","date_updated":"2023-11-07T08:27:23Z","file_id":"14496","file_name":"2021_NatureHumanBehaviour_Schmid_accepted.pdf","file_size":5232761}],"doi":"10.1038/s41562-021-01114-8","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.","author":[{"full_name":"Schmid, Laura","id":"38B437DE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6978-7329","first_name":"Laura","last_name":"Schmid"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0001-5116-955X","first_name":"Christian","last_name":"Hilbe","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin A.","last_name":"Nowak","full_name":"Nowak, Martin A."}],"page":"1292–1302","pmid":1,"publication_status":"published","file_date_updated":"2023-11-07T08:27:23Z","year":"2021","month":"05","volume":5,"related_material":{"record":[{"status":"public","id":"10293","relation":"dissertation_contains"}],"link":[{"description":"News on IST Homepage","relation":"press_release","url":"https://ist.ac.at/en/news/the-emergence-of-cooperation/"}]},"issue":"10","status":"public","external_id":{"pmid":["33986519"],"isi":["000650304000002"]},"has_accepted_license":"1","abstract":[{"lang":"eng","text":"Direct and indirect reciprocity are key mechanisms for the evolution of cooperation. Direct reciprocity means that individuals use their own experience to decide whether to cooperate with another person. Indirect reciprocity means that they also consider the experiences of others. Although these two mechanisms are intertwined, they are typically studied in isolation. Here, we introduce a mathematical framework that allows us to explore both kinds of reciprocity simultaneously. We show that the well-known ‘generous tit-for-tat’ strategy of direct reciprocity has a natural analogue in indirect reciprocity, which we call ‘generous scoring’. Using an equilibrium analysis, we characterize under which conditions either of the two strategies can maintain cooperation. With simulations, we additionally explore which kind of reciprocity evolves when members of a population engage in social learning to adapt to their environment. Our results draw unexpected connections between direct and indirect reciprocity while highlighting important differences regarding their evolvability."}],"corr_author":"1","type":"journal_article","scopus_import":"1","oa_version":"Submitted Version","date_created":"2021-05-18T16:56:57Z","publication":"Nature Human Behaviour","language":[{"iso":"eng"}],"article_type":"original","citation":{"short":"L. Schmid, K. Chatterjee, C. Hilbe, M.A. Nowak, Nature Human Behaviour 5 (2021) 1292–1302.","mla":"Schmid, Laura, et al. “A Unified Framework of Direct and Indirect Reciprocity.” Nature Human Behaviour, vol. 5, no. 10, Springer Nature, 2021, pp. 1292–1302, doi:10.1038/s41562-021-01114-8.","ieee":"L. Schmid, K. Chatterjee, C. Hilbe, and M. A. Nowak, “A unified framework of direct and indirect reciprocity,” Nature Human Behaviour, 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.","ama":"Schmid L, Chatterjee K, Hilbe C, Nowak MA. A unified framework of direct and indirect reciprocity. Nature Human Behaviour. 2021;5(10):1292–1302. doi:10.1038/s41562-021-01114-8","apa":"Schmid, L., Chatterjee, K., Hilbe, C., & Nowak, M. A. (2021). A unified framework of direct and indirect reciprocity. Nature Human Behaviour. Springer Nature. https://doi.org/10.1038/s41562-021-01114-8","chicago":"Schmid, Laura, Krishnendu Chatterjee, Christian Hilbe, and Martin A. Nowak. “A Unified Framework of Direct and Indirect Reciprocity.” Nature Human Behaviour. Springer Nature, 2021. https://doi.org/10.1038/s41562-021-01114-8."},"ec_funded":1,"ddc":["000"],"date_updated":"2026-09-03T22:30:51Z","intvolume":" 5","project":[{"grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"}]},{"page":"278","author":[{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady"}],"alternative_title":["ISTA Thesis"],"month":"01","related_material":{"record":[{"relation":"part_of_dissertation","id":"6490","status":"public"},{"status":"public","id":"6780","relation":"part_of_dissertation"},{"status":"public","id":"7158","relation":"part_of_dissertation"},{"id":"66","status":"public","relation":"part_of_dissertation"},{"id":"6378","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"311","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"6175"},{"relation":"part_of_dissertation","status":"public","id":"6340"},{"relation":"part_of_dissertation","id":"7014","status":"public"},{"relation":"part_of_dissertation","id":"6009","status":"public"},{"relation":"part_of_dissertation","id":"1437","status":"public"},{"relation":"part_of_dissertation","id":"8728","status":"public"},{"status":"public","id":"8089","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","status":"public","id":"6380"},{"status":"public","id":"5977","relation":"part_of_dissertation"},{"status":"public","id":"6056","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"639","status":"public"},{"relation":"part_of_dissertation","id":"1386","status":"public"},{"id":"6918","status":"public","relation":"part_of_dissertation"},{"id":"7810","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"949","status":"public"}]},"file_date_updated":"2021-12-23T23:30:04Z","publication_status":"published","year":"2021","language":[{"iso":"eng"}],"citation":{"short":"A.K. Goharshady, Parameterized and Algebro-Geometric Advances in Static Program Analysis, Institute of Science and Technology Austria, 2021.","mla":"Goharshady, Amir Kafshdar. Parameterized and Algebro-Geometric Advances in Static Program Analysis. Institute of Science and Technology Austria, 2021, doi:10.15479/AT:ISTA:8934.","ama":"Goharshady AK. Parameterized and algebro-geometric advances in static program analysis. 2021. doi:10.15479/AT:ISTA:8934","ista":"Goharshady AK. 2021. Parameterized and algebro-geometric advances in static program analysis. Institute of Science and Technology Austria.","ieee":"A. K. Goharshady, “Parameterized and algebro-geometric advances in static program analysis,” Institute of Science and Technology Austria, 2021.","apa":"Goharshady, A. K. (2021). Parameterized and algebro-geometric advances in static program analysis. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:8934","chicago":"Goharshady, Amir Kafshdar. “Parameterized and Algebro-Geometric Advances in Static Program Analysis.” Institute of Science and Technology Austria, 2021. https://doi.org/10.15479/AT:ISTA:8934."},"status":"public","has_accepted_license":"1","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"}],"corr_author":"1","type":"dissertation","date_created":"2020-12-10T12:17:07Z","oa_version":"Published Version","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"}],"ddc":["005"],"date_updated":"2026-04-16T10:07:18Z","OA_place":"publisher","tmp":{"short":"CC0 (1.0)","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","image":"/images/cc_0.png","name":"Creative Commons Public Domain Dedication (CC0 1.0)"},"publication_identifier":{"issn":["2663-337X"]},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"day":"01","title":"Parameterized and algebro-geometric advances in static program analysis","oa":1,"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","date_published":"2021-01-01T00:00:00Z","_id":"8934","supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"}],"publisher":"Institute of Science and Technology Austria","degree_awarded":"PhD","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).","file":[{"file_name":"Thesis-pdfa.pdf","file_id":"8969","date_updated":"2021-12-23T23:30:04Z","embargo":"2021-12-22","checksum":"d1b9db3725aed34dadd81274aeb9426c","file_size":5251507,"content_type":"application/pdf","date_created":"2020-12-22T20:08:44Z","access_level":"open_access","creator":"akafshda","relation":"main_file"},{"file_name":"source.zip","file_id":"8970","date_updated":"2021-03-04T23:30:04Z","checksum":"1661df7b393e6866d2460eba3c905130","embargo_to":"open_access","file_size":10636756,"date_created":"2020-12-22T20:08:50Z","content_type":"application/zip","access_level":"closed","creator":"akafshda","relation":"source_file"}]},{"tmp":{"short":"CC0 (1.0)","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","image":"/images/cc_0.png","name":"Creative Commons Public Domain Dedication (CC0 1.0)"},"article_processing_charge":"No","author":[{"full_name":"Milutinovic, Barbara","id":"2CDC32B8-F248-11E8-B48F-1D18A9856A87","last_name":"Milutinovic","orcid":"0000-0002-8214-4758","first_name":"Barbara"},{"id":"42462816-F248-11E8-B48F-1D18A9856A87","full_name":"Stock, Miriam","last_name":"Stock","first_name":"Miriam"},{"last_name":"Grasse","first_name":"Anna V","id":"406F989C-F248-11E8-B48F-1D18A9856A87","full_name":"Grasse, Anna V"},{"first_name":"Elisabeth","last_name":"Naderlinger","full_name":"Naderlinger, Elisabeth","id":"31757262-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Christian","orcid":"0000-0001-5116-955X","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian"},{"last_name":"Cremer","orcid":"0000-0002-2193-3868","first_name":"Sylvia","full_name":"Cremer, Sylvia","id":"2F64EC8C-F248-11E8-B48F-1D18A9856A87"}],"department":[{"_id":"SyCr"},{"_id":"KrCh"}],"month":"12","related_material":{"record":[{"relation":"used_in_publication","id":"7343","status":"public"}]},"day":"19","oa":1,"title":"Social immunity modulates competition between coinfecting pathogens","year":"2020","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Milutinovic, B., Stock, M., Grasse, A. V., Naderlinger, E., Hilbe, C., & Cremer, S. (2020). Social immunity modulates competition between coinfecting pathogens. Dryad. https://doi.org/10.5061/DRYAD.CRJDFN318","ista":"Milutinovic B, Stock M, Grasse AV, Naderlinger E, Hilbe C, Cremer S. 2020. Social immunity modulates competition between coinfecting pathogens, Dryad, 10.5061/DRYAD.CRJDFN318.","ieee":"B. Milutinovic, M. Stock, A. V. Grasse, E. Naderlinger, C. Hilbe, and S. Cremer, “Social immunity modulates competition between coinfecting pathogens.” Dryad, 2020.","ama":"Milutinovic B, Stock M, Grasse AV, Naderlinger E, Hilbe C, Cremer S. Social immunity modulates competition between coinfecting pathogens. 2020. doi:10.5061/DRYAD.CRJDFN318","mla":"Milutinovic, Barbara, et al. Social Immunity Modulates Competition between Coinfecting Pathogens. Dryad, 2020, doi:10.5061/DRYAD.CRJDFN318.","short":"B. Milutinovic, M. Stock, A.V. Grasse, E. Naderlinger, C. Hilbe, S. Cremer, (2020).","chicago":"Milutinovic, Barbara, Miriam Stock, Anna V Grasse, Elisabeth Naderlinger, Christian Hilbe, and Sylvia Cremer. “Social Immunity Modulates Competition between Coinfecting Pathogens.” Dryad, 2020. https://doi.org/10.5061/DRYAD.CRJDFN318."},"date_published":"2020-12-19T00:00:00Z","_id":"13060","abstract":[{"lang":"eng","text":"Coinfections with multiple pathogens can result in complex within-host dynamics affecting virulence and transmission. Whilst multiple infections are intensively studied in solitary hosts, it is so far unresolved how social host interactions interfere with pathogen competition, and if this depends on coinfection diversity. We studied how the collective disease defenses of ants – their social immunity – influence pathogen competition in coinfections of same or different fungal pathogen species. Social immunity reduced virulence for all pathogen combinations, but interfered with spore production only in different-species coinfections. Here, it decreased overall pathogen sporulation success, whilst simultaneously increasing co-sporulation on individual cadavers and maintaining a higher pathogen diversity at the community-level. Mathematical modeling revealed that host sanitary care alone can modulate competitive outcomes between pathogens, giving advantage to fast-germinating, thus less grooming-sensitive ones. Host social interactions can hence modulate infection dynamics in coinfected group members, thereby altering pathogen communities at the host- and population-level."}],"status":"public","oa_version":"Published Version","date_created":"2023-05-23T16:11:22Z","corr_author":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5061/dryad.crjdfn318"}],"type":"research_data_reference","publisher":"Dryad","doi":"10.5061/DRYAD.CRJDFN318","date_updated":"2025-06-12T07:32:35Z","ddc":["570"]},{"intvolume":" 34","date_updated":"2025-04-15T06:30:08Z","arxiv":1,"project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF","grant_number":"S11407"}],"oa_version":"Preprint","publication":"Proceedings of the 34th AAAI Conference on Artificial Intelligence","date_created":"2024-03-04T08:07:22Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2002.12086","open_access":"1"}],"type":"journal_article","abstract":[{"lang":"eng","text":"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."}],"status":"public","external_id":{"arxiv":["2002.12086"]},"citation":{"ieee":"T. Brázdil, K. Chatterjee, P. Novotný, and J. Vahala, “Reinforcement learning of risk-constrained policies in Markov decision processes,” Proceedings of the 34th AAAI Conference on Artificial Intelligence, vol. 34, no. 06. Association for the Advancement of Artificial Intelligence, pp. 9794–9801, 2020.","ama":"Brázdil T, Chatterjee K, Novotný P, Vahala J. Reinforcement learning of risk-constrained policies in Markov decision processes. Proceedings of the 34th AAAI Conference on Artificial Intelligence. 2020;34(06):9794-9801. doi:10.1609/aaai.v34i06.6531","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.","apa":"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. New York, NY, United States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v34i06.6531","short":"T. Brázdil, K. Chatterjee, P. Novotný, J. Vahala, Proceedings of the 34th AAAI Conference on Artificial Intelligence 34 (2020) 9794–9801.","mla":"Brázdil, Tomáš, et al. “Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes.” Proceedings of the 34th AAAI Conference on Artificial Intelligence, vol. 34, no. 06, Association for the Advancement of Artificial Intelligence, 2020, pp. 9794–801, doi:10.1609/aaai.v34i06.6531.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Petr Novotný, and Jiří Vahala. “Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes.” Proceedings of the 34th AAAI Conference on Artificial Intelligence. Association for the Advancement of Artificial Intelligence, 2020. https://doi.org/10.1609/aaai.v34i06.6531."},"article_type":"original","language":[{"iso":"eng"}],"year":"2020","publication_status":"published","issue":"06","volume":34,"month":"04","author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Petr","last_name":"Novotný","full_name":"Novotný, Petr"},{"first_name":"Jiří","last_name":"Vahala","full_name":"Vahala, Jiří"}],"page":"9794-9801","conference":{"start_date":"2020-02-07","location":"New York, NY, United States","end_date":"2020-02-12","name":"AAAI: Conference on Artificial Intelligence"},"doi":"10.1609/aaai.v34i06.6531","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.","publisher":"Association for the Advancement of Artificial Intelligence","_id":"15055","quality_controlled":"1","date_published":"2020-04-03T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"title":"Reinforcement learning of risk-constrained policies in Markov decision processes","day":"03","keyword":["General Medicine"],"department":[{"_id":"KrCh"}],"article_processing_charge":"No","publication_identifier":{"issn":["2374-3468"]}},{"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.","date_updated":"2026-06-18T17:45:52Z","conference":{"name":"EuroCG: European Workshop on Computational Geometry","location":"Würzburg, Germany, Virtual","start_date":"2020-03-16","end_date":"2020-03-18"},"ddc":["000"],"citation":{"mla":"Aichholzer, Oswin, et al. “Disjoint Tree-Compatible Plane Perfect Matchings.” 36th European Workshop on Computational Geometry, 56, 2020.","short":"O. Aichholzer, J. Obmann, P. Patak, D. Perz, J. Tkadlec, in:, 36th European Workshop on Computational Geometry, 2020.","apa":"Aichholzer, O., Obmann, J., Patak, P., Perz, D., & Tkadlec, J. (2020). Disjoint tree-compatible plane perfect matchings. In 36th European Workshop on Computational Geometry. Würzburg, Germany, Virtual.","ieee":"O. Aichholzer, J. Obmann, P. Patak, D. Perz, and J. Tkadlec, “Disjoint tree-compatible plane perfect matchings,” in 36th European Workshop on Computational Geometry, Würzburg, Germany, Virtual, 2020.","ama":"Aichholzer O, Obmann J, Patak P, Perz D, Tkadlec J. Disjoint tree-compatible plane perfect matchings. In: 36th European Workshop on Computational Geometry. ; 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.","chicago":"Aichholzer, Oswin, Julia Obmann, Pavel Patak, Daniel Perz, and Josef Tkadlec. “Disjoint Tree-Compatible Plane Perfect Matchings.” In 36th European Workshop on Computational Geometry, 2020."},"language":[{"iso":"eng"}],"article_number":"56","date_published":"2020-04-01T00:00:00Z","_id":"15082","quality_controlled":"1","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."}],"status":"public","oa_version":"Published Version","publication":"36th European Workshop on Computational Geometry","date_created":"2024-03-05T08:57:17Z","corr_author":"1","main_file_link":[{"url":"https://www1.pub.informatik.uni-wuerzburg.de/eurocg2020/data/uploads/papers/eurocg20_paper_56.pdf","open_access":"1"}],"type":"conference","department":[{"_id":"KrCh"},{"_id":"UlWa"}],"month":"04","day":"01","publication_status":"published","oa":1,"title":"Disjoint tree-compatible plane perfect matchings","year":"2020","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","author":[{"full_name":"Aichholzer, Oswin","first_name":"Oswin","last_name":"Aichholzer"},{"full_name":"Obmann, Julia","last_name":"Obmann","first_name":"Julia"},{"full_name":"Patak, Pavel","id":"B593B804-1035-11EA-B4F1-947645A5BB83","first_name":"Pavel","last_name":"Patak"},{"last_name":"Perz","first_name":"Daniel","full_name":"Perz, Daniel"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","first_name":"Josef","last_name":"Tkadlec"}]},{"project":[{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"}],"ddc":["000"],"date_updated":"2025-09-23T12:10:25Z","OA_place":"publisher","language":[{"iso":"eng"}],"citation":{"chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Petr Novotný. “Termination Analysis of Probabilistic Programs with Martingales.” In Foundations of Probabilistic Programming, 221–58. Cambridge University Press, 2020. https://doi.org/10.1017/9781108770750.008.","apa":"Chatterjee, K., Fu, H., & Novotný, P. (2020). Termination Analysis of Probabilistic Programs with Martingales. In Foundations of Probabilistic Programming (pp. 221–258). Cambridge University Press. https://doi.org/10.1017/9781108770750.008","ama":"Chatterjee K, Fu H, Novotný P. Termination Analysis of Probabilistic Programs with Martingales. In: Foundations of Probabilistic Programming. Cambridge University Press; 2020:221-258. doi:10.1017/9781108770750.008","ieee":"K. Chatterjee, H. Fu, and P. Novotný, “Termination Analysis of Probabilistic Programs with Martingales,” in Foundations of Probabilistic Programming, 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.” Foundations of Probabilistic Programming, Cambridge University Press, 2020, pp. 221–58, doi:10.1017/9781108770750.008.","short":"K. Chatterjee, H. Fu, P. Novotný, in:, Foundations of Probabilistic Programming, Cambridge University Press, 2020, pp. 221–258."},"status":"public","has_accepted_license":"1","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"}],"type":"book_chapter","corr_author":"1","oa_version":"Published Version","date_created":"2025-07-10T13:28:51Z","publication":"Foundations of Probabilistic Programming","month":"11","file_date_updated":"2025-09-23T12:03:09Z","publication_status":"published","year":"2020","page":"221-258","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei"},{"last_name":"Novotný","first_name":"Petr","full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Cambridge University Press","file":[{"file_size":316681,"checksum":"28ece115e8d2d9263e253a598e7caef2","success":1,"file_name":"2020_ProbProgramming_Chatterjee.pdf","file_id":"20380","date_updated":"2025-09-23T12:03:09Z","creator":"dernst","relation":"main_file","access_level":"open_access","content_type":"application/pdf","date_created":"2025-09-23T12:03:09Z"}],"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.","quality_controlled":"1","_id":"19986","date_published":"2020-11-18T00:00:00Z","department":[{"_id":"KrCh"}],"day":"18","title":"Termination Analysis of Probabilistic Programs with Martingales","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publication_identifier":{"eisbn":["9781108770750"],"isbn":["9781108488518"]},"article_processing_charge":"No"},{"page":"102-115","author":[{"last_name":"Ashok","first_name":"Pranav","full_name":"Ashok, Pranav"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian"},{"first_name":"Tobias","last_name":"Winkler","full_name":"Winkler, Tobias"}],"month":"07","year":"2020","file_date_updated":"2020-11-25T09:38:14Z","publication_status":"published","citation":{"ama":"Ashok P, Chatterjee K, Kretinsky J, Weininger M, Winkler T. Approximating values of generalized-reachability stochastic games. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science . Association for Computing Machinery; 2020:102-115. doi:10.1145/3373718.3394761","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.","ieee":"P. Ashok, K. Chatterjee, J. Kretinsky, M. Weininger, and T. Winkler, “Approximating values of generalized-reachability stochastic games,” in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , Saarbrücken, Germany, 2020, pp. 102–115.","apa":"Ashok, P., Chatterjee, K., Kretinsky, J., Weininger, M., & Winkler, T. (2020). Approximating values of generalized-reachability stochastic games. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 102–115). Saarbrücken, Germany: Association for Computing Machinery. https://doi.org/10.1145/3373718.3394761","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.","mla":"Ashok, Pranav, et al. “Approximating Values of Generalized-Reachability Stochastic Games.” Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , Association for Computing Machinery, 2020, pp. 102–15, doi:10.1145/3373718.3394761.","chicago":"Ashok, Pranav, Krishnendu Chatterjee, Jan Kretinsky, Maximilian Weininger, and Tobias Winkler. “Approximating Values of Generalized-Reachability Stochastic Games.” In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , 102–15. Association for Computing Machinery, 2020. https://doi.org/10.1145/3373718.3394761."},"ec_funded":1,"language":[{"iso":"eng"}],"publication":"Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science ","date_created":"2020-06-14T22:00:48Z","oa_version":"Published Version","scopus_import":"1","type":"conference","abstract":[{"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.","lang":"eng"}],"external_id":{"arxiv":["1908.05106"],"isi":["000665014900010"]},"status":"public","has_accepted_license":"1","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"date_updated":"2025-07-10T11:54:53Z","arxiv":1,"ddc":["000"],"article_processing_charge":"No","publication_identifier":{"isbn":["9781450371049"]},"day":"08","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"title":"Approximating values of generalized-reachability stochastic games","_id":"7955","quality_controlled":"1","date_published":"2020-07-08T00:00:00Z","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.","isi":1,"doi":"10.1145/3373718.3394761","file":[{"access_level":"open_access","relation":"main_file","creator":"dernst","date_created":"2020-11-25T09:38:14Z","content_type":"application/pdf","file_size":1001395,"date_updated":"2020-11-25T09:38:14Z","file_name":"2020_LICS_Ashok.pdf","file_id":"8804","success":1,"checksum":"d0d0288fe991dd16cf5f02598b794240"}],"publisher":"Association for Computing Machinery","conference":{"name":"LICS: Logic in Computer Science","location":"Saarbrücken, Germany","start_date":"2020-07-08","end_date":"2020-07-11"}},{"date_updated":"2026-04-08T07:26:44Z","intvolume":" 30","project":[{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"}],"abstract":[{"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.","lang":"eng"}],"status":"public","oa_version":"None","scopus_import":"1","publication":"Proceedings of the 30th International Conference on Automated Planning and Scheduling","date_created":"2020-08-02T22:00:58Z","type":"conference","citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, Deep Karkhanis, Petr Novotný, and Amélie Royer. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” In Proceedings of the 30th International Conference on Automated Planning and Scheduling, 30:48–56. Association for the Advancement of Artificial Intelligence, 2020.","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.","mla":"Chatterjee, Krishnendu, et al. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” Proceedings of the 30th International Conference on Automated Planning and Scheduling, vol. 30, Association for the Advancement of Artificial Intelligence, 2020, 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.","ieee":"K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, and A. Royer, “Multiple-environment Markov decision processes: Efficient analysis and applications,” in Proceedings of the 30th International Conference on Automated Planning and Scheduling, Nancy, France, 2020, vol. 30, pp. 48–56.","ama":"Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. Multiple-environment Markov decision processes: Efficient analysis and applications. In: Proceedings of the 30th International Conference on Automated Planning and Scheduling. Vol 30. Association for the Advancement of Artificial Intelligence; 2020:48-56.","apa":"Chatterjee, K., Chmelik, M., Karkhanis, D., Novotný, P., & Royer, A. (2020). Multiple-environment Markov decision processes: Efficient analysis and applications. In Proceedings of the 30th International Conference on Automated Planning and Scheduling (Vol. 30, pp. 48–56). Nancy, France: Association for the Advancement of Artificial Intelligence."},"language":[{"iso":"eng"}],"publication_status":"published","year":"2020","month":"06","related_material":{"record":[{"status":"public","id":"8390","relation":"dissertation_contains"}]},"volume":30,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Karkhanis, Deep","last_name":"Karkhanis","first_name":"Deep"},{"last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"last_name":"Royer","first_name":"Amélie","orcid":"0000-0002-8407-0705","id":"3811D890-F248-11E8-B48F-1D18A9856A87","full_name":"Royer, Amélie"}],"page":"48-56","conference":{"name":"ICAPS: International Conference on Automated Planning and Scheduling","end_date":"2020-10-30","start_date":"2020-10-26","location":"Nancy, France"},"publisher":"Association for the Advancement of Artificial Intelligence","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.","date_published":"2020-06-01T00:00:00Z","_id":"8193","quality_controlled":"1","title":"Multiple-environment Markov decision processes: Efficient analysis and applications","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"day":"01","publication_identifier":{"issn":["2334-0835"],"eissn":["2334-0843"]},"article_processing_charge":"No"},{"conference":{"name":"CAV: Computer Aided Verification"},"publisher":"Springer Nature","isi":1,"file":[{"file_name":"2020_LNCS_CAV_Chatterjee.pdf","file_id":"8276","date_updated":"2020-08-17T11:32:44Z","checksum":"093d4788d7d5b2ce0ffe64fbe7820043","success":1,"file_size":625056,"content_type":"application/pdf","date_created":"2020-08-17T11:32:44Z","access_level":"open_access","creator":"dernst","relation":"main_file"}],"doi":"10.1007/978-3-030-53291-8_21","quality_controlled":"1","_id":"8272","date_published":"2020-07-14T00:00:00Z","title":"Stochastic games with lexicographic reachability-safety objectives","oa":1,"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","department":[{"_id":"KrCh"}],"day":"14","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783030532901"],"issn":["0302-9743"]},"article_processing_charge":"No","arxiv":1,"ddc":["000"],"date_updated":"2026-04-16T09:31:14Z","intvolume":" 12225","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","status":"public","external_id":{"arxiv":["2005.04018"],"isi":["000695272500021"]},"abstract":[{"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.","lang":"eng"}],"type":"conference","publication":"International Conference on Computer Aided Verification","date_created":"2020-08-16T22:00:58Z","oa_version":"Published Version","scopus_import":"1","language":[{"iso":"eng"}],"citation":{"ieee":"K. Chatterjee, J. P. Katoen, M. Weininger, and T. Winkler, “Stochastic games with lexicographic reachability-safety objectives,” in International Conference on Computer Aided Verification, 2020, vol. 12225, pp. 398–420.","ama":"Chatterjee K, Katoen JP, Weininger M, Winkler T. Stochastic games with lexicographic reachability-safety objectives. In: International Conference on Computer Aided Verification. Vol 12225. Springer Nature; 2020:398-420. doi:10.1007/978-3-030-53291-8_21","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.","apa":"Chatterjee, K., Katoen, J. P., Weininger, M., & Winkler, T. (2020). Stochastic games with lexicographic reachability-safety objectives. In International Conference on Computer Aided Verification (Vol. 12225, pp. 398–420). Springer Nature. https://doi.org/10.1007/978-3-030-53291-8_21","short":"K. Chatterjee, J.P. Katoen, M. Weininger, T. Winkler, in:, International Conference on Computer Aided Verification, Springer Nature, 2020, pp. 398–420.","mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Reachability-Safety Objectives.” International Conference on Computer Aided Verification, vol. 12225, Springer Nature, 2020, pp. 398–420, doi:10.1007/978-3-030-53291-8_21.","chicago":"Chatterjee, Krishnendu, Joost P Katoen, Maximilian Weininger, and Tobias Winkler. “Stochastic Games with Lexicographic Reachability-Safety Objectives.” In International Conference on Computer Aided Verification, 12225:398–420. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-53291-8_21."},"ec_funded":1,"publication_status":"published","file_date_updated":"2020-08-17T11:32:44Z","year":"2020","month":"07","volume":12225,"related_material":{"record":[{"relation":"later_version","id":"12738","status":"public"}]},"author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P","last_name":"Katoen","first_name":"Joost P","orcid":"0000-0002-6143-1926"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian"},{"full_name":"Winkler, Tobias","first_name":"Tobias","last_name":"Winkler"}],"alternative_title":["LNCS"],"page":"398-420"},{"article_number":"25","quality_controlled":"1","_id":"8324","date_published":"2020-01-01T00:00:00Z","publisher":"ACM","file":[{"file_size":564151,"checksum":"c6193d109ff4ecb17e7a6513d8eb34c0","success":1,"date_updated":"2020-09-01T11:12:58Z","file_id":"8328","file_name":"2019_ACM_POPL_Wang.pdf","relation":"main_file","creator":"cziletti","access_level":"open_access","content_type":"application/pdf","date_created":"2020-09-01T11:12:58Z"}],"doi":"10.1145/3371093","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.","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publication_identifier":{"eissn":["2475-1421"]},"article_processing_charge":"No","department":[{"_id":"KrCh"}],"day":"01","title":"Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time","oa":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"citation":{"apa":"Wang, P., Fu, H., Chatterjee, K., Deng, Y., & Xu, M. (2020). Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In Proceedings of the ACM on Programming Languages (Vol. 4). ACM. https://doi.org/10.1145/3371093","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 Proceedings of the ACM on Programming Languages, 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: Proceedings of the ACM on Programming Languages. Vol 4. ACM; 2020. doi:10.1145/3371093","mla":"Wang, Peixin, et al. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, 25, ACM, 2020, doi:10.1145/3371093.","short":"P. Wang, H. Fu, K. Chatterjee, Y. Deng, M. Xu, in:, Proceedings of the ACM on Programming Languages, ACM, 2020.","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 Proceedings of the ACM on Programming Languages, Vol. 4. ACM, 2020. https://doi.org/10.1145/3371093."},"has_accepted_license":"1","external_id":{"arxiv":["1902.04744"]},"status":"public","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"}],"type":"conference","date_created":"2020-08-30T22:01:12Z","publication":"Proceedings of the ACM on Programming Languages","scopus_import":"1","oa_version":"Published Version","project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"}],"ddc":["004"],"arxiv":1,"date_updated":"2025-04-15T06:30:10Z","intvolume":" 4","author":[{"first_name":"Peixin","last_name":"Wang","full_name":"Wang, Peixin"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Yuxin","last_name":"Deng","full_name":"Deng, Yuxin"},{"full_name":"Xu, Ming","first_name":"Ming","last_name":"Xu"}],"month":"01","volume":4,"related_material":{"link":[{"url":"https://doi.org/10.5281/zenodo.3533633","relation":"software"}]},"issue":"POPL","file_date_updated":"2020-09-01T11:12:58Z","publication_status":"published","year":"2020"},{"article_processing_charge":"No","tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","short":"CC BY (3.0)"},"publication_identifier":{"isbn":["9783959771597"],"issn":["1868-8969"]},"day":"18","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Simplified game of life: Algorithms and complexity","oa":1,"date_published":"2020-08-18T00:00:00Z","_id":"8533","quality_controlled":"1","article_number":"22:1-22:13","doi":"10.4230/LIPIcs.MFCS.2020.22","file":[{"access_level":"open_access","relation":"main_file","creator":"dernst","content_type":"application/pdf","date_created":"2020-09-21T13:57:34Z","file_size":491374,"date_updated":"2020-09-21T13:57:34Z","file_id":"8550","file_name":"2020_LIPIcs_Chatterjee.pdf","success":1,"checksum":"bbd7c4f55d45f2ff2a0a4ef0e10a77b1"}],"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.","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","end_date":"2020-08-28","start_date":"2020-08-24","location":"Prague, Czech Republic"},"alternative_title":["LIPIcs"],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"first_name":"Ismael R","last_name":"Jecker","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","full_name":"Jecker, Ismael R"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","last_name":"Svoboda","first_name":"Jakub","orcid":"0000-0002-1419-3267"}],"volume":170,"month":"08","year":"2020","file_date_updated":"2020-09-21T13:57:34Z","publication_status":"published","language":[{"iso":"eng"}],"citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Ismael R Jecker, and Jakub Svoboda. “Simplified Game of Life: Algorithms and Complexity.” In 45th International Symposium on Mathematical Foundations of Computer Science, Vol. 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.MFCS.2020.22.","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 45th International Symposium on Mathematical Foundations of Computer Science, Prague, Czech Republic, 2020, vol. 170.","ama":"Chatterjee K, Ibsen-Jensen R, Jecker IR, Svoboda J. Simplified game of life: Algorithms and complexity. In: 45th International Symposium on Mathematical Foundations of Computer Science. Vol 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.MFCS.2020.22","apa":"Chatterjee, K., Ibsen-Jensen, R., Jecker, I. R., & Svoboda, J. (2020). Simplified game of life: Algorithms and complexity. In 45th International Symposium on Mathematical Foundations of Computer Science (Vol. 170). Prague, Czech Republic: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2020.22","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.","mla":"Chatterjee, Krishnendu, et al. “Simplified Game of Life: Algorithms and Complexity.” 45th International Symposium on Mathematical Foundations of Computer Science, vol. 170, 22:1-22:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.MFCS.2020.22."},"ec_funded":1,"type":"conference","oa_version":"Published Version","scopus_import":"1","date_created":"2020-09-20T22:01:36Z","publication":"45th International Symposium on Mathematical Foundations of Computer Science","status":"public","external_id":{"arxiv":["2007.02894"]},"has_accepted_license":"1","abstract":[{"lang":"eng","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."}],"project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"754411","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"intvolume":" 170","ddc":["000"],"arxiv":1,"date_updated":"2025-07-10T11:57:06Z"},{"author":[{"full_name":"Jecker, Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","last_name":"Jecker","first_name":"Ismael R"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"},{"full_name":"Mazzocchi, Nicolas","last_name":"Mazzocchi","first_name":"Nicolas"}],"alternative_title":["LIPIcs"],"month":"08","volume":170,"file_date_updated":"2020-09-21T14:17:08Z","publication_status":"published","year":"2020","ec_funded":1,"citation":{"chicago":"Jecker, Ismael R, Orna Kupferman, and Nicolas Mazzocchi. “Unary Prime Languages.” In 45th International Symposium on Mathematical Foundations of Computer Science, Vol. 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.MFCS.2020.51.","apa":"Jecker, I. R., Kupferman, O., & Mazzocchi, N. (2020). Unary prime languages. In 45th International Symposium on Mathematical Foundations of Computer Science (Vol. 170). Prague, Czech Republic: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2020.51","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.","ama":"Jecker IR, Kupferman O, Mazzocchi N. Unary prime languages. In: 45th International Symposium on Mathematical Foundations of Computer Science. Vol 170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.MFCS.2020.51","ieee":"I. R. Jecker, O. Kupferman, and N. Mazzocchi, “Unary prime languages,” in 45th International Symposium on Mathematical Foundations of Computer Science, Prague, Czech Republic, 2020, vol. 170.","mla":"Jecker, Ismael R., et al. “Unary Prime Languages.” 45th International Symposium on Mathematical Foundations of Computer Science, vol. 170, 51:1-51:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.MFCS.2020.51.","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."},"language":[{"iso":"eng"}],"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."}],"has_accepted_license":"1","status":"public","date_created":"2020-09-20T22:01:36Z","scopus_import":"1","publication":"45th International Symposium on Mathematical Foundations of Computer Science","oa_version":"Published Version","corr_author":"1","type":"conference","project":[{"grant_number":"754411","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"date_updated":"2025-07-10T11:57:07Z","ddc":["000"],"intvolume":" 170","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959771597"]},"tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","short":"CC BY (3.0)"},"article_processing_charge":"No","department":[{"_id":"KrCh"}],"day":"18","oa":1,"title":"Unary prime languages","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_number":"51:1-51:12","date_published":"2020-08-18T00:00:00Z","_id":"8534","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","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.","file":[{"file_size":597977,"file_name":"2020_LIPIcsMFCS_Jecker.pdf","file_id":"8552","date_updated":"2020-09-21T14:17:08Z","checksum":"2dc9e2fad6becd4563aef3e27a473f70","success":1,"access_level":"open_access","creator":"dernst","relation":"main_file","content_type":"application/pdf","date_created":"2020-09-21T14:17:08Z"}],"conference":{"location":"Prague, Czech Republic","start_date":"2020-08-24","end_date":"2020-08-28","name":"MFCS: Mathematical Foundations of Computer Science"}}]