[{"status":"public","publisher":"Springer Nature","project":[{"grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program"}],"quality_controlled":"1","license":"https://creativecommons.org/licenses/by/4.0/","title":"Playing games with your PET: Extending the Partial Exploration Tool to stochastic games","abstract":[{"text":"We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic games, based on a recent unified framework for sound value iteration algorithms. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability/safety and mean payoff. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.","lang":"eng"}],"acknowledgement":"M. Weininger has received funding from the EU’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101034413.","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"volume":14683,"year":"2024","researchdata_availability":"yes","citation":{"ista":"Meggendorfer T, Weininger M. 2024. Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. 36th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 14683, 359–372.","ama":"Meggendorfer T, Weininger M. Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. In: 36th International Conference on Computer Aided Verification. Vol 14683. Springer Nature; 2024:359-372. doi:10.1007/978-3-031-65633-0_16","mla":"Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games.” 36th International Conference on Computer Aided Verification, vol. 14683, Springer Nature, 2024, pp. 359–72, doi:10.1007/978-3-031-65633-0_16.","chicago":"Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games.” In 36th International Conference on Computer Aided Verification, 14683:359–72. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-65633-0_16.","apa":"Meggendorfer, T., & Weininger, M. (2024). Playing games with your PET: Extending the Partial Exploration Tool to stochastic games. In 36th International Conference on Computer Aided Verification (Vol. 14683, pp. 359–372). Montreal, Canada: Springer Nature. https://doi.org/10.1007/978-3-031-65633-0_16","short":"T. Meggendorfer, M. Weininger, in:, 36th International Conference on Computer Aided Verification, Springer Nature, 2024, pp. 359–372.","ieee":"T. Meggendorfer and M. Weininger, “Playing games with your PET: Extending the Partial Exploration Tool to stochastic games,” in 36th International Conference on Computer Aided Verification, Montreal, Canada, 2024, vol. 14683, pp. 359–372."},"publication_status":"published","doi":"10.1007/978-3-031-65633-0_16","file_date_updated":"2024-08-12T08:39:12Z","intvolume":" 14683","oa_version":"Published Version","publication":"36th International Conference on Computer Aided Verification","date_updated":"2026-10-15T10:06:48Z","file":[{"checksum":"c888231d0a47b55786b7b4c0f02216bb","file_size":368487,"relation":"main_file","access_level":"open_access","date_created":"2024-08-12T08:39:12Z","content_type":"application/pdf","success":1,"date_updated":"2024-08-12T08:39:12Z","file_id":"17419","creator":"dernst","file_name":"2024_CAV_Meggendorfer.pdf"}],"isi":1,"oa":1,"das_tickbox":"1","department":[{"_id":"KrCh"}],"date_created":"2024-08-09T11:24:54Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","dataavailabilitystatement":"We refer to the artefact with the exact code used for the submission and all logs [31], and the gitlab with the continually developed source code [30].","month":"07","_id":"17402","ec_funded":1,"conference":{"name":"CAV: Computer Aided Verification","end_date":"2024-07-27","location":"Montreal, Canada","start_date":"2024-07-24"},"day":"01","article_processing_charge":"Yes (in subscription journal)","type":"conference","supplementarymaterial":"no","page":"359-372","corr_author":"1","author":[{"first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer"},{"first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","orcid":"0000-0002-0163-2152","last_name":"Weininger"}],"publication_identifier":{"eisbn":["9783031656330"],"eissn":["1611-3349"],"isbn":["9783031656323"],"issn":["0302-9743"]},"scopus_import":"1","arxiv":1,"date_published":"2024-07-01T00:00:00Z","external_id":{"arxiv":["2405.03885"],"isi":["001307897000016"]},"alternative_title":["LNCS"],"language":[{"iso":"eng"}],"ddc":["000"],"fulldoi":"https://doi.org/10.1007/978-3-031-65633-0_16","has_accepted_license":"1"},{"publication_status":"published","citation":{"mla":"Chatterjee, Krishnendu, et al. “Quantitative Bounds on Resource Usage of Probabilistic Programs.” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1, 107, Association for Computing Machinery, 2024, doi:10.1145/3649824.","ama":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. 2024;8(OOPSLA1). doi:10.1145/3649824","ista":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2024. Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. 8(OOPSLA1), 107.","ieee":"K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Quantitative bounds on resource usage of probabilistic programs,” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1. Association for Computing Machinery, 2024.","short":"K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).","apa":"Chatterjee, K., Goharshady, A. K., Meggendorfer, T., & Zikelic, D. (2024). Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3649824","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. “Quantitative Bounds on Resource Usage of Probabilistic Programs.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2024. https://doi.org/10.1145/3649824."},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"volume":8,"researchdata_availability":"yes","year":"2024","doi":"10.1145/3649824","quality_controlled":"1","publisher":"Association for Computing Machinery","project":[{"call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"status":"public","issue":"OOPSLA1","acknowledgement":"This work was supported in part by the European Research Council (ERC) under Grant No. 863818\r\n(ForM-SMArt) and the Hong Kong Research Grants Council under ECS Project No. 26208122.","abstract":[{"lang":"eng","text":"Cost analysis, also known as resource usage analysis, is the task of finding bounds on the total cost of a program and is a well-studied problem in static analysis. In this work, we consider two classical quantitative problems in cost analysis for probabilistic programs. The first problem is to find a bound on the expected total cost of the program. This is a natural measure for the resource usage of the program and can also be directly applied to average-case runtime analysis. The second problem asks for a tail bound, i.e. given a threshold t the goal is to find a probability bound p such that ℙ[total cost ≥ t] ≤ p. Intuitively, given a threshold t on the resource, the problem is to find the likelihood that the total cost exceeds this threshold.\r\nFirst, for expectation bounds, a major obstacle in previous works on cost analysis is that they can handle only non-negative costs or bounded variable updates. In contrast, we provide a new variant of the standard notion of cost martingales, that allows us to find expectation bounds for a class of programs with general positive or negative costs and no restriction on the variable updates. More specifically, our approach is applicable as long as there is a lower bound on the total cost incurred along every path.\r\nSecond, for tail bounds, all previous methods are limited to programs in which the expected total cost is finite. In contrast, we present a novel approach, based on a combination of our martingale-based method for expectation bounds with a quantitative safety analysis, to obtain a solution to the tail bound problem that is applicable even to programs with infinite expected cost. Specifically, this allows us to obtain runtime tail bounds for programs that do not terminate almost-surely.\r\nIn summary, we provide a novel combination of martingale-based cost analysis and quantitative safety analysis that is able to find expectation and tail cost bounds for probabilistic programs, without the restrictions of non-negative costs, bounded updates, or finiteness of the expected total cost. Finally, we provide experimental results showcasing that our approach can solve instances that were beyond the reach of previous methods."}],"title":"Quantitative bounds on resource usage of probabilistic programs","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2024-06-23T22:01:02Z","article_type":"original","department":[{"_id":"KrCh"}],"_id":"17162","ec_funded":1,"month":"04","dataavailabilitystatement":"The software that supports Section 8 is available on Zenodo [Meggendorfer and Žikelić 2024]. https://doi.org/10.5281/zenodo.10457566","publication":"Proceedings of the ACM on Programming Languages","oa_version":"Published Version","intvolume":" 8","file_date_updated":"2024-06-27T07:48:16Z","das_tickbox":"1","related_material":{"record":[{"relation":"research_data","id":"23140","status":"public"}]},"oa":1,"date_updated":"2026-10-15T10:02:32Z","file":[{"creator":"dernst","file_name":"2024_ProcACMProgLanguage_Chatterjee.pdf","success":1,"file_id":"17182","date_updated":"2024-06-27T07:48:16Z","access_level":"open_access","date_created":"2024-06-27T07:48:16Z","content_type":"application/pdf","file_size":413096,"checksum":"9243ded966f71df1572be5466019be5c","relation":"main_file"}],"article_number":"107","supplementarymaterial":"no","scopus_import":"1","publication_identifier":{"eissn":["2475-1421"]},"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","last_name":"Goharshady"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165"},{"first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699"}],"day":"29","type":"journal_article","article_processing_charge":"Yes (in subscription journal)","has_accepted_license":"1","fulldoi":"https://doi.org/10.1145/3649824","ddc":["000"],"date_published":"2024-04-29T00:00:00Z","language":[{"iso":"eng"}]},{"month":"12","ec_funded":1,"_id":"19512","conference":{"location":"Vancouver, Canada","end_date":"2024-12-15","name":"NeurIPS: Neural Information Processing Systems","start_date":"2024-12-09"},"department":[{"_id":"MoHe"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2025-04-06T22:01:32Z","date_updated":"2026-10-15T09:52:07Z","oa":1,"intvolume":" 37","publication":"38th Conference on Neural Information Processing Systems","oa_version":"Preprint","OA_type":"green","doi":"10.52202/079017-0299","year":"2024","volume":37,"citation":{"ista":"Andersson JD, Henzinger M, Pagh R, Steiner TA, Upadhyay J. 2024. Continual counting with gradual privacy expiration. 38th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, vol. 37.","mla":"Andersson, Joel Daniel, et al. “Continual Counting with Gradual Privacy Expiration.” 38th Conference on Neural Information Processing Systems, vol. 37, Neural Information Processing Systems Foundation, 2024, doi:10.52202/079017-0299.","ama":"Andersson JD, Henzinger M, Pagh R, Steiner TA, Upadhyay J. Continual counting with gradual privacy expiration. In: 38th Conference on Neural Information Processing Systems. Vol 37. Neural Information Processing Systems Foundation; 2024. doi:10.52202/079017-0299","apa":"Andersson, J. D., Henzinger, M., Pagh, R., Steiner, T. A., & Upadhyay, J. (2024). Continual counting with gradual privacy expiration. In 38th Conference on Neural Information Processing Systems (Vol. 37). Vancouver, Canada: Neural Information Processing Systems Foundation. https://doi.org/10.52202/079017-0299","chicago":"Andersson, Joel Daniel, Monika Henzinger, Rasmus Pagh, Teresa Anna Steiner, and Jalaj Upadhyay. “Continual Counting with Gradual Privacy Expiration.” In 38th Conference on Neural Information Processing Systems, Vol. 37. Neural Information Processing Systems Foundation, 2024. https://doi.org/10.52202/079017-0299.","ieee":"J. D. Andersson, M. Henzinger, R. Pagh, T. A. Steiner, and J. Upadhyay, “Continual counting with gradual privacy expiration,” in 38th Conference on Neural Information Processing Systems, Vancouver, Canada, 2024, vol. 37.","short":"J.D. Andersson, M. Henzinger, R. Pagh, T.A. Steiner, J. Upadhyay, in:, 38th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2024."},"publication_status":"published","OA_place":"repository","title":"Continual counting with gradual privacy expiration","abstract":[{"lang":"eng","text":"Differential privacy with gradual expiration models the setting where data items\r\narrive in a stream and at a given time t the privacy loss guaranteed for a data item\r\nseen at time (t − d) is εg(d), where g is a monotonically non-decreasing function.\r\nWe study the fundamental continual (binary) counting problem where each data\r\nitem consists of a bit, and the algorithm needs to output at each time step the sum of\r\nall the bits streamed so far. For a stream of length T and privacy without expiration\r\ncontinual counting is possible with maximum (over all time steps) additive error\r\nO(log2\r\n(T)/ε) and the best known lower bound is Ω(log(T)/ε); closing this gap\r\nis a challenging open problem.\r\nWe show that the situation is very different for privacy with gradual expiration by\r\ngiving upper and lower bounds for a large set of expiration functions g. Specifically,\r\nour algorithm achieves an additive error of O(log(T)/ε) for a large set of privacy\r\nexpiration functions. We also give a lower bound that shows that if C is the additive\r\nerror of any ε-DP algorithm for this problem, then the product of C and the privacy\r\nexpiration function after 2C steps must be Ω(log(T)/ε). Our algorithm matches\r\nthis lower bound as its additive error is O(log(T)/ε), even when g(2C) = O(1).\r\nOur empirical evaluation shows that we achieve a slowly growing privacy loss\r\nwith significantly smaller empirical privacy loss for large values of d than a natural\r\nbaseline algorithm."}],"acknowledgement":"Monika Henzinger: This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 101019564) and the Austrian Science Fund (FWF) grant DOI 10.55776/Z422, grant DOI 10.55776/I5982, and grant DOI 10.55776/P33775 with additional funding from the netidee SCIENCE Stiftung, 2020–2024. Joel Daniel Andersson and Rasmus Pagh are affiliated with Basic Algorithms Research Copenhagen (BARC), supported by the VILLUM Foundation grant 16582, and are also supported by Providentia, a Data Science Distinguished Investigator grant from Novo Nordisk Fonden. Teresa Anna Steiner is supported by a research grant (VIL51463) from VILLUM FONDEN. This work was done while Teresa Anna Steiner was a Postdoc at the Technical University of Denmark. Jalaj Upadhyay’s research was funded by the Rutgers Decanal Grant no. 302918 and an unrestricted gift from Google.","status":"public","project":[{"grant_number":"101019564","_id":"bd9ca328-d553-11ed-ba76-dc4f890cfe62","call_identifier":"H2020","name":"The design and evaluation of modern fully dynamic data structures"},{"name":"Efficient algorithms","_id":"34def286-11ca-11ed-8bc3-da5948e1613c","grant_number":"Z00422"},{"grant_number":"I05982","_id":"bda196b2-d553-11ed-ba76-8e8ee6c21103","name":"Static and Dynamic Hierarchical Graph Decompositions"},{"_id":"bd9e3a2e-d553-11ed-ba76-8aa684ce17fe","grant_number":"P33775","name":"Fast Algorithms for a Reactive Network Layer"}],"publisher":"Neural Information Processing Systems Foundation","quality_controlled":"1","fulldoi":"https://doi.org/10.52202/079017-0299","language":[{"iso":"eng"}],"arxiv":1,"date_published":"2024-12-20T00:00:00Z","external_id":{"arxiv":["2406.03802"]},"alternative_title":["Advances in Neural Information Processing Systems"],"author":[{"last_name":"Andersson","first_name":"Joel Daniel","full_name":"Andersson, Joel Daniel"},{"first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530"},{"last_name":"Pagh","full_name":"Pagh, Rasmus","first_name":"Rasmus"},{"last_name":"Steiner","full_name":"Steiner, Teresa Anna","first_name":"Teresa Anna"},{"full_name":"Upadhyay, Jalaj","first_name":"Jalaj","last_name":"Upadhyay"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2406.03802","open_access":"1"}],"publication_identifier":{"eissn":["1049-5258"]},"scopus_import":"1","corr_author":"1","article_processing_charge":"No","type":"conference","day":"20"},{"fulldoi":"https://doi.org/10.52202/079017-2115","alternative_title":["Advances in Neural Information Processing Systems"],"external_id":{"arxiv":["2406.14183"]},"date_published":"2024-12-20T00:00:00Z","arxiv":1,"language":[{"iso":"eng"}],"corr_author":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2406.14183"}],"scopus_import":"1","publication_identifier":{"eissn":["1049-5258"]},"author":[{"last_name":"Fumero","first_name":"Marco","id":"1c1593eb-393f-11ef-bb8e-ab4f1e979650","full_name":"Fumero, Marco"},{"last_name":"Pegoraro","full_name":"Pegoraro, Marco","first_name":"Marco"},{"first_name":"Valentino","full_name":"Maiorca, Valentino","last_name":"Maiorca"},{"last_name":"Locatello","orcid":"0000-0002-4850-0683","id":"26cfd52f-2483-11ee-8040-88983bcc06d4","first_name":"Francesco","full_name":"Locatello, Francesco"},{"last_name":"Rodolà","full_name":"Rodolà, Emanuele","first_name":"Emanuele"}],"day":"20","type":"conference","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2025-04-06T22:01:32Z","department":[{"_id":"FrLo"}],"_id":"19515","ec_funded":1,"conference":{"start_date":"2024-12-09","end_date":"2024-12-15","name":"NeurIPS: Neural Information Processing Systems","location":"Vancouver, Canada"},"month":"12","publication":"38th Conference on Neural Information Processing Systems","oa_version":"Preprint","intvolume":" 37","date_updated":"2026-10-15T09:52:55Z","oa":1,"citation":{"ista":"Fumero M, Pegoraro M, Maiorca V, Locatello F, Rodolà E. 2024. Latent functional maps: A spectral framework for representation alignment. 38th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, vol. 37.","ama":"Fumero M, Pegoraro M, Maiorca V, Locatello F, Rodolà E. Latent functional maps: A spectral framework for representation alignment. In: 38th Conference on Neural Information Processing Systems. Vol 37. Neural Information Processing Systems Foundation; 2024. doi:10.52202/079017-2115","mla":"Fumero, Marco, et al. “Latent Functional Maps: A Spectral Framework for Representation Alignment.” 38th Conference on Neural Information Processing Systems, vol. 37, Neural Information Processing Systems Foundation, 2024, doi:10.52202/079017-2115.","chicago":"Fumero, Marco, Marco Pegoraro, Valentino Maiorca, Francesco Locatello, and Emanuele Rodolà. “Latent Functional Maps: A Spectral Framework for Representation Alignment.” In 38th Conference on Neural Information Processing Systems, Vol. 37. Neural Information Processing Systems Foundation, 2024. https://doi.org/10.52202/079017-2115.","apa":"Fumero, M., Pegoraro, M., Maiorca, V., Locatello, F., & Rodolà, E. (2024). Latent functional maps: A spectral framework for representation alignment. In 38th Conference on Neural Information Processing Systems (Vol. 37). Vancouver, Canada: Neural Information Processing Systems Foundation. https://doi.org/10.52202/079017-2115","short":"M. Fumero, M. Pegoraro, V. Maiorca, F. Locatello, E. Rodolà, in:, 38th Conference on Neural Information Processing Systems, Neural Information Processing Systems Foundation, 2024.","ieee":"M. Fumero, M. Pegoraro, V. Maiorca, F. Locatello, and E. Rodolà, “Latent functional maps: A spectral framework for representation alignment,” in 38th Conference on Neural Information Processing Systems, Vancouver, Canada, 2024, vol. 37."},"publication_status":"published","OA_place":"repository","year":"2024","volume":37,"doi":"10.52202/079017-2115","OA_type":"green","quality_controlled":"1","status":"public","publisher":"Neural Information Processing Systems Foundation","project":[{"name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413"}],"acknowledgement":"MF is supported by the MSCA IST-Bridge fellowship which has received funding from the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie grant agreement No 101034413. ER and VM are supported by the PNRR MUR project PE0000013-FAIR. MP is supported by the Sapienza grant \"Predicting and Explaining Clinical Trial Outcomes\", prot. RG12218166FA3F13.","title":"Latent functional maps: A spectral framework for representation alignment","abstract":[{"lang":"eng","text":"Neural models learn data representations that lie on low-dimensional manifolds,\r\nyet modeling the relation between these representational spaces is an ongoing challenge. By integrating spectral geometry principles into neural modeling, we show\r\nthat this problem can be better addressed in the functional domain, mitigating complexity, while enhancing interpretability and performances on downstream tasks.\r\nTo this end, we introduce a multi-purpose framework to the representation learning\r\ncommunity, which allows to: (i) compare different spaces in an interpretable way\r\nand measure their intrinsic similarity; (ii) find correspondences between them, both\r\nin unsupervised and weakly supervised settings, and (iii) to effectively transfer\r\nrepresentations between distinct spaces. We validate our framework on various\r\napplications, ranging from stitching to retrieval tasks, and on multiple modalities,\r\ndemonstrating that Latent Functional Maps can serve as a swiss-army knife for\r\nrepresentation alignment"}]},{"type":"research_data_reference","contributor":[{"last_name":"Meggendorfer","first_name":"Tobias","contributor_type":"contact_person"}],"title":"Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs","abstract":[{"lang":"eng","text":"The artefact for the OOPSLA 2024 paper \"Quantitative Bounds on Resource Usage of Probabilistic Programs\".\r\n\r\n"}],"article_processing_charge":"No","status":"public","publisher":"Zenodo","day":"05","main_file_link":[{"url":"https://doi.org/10.5281/zenodo.10457565","open_access":"1"}],"doi":"10.5281/zenodo.10457565","author":[{"last_name":" Žikelić","full_name":" Žikelić, Đorđe","first_name":"Đorđe"}],"OA_type":"green","citation":{"ista":" Žikelić Đ. 2024. Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs, Zenodo, 10.5281/zenodo.10457565.","mla":" Žikelić, Đorđe. Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs. Zenodo, 2024, doi:10.5281/zenodo.10457565.","ama":" Žikelić Đ. Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs. 2024. doi:10.5281/zenodo.10457565","apa":" Žikelić, Đ. (2024). Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs. Zenodo. https://doi.org/10.5281/zenodo.10457565","chicago":" Žikelić, Đorđe. “Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs.” Zenodo, 2024. https://doi.org/10.5281/zenodo.10457565.","ieee":"Đ. Žikelić, “Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs.” Zenodo, 2024.","short":"Đ. Žikelić, (2024)."},"OA_place":"repository","year":"2024","related_material":{"record":[{"id":"17162","status":"public","relation":"used_in_publication"}]},"date_updated":"2026-10-15T10:02:33Z","oa":1,"oa_version":"None","date_published":"2024-03-05T00:00:00Z","_id":"23140","ddc":["000"],"month":"03","fulldoi":"https://doi.org/10.5281/zenodo.10457565","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2026-10-15T10:02:22Z","department":[{"_id":"KrCh"}]},{"month":"03","dataavailabilitystatement":"Figures are based on simulation averages over many independent runs of the respective simulation. Results were analyzed and visualized with Python and Matlab R2023a. The computer code is published in (65). All other data are included in the manuscript and/or SI Appendix.","ec_funded":1,"_id":"15083","article_type":"original","APC_amount":"3041,76 EUR","department":[{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2024-03-05T09:18:49Z","oa":1,"file":[{"success":1,"file_id":"15109","date_updated":"2024-03-12T13:12:22Z","file_name":"2024_PNAS_Huebner.pdf","creator":"dernst","relation":"main_file","checksum":"068520e3efd4d008bb9177e8aedb7d22","file_size":2203220,"date_created":"2024-03-12T13:12:22Z","content_type":"application/pdf","access_level":"open_access"}],"isi":1,"date_updated":"2026-10-15T10:10:26Z","related_material":{"record":[{"status":"public","id":"15108","relation":"research_data"},{"relation":"dissertation_contains","id":"19903","status":"public"}],"link":[{"relation":"press_release","url":"https://ista.ac.at/en/news/what-math-tells-us-about-social-dilemmas/","description":"News on ISTA Website"}]},"das_tickbox":"1","intvolume":" 121","file_date_updated":"2024-03-12T13:12:22Z","publication":"Proceedings of the National Academy of Sciences of the United States of America","oa_version":"Published Version","OA_type":"hybrid","doi":"10.1073/pnas.2315558121","researchdata_availability":"yes","tmp":{"image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"year":"2024","volume":121,"publication_status":"published","OA_place":"publisher","citation":{"ista":"Hübner V, Staab M, Hilbe C, Chatterjee K, Kleshnina M. 2024. Efficiency and resilience of cooperation in asymmetric social dilemmas. Proceedings of the National Academy of Sciences of the United States of America. 121(10), e2315558121.","ama":"Hübner V, Staab M, Hilbe C, Chatterjee K, Kleshnina M. Efficiency and resilience of cooperation in asymmetric social dilemmas. Proceedings of the National Academy of Sciences of the United States of America. 2024;121(10). doi:10.1073/pnas.2315558121","mla":"Hübner, Valentin, et al. “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.” Proceedings of the National Academy of Sciences of the United States of America, vol. 121, no. 10, e2315558121, National Academy of Sciences, 2024, doi:10.1073/pnas.2315558121.","chicago":"Hübner, Valentin, Manuel Staab, Christian Hilbe, Krishnendu Chatterjee, and Maria Kleshnina. “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.” Proceedings of the National Academy of Sciences of the United States of America. National Academy of Sciences, 2024. https://doi.org/10.1073/pnas.2315558121.","apa":"Hübner, V., Staab, M., Hilbe, C., Chatterjee, K., & Kleshnina, M. (2024). Efficiency and resilience of cooperation in asymmetric social dilemmas. Proceedings of the National Academy of Sciences of the United States of America. National Academy of Sciences. https://doi.org/10.1073/pnas.2315558121","short":"V. Hübner, M. Staab, C. Hilbe, K. Chatterjee, M. Kleshnina, Proceedings of the National Academy of Sciences of the United States of America 121 (2024).","ieee":"V. Hübner, M. Staab, C. Hilbe, K. Chatterjee, and M. Kleshnina, “Efficiency and resilience of cooperation in asymmetric social dilemmas,” Proceedings of the National Academy of Sciences of the United States of America, vol. 121, no. 10. National Academy of Sciences, 2024."},"abstract":[{"text":"Direct reciprocity is a powerful mechanism for cooperation in social dilemmas. The very logic of reciprocity, however, seems to require that individuals are symmetric, and that everyone has the same means to influence each others’ payoffs. Yet in many applications, individuals are asymmetric. Herein, we study the effect of asymmetry in linear public good games. Individuals may differ in their endowments (their ability to contribute to a public good) and in their productivities (how effective their contributions are). Given the individuals’ productivities, we ask which allocation of endowments is optimal for cooperation. To this end, we consider two notions of optimality. The first notion focuses on the resilience of cooperation. The respective endowment distribution ensures that full cooperation is feasible even under the most adverse conditions. The second notion focuses on efficiency. The corresponding endowment distribution maximizes group welfare. Using analytical methods, we fully characterize these two endowment distributions. This analysis reveals that both optimality notions favor some endowment inequality: More productive players ought to get higher endowments. Yet the two notions disagree on how unequal endowments are supposed to be. A focus on resilience results in less inequality. With additional simulations, we show that the optimal endowment allocation needs to account for both the resilience and the efficiency of cooperation.","lang":"eng"}],"title":"Efficiency and resilience of cooperation in asymmetric social dilemmas","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.), the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie Grant Agreement #754411 and the French Agence Nationale de la Recherche (under the Investissement d’Avenir Programme, ANR-17-EURE-0010) (to M.K.).","publisher":"National Academy of Sciences","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"H2020","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships"}],"status":"public","issue":"10","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","quality_controlled":"1","fulldoi":"https://doi.org/10.1073/pnas.2315558121","ddc":["000"],"has_accepted_license":"1","language":[{"iso":"eng"}],"pmid":1,"date_published":"2024-03-05T00:00:00Z","external_id":{"isi":["001207786500004"],"pmid":["38408249"]},"author":[{"first_name":"Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","full_name":"Hübner, Valentin","last_name":"Hübner","orcid":"0009-0001-5009-4987"},{"last_name":"Staab","full_name":"Staab, Manuel","first_name":"Manuel"},{"last_name":"Hilbe","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","first_name":"Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kleshnina","full_name":"Kleshnina, Maria","first_name":"Maria"}],"scopus_import":"1","publication_identifier":{"issn":["0027-8424"],"eissn":["1091-6490"]},"supplementarymaterial":"yes","article_number":"e2315558121","corr_author":"1","article_processing_charge":"Yes (in subscription journal)","type":"journal_article","day":"05"},{"article_number":"e1012008","corr_author":"1","supplementarymaterial":"yes","scopus_import":"1","publication_identifier":{"eissn":["1553-7358"],"issn":["1553-734X"]},"author":[{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","full_name":"Svoboda, Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267"},{"id":"f97aac0e-f57c-11ee-93d0-a5a82d8df168","first_name":"Soham Shrikant","full_name":"Joshi, Soham Shrikant","last_name":"Joshi"},{"orcid":"0000-0002-1097-9684","last_name":"Tkadlec","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"}],"day":"29","type":"journal_article","article_processing_charge":"Yes","has_accepted_license":"1","fulldoi":"https://doi.org/10.1371/journal.pcbi.1012008","ddc":["000"],"date_published":"2024-03-29T00:00:00Z","external_id":{"arxiv":["2401.14914"],"isi":["001194482400002"]},"arxiv":1,"language":[{"iso":"eng"}],"OA_place":"publisher","publication_status":"published","citation":{"ama":"Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. PLoS Computational Biology. 2024;20(3). doi:10.1371/journal.pcbi.1012008","mla":"Svoboda, Jakub, et al. “Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth Updating.” PLoS Computational Biology, vol. 20, no. 3, e1012008, Public Library of Science, 2024, doi:10.1371/journal.pcbi.1012008.","ista":"Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. 2024. Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. PLoS Computational Biology. 20(3), e1012008.","short":"J. Svoboda, S.S. Joshi, J. Tkadlec, K. Chatterjee, PLoS Computational Biology 20 (2024).","ieee":"J. Svoboda, S. S. Joshi, J. Tkadlec, and K. Chatterjee, “Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating,” PLoS Computational Biology, vol. 20, no. 3. Public Library of Science, 2024.","chicago":"Svoboda, Jakub, Soham Shrikant Joshi, Josef Tkadlec, and Krishnendu Chatterjee. “Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth Updating.” PLoS Computational Biology. Public Library of Science, 2024. https://doi.org/10.1371/journal.pcbi.1012008.","apa":"Svoboda, J., Joshi, S. S., Tkadlec, J., & Chatterjee, K. (2024). Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1012008"},"volume":20,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"researchdata_availability":"yes","year":"2024","doi":"10.1371/journal.pcbi.1012008","OA_type":"gold","quality_controlled":"1","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"}],"publisher":"Public Library of Science","issue":"3","status":"public","acknowledgement":"We thank Gavin Rees for helpful discussions. J.S., S.J., and K.C were supported by\r\nEuropean Research Council (ERC) CoG 863818 (ForM-SMArt). J.T was supported by Center for Foundations of Modern Computer Science (Charles University project UNCE/SCI/004) and by the project PRIMUS/24/SCI/012 from Charles University. ","title":"Amplifiers of selection for the Moran process with both Birth-death and death-Birth updating","abstract":[{"text":"Populations evolve by accumulating advantageous mutations. Every population has some spatial structure that can be modeled by an underlying network. The network then influences the probability that new advantageous mutations fixate. Amplifiers of selection are networks that increase the fixation probability of advantageous mutants, as compared to the unstructured fully-connected network. Whether or not a network is an amplifier depends on the choice of the random process that governs the evolutionary dynamics. Two popular choices are Moran process with Birth-death updating and Moran process with death-Birth updating. Interestingly, while some networks are amplifiers under Birth-death updating and other networks are amplifiers under death-Birth updating, so far no spatial structures have been found that function as an amplifier under both types of updating simultaneously. In this work, we identify networks that act as amplifiers of selection under both versions of the Moran process. The amplifiers are robust, modular, and increase fixation probability for any mutant fitness advantage in a range r ∈ (1, 1.2). To complement this positive result, we also prove that for certain quantities closely related to fixation probability, it is impossible to improve them simultaneously for both versions of the Moran process. Together, our results highlight how the two versions of the Moran process differ and what they have in common.","lang":"eng"}],"date_created":"2024-04-07T22:00:55Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","APC_amount":"3149,96 EUR","article_type":"original","department":[{"_id":"KrCh"}],"DOAJ_listed":"1","_id":"15297","ec_funded":1,"month":"03","dataavailabilitystatement":"Code for the figures and the computational experiments is available from the Figshare repository: https://figshare.com/s/4e08d78c892749f84201.","publication":"PLoS Computational Biology","oa_version":"Published Version","intvolume":" 20","file_date_updated":"2024-08-20T10:52:28Z","das_tickbox":"1","related_material":{"record":[{"status":"public","id":"20138","relation":"dissertation_contains"}]},"oa":1,"file":[{"checksum":"a511cf369d9172beb123fe73f291b5cc","file_size":1425292,"relation":"main_file","access_level":"open_access","date_created":"2024-08-20T10:52:28Z","content_type":"application/pdf","success":1,"date_updated":"2024-08-20T10:52:28Z","file_id":"17450","creator":"dernst","file_name":"2024_PloSComBio_Svoboda.pdf"}],"isi":1,"date_updated":"2026-10-15T12:28:11Z"},{"date_published":"2024-02-09T00:00:00Z","oa_version":"Published Version","oa":1,"date_updated":"2026-10-15T10:10:25Z","related_material":{"record":[{"id":"15083","status":"public","relation":"used_in_publication"}]},"department":[{"_id":"KrCh"}],"date_created":"2024-03-12T13:02:58Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","fulldoi":"https://doi.org/10.5281/ZENODO.10639167","month":"02","ddc":["000"],"has_accepted_license":"1","_id":"15108","day":"09","publisher":"Zenodo","status":"public","abstract":[{"text":"in the research article \"Efficiency and resilience of cooperation in asymmetric social dilemmas\" (by Valentin Hübner, Manuel Staab, Christian Hilbe, Krishnendu Chatterjee, and Maria Kleshnina).\r\n\r\nWe used different implementations for the case of two and three players, both described below.","lang":"eng"}],"article_processing_charge":"No","title":"Computer code for \"Efficiency and resilience of cooperation in asymmetric social dilemmas\"","type":"research_data_reference","year":"2024","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"citation":{"short":"V. Hübner, M. Kleshnina, (2024).","ieee":"V. Hübner and M. Kleshnina, “Computer code for ‘Efficiency and resilience of cooperation in asymmetric social dilemmas.’” Zenodo, 2024.","chicago":"Hübner, Valentin, and Maria Kleshnina. “Computer Code for ‘Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.’” Zenodo, 2024. https://doi.org/10.5281/ZENODO.10639167.","apa":"Hübner, V., & Kleshnina, M. (2024). Computer code for “Efficiency and resilience of cooperation in asymmetric social dilemmas.” Zenodo. https://doi.org/10.5281/ZENODO.10639167","ama":"Hübner V, Kleshnina M. Computer code for “Efficiency and resilience of cooperation in asymmetric social dilemmas.” 2024. doi:10.5281/ZENODO.10639167","mla":"Hübner, Valentin, and Maria Kleshnina. Computer Code for “Efficiency and Resilience of Cooperation in Asymmetric Social Dilemmas.” Zenodo, 2024, doi:10.5281/ZENODO.10639167.","ista":"Hübner V, Kleshnina M. 2024. Computer code for ‘Efficiency and resilience of cooperation in asymmetric social dilemmas’, Zenodo, 10.5281/ZENODO.10639167."},"corr_author":"1","author":[{"last_name":"Hübner","orcid":"0009-0001-5009-4987","first_name":"Valentin","id":"2c8aa207-dc7d-11ea-9b2f-f22972ecd910","full_name":"Hübner, Valentin"},{"full_name":"Kleshnina, Maria","first_name":"Maria","last_name":"Kleshnina"}],"doi":"10.5281/ZENODO.10639167","main_file_link":[{"url":"https://10.5281/zenodo.10639167","open_access":"1"}]},{"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"researchdata_availability":"yes","year":"2024","volume":14933,"publication_status":"published","citation":{"apa":"Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., & Zikelic, D. (2024). Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 14933, pp. 600–619). Milan, Italy: Springer Nature. https://doi.org/10.1007/978-3-031-71162-6_31","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad Karrabi, and Dorde Zikelic. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 14933:600–619. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-71162-6_31.","ieee":"K. Chatterjee, A. K. Goharshady, E. Goharshady, M. Karrabi, and D. Zikelic, “Sound and complete witnesses for template-based verification of LTL properties on polynomial programs,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Milan, Italy, 2024, vol. 14933, pp. 600–619.","short":"K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, D. Zikelic, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp. 600–619.","ista":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods, LNCS, vol. 14933, 600–619.","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14933, Springer Nature, 2024, pp. 600–19, doi:10.1007/978-3-031-71162-6_31.","ama":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 14933. Springer Nature; 2024:600-619. doi:10.1007/978-3-031-71162-6_31"},"doi":"10.1007/978-3-031-71162-6_31","project":[{"call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"publisher":"Springer Nature","status":"public","quality_controlled":"1","title":"Sound and complete witnesses for template-based verification of LTL properties on polynomial programs","abstract":[{"text":"We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools.","lang":"eng"}],"acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Hong Kong Research Grants Council ECS Project Number 26208122.","department":[{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2024-09-29T22:01:37Z","month":"09","dataavailabilitystatement":"The implementations of the algorithms mentioned in the experiments section and the benchmarks are available at doi.org/10.5281/zenodo.12518217.","conference":{"location":"Milan, Italy","name":"FM: Formal Methods","end_date":"2024-09-13","start_date":"2024-09-09"},"ec_funded":1,"_id":"18155","intvolume":" 14933","file_date_updated":"2024-10-01T09:56:54Z","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","oa_version":"Published Version","oa":1,"isi":1,"file":[{"date_created":"2024-10-01T09:56:54Z","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_size":650495,"checksum":"223845be9e754681ee218866827c95e7","creator":"dernst","file_name":"2024_LNCS_Chatterjee.pdf","success":1,"date_updated":"2024-10-01T09:56:54Z","file_id":"18165"}],"date_updated":"2026-10-16T07:29:39Z","das_tickbox":"1","related_material":{"record":[{"relation":"research_data","status":"public","id":"22798"}]},"supplementarymaterial":"no","page":"600-619","corr_author":"1","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","orcid":"0000-0003-1702-6584"},{"full_name":"Goharshady, Ehsan","first_name":"Ehsan","last_name":"Goharshady"},{"id":"67638922-f394-11eb-9cf6-f20423e08757","first_name":"Mehrdad","full_name":"Karrabi, Mehrdad","last_name":"Karrabi","orcid":"0009-0007-5253-9170"},{"full_name":"Zikelic, Dorde","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","last_name":"Zikelic"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031711619"]},"scopus_import":"1","day":"11","article_processing_charge":"Yes (in subscription journal)","type":"conference","fulldoi":"https://doi.org/10.1007/978-3-031-71162-6_31","ddc":["000"],"has_accepted_license":"1","arxiv":1,"alternative_title":["LNCS"],"external_id":{"arxiv":["2403.05386"],"isi":["001336893300031"]},"date_published":"2024-09-11T00:00:00Z","language":[{"iso":"eng"}]},{"status":"public","day":"24","publisher":"Repository","type":"research_data_reference","title":"Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs","abstract":[{"lang":"eng","text":"This repository contains the artifact of the paper titled \"Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs\" accepted at FM 2024.\r\n\r\nThe task of verifying an LTL formula on a program can be reduced to verifying a Büchi specification on the product transition system. This tool takes a non-deterministic transition system together with a Büchi specification as input and based on user preferences tries to either (i) prove the existence of a run in the program that satisfies the Büchi condition or (ii) demonstrate that every run of the program satisfies the Büchi condition.\r\n \r\nThe tool is written in Java and works well with openjdk 11 on Ubuntu 22.04. Running all the experiments can take weeks to finish. We have provided a script for running the strongest configuration of our tool which solves most of the benchmarks and takes less than 48 hours. Detailed guidance is given in the readme file."}],"article_processing_charge":"No","OA_place":"repository","citation":{"ista":"Chatterjee K, Kafshdar Goharshady A, Kafshdar Goharshady E, Karrabi M, Žikelić Ð. 2024. Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs, Repository, 10.5281/zenodo.12518216.","ama":"Chatterjee K, Kafshdar Goharshady A, Kafshdar Goharshady E, Karrabi M, Žikelić Ð. Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs. 2024. doi:10.5281/zenodo.12518216","mla":"Chatterjee, Krishnendu, et al. Data for Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs. Repository, 2024, doi:10.5281/zenodo.12518216.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, and Ðorđe Žikelić. “Data for Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” Repository, 2024. https://doi.org/10.5281/zenodo.12518216.","apa":"Chatterjee, K., Kafshdar Goharshady, A., Kafshdar Goharshady, E., Karrabi, M., & Žikelić, Ð. (2024). Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs. Repository. https://doi.org/10.5281/zenodo.12518216","short":"K. Chatterjee, A. Kafshdar Goharshady, E. Kafshdar Goharshady, M. Karrabi, Ð. Žikelić, (2024).","ieee":"K. Chatterjee, A. Kafshdar Goharshady, E. Kafshdar Goharshady, M. Karrabi, and Ð. Žikelić, “Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs.” Repository, 2024."},"year":"2024","main_file_link":[{"open_access":"1","url":"https://doi.org/10.5281/zenodo.12518216"}],"doi":"10.5281/zenodo.12518216","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":" Kafshdar Goharshady","first_name":"Amir","full_name":" Kafshdar Goharshady, Amir"},{"first_name":"Ehsan","full_name":"Kafshdar Goharshady, Ehsan","last_name":"Kafshdar Goharshady"},{"last_name":"Karrabi","first_name":"Mehrdad","full_name":"Karrabi, Mehrdad"},{"first_name":"Ðorđe","full_name":"Žikelić, Ðorđe","last_name":"Žikelić"}],"OA_type":"green","oa_version":"None","date_published":"2024-06-24T00:00:00Z","related_material":{"record":[{"id":"18155","status":"public","relation":"used_in_publication"}]},"date_updated":"2026-10-16T07:29:39Z","oa":1,"date_created":"2026-09-03T11:50:15Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"_id":"22798","ddc":["000"],"month":"06","fulldoi":"https://doi.org/10.5281/zenodo.12518216"},{"type":"journal_article","article_processing_charge":"Yes","day":"10","scopus_import":"1","publication_identifier":{"issn":["0027-8424"],"eissn":["1091-6490"]},"author":[{"last_name":"Svoboda","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"}],"corr_author":"1","article_number":"e2405605121","supplementarymaterial":"yes","language":[{"iso":"eng"}],"external_id":{"isi":["001379596100014"],"pmid":["39642209"]},"date_published":"2024-12-10T00:00:00Z","pmid":1,"has_accepted_license":"1","ddc":["000"],"fulldoi":"https://doi.org/10.1073/pnas.2405605121","acknowledgement":"J.S. and K.C. were supported by the European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.","abstract":[{"lang":"eng","text":"Spatial games provide a simple and elegant mathematical model to study the evolution of cooperation in networks. In spatial games, individuals reside in vertices, adopt simple strategies, and interact with neighbors to receive a payoff. Depending on their own and neighbors’ payoffs, individuals can change their strategy. The payoff is determined by the Prisoners’ Dilemma, a classical matrix game, where players cooperate or defect. While cooperation is the desired behavior, defection provides a higher payoff for a selfish individual. There are many theoretical and empirical studies related to the role of the network in the evolution of cooperation. However, the fundamental question of whether there exist networks that for low initial cooperation rate ensure a high chance of fixation, i.e., cooperation spreads across the whole population, has remained elusive for spatial games with strong selection. In this work, we answer this fundamental question in the affirmative by presenting network structures that ensure high fixation probability for cooperators in the strong selection regime. Besides, our structures have many desirable properties: (a) they ensure the spread of cooperation even for a low initial density of cooperation and high temptation of defection, (b) they have constant degrees, and (c) the number of steps, until cooperation spreads, is at most quadratic in the size of the network."}],"title":"Density amplifiers of cooperation for spatial games","quality_controlled":"1","issue":"50","status":"public","publisher":"National Academy of Sciences","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"doi":"10.1073/pnas.2405605121","OA_type":"hybrid","publication_status":"published","citation":{"ista":"Svoboda J, Chatterjee K. 2024. Density amplifiers of cooperation for spatial games. Proceedings of the National Academy of Sciences of the United States of America. 121(50), e2405605121.","mla":"Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation for Spatial Games.” Proceedings of the National Academy of Sciences of the United States of America, vol. 121, no. 50, e2405605121, National Academy of Sciences, 2024, doi:10.1073/pnas.2405605121.","ama":"Svoboda J, Chatterjee K. Density amplifiers of cooperation for spatial games. Proceedings of the National Academy of Sciences of the United States of America. 2024;121(50). doi:10.1073/pnas.2405605121","apa":"Svoboda, J., & Chatterjee, K. (2024). Density amplifiers of cooperation for spatial games. Proceedings of the National Academy of Sciences of the United States of America. National Academy of Sciences. https://doi.org/10.1073/pnas.2405605121","chicago":"Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation for Spatial Games.” Proceedings of the National Academy of Sciences of the United States of America. National Academy of Sciences, 2024. https://doi.org/10.1073/pnas.2405605121.","ieee":"J. Svoboda and K. Chatterjee, “Density amplifiers of cooperation for spatial games,” Proceedings of the National Academy of Sciences of the United States of America, vol. 121, no. 50. National Academy of Sciences, 2024.","short":"J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences of the United States of America 121 (2024)."},"OA_place":"publisher","volume":121,"tmp":{"image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"year":"2024","researchdata_availability":"yes","das_tickbox":"1","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"20138"}]},"date_updated":"2026-10-16T08:00:05Z","isi":1,"file":[{"date_updated":"2025-01-02T12:14:15Z","file_id":"18721","success":1,"file_name":"2024_PNAS_Svoboda.pdf","creator":"dernst","file_size":2491151,"checksum":"0115e9090b478e0644308c6dab58605b","relation":"main_file","access_level":"open_access","content_type":"application/pdf","date_created":"2025-01-02T12:14:15Z"}],"oa":1,"publication":"Proceedings of the National Academy of Sciences of the United States of America","oa_version":"Published Version","file_date_updated":"2025-01-02T12:14:15Z","intvolume":" 121","ec_funded":1,"_id":"18703","dataavailabilitystatement":"Code data have been deposited in Code: Amplifiers of Cooperation (DOI: https://doi.org/10.5281/zenodo.10832535)","month":"12","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2024-12-22T23:01:47Z","department":[{"_id":"KrCh"}],"APC_amount":"3143,76 EUR","article_type":"original"},{"has_accepted_license":"1","fulldoi":"https://doi.org/10.46298/lmcs-20(4:11)2024","ddc":["000"],"language":[{"iso":"eng"}],"date_published":"2024-11-12T00:00:00Z","external_id":{"isi":["001367316400002"],"arxiv":["2104.07278"]},"alternative_title":["LMCS"],"arxiv":1,"scopus_import":"1","publication_identifier":{"eissn":["1860-5974"]},"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"}],"page":"11:1-11:34","corr_author":"1","supplementarymaterial":"no","type":"journal_article","article_processing_charge":"Yes","day":"12","DOAJ_listed":"1","ec_funded":1,"_id":"18630","month":"11","date_created":"2024-12-08T23:01:56Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_type":"original","department":[{"_id":"KrCh"}],"das_tickbox":"0","related_material":{"record":[{"id":"10004","status":"public","relation":"earlier_version"}]},"oa":1,"isi":1,"date_updated":"2026-10-16T07:57:38Z","file":[{"content_type":"application/pdf","date_created":"2024-12-09T08:38:48Z","access_level":"open_access","relation":"main_file","checksum":"b3315c74ce18ce0a30ed33d8c9972992","file_size":416814,"file_name":"2024_LMCS_Chatterjee.pdf","creator":"dernst","file_id":"18633","date_updated":"2024-12-09T08:38:48Z","success":1}],"publication":"Logical Methods in Computer Science","oa_version":"Published Version","intvolume":" 20","file_date_updated":"2024-12-09T08:38:48Z","doi":"10.46298/lmcs-20(4:11)2024","OA_type":"gold","citation":{"short":"K. Chatterjee, L. Doyen, Logical Methods in Computer Science 20 (2024) 11:1-11:34.","ieee":"K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,” Logical Methods in Computer Science, vol. 20, no. 4. EPI Sciences, p. 11:1-11:34, 2024.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” Logical Methods in Computer Science. EPI Sciences, 2024. https://doi.org/10.46298/lmcs-20(4:11)2024.","apa":"Chatterjee, K., & Doyen, L. (2024). Stochastic processes with expected stopping time. Logical Methods in Computer Science. EPI Sciences. https://doi.org/10.46298/lmcs-20(4:11)2024","ama":"Chatterjee K, Doyen L. Stochastic processes with expected stopping time. Logical Methods in Computer Science. 2024;20(4):11:1-11:34. doi:10.46298/lmcs-20(4:11)2024","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected Stopping Time.” Logical Methods in Computer Science, vol. 20, no. 4, EPI Sciences, 2024, p. 11:1-11:34, doi:10.46298/lmcs-20(4:11)2024.","ista":"Chatterjee K, Doyen L. 2024. Stochastic processes with expected stopping time. Logical Methods in Computer Science. 20(4), 11:1-11:34."},"publication_status":"published","OA_place":"publisher","researchdata_availability":"no","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"year":"2024","volume":20,"acknowledgement":"The authors 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. The research presented in this paper was partially supported by the grant ERC CoG 863818 (ForM-SMArt).","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"}],"title":"Stochastic processes with expected stopping time","quality_controlled":"1","project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"publisher":"EPI Sciences","issue":"4","status":"public"},{"intvolume":" 14550","publication":"TOOLympics Challenge 2023","oa_version":"Preprint","oa":1,"isi":1,"date_updated":"2026-10-16T07:53:26Z","das_tickbox":"1","related_material":{"record":[{"relation":"research_data","status":"public","id":"23142"}]},"department":[{"_id":"KrCh"}],"date_created":"2024-12-01T23:01:53Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"11","dataavailabilitystatement":"All model files used for the comparison, as well as the resulting log files, are available at DOI 10.5281/zenodo.8219191","_id":"18600","publisher":"Springer Nature","status":"public","quality_controlled":"1","title":"Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report","abstract":[{"text":"The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today’s active areas and tomorrow’s challenges in tool-focused research for quantitative verification.","lang":"eng"}],"acknowledgement":"The authors are ordered alphabetically. This work was supported by DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075 (CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA), by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006 (SMARTITUDE), and by NWO VENI grant 639.021.754.","researchdata_availability":"yes","year":"2024","volume":14550,"OA_place":"repository","publication_status":"published","citation":{"mla":"Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” TOOLympics Challenge 2023, vol. 14550, Springer Nature, 2024, pp. 90–146, doi:10.1007/978-3-031-67695-6_4.","ama":"Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In: TOOLympics Challenge 2023. Vol 14550. Springer Nature; 2024:90-146. doi:10.1007/978-3-031-67695-6_4","ista":"Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550, 90–146.","ieee":"R. Andriushchenko et al., “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report,” in TOOLympics Challenge 2023, 2024, vol. 14550, pp. 90–146.","short":"R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A. Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer, J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters, L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer Nature, 2024, pp. 90–146.","apa":"Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E. M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In TOOLympics Challenge 2023 (Vol. 14550, pp. 90–146). Springer Nature. https://doi.org/10.1007/978-3-031-67695-6_4","chicago":"Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” In TOOLympics Challenge 2023, 14550:90–146. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-67695-6_4."},"OA_type":"green","doi":"10.1007/978-3-031-67695-6_4","arxiv":1,"alternative_title":["LNCS"],"date_published":"2024-11-01T00:00:00Z","external_id":{"arxiv":["2405.13583"],"isi":["001434957500004"]},"language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1007/978-3-031-67695-6_4","day":"01","article_processing_charge":"No","type":"conference","supplementarymaterial":"no","page":"90-146","author":[{"full_name":"Andriushchenko, Roman","first_name":"Roman","last_name":"Andriushchenko"},{"first_name":"Alexander","full_name":"Bork, Alexander","last_name":"Bork"},{"last_name":"Budde","full_name":"Budde, Carlos E.","first_name":"Carlos E."},{"last_name":"Češka","first_name":"Milan","full_name":"Češka, Milan"},{"last_name":"Grover","first_name":"Kush","full_name":"Grover, Kush"},{"last_name":"Hahn","first_name":"Ernst Moritz","full_name":"Hahn, Ernst Moritz"},{"full_name":"Hartmanns, Arnd","first_name":"Arnd","last_name":"Hartmanns"},{"last_name":"Israelsen","full_name":"Israelsen, Bryant","first_name":"Bryant"},{"first_name":"Nils","full_name":"Jansen, Nils","last_name":"Jansen"},{"last_name":"Jeppson","full_name":"Jeppson, Joshua","first_name":"Joshua"},{"last_name":"Junges","first_name":"Sebastian","full_name":"Junges, Sebastian"},{"last_name":"Köhl","full_name":"Köhl, Maximilian A.","first_name":"Maximilian A."},{"last_name":"Könighofer","first_name":"Bettina","full_name":"Könighofer, Bettina"},{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"},{"first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer"},{"last_name":"Parker","first_name":"David","full_name":"Parker, David"},{"first_name":"Stefan","full_name":"Pranger, Stefan","last_name":"Pranger"},{"last_name":"Quatmann","full_name":"Quatmann, Tim","first_name":"Tim"},{"last_name":"Ruijters","full_name":"Ruijters, Enno","first_name":"Enno"},{"last_name":"Taylor","full_name":"Taylor, Landon","first_name":"Landon"},{"last_name":"Volk","first_name":"Matthias","full_name":"Volk, Matthias"},{"full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","last_name":"Weininger","orcid":"0000-0002-0163-2152"},{"last_name":"Zhang","full_name":"Zhang, Zhen","first_name":"Zhen"}],"publication_identifier":{"isbn":["9783031676949"],"eissn":["1611-3349"],"issn":["0302-9743"]},"scopus_import":"1","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.2405.13583"}]},{"OA_type":"gold","doi":"10.4230/LIPIcs.FSTTCS.2024.5","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"volume":323,"researchdata_availability":"no","year":"2024","citation":{"mla":"Asadi, Ali, et al. “Concurrent Stochastic Games with Stateful-Discounted and Parity Objectives: Complexity and Algorithms.” 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 323, 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:10.4230/LIPIcs.FSTTCS.2024.5.","ama":"Asadi A, Chatterjee K, Saona Urmeneta RJ, Svoboda J. Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms. In: 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Vol 323. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.FSTTCS.2024.5","ista":"Asadi A, Chatterjee K, Saona Urmeneta RJ, Svoboda J. 2024. Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms. 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 323, 5.","ieee":"A. Asadi, K. Chatterjee, R. J. Saona Urmeneta, and J. Svoboda, “Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms,” in 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Gujarat, India, 2024, vol. 323.","short":"A. Asadi, K. Chatterjee, R.J. Saona Urmeneta, J. Svoboda, in:, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","apa":"Asadi, A., Chatterjee, K., Saona Urmeneta, R. J., & Svoboda, J. (2024). Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (Vol. 323). Gujarat, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5","chicago":"Asadi, Ali, Krishnendu Chatterjee, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Concurrent Stochastic Games with Stateful-Discounted and Parity Objectives: Complexity and Algorithms.” In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Vol. 323. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5."},"OA_place":"publisher","publication_status":"published","abstract":[{"text":"We study two-player zero-sum concurrent stochastic games with finite state and action space played for an infinite number of steps. In every step, the two players simultaneously and independently choose an action. Given the current state and the chosen actions, the next state is obtained according to a stochastic transition function. An objective is a measurable function on plays (or infinite trajectories) of the game, and the value for an objective is the maximal expectation that the player can guarantee against the adversarial player. We consider: (a) stateful-discounted objectives, which are similar to the classical discounted-sum objectives, but states are associated with different discount factors rather than a single discount factor; and (b) parity objectives, which are a canonical representation for ω-regular objectives. For stateful-discounted objectives, given an ordering of the discount factors, the limit value is the limit of the value of the stateful-discounted objectives, as the discount factors approach zero according to the given order.\r\nThe computational problem we consider is the approximation of the value within an arbitrary\r\nadditive error. The above problem is known to be in EXPSPACE for the limit value of statefuldiscounted objectives and in PSPACE for parity objectives. The best-known algorithms for both the above problems are at least exponential time, with an exponential dependence on the number of states and actions. Our main results for the value approximation problem for the limit value of stateful-discounted objectives and parity objectives are as follows: (a) we establish TFNP[NP] complexity; and (b) we present algorithms that improve the dependency on the number of actions in the exponent from linear to logarithmic. In particular, if the number of states is constant, our algorithms run in polynomial time.","lang":"eng"}],"title":"Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms","acknowledgement":"This research was partially supported by ERC CoG 863818 (ForM-SMArt), Austrian\r\nScience Fund (FWF) 10.55776/COE12, and French Agence Nationale de la Recherche (ANR)\r\nANR-21-CE40-0020 (CONVERGENCE project)","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","status":"public","quality_controlled":"1","month":"12","conference":{"location":"Gujarat, India","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science","end_date":"2024-12-18","start_date":"2024-12-16"},"_id":"17099","ec_funded":1,"department":[{"_id":"KrCh"}],"date_created":"2024-06-03T07:44:27Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa":1,"isi":1,"date_updated":"2026-10-16T08:00:46Z","file":[{"file_name":"2024_LIPIcs_Asadi.pdf","creator":"dernst","file_id":"18777","date_updated":"2025-01-08T09:49:31Z","success":1,"content_type":"application/pdf","date_created":"2025-01-08T09:49:31Z","access_level":"open_access","relation":"main_file","file_size":847960,"checksum":"5b544ab4692b93300b404435c036ddd4"}],"das_tickbox":"0","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"23079"}]},"intvolume":" 323","file_date_updated":"2025-01-08T09:49:31Z","publication":"44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science","oa_version":"Published Version","author":[{"full_name":"Asadi, Ali","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb","first_name":"Ali","last_name":"Asadi"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Saona Urmeneta","orcid":"0000-0001-5103-038X","full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","first_name":"Raimundo J"},{"full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267"}],"publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773553"]},"scopus_import":"1","supplementarymaterial":"no","article_number":"5","corr_author":"1","article_processing_charge":"No","type":"conference","day":"05","fulldoi":"https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5","ddc":["000"],"has_accepted_license":"1","language":[{"iso":"eng"}],"arxiv":1,"alternative_title":["LIPIcs"],"external_id":{"arxiv":["2405.02486"],"isi":["001537516500005"]},"date_published":"2024-12-05T00:00:00Z"},{"quality_controlled":"1","status":"public","project":[{"call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"publisher":"International Joint Conferences on Artificial Intelligence","acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt), the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant, Google Research Award 2023 and the SBI Foundation Hub for Data and Analytics.","title":"Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties","abstract":[{"lang":"eng","text":"Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defned with respect to paths over MDP states. An increasingly\r\npopular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defned in terms of probability distributions over states. Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verifcation techniques. In this work, we consider the problems of certifed policy (i.e. controller) verifcation and synthesis in MDPs under distributional reach-avoidance specifcations. By certifed we mean that, along with a policy, we also aim to synthesize a (checkable) certifcate ensuring that the MDP indeed satisfes the property. Thus, given the target set of distributions and an unsafe set of distributions over MDP states, our goal is to either synthesize a certifcate for a given policy or synthesize a policy along with a certifcate, proving that the target distribution can be reached while avoiding unsafe distributions. To solve this problem, we introduce the novel notion of distributional reach-avoid certifcates and present automated procedures for (1) synthesizing a certifcate for a given policy, and (2) synthesizing a policy together with the certifcate, both providing formal guarantees on certifcate correctness. Our experimental evaluation demonstrates the ability of our method to solve several non-trivial examples, including a multi-agent robot-swarm model, to synthesize certifed policies and to certify existing policies. "}],"citation":{"ieee":"S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties,” in Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, Jeju, Korea, 2024, pp. 3–12.","short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 3–12.","apa":"Akshay, S., Chatterjee, K., Meggendorfer, T., & Zikelic, D. (2024). Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (pp. 3–12). Jeju, Korea: International Joint Conferences on Artificial Intelligence. https://doi.org/10.24963/ijcai.2024/1","chicago":"Akshay, S, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. “Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.” In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, 3–12. International Joint Conferences on Artificial Intelligence, 2024. https://doi.org/10.24963/ijcai.2024/1.","mla":"Akshay, S., et al. “Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.” Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 3–12, doi:10.24963/ijcai.2024/1.","ama":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. In: Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence; 2024:3-12. doi:10.24963/ijcai.2024/1","ista":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2024. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 3–12."},"publication_status":"published","year":"2024","researchdata_availability":"no","doi":"10.24963/ijcai.2024/1","oa_version":"Preprint","publication":"Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence","das_tickbox":"0","date_updated":"2026-10-16T08:08:15Z","oa":1,"date_created":"2024-09-29T22:01:38Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"ec_funded":1,"_id":"18159","conference":{"start_date":"2024-08-03","name":"IJCAI: International Joint Conference on Artificial Intelligence","end_date":"2024-08-09","location":"Jeju, Korea"},"month":"09","day":"01","type":"conference","article_processing_charge":"No","corr_author":"1","page":"3-12","supplementarymaterial":"no","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2405.04015","open_access":"1"}],"scopus_import":"1","publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"author":[{"last_name":"Akshay","first_name":"S","full_name":"Akshay, S"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer"},{"last_name":"Zikelic","orcid":"0000-0002-4681-1699","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"external_id":{"arxiv":["2405.04015"]},"date_published":"2024-09-01T00:00:00Z","arxiv":1,"language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.24963/ijcai.2024/1"},{"language":[{"iso":"eng"}],"date_published":"2024-10-01T00:00:00Z","external_id":{"isi":["000946174300001"]},"ddc":["000"],"fulldoi":"https://doi.org/10.1007/s10703-023-00411-4","has_accepted_license":"1","article_processing_charge":"Yes (via OA deal)","type":"journal_article","day":"01","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Katoen","orcid":"0000-0002-6143-1926","full_name":"Katoen, Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87","first_name":"Joost P"},{"last_name":"Mohr","first_name":"Stefanie","full_name":"Mohr, Stefanie"},{"last_name":"Weininger","first_name":"Maximilian","full_name":"Weininger, Maximilian"},{"first_name":"Tobias","full_name":"Winkler, Tobias","last_name":"Winkler"}],"publication_identifier":{"eissn":["1572-8102"]},"scopus_import":"1","supplementarymaterial":"no","page":"40-80","date_updated":"2026-10-16T08:04:16Z","isi":1,"file":[{"relation":"main_file","checksum":"111e76b76163640a2c89237642af586f","file_size":2614190,"content_type":"application/pdf","date_created":"2025-01-09T07:31:31Z","access_level":"open_access","date_updated":"2025-01-09T07:31:31Z","file_id":"18781","success":1,"file_name":"2024_FromMethodsSys_Chatterjee.pdf","creator":"dernst"}],"oa":1,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"8272"}]},"das_tickbox":"1","file_date_updated":"2025-01-09T07:31:31Z","intvolume":" 63","oa_version":"Published Version","publication":"Formal Methods in System Design","dataavailabilitystatement":"The software and data used to generate the experimental results of this paper are available online(See https://doi.org/10.5281/zenodo.5798108 and https://doi.org/10.5281/zenodo.7233605 for the experiments described in Sect. 5.1 and Sect. 5.2, respectively.).","month":"10","_id":"12738","ec_funded":1,"department":[{"_id":"KrCh"}],"article_type":"original","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2023-03-19T23:00:59Z","abstract":[{"lang":"eng","text":"We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as controllable and adversarial non-determinism. Lexicographic order allows one to consider multiple objectives with a strict preference order. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. For a mixture of reachability and safety objectives, we show that deterministic lexicographically optimal strategies exist 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 the computation of optimal strategies in a sequence of single-objectives games. For omega-regular objectives, we restrict our analysis to one-player games, also known as Markov decision processes. We show that lexicographically optimal strategies exist and need either randomization or finite memory. We present an algorithm that solves the relevant decision problem in polynomial time. We have implemented our algorithms and report experimental results on various case studies."}],"title":"Stochastic games with lexicographic objectives","acknowledgement":"Tobias Winkler and Joost-Pieter Katoen are supported by the DFG RTG 2236 UnRAVeL and the innovation programme under the Marie Skłodowska-Curie grant agreement No. 101008233 (Mission). Krishnendu Chatterjee is supported by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) Project ICT15-003. Maximilian Weininger is supported by the DFG projects 383882557 Statistical Unbounded Verification (SUV) and 427755713 Group-By Objectives in Probabilistic Verification (GOPro). Stefanie Mohr is supported by the DFG RTG 2428 CONVEY. Open Access funding enabled and organized by Projekt DEAL.","status":"public","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"publisher":"Springer Nature","quality_controlled":"1","OA_type":"hybrid","doi":"10.1007/s10703-023-00411-4","volume":63,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"year":"2024","researchdata_availability":"yes","citation":{"ama":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. Stochastic games with lexicographic objectives. Formal Methods in System Design. 2024;63:40-80. doi:10.1007/s10703-023-00411-4","mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Objectives.” Formal Methods in System Design, vol. 63, Springer Nature, 2024, pp. 40–80, doi:10.1007/s10703-023-00411-4.","ista":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2024. Stochastic games with lexicographic objectives. Formal Methods in System Design. 63, 40–80.","short":"K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods in System Design 63 (2024) 40–80.","ieee":"K. Chatterjee, J. P. Katoen, S. Mohr, M. Weininger, and T. Winkler, “Stochastic games with lexicographic objectives,” Formal Methods in System Design, vol. 63. Springer Nature, pp. 40–80, 2024.","chicago":"Chatterjee, Krishnendu, Joost P Katoen, Stefanie Mohr, Maximilian Weininger, and Tobias Winkler. “Stochastic Games with Lexicographic Objectives.” Formal Methods in System Design. Springer Nature, 2024. https://doi.org/10.1007/s10703-023-00411-4.","apa":"Chatterjee, K., Katoen, J. P., Mohr, S., Weininger, M., & Winkler, T. (2024). Stochastic games with lexicographic objectives. Formal Methods in System Design. Springer Nature. https://doi.org/10.1007/s10703-023-00411-4"},"OA_place":"publisher","publication_status":"published"},{"fulldoi":"https://doi.org/10.24963/ijcai.2024/741","external_id":{"arxiv":["2312.13912"]},"date_published":"2024-09-01T00:00:00Z","arxiv":1,"language":[{"iso":"eng"}],"page":"6707-6715","corr_author":"1","supplementarymaterial":"no","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2312.13912","open_access":"1"}],"publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"scopus_import":"1","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Kafshdar Goharshadi","orcid":"0000-0002-8595-0587","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan"},{"full_name":"Karrabi, Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757","first_name":"Mehrdad","orcid":"0009-0007-5253-9170","last_name":"Karrabi"},{"first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","last_name":"Novotný"},{"last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"day":"01","type":"conference","article_processing_charge":"No","date_created":"2024-09-29T22:01:39Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"ec_funded":1,"_id":"18160","conference":{"location":"Jeju, South Korea","end_date":"2024-08-09","name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2024-08-03"},"month":"09","oa_version":"Preprint","publication":"33rd International Joint Conference on Artificial Intelligence","das_tickbox":"0","date_updated":"2026-10-16T08:07:05Z","oa":1,"publication_status":"published","OA_place":"repository","citation":{"ista":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving long-run average reward robust MDPs via stochastic games. 33rd International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 6707–6715.","mla":"Chatterjee, Krishnendu, et al. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” 33rd International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–15, doi:10.24963/ijcai.2024/741.","ama":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. Solving long-run average reward robust MDPs via stochastic games. In: 33rd International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence; 2024:6707-6715. doi:10.24963/ijcai.2024/741","apa":"Chatterjee, K., Goharshady, E., Karrabi, M., Novotný, P., & Zikelic, D. (2024). Solving long-run average reward robust MDPs via stochastic games. In 33rd International Joint Conference on Artificial Intelligence (pp. 6707–6715). Jeju, South Korea: International Joint Conferences on Artificial Intelligence. https://doi.org/10.24963/ijcai.2024/741","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Petr Novotný, and Dorde Zikelic. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” In 33rd International Joint Conference on Artificial Intelligence, 6707–15. International Joint Conferences on Artificial Intelligence, 2024. https://doi.org/10.24963/ijcai.2024/741.","ieee":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, and D. Zikelic, “Solving long-run average reward robust MDPs via stochastic games,” in 33rd International Joint Conference on Artificial Intelligence, Jeju, South Korea, 2024, pp. 6707–6715.","short":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, D. Zikelic, in:, 33rd International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–6715."},"researchdata_availability":"no","year":"2024","doi":"10.24963/ijcai.2024/741","OA_type":"green","quality_controlled":"1","status":"public","publisher":"International Joint Conferences on Artificial Intelligence","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Czech Science Foundation\r\ngrant no. GA23-06963S.","abstract":[{"lang":"eng","text":"Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs in which all uncertainty sets are polytopes and study the problem of solving long-run average reward polytopic RMDPs. We present a novel perspective on this problem and show that it can be reduced to solving long-run average reward turn-based stochastic games with finite state and action spaces. This reduction allows us to derive several important consequences that were hitherto not known to hold for polytopic RMDPs. First, we derive new computational complexity bounds for solving long-run average reward polytopic RMDPs, showing for the first time that the threshold decision problem for them is in NP∩CONP and that they admit a randomized algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is much more efficient in solving long-run average reward polytopic RMDPs compared to state-of-the-art methods based on value iteration. "}],"title":"Solving long-run average reward robust MDPs via stochastic games"},{"quality_controlled":"1","publisher":"Elsevier","status":"public","acknowledgement":"Krishnendu Chatterjee reports financial support was provided by European Research Council.","title":"Entropic risk for turn-based stochastic games","abstract":[{"text":"Entropic risk (ERisk) is an established risk measure in finance, quantifying risk by an exponential re-weighting of rewards. We study ERisk for the first time in the context of turn-based stochastic games with the total reward objective. This gives rise to an objective function that demands the control of systems in a risk-averse manner. We show that the resulting games are determined and, in particular, admit optimal memoryless deterministic strategies. This contrasts risk measures that previously have been considered in the special case of Markov decision processes and that require randomization and/or memory. We provide several results on the decidability and the computational complexity of the threshold problem, i.e. whether the optimal value of ERisk exceeds a given threshold. Furthermore, an approximation algorithm for the optimal value of ERisk is provided.","lang":"eng"}],"OA_place":"publisher","citation":{"chicago":"Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer. “Entropic Risk for Turn-Based Stochastic Games.” Information and Computation. Elsevier, 2024. https://doi.org/10.1016/j.ic.2024.105214.","apa":"Baier, C., Chatterjee, K., Meggendorfer, T., & Piribauer, J. (2024). Entropic risk for turn-based stochastic games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2024.105214","short":"C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, Information and Computation 301 (2024).","ieee":"C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Entropic risk for turn-based stochastic games,” Information and Computation, vol. 301. Elsevier, 2024.","ista":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2024. Entropic risk for turn-based stochastic games. Information and Computation. 301, 105214.","ama":"Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Entropic risk for turn-based stochastic games. Information and Computation. 2024;301. doi:10.1016/j.ic.2024.105214","mla":"Baier, Christel, et al. “Entropic Risk for Turn-Based Stochastic Games.” Information and Computation, vol. 301, 105214, Elsevier, 2024, doi:10.1016/j.ic.2024.105214."},"publication_status":"published","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"volume":301,"researchdata_availability":"no","year":"2024","doi":"10.1016/j.ic.2024.105214","OA_type":"hybrid","oa_version":"Published Version","publication":"Information and Computation","intvolume":" 301","file_date_updated":"2025-01-09T13:49:03Z","das_tickbox":"0","related_material":{"record":[{"relation":"earlier_version","id":"14417","status":"public"}]},"oa":1,"isi":1,"file":[{"file_id":"18817","date_updated":"2025-01-09T13:49:03Z","success":1,"file_name":"2024_InformationComputation_Baier.pdf","creator":"dernst","file_size":724703,"checksum":"f68e0c2f46f9b9c86815406bcf2ee2d4","relation":"main_file","access_level":"open_access","content_type":"application/pdf","date_created":"2025-01-09T13:49:03Z"}],"date_updated":"2026-10-16T08:04:31Z","date_created":"2024-09-01T22:01:07Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_type":"original","department":[{"_id":"KrCh"}],"_id":"17474","month":"12","day":"01","type":"journal_article","article_processing_charge":"Yes (in subscription journal)","article_number":"105214","corr_author":"1","supplementarymaterial":"no","scopus_import":"1","publication_identifier":{"issn":["0890-5401"],"eissn":["1090-2651"]},"author":[{"last_name":"Baier","full_name":"Baier, Christel","first_name":"Christel"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"full_name":"Piribauer, Jakob","first_name":"Jakob","last_name":"Piribauer"}],"external_id":{"isi":["001301143400001"],"arxiv":["2307.06611"]},"date_published":"2024-12-01T00:00:00Z","arxiv":1,"language":[{"iso":"eng"}],"has_accepted_license":"1","fulldoi":"https://doi.org/10.1016/j.ic.2024.105214","ddc":["000"]},{"language":[{"iso":"eng"}],"date_published":"2024-05-01T00:00:00Z","external_id":{"isi":["001270140300143"]},"fulldoi":"https://doi.org/10.1109/noms59830.2024.10575579","type":"conference","article_processing_charge":"No","day":"01","publication_identifier":{"isbn":["9798350327946"],"eissn":["2374-9709"]},"scopus_import":"1","main_file_link":[{"url":"https://schmiste.github.io/noms24.pdf","open_access":"1"}],"author":[{"full_name":"Ceylan, Esra","id":"cb1ca1d8-dcc0-11ef-baa5-9f1b3ef75933","first_name":"Esra","last_name":"Ceylan"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"first_name":"Stefan","full_name":"Schmid, Stefan","last_name":"Schmid"},{"last_name":"Svoboda","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","first_name":"Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"}],"corr_author":"1","supplementarymaterial":"no","das_tickbox":"0","oa":1,"date_updated":"2026-10-16T08:07:55Z","isi":1,"publication":"NOMS 2024-2024 IEEE Network Operations and Management Symposium","oa_version":"Submitted Version","conference":{"start_date":"2024-05-06","name":"NOMS: Network Operations and Management Symposiu ","end_date":"2024-05-10","location":"Seoul, Republic of Korea"},"_id":"18925","ec_funded":1,"month":"05","date_created":"2025-01-27T15:06:45Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"acknowledgement":"Research was supported by the Austrian Science Fund (FWF), project I 5025-N (DELTA), 2020-2024. Esra Ceylan’s research was supported by FFG, FEMtech Praktika für Studentinnen. Jakub Svoboda and Krishnendu Chatterjee were supported by the European Research Council (ERC) CoG 863818 (ForM-SMArt).","title":"Congestion-free rerouting of network flows: Hardness and an FPT algorithm","abstract":[{"lang":"eng","text":"Given the increasingly stringent requirements on the performance and efficiency of communication networks, over the last years, great efforts have been made to render networks more flexible and programmable. In particular, modern networks support a flexible rerouting of flows, e.g., depending on the dynamically changing traffic or network conditions. However, the underlying algorithmic problems are still not well-understood today.In this paper, we revisit the k-Network Flow Update problem that asks for a schedule to reroute k unsplittable flows from their current paths to the given new paths, in a congestion-free manner in a capacitated network. We show that the problem is already NP-hard for three acyclic flows on simple directed graphs. Our main contribution is an efficient algorithm for sparse networks; specifically the algorithm is fixed parameter tractable in the number of flows and the treewidth of a graph that is the union of all flows. Our results also settle the open complexity question in the literature."}],"quality_controlled":"1","publisher":"IEEE","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"name":"Graphical Games","_id":"bd622a5c-d553-11ed-ba76-bae280ba8aff","grant_number":"894907"}],"status":"public","doi":"10.1109/noms59830.2024.10575579","OA_type":"green","OA_place":"other","publication_status":"published","citation":{"ieee":"E. Ceylan, K. Chatterjee, S. Schmid, and J. Svoboda, “Congestion-free rerouting of network flows: Hardness and an FPT algorithm,” in NOMS 2024-2024 IEEE Network Operations and Management Symposium, Seoul, Republic of Korea, 2024.","short":"E. Ceylan, K. Chatterjee, S. Schmid, J. Svoboda, in:, NOMS 2024-2024 IEEE Network Operations and Management Symposium, IEEE, 2024.","apa":"Ceylan, E., Chatterjee, K., Schmid, S., & Svoboda, J. (2024). Congestion-free rerouting of network flows: Hardness and an FPT algorithm. In NOMS 2024-2024 IEEE Network Operations and Management Symposium. Seoul, Republic of Korea: IEEE. https://doi.org/10.1109/noms59830.2024.10575579","chicago":"Ceylan, Esra, Krishnendu Chatterjee, Stefan Schmid, and Jakub Svoboda. “Congestion-Free Rerouting of Network Flows: Hardness and an FPT Algorithm.” In NOMS 2024-2024 IEEE Network Operations and Management Symposium. IEEE, 2024. https://doi.org/10.1109/noms59830.2024.10575579.","mla":"Ceylan, Esra, et al. “Congestion-Free Rerouting of Network Flows: Hardness and an FPT Algorithm.” NOMS 2024-2024 IEEE Network Operations and Management Symposium, IEEE, 2024, doi:10.1109/noms59830.2024.10575579.","ama":"Ceylan E, Chatterjee K, Schmid S, Svoboda J. Congestion-free rerouting of network flows: Hardness and an FPT algorithm. In: NOMS 2024-2024 IEEE Network Operations and Management Symposium. IEEE; 2024. doi:10.1109/noms59830.2024.10575579","ista":"Ceylan E, Chatterjee K, Schmid S, Svoboda J. 2024. Congestion-free rerouting of network flows: Hardness and an FPT algorithm. NOMS 2024-2024 IEEE Network Operations and Management Symposium. NOMS: Network Operations and Management Symposiu ."},"researchdata_availability":"no","year":"2024"},{"arxiv":1,"date_published":"2024-06-17T00:00:00Z","external_id":{"arxiv":["2405.04420"]},"language":[{"iso":"eng"}],"ddc":["000"],"fulldoi":"https://doi.org/10.1145/3662158.3662769","has_accepted_license":"1","day":"17","article_processing_charge":"Yes (via OA deal)","type":"conference","supplementarymaterial":"no","corr_author":"1","page":"268-278","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Ebrahimzadeh","first_name":"Amirali","full_name":"Ebrahimzadeh, Amirali"},{"full_name":"Karrabi, Mehrdad","first_name":"Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757","orcid":"0009-0007-5253-9170","last_name":"Karrabi"},{"last_name":"Pietrzak","orcid":"0000-0002-9139-1654","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z","full_name":"Pietrzak, Krzysztof Z"},{"first_name":"Michelle X","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","full_name":"Yeo, Michelle X","orcid":"0009-0001-3676-4809","last_name":"Yeo"},{"first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699"}],"publication_identifier":{"isbn":["9798400706684"]},"scopus_import":"1","file_date_updated":"2024-07-29T07:18:12Z","publication":"Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing","oa_version":"Published Version","date_updated":"2026-10-16T08:09:09Z","file":[{"creator":"dernst","file_name":"2024_ACM_Chatterjee.pdf","date_updated":"2024-07-29T07:18:12Z","file_id":"17334","success":1,"access_level":"open_access","content_type":"application/pdf","date_created":"2024-07-29T07:18:12Z","checksum":"6122bd97b42751ff81c452a19970f67d","file_size":832034,"relation":"main_file"}],"oa":1,"das_tickbox":"0","department":[{"_id":"KrCh"},{"_id":"KrPi"}],"date_created":"2024-07-28T22:01:10Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"06","ec_funded":1,"_id":"17328","conference":{"start_date":"2024-06-17","location":"Nantes, France","end_date":"2024-06-21","name":"PODC: Symposium on Principles of Distributed Computing"},"status":"public","publisher":"Association for Computing Machinery","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"quality_controlled":"1","title":"Fully automated selfish mining analysis in efficient proof systems blockchains","abstract":[{"text":"We study selfish mining attacks in longest-chain blockchains like Bitcoin, but where the proof of work is replaced with efficient proof systems - like proofs of stake or proofs of space - and consider the problem of computing an optimal selfish mining attack which maximizes expected relative revenue of the adversary, thus minimizing the chain quality. To this end, we propose a novel selfish mining attack that aims to maximize this objective and formally model the attack as a Markov decision process (MDP). We then present a formal analysis procedure which computes an ϵ-tight lower bound on the optimal expected relative revenue in the MDP and a strategy that achieves this ϵ-tight lower bound, where ϵ > 0 may be any specified precision. Our analysis is fully automated and provides formal guarantees on the correctness. We evaluate our selfish mining attack and observe that it achieves superior expected relative revenue compared to two considered baselines.\r\nIn concurrent work [Sarenche FC'24] does an automated analysis on selfish mining in predictable longest-chain blockchains based on efficient proof systems. Predictable means the randomness for the challenges is fixed for many blocks (as used e.g., in Ouroboros), while we consider unpredictable (Bitcoin-like) chains where the challenge is derived from the previous block.","lang":"eng"}],"acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) grant and the MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms) grant.\r\n","year":"2024","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"researchdata_availability":"no","publication_status":"published","citation":{"ama":"Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D. Fully automated selfish mining analysis in efficient proof systems blockchains. In: Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing. Association for Computing Machinery; 2024:268-278. doi:10.1145/3662158.3662769","mla":"Chatterjee, Krishnendu, et al. “Fully Automated Selfish Mining Analysis in Efficient Proof Systems Blockchains.” Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing, Association for Computing Machinery, 2024, pp. 268–78, doi:10.1145/3662158.3662769.","ista":"Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D. 2024. Fully automated selfish mining analysis in efficient proof systems blockchains. Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing. PODC: Symposium on Principles of Distributed Computing, 268–278.","short":"K. Chatterjee, A. Ebrahimzadeh, M. Karrabi, K.Z. Pietrzak, M.X. Yeo, D. Zikelic, in:, Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing, Association for Computing Machinery, 2024, pp. 268–278.","ieee":"K. Chatterjee, A. Ebrahimzadeh, M. Karrabi, K. Z. Pietrzak, M. X. Yeo, and D. Zikelic, “Fully automated selfish mining analysis in efficient proof systems blockchains,” in Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing, Nantes, France, 2024, pp. 268–278.","chicago":"Chatterjee, Krishnendu, Amirali Ebrahimzadeh, Mehrdad Karrabi, Krzysztof Z Pietrzak, Michelle X Yeo, and Dorde Zikelic. “Fully Automated Selfish Mining Analysis in Efficient Proof Systems Blockchains.” In Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing, 268–78. Association for Computing Machinery, 2024. https://doi.org/10.1145/3662158.3662769.","apa":"Chatterjee, K., Ebrahimzadeh, A., Karrabi, M., Pietrzak, K. Z., Yeo, M. X., & Zikelic, D. (2024). Fully automated selfish mining analysis in efficient proof systems blockchains. In Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing (pp. 268–278). Nantes, France: Association for Computing Machinery. https://doi.org/10.1145/3662158.3662769"},"doi":"10.1145/3662158.3662769"}]