--- _id: '15108' abstract: - lang: eng 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." article_processing_charge: No author: - first_name: Valentin full_name: Hübner, Valentin id: 2c8aa207-dc7d-11ea-9b2f-f22972ecd910 last_name: Hübner orcid: 0009-0001-5009-4987 - first_name: Maria full_name: Kleshnina, Maria last_name: Kleshnina citation: ama: Hübner V, Kleshnina M. Computer code for “Efficiency and resilience of cooperation in asymmetric social dilemmas.” 2024. doi: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 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. ieee: V. Hübner and M. Kleshnina, “Computer code for ‘Efficiency and resilience of cooperation in asymmetric social dilemmas.’” Zenodo, 2024. ista: Hübner V, Kleshnina M. 2024. Computer code for ‘Efficiency and resilience of cooperation in asymmetric social dilemmas’, Zenodo, 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. short: V. Hübner, M. Kleshnina, (2024). corr_author: '1' date_created: 2024-03-12T13:02:58Z date_published: 2024-02-09T00:00:00Z date_updated: 2026-10-15T10:10:25Z day: '09' ddc: - '000' department: - _id: KrCh doi: 10.5281/ZENODO.10639167 fulldoi: https://doi.org/10.5281/ZENODO.10639167 has_accepted_license: '1' main_file_link: - open_access: '1' url: https://10.5281/zenodo.10639167 month: '02' oa: 1 oa_version: Published Version publisher: Zenodo related_material: record: - id: '15083' relation: used_in_publication status: public status: public title: Computer code for "Efficiency and resilience of cooperation in asymmetric social dilemmas" tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: research_data_reference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2024' ... --- _id: '18155' abstract: - lang: eng 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. 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. alternative_title: - LNCS article_processing_charge: Yes (in subscription journal) arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Amir Kafshdar full_name: Goharshady, Amir Kafshdar id: 391365CE-F248-11E8-B48F-1D18A9856A87 last_name: Goharshady orcid: 0000-0003-1702-6584 - first_name: Ehsan full_name: Goharshady, Ehsan last_name: Goharshady - first_name: Mehrdad full_name: Karrabi, Mehrdad id: 67638922-f394-11eb-9cf6-f20423e08757 last_name: Karrabi orcid: 0009-0007-5253-9170 - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 citation: 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' 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. 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. 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. conference: end_date: 2024-09-13 location: Milan, Italy name: 'FM: Formal Methods' start_date: 2024-09-09 corr_author: '1' das_tickbox: '1' dataavailabilitystatement: The implementations of the algorithms mentioned in the experiments section and the benchmarks are available at doi.org/10.5281/zenodo.12518217. date_created: 2024-09-29T22:01:37Z date_published: 2024-09-11T00:00:00Z date_updated: 2026-10-16T07:29:39Z day: '11' ddc: - '000' department: - _id: KrCh doi: 10.1007/978-3-031-71162-6_31 ec_funded: 1 external_id: arxiv: - '2403.05386' isi: - '001336893300031' file: - access_level: open_access checksum: 223845be9e754681ee218866827c95e7 content_type: application/pdf creator: dernst date_created: 2024-10-01T09:56:54Z date_updated: 2024-10-01T09:56:54Z file_id: '18165' file_name: 2024_LNCS_Chatterjee.pdf file_size: 650495 relation: main_file success: 1 file_date_updated: 2024-10-01T09:56:54Z fulldoi: https://doi.org/10.1007/978-3-031-71162-6_31 has_accepted_license: '1' intvolume: ' 14933' isi: 1 language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: 600-619 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) publication_identifier: eissn: - 1611-3349 isbn: - '9783031711619' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '22798' relation: research_data status: public researchdata_availability: yes scopus_import: '1' status: public supplementarymaterial: no title: Sound and complete witnesses for template-based verification of LTL properties on polynomial programs tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 14933 year: '2024' ... --- OA_place: repository OA_type: green _id: '22798' 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 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu last_name: Chatterjee - first_name: Amir full_name: ' Kafshdar Goharshady, Amir' last_name: ' Kafshdar Goharshady' - first_name: Ehsan full_name: Kafshdar Goharshady, Ehsan last_name: Kafshdar Goharshady - first_name: Mehrdad full_name: Karrabi, Mehrdad last_name: Karrabi - first_name: Ðorđe full_name: Žikelić, Ðorđe last_name: Žikelić citation: 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 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 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. 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. 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. 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. short: K. Chatterjee, A.   Kafshdar Goharshady, E. Kafshdar Goharshady, M. Karrabi, Ð. Žikelić, (2024). date_created: 2026-09-03T11:50:15Z date_published: 2024-06-24T00:00:00Z date_updated: 2026-10-16T07:29:39Z day: '24' ddc: - '000' department: - _id: KrCh doi: 10.5281/zenodo.12518216 fulldoi: https://doi.org/10.5281/zenodo.12518216 main_file_link: - open_access: '1' url: https://doi.org/10.5281/zenodo.12518216 month: '06' oa: 1 oa_version: None publisher: Repository related_material: record: - id: '18155' relation: used_in_publication status: public status: public title: Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs type: research_data_reference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 year: '2024' ... --- APC_amount: 3143,76 EUR OA_place: publisher OA_type: hybrid _id: '18703' 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.' acknowledgement: J.S. and K.C. were supported by the European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12. article_number: e2405605121 article_processing_charge: Yes article_type: original author: - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: 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. 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. short: J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences of the United States of America 121 (2024). corr_author: '1' das_tickbox: '1' dataavailabilitystatement: 'Code data have been deposited in Code: Amplifiers of Cooperation (DOI: https://doi.org/10.5281/zenodo.10832535)' date_created: 2024-12-22T23:01:47Z date_published: 2024-12-10T00:00:00Z date_updated: 2026-10-16T08:00:05Z day: '10' ddc: - '000' department: - _id: KrCh doi: 10.1073/pnas.2405605121 ec_funded: 1 external_id: isi: - '001379596100014' pmid: - '39642209' file: - access_level: open_access checksum: 0115e9090b478e0644308c6dab58605b content_type: application/pdf creator: dernst date_created: 2025-01-02T12:14:15Z date_updated: 2025-01-02T12:14:15Z file_id: '18721' file_name: 2024_PNAS_Svoboda.pdf file_size: 2491151 relation: main_file success: 1 file_date_updated: 2025-01-02T12:14:15Z fulldoi: https://doi.org/10.1073/pnas.2405605121 has_accepted_license: '1' intvolume: ' 121' isi: 1 issue: '50' language: - iso: eng license: https://creativecommons.org/licenses/by-nc-nd/4.0/ month: '12' oa: 1 oa_version: Published Version pmid: 1 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Proceedings of the National Academy of Sciences of the United States of America publication_identifier: eissn: - 1091-6490 issn: - 0027-8424 publication_status: published publisher: National Academy of Sciences quality_controlled: '1' related_material: record: - id: '20138' relation: dissertation_contains status: public researchdata_availability: yes scopus_import: '1' status: public supplementarymaterial: yes title: Density amplifiers of cooperation for spatial games tmp: image: /images/cc_by_nc_nd.png legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) short: CC BY-NC-ND (4.0) type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 121 year: '2024' ... --- DOAJ_listed: '1' OA_place: publisher OA_type: gold _id: '18630' abstract: - lang: eng text: 'Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs.' 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). alternative_title: - LMCS article_processing_charge: Yes article_type: original arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen citation: 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 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 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. 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. ista: Chatterjee K, Doyen L. 2024. Stochastic processes with expected stopping time. Logical Methods in Computer Science. 20(4), 11:1-11:34. 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. short: K. Chatterjee, L. Doyen, Logical Methods in Computer Science 20 (2024) 11:1-11:34. corr_author: '1' das_tickbox: '0' date_created: 2024-12-08T23:01:56Z date_published: 2024-11-12T00:00:00Z date_updated: 2026-10-16T07:57:38Z day: '12' ddc: - '000' department: - _id: KrCh doi: 10.46298/lmcs-20(4:11)2024 ec_funded: 1 external_id: arxiv: - '2104.07278' isi: - '001367316400002' file: - access_level: open_access checksum: b3315c74ce18ce0a30ed33d8c9972992 content_type: application/pdf creator: dernst date_created: 2024-12-09T08:38:48Z date_updated: 2024-12-09T08:38:48Z file_id: '18633' file_name: 2024_LMCS_Chatterjee.pdf file_size: 416814 relation: main_file success: 1 file_date_updated: 2024-12-09T08:38:48Z fulldoi: https://doi.org/10.46298/lmcs-20(4:11)2024 has_accepted_license: '1' intvolume: ' 20' isi: 1 issue: '4' language: - iso: eng month: '11' oa: 1 oa_version: Published Version page: 11:1-11:34 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Logical Methods in Computer Science publication_identifier: eissn: - 1860-5974 publication_status: published publisher: EPI Sciences quality_controlled: '1' related_material: record: - id: '10004' relation: earlier_version status: public researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: Stochastic processes with expected stopping time tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 20 year: '2024' ... --- OA_place: repository OA_type: green _id: '18600' abstract: - lang: eng 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.' 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. alternative_title: - LNCS article_processing_charge: No arxiv: 1 author: - first_name: Roman full_name: Andriushchenko, Roman last_name: Andriushchenko - first_name: Alexander full_name: Bork, Alexander last_name: Bork - first_name: Carlos E. full_name: Budde, Carlos E. last_name: Budde - first_name: Milan full_name: Češka, Milan last_name: Češka - first_name: Kush full_name: Grover, Kush last_name: Grover - first_name: Ernst Moritz full_name: Hahn, Ernst Moritz last_name: Hahn - first_name: Arnd full_name: Hartmanns, Arnd last_name: Hartmanns - first_name: Bryant full_name: Israelsen, Bryant last_name: Israelsen - first_name: Nils full_name: Jansen, Nils last_name: Jansen - first_name: Joshua full_name: Jeppson, Joshua last_name: Jeppson - first_name: Sebastian full_name: Junges, Sebastian last_name: Junges - first_name: Maximilian A. full_name: Köhl, Maximilian A. last_name: Köhl - first_name: Bettina full_name: Könighofer, Bettina last_name: Könighofer - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: David full_name: Parker, David last_name: Parker - first_name: Stefan full_name: Pranger, Stefan last_name: Pranger - first_name: Tim full_name: Quatmann, Tim last_name: Quatmann - first_name: Enno full_name: Ruijters, Enno last_name: Ruijters - first_name: Landon full_name: Taylor, Landon last_name: Taylor - first_name: Matthias full_name: Volk, Matthias last_name: Volk - first_name: Maximilian full_name: Weininger, Maximilian id: 02ab0197-cc70-11ed-ab61-918e71f56881 last_name: Weininger orcid: 0000-0002-0163-2152 - first_name: Zhen full_name: Zhang, Zhen last_name: Zhang citation: 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' 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.' 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.' 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.' 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.' 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. das_tickbox: '1' dataavailabilitystatement: All model files used for the comparison, as well as the resulting log files, are available at DOI 10.5281/zenodo.8219191 date_created: 2024-12-01T23:01:53Z date_published: 2024-11-01T00:00:00Z date_updated: 2026-10-16T07:53:26Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-031-67695-6_4 external_id: arxiv: - '2405.13583' isi: - '001434957500004' fulldoi: https://doi.org/10.1007/978-3-031-67695-6_4 intvolume: ' 14550' isi: 1 language: - iso: eng main_file_link: - open_access: '1' url: ' https://doi.org/10.48550/arXiv.2405.13583' month: '11' oa: 1 oa_version: Preprint page: 90-146 publication: TOOLympics Challenge 2023 publication_identifier: eissn: - 1611-3349 isbn: - '9783031676949' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '23142' relation: research_data status: public researchdata_availability: yes scopus_import: '1' status: public supplementarymaterial: no title: 'Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report' type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 14550 year: '2024' ... --- OA_place: publisher OA_type: gold _id: '17099' abstract: - lang: eng 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." 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)" alternative_title: - LIPIcs article_number: '5' article_processing_charge: No arxiv: 1 author: - first_name: Ali full_name: Asadi, Ali id: 02d96aae-000e-11ec-b801-cadd0a5eefbb last_name: Asadi - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Raimundo J full_name: Saona Urmeneta, Raimundo J id: BD1DF4C4-D767-11E9-B658-BC13E6697425 last_name: Saona Urmeneta orcid: 0000-0001-5103-038X - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 citation: 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' 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.' 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.' 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.' 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.' 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. conference: end_date: 2024-12-18 location: Gujarat, India name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science' start_date: 2024-12-16 corr_author: '1' das_tickbox: '0' date_created: 2024-06-03T07:44:27Z date_published: 2024-12-05T00:00:00Z date_updated: 2026-10-16T08:00:46Z day: '05' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.FSTTCS.2024.5 ec_funded: 1 external_id: arxiv: - '2405.02486' isi: - '001537516500005' file: - access_level: open_access checksum: 5b544ab4692b93300b404435c036ddd4 content_type: application/pdf creator: dernst date_created: 2025-01-08T09:49:31Z date_updated: 2025-01-08T09:49:31Z file_id: '18777' file_name: 2024_LIPIcs_Asadi.pdf file_size: 847960 relation: main_file success: 1 file_date_updated: 2025-01-08T09:49:31Z fulldoi: https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5 has_accepted_license: '1' intvolume: ' 323' isi: 1 language: - iso: eng month: '12' oa: 1 oa_version: Published Version project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science publication_identifier: isbn: - '9783959773553' issn: - 1868-8969 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' related_material: record: - id: '23079' relation: dissertation_contains status: public researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: 'Concurrent stochastic games with stateful-discounted and parity objectives: Complexity and algorithms' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 323 year: '2024' ... --- _id: '18159' 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. " 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. article_processing_charge: No arxiv: 1 author: - first_name: S full_name: Akshay, S last_name: Akshay - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 citation: 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' 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. 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. 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.' 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. 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. conference: end_date: 2024-08-09 location: Jeju, Korea name: 'IJCAI: International Joint Conference on Artificial Intelligence' start_date: 2024-08-03 corr_author: '1' das_tickbox: '0' date_created: 2024-09-29T22:01:38Z date_published: 2024-09-01T00:00:00Z date_updated: 2026-10-16T08:08:15Z day: '01' department: - _id: KrCh doi: 10.24963/ijcai.2024/1 ec_funded: 1 external_id: arxiv: - '2405.04015' fulldoi: https://doi.org/10.24963/ijcai.2024/1 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2405.04015 month: '09' oa: 1 oa_version: Preprint page: 3-12 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence publication_identifier: isbn: - '9781956792041' issn: - 1045-0823 publication_status: published publisher: International Joint Conferences on Artificial Intelligence quality_controlled: '1' researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 year: '2024' ... --- OA_place: publisher OA_type: hybrid _id: '12738' 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. 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. article_processing_charge: Yes (via OA deal) article_type: original author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Joost P full_name: Katoen, Joost P id: 4524F760-F248-11E8-B48F-1D18A9856A87 last_name: Katoen orcid: 0000-0002-6143-1926 - first_name: Stefanie full_name: Mohr, Stefanie last_name: Mohr - first_name: Maximilian full_name: Weininger, Maximilian last_name: Weininger - first_name: Tobias full_name: Winkler, Tobias last_name: Winkler 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 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 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. 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. 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. 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. short: K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods in System Design 63 (2024) 40–80. das_tickbox: '1' 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.). date_created: 2023-03-19T23:00:59Z date_published: 2024-10-01T00:00:00Z date_updated: 2026-10-16T08:04:16Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.1007/s10703-023-00411-4 ec_funded: 1 external_id: isi: - '000946174300001' file: - access_level: open_access checksum: 111e76b76163640a2c89237642af586f content_type: application/pdf creator: dernst date_created: 2025-01-09T07:31:31Z date_updated: 2025-01-09T07:31:31Z file_id: '18781' file_name: 2024_FromMethodsSys_Chatterjee.pdf file_size: 2614190 relation: main_file success: 1 file_date_updated: 2025-01-09T07:31:31Z fulldoi: https://doi.org/10.1007/s10703-023-00411-4 has_accepted_license: '1' intvolume: ' 63' isi: 1 language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 40-80 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 25892FC0-B435-11E9-9278-68D0E5697425 grant_number: ICT15-003 name: Efficient Algorithms for Computer Aided Verification publication: Formal Methods in System Design publication_identifier: eissn: - 1572-8102 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '8272' relation: earlier_version status: public researchdata_availability: yes scopus_import: '1' status: public supplementarymaterial: no title: Stochastic games with lexicographic objectives tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 63 year: '2024' ... --- OA_place: repository OA_type: green _id: '18160' 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. ' 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." article_processing_charge: No arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ehsan full_name: Kafshdar Goharshadi, Ehsan id: 103b4fa0-896a-11ed-bdf8-87b697bef40d last_name: Kafshdar Goharshadi orcid: 0000-0002-8595-0587 - first_name: Mehrdad full_name: Karrabi, Mehrdad id: 67638922-f394-11eb-9cf6-f20423e08757 last_name: Karrabi orcid: 0009-0007-5253-9170 - first_name: Petr full_name: Novotný, Petr id: 3CC3B868-F248-11E8-B48F-1D18A9856A87 last_name: Novotný - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 citation: 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. 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. 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. conference: end_date: 2024-08-09 location: Jeju, South Korea name: 'IJCAI: International Joint Conference on Artificial Intelligence' start_date: 2024-08-03 corr_author: '1' das_tickbox: '0' date_created: 2024-09-29T22:01:39Z date_published: 2024-09-01T00:00:00Z date_updated: 2026-10-16T08:07:05Z day: '01' department: - _id: KrCh doi: 10.24963/ijcai.2024/741 ec_funded: 1 external_id: arxiv: - '2312.13912' fulldoi: https://doi.org/10.24963/ijcai.2024/741 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2312.13912 month: '09' oa: 1 oa_version: Preprint page: 6707-6715 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: 33rd International Joint Conference on Artificial Intelligence publication_identifier: isbn: - '9781956792041' issn: - 1045-0823 publication_status: published publisher: International Joint Conferences on Artificial Intelligence quality_controlled: '1' researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: Solving long-run average reward robust MDPs via stochastic games type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 year: '2024' ... --- OA_place: publisher OA_type: hybrid _id: '17474' abstract: - lang: eng 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. acknowledgement: Krishnendu Chatterjee reports financial support was provided by European Research Council. article_number: '105214' article_processing_charge: Yes (in subscription journal) article_type: original arxiv: 1 author: - first_name: Christel full_name: Baier, Christel last_name: Baier - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Jakob full_name: Piribauer, Jakob last_name: Piribauer citation: 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 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 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. 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. 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. short: C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, Information and Computation 301 (2024). corr_author: '1' das_tickbox: '0' date_created: 2024-09-01T22:01:07Z date_published: 2024-12-01T00:00:00Z date_updated: 2026-10-16T08:04:31Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.1016/j.ic.2024.105214 external_id: arxiv: - '2307.06611' isi: - '001301143400001' file: - access_level: open_access checksum: f68e0c2f46f9b9c86815406bcf2ee2d4 content_type: application/pdf creator: dernst date_created: 2025-01-09T13:49:03Z date_updated: 2025-01-09T13:49:03Z file_id: '18817' file_name: 2024_InformationComputation_Baier.pdf file_size: 724703 relation: main_file success: 1 file_date_updated: 2025-01-09T13:49:03Z fulldoi: https://doi.org/10.1016/j.ic.2024.105214 has_accepted_license: '1' intvolume: ' 301' isi: 1 language: - iso: eng month: '12' oa: 1 oa_version: Published Version publication: Information and Computation publication_identifier: eissn: - 1090-2651 issn: - 0890-5401 publication_status: published publisher: Elsevier quality_controlled: '1' related_material: record: - id: '14417' relation: earlier_version status: public researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: Entropic risk for turn-based stochastic games tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 301 year: '2024' ... --- OA_place: other OA_type: green _id: '18925' 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. 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). article_processing_charge: No author: - first_name: Esra full_name: Ceylan, Esra id: cb1ca1d8-dcc0-11ef-baa5-9f1b3ef75933 last_name: Ceylan - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Stefan full_name: Schmid, Stefan last_name: Schmid - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 citation: 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' 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.' 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.' 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 .' 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.' short: E. Ceylan, K. Chatterjee, S. Schmid, J. Svoboda, in:, NOMS 2024-2024 IEEE Network Operations and Management Symposium, IEEE, 2024. conference: end_date: 2024-05-10 location: Seoul, Republic of Korea name: 'NOMS: Network Operations and Management Symposiu ' start_date: 2024-05-06 corr_author: '1' das_tickbox: '0' date_created: 2025-01-27T15:06:45Z date_published: 2024-05-01T00:00:00Z date_updated: 2026-10-16T08:07:55Z day: '01' department: - _id: KrCh doi: 10.1109/noms59830.2024.10575579 ec_funded: 1 external_id: isi: - '001270140300143' fulldoi: https://doi.org/10.1109/noms59830.2024.10575579 isi: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://schmiste.github.io/noms24.pdf month: '05' oa: 1 oa_version: Submitted Version project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: bd622a5c-d553-11ed-ba76-bae280ba8aff grant_number: '894907' name: Graphical Games publication: NOMS 2024-2024 IEEE Network Operations and Management Symposium publication_identifier: eissn: - 2374-9709 isbn: - '9798350327946' publication_status: published publisher: IEEE quality_controlled: '1' researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: 'Congestion-free rerouting of network flows: Hardness and an FPT algorithm' type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 year: '2024' ... --- _id: '17328' abstract: - lang: eng 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." 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" article_processing_charge: Yes (via OA deal) arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Amirali full_name: Ebrahimzadeh, Amirali last_name: Ebrahimzadeh - first_name: Mehrdad full_name: Karrabi, Mehrdad id: 67638922-f394-11eb-9cf6-f20423e08757 last_name: Karrabi orcid: 0009-0007-5253-9170 - first_name: Krzysztof Z full_name: Pietrzak, Krzysztof Z id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87 last_name: Pietrzak orcid: 0000-0002-9139-1654 - first_name: Michelle X full_name: Yeo, Michelle X id: 2D82B818-F248-11E8-B48F-1D18A9856A87 last_name: Yeo orcid: 0009-0001-3676-4809 - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 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' 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' 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. 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. 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.' 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. 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. conference: end_date: 2024-06-21 location: Nantes, France name: 'PODC: Symposium on Principles of Distributed Computing' start_date: 2024-06-17 corr_author: '1' das_tickbox: '0' date_created: 2024-07-28T22:01:10Z date_published: 2024-06-17T00:00:00Z date_updated: 2026-10-16T08:09:09Z day: '17' ddc: - '000' department: - _id: KrCh - _id: KrPi doi: 10.1145/3662158.3662769 ec_funded: 1 external_id: arxiv: - '2405.04420' file: - access_level: open_access checksum: 6122bd97b42751ff81c452a19970f67d content_type: application/pdf creator: dernst date_created: 2024-07-29T07:18:12Z date_updated: 2024-07-29T07:18:12Z file_id: '17334' file_name: 2024_ACM_Chatterjee.pdf file_size: 832034 relation: main_file success: 1 file_date_updated: 2024-07-29T07:18:12Z fulldoi: https://doi.org/10.1145/3662158.3662769 has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Published Version page: 268-278 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing publication_identifier: isbn: - '9798400706684' publication_status: published publisher: Association for Computing Machinery quality_controlled: '1' researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: Fully automated selfish mining analysis in efficient proof systems blockchains tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 year: '2024' ... --- OA_place: publisher OA_type: hybrid _id: '17283' abstract: - lang: eng text: 'We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.' acknowledgement: "This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant. Petr Novotný\r\nis supported by the Czech Science Foundation grant no. GA23-06963S.\r\n" article_number: '232' article_processing_charge: Yes (via OA deal) article_type: original arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ehsan full_name: Kafshdar Goharshadi, Ehsan id: 103b4fa0-896a-11ed-bdf8-87b697bef40d last_name: Kafshdar Goharshadi orcid: 0000-0002-8595-0587 - first_name: Petr full_name: Novotný, Petr id: 3CC3B868-F248-11E8-B48F-1D18A9856A87 last_name: Novotný - first_name: Dorde full_name: Zikelic, Dorde id: 294AA7A6-F248-11E8-B48F-1D18A9856A87 last_name: Zikelic orcid: 0000-0002-4681-1699 citation: ama: Chatterjee K, Goharshady E, Novotný P, Zikelic D. Equivalence and similarity refutation for probabilistic programs. Proceedings of the ACM on Programming Languages. 2024;8. doi:10.1145/3656462 apa: Chatterjee, K., Goharshady, E., Novotný, P., & Zikelic, D. (2024). Equivalence and similarity refutation for probabilistic programs. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3656462 chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Equivalence and Similarity Refutation for Probabilistic Programs.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2024. https://doi.org/10.1145/3656462. ieee: K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Equivalence and similarity refutation for probabilistic programs,” Proceedings of the ACM on Programming Languages, vol. 8. Association for Computing Machinery, 2024. ista: Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2024. Equivalence and similarity refutation for probabilistic programs. Proceedings of the ACM on Programming Languages. 8, 232. mla: Chatterjee, Krishnendu, et al. “Equivalence and Similarity Refutation for Probabilistic Programs.” Proceedings of the ACM on Programming Languages, vol. 8, 232, Association for Computing Machinery, 2024, doi:10.1145/3656462. short: K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024). corr_author: '1' das_tickbox: '0' date_created: 2024-07-21T22:01:01Z date_published: 2024-06-20T00:00:00Z date_updated: 2026-10-16T08:08:51Z day: '20' ddc: - '000' department: - _id: KrCh - _id: GradSch doi: 10.1145/3656462 ec_funded: 1 external_id: arxiv: - '2404.03430' file: - access_level: open_access checksum: 8cbf220f284a4a87d093db5320c5afdd content_type: application/pdf creator: dernst date_created: 2024-07-22T07:17:14Z date_updated: 2024-07-22T07:17:14Z file_id: '17290' file_name: 2024_ACMProgLang_Chatterjee.pdf file_size: 355421 relation: main_file success: 1 file_date_updated: 2024-07-22T07:17:14Z fulldoi: https://doi.org/10.1145/3656462 has_accepted_license: '1' intvolume: ' 8' language: - iso: eng month: '06' oa: 1 oa_version: Published Version project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Proceedings of the ACM on Programming Languages publication_identifier: eissn: - 2475-1421 publication_status: published publisher: Association for Computing Machinery quality_controlled: '1' researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: Equivalence and similarity refutation for probabilistic programs tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 8 year: '2024' ... --- _id: '14820' abstract: - lang: eng text: "We consider a natural problem dealing with weighted packet selection across a rechargeable link, which e.g., finds applications in cryptocurrency networks. The capacity of a link (u, v) is determined by how many nodes u and v allocate for this link. Specifically, the input is a finite ordered sequence of packets that arrive in both directions along a link. Given (u, v) and a packet of weight x going from u to v, node u can either accept or reject the packet. If u accepts the packet, the capacity on link (u, v) decreases by x. Correspondingly, v's capacity on \r\n increases by x. If a node rejects the packet, this will entail a cost affinely linear in the weight of the packet. A link is “rechargeable” in the sense that the total capacity of the link has to remain constant, but the allocation of capacity at the ends of the link can depend arbitrarily on the nodes' decisions. The goal is to minimise the sum of the capacity injected into the link and the cost of rejecting packets. We show that the problem is NP-hard, but can be approximated efficiently with a ratio of (1+E) . (1+3) for some arbitrary E>0." acknowledgement: We thank Mahsa Bastankhah and Mohammad Ali Maddah-Ali for fruitful discussions about different variants of the problem. This work is supported by the European Research Council (ERC) Consolidator Project 864228 (AdjustNet), 2020-2025, the ERC CoG 863818 (ForM-SMArt), and the German Research Foundation (DFG) grant 470029389 (FlexNets), 2021-2024. article_number: '114353' article_processing_charge: Yes (via OA deal) article_type: original author: - first_name: Stefan full_name: Schmid, Stefan last_name: Schmid - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 - first_name: Michelle X full_name: Yeo, Michelle X id: 2D82B818-F248-11E8-B48F-1D18A9856A87 last_name: Yeo orcid: 0009-0001-3676-4809 citation: ama: 'Schmid S, Svoboda J, Yeo MX. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. Theoretical Computer Science. 2024;989. doi:10.1016/j.tcs.2023.114353' apa: 'Schmid, S., Svoboda, J., & Yeo, M. X. (2024). Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2023.114353' chicago: 'Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” Theoretical Computer Science. Elsevier, 2024. https://doi.org/10.1016/j.tcs.2023.114353.' ieee: 'S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation,” Theoretical Computer Science, vol. 989. Elsevier, 2024.' ista: 'Schmid S, Svoboda J, Yeo MX. 2024. Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. Theoretical Computer Science. 989, 114353.' mla: 'Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” Theoretical Computer Science, vol. 989, 114353, Elsevier, 2024, doi:10.1016/j.tcs.2023.114353.' short: S. Schmid, J. Svoboda, M.X. Yeo, Theoretical Computer Science 989 (2024). corr_author: '1' das_tickbox: '0' date_created: 2024-01-16T13:40:41Z date_published: 2024-03-21T00:00:00Z date_updated: 2026-10-16T08:09:27Z day: '21' ddc: - '000' department: - _id: KrCh - _id: KrPi doi: 10.1016/j.tcs.2023.114353 ec_funded: 1 external_id: isi: - '001168211400001' file: - access_level: open_access checksum: efd5b7e738bf845312ba53889a3e13e4 content_type: application/pdf creator: dernst date_created: 2024-07-16T12:02:25Z date_updated: 2024-07-16T12:02:25Z file_id: '17263' file_name: 2024_TheorComputerScience_Schmid.pdf file_size: 603570 relation: main_file success: 1 file_date_updated: 2024-07-16T12:02:25Z fulldoi: https://doi.org/10.1016/j.tcs.2023.114353 has_accepted_license: '1' intvolume: ' 989' isi: 1 keyword: - General Computer Science - Theoretical Computer Science language: - iso: eng month: '03' oa: 1 oa_version: Published Version project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Theoretical Computer Science publication_identifier: issn: - 0304-3975 publication_status: published publisher: Elsevier quality_controlled: '1' related_material: record: - id: '19985' relation: earlier_version status: public researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: 'Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation' tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 989 year: '2024' ... --- OA_place: publisher OA_type: green _id: '18974' abstract: - lang: eng text: Reinforcement Learning (RL) from temporal logical specifications is a fundamental problem in sequential decision making. One of the basic and core such specification is the reachability specification that requires a target set to be eventually visited. Despite strong empirical results for RL from such specifications, the theoretical guarantees are bleak, including the impossibility of Probably Approximately Correct (PAC) guarantee for reachability specifications. Given the impossibility result, in this work we consider the problem of RL from reachability specifications along with the information of expected conditional distance (ECD). We present (a) lower bound results which establish the necessity of ECD information for PAC guarantees and (b) an algorithm that establishes PAC-guarantees given the ECD information. To the best of our knowledge, this is the first RL from reachability specifications that does not make any assumptions on the underlying environment to learn policies. alternative_title: - PMLR article_processing_charge: No author: - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 - first_name: Suguman full_name: Bansal, Suguman last_name: Bansal - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: 'Svoboda J, Bansal S, Chatterjee K. Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. In: 41st International Conference on Machine Learning. Vol 235. ML Research Press; 2024:47331-47344.' apa: 'Svoboda, J., Bansal, S., & Chatterjee, K. (2024). Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. In 41st International Conference on Machine Learning (Vol. 235, pp. 47331–47344). Vienna, Austria: ML Research Press.' chicago: 'Svoboda, Jakub, Suguman Bansal, and Krishnendu Chatterjee. “Reinforcement Learning from Reachability Specifications: PAC Guarantees with Expected Conditional Distance.” In 41st International Conference on Machine Learning, 235:47331–44. ML Research Press, 2024.' ieee: 'J. Svoboda, S. Bansal, and K. Chatterjee, “Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance,” in 41st International Conference on Machine Learning, Vienna, Austria, 2024, vol. 235, pp. 47331–47344.' ista: 'Svoboda J, Bansal S, Chatterjee K. 2024. Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance. 41st International Conference on Machine Learning. ICML: International Conference on Machine Learning, PMLR, vol. 235, 47331–47344.' mla: 'Svoboda, Jakub, et al. “Reinforcement Learning from Reachability Specifications: PAC Guarantees with Expected Conditional Distance.” 41st International Conference on Machine Learning, vol. 235, ML Research Press, 2024, pp. 47331–44.' short: J. Svoboda, S. Bansal, K. Chatterjee, in:, 41st International Conference on Machine Learning, ML Research Press, 2024, pp. 47331–47344. conference: end_date: 2024-07-27 location: Vienna, Austria name: 'ICML: International Conference on Machine Learning' start_date: 2024-07-21 corr_author: '1' das_tickbox: '0' date_created: 2025-01-30T07:45:22Z date_published: 2024-07-29T00:00:00Z date_updated: 2026-10-16T08:08:33Z day: '29' department: - _id: KrCh intvolume: ' 235' language: - iso: eng main_file_link: - open_access: '1' url: https://openreview.net/forum?id=mXUDDL4r1Q month: '07' oa: 1 oa_version: Preprint page: 47331-47344 publication: 41st International Conference on Machine Learning publication_status: published publisher: ML Research Press quality_controlled: '1' researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: no title: 'Reinforcement learning from reachability specifications: PAC guarantees with expected conditional distance' type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 235 year: '2024' ... --- _id: '12676' abstract: - lang: eng text: Turn-based stochastic games (aka simple stochastic games) are two-player zero-sum games played on directed graphs with probabilistic transitions. The goal of player-max is to maximize the probability to reach a target state against the adversarial player-min. These games lie in NP ∩ coNP and are among the rare combinatorial problems that belong to this complexity class for which the existence of polynomial-time algorithm is a major open question. While randomized sub-exponential time algorithm exists, all known deterministic algorithms require exponential time in the worst-case. An important open question has been whether faster algorithms can be obtained parametrized by the treewidth of the game graph. Even deterministic sub-exponential time algorithm for constant treewidth turn-based stochastic games has remain elusive. In this work our main result is a deterministic algorithm to solve turn-based stochastic games that, given a game with n states, treewidth at most t, and the bit-complexity of the probabilistic transition function log D, has running time O ((tn2 log D)t log n). In particular, our algorithm is quasi-polynomial time for games with constant or poly-logarithmic treewidth. acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant. article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Tobias full_name: Meggendorfer, Tobias id: b21b0c15-30a2-11eb-80dc-f13ca25802e1 last_name: Meggendorfer orcid: 0000-0002-1712-2165 - first_name: Raimundo J full_name: Saona Urmeneta, Raimundo J id: BD1DF4C4-D767-11E9-B658-BC13E6697425 last_name: Saona Urmeneta orcid: 0000-0001-5103-038X - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 citation: ama: 'Chatterjee K, Meggendorfer T, Saona Urmeneta RJ, Svoboda J. Faster algorithm for turn-based stochastic games with bounded treewidth. In: Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms. Society for Industrial and Applied Mathematics; 2023:4590-4605. doi:10.1137/1.9781611977554.ch173' apa: 'Chatterjee, K., Meggendorfer, T., Saona Urmeneta, R. J., & Svoboda, J. (2023). Faster algorithm for turn-based stochastic games with bounded treewidth. In Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms (pp. 4590–4605). Florence, Italy: Society for Industrial and Applied Mathematics. https://doi.org/10.1137/1.9781611977554.ch173' chicago: Chatterjee, Krishnendu, Tobias Meggendorfer, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Faster Algorithm for Turn-Based Stochastic Games with Bounded Treewidth.” In Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms, 4590–4605. Society for Industrial and Applied Mathematics, 2023. https://doi.org/10.1137/1.9781611977554.ch173. ieee: K. Chatterjee, T. Meggendorfer, R. J. Saona Urmeneta, and J. Svoboda, “Faster algorithm for turn-based stochastic games with bounded treewidth,” in Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms, Florence, Italy, 2023, pp. 4590–4605. ista: 'Chatterjee K, Meggendorfer T, Saona Urmeneta RJ, Svoboda J. 2023. Faster algorithm for turn-based stochastic games with bounded treewidth. Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 4590–4605.' mla: Chatterjee, Krishnendu, et al. “Faster Algorithm for Turn-Based Stochastic Games with Bounded Treewidth.” Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial and Applied Mathematics, 2023, pp. 4590–605, doi:10.1137/1.9781611977554.ch173. short: K. Chatterjee, T. Meggendorfer, R.J. Saona Urmeneta, J. Svoboda, in:, Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial and Applied Mathematics, 2023, pp. 4590–4605. conference: end_date: 2023-01-25 location: Florence, Italy name: 'SODA: Symposium on Discrete Algorithms' start_date: 2023-01-22 corr_author: '1' date_created: 2023-02-24T12:20:47Z date_published: 2023-02-01T00:00:00Z date_updated: 2026-06-18T17:28:38Z day: '01' ddc: - '000' department: - _id: GradSch - _id: KrCh doi: 10.1137/1.9781611977554.ch173 ec_funded: 1 fulldoi: https://doi.org/10.1137/1.9781611977554.ch173 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.1137/1.9781611977554.ch173 month: '02' oa: 1 oa_version: Published Version page: 4590-4605 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms publication_identifier: isbn: - '9781611977554' publication_status: published publisher: Society for Industrial and Applied Mathematics quality_controlled: '1' status: public title: Faster algorithm for turn-based stochastic games with bounded treewidth type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2023' ... --- _id: '12706' abstract: - lang: eng text: Allometric settings of population dynamics models are appealing due to their parsimonious nature and broad utility when studying system level effects. Here, we parameterise the size-scaled Rosenzweig-MacArthur differential equations to eliminate prey-mass dependency, facilitating an in depth analytic study of the equations which incorporates scaling parameters’ contributions to coexistence. We define the functional response term to match empirical findings, and examine situations where metabolic theory derivations and observation diverge. The dynamical properties of the Rosenzweig-MacArthur system, encompassing the distribution of size-abundance equilibria, the scaling of period and amplitude of population cycling, and relationships between predator and prey abundances, are consistent with empirical observation. Our parameterisation is an accurate minimal model across 15+ orders of mass magnitude. acknowledgement: "This research was supported by an Australian Government Research Training Program\r\n(RTP) Scholarship to JCM (https://www.dese.gov.au), and LB is supported by the Centre de\r\nrecherche sur le vieillissement Fellowship Program. The funders had no role in study design, data collection and analysis, decision to publish, or preparation of the manuscript." article_processing_charge: No article_type: original author: - first_name: Jody C. full_name: Mckerral, Jody C. last_name: Mckerral - first_name: Maria full_name: Kleshnina, Maria id: 4E21749C-F248-11E8-B48F-1D18A9856A87 last_name: Kleshnina - first_name: Vladimir full_name: Ejov, Vladimir last_name: Ejov - first_name: Louise full_name: Bartle, Louise last_name: Bartle - first_name: James G. full_name: Mitchell, James G. last_name: Mitchell - first_name: Jerzy A. full_name: Filar, Jerzy A. last_name: Filar citation: ama: Mckerral JC, Kleshnina M, Ejov V, Bartle L, Mitchell JG, Filar JA. Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations. PLoS One. 2023;18(2):e0279838. doi:10.1371/journal.pone.0279838 apa: Mckerral, J. C., Kleshnina, M., Ejov, V., Bartle, L., Mitchell, J. G., & Filar, J. A. (2023). Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations. PLoS One. Public Library of Science. https://doi.org/10.1371/journal.pone.0279838 chicago: Mckerral, Jody C., Maria Kleshnina, Vladimir Ejov, Louise Bartle, James G. Mitchell, and Jerzy A. Filar. “Empirical Parameterisation and Dynamical Analysis of the Allometric Rosenzweig-MacArthur Equations.” PLoS One. Public Library of Science, 2023. https://doi.org/10.1371/journal.pone.0279838. ieee: J. C. Mckerral, M. Kleshnina, V. Ejov, L. Bartle, J. G. Mitchell, and J. A. Filar, “Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations,” PLoS One, vol. 18, no. 2. Public Library of Science, p. e0279838, 2023. ista: Mckerral JC, Kleshnina M, Ejov V, Bartle L, Mitchell JG, Filar JA. 2023. Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations. PLoS One. 18(2), e0279838. mla: Mckerral, Jody C., et al. “Empirical Parameterisation and Dynamical Analysis of the Allometric Rosenzweig-MacArthur Equations.” PLoS One, vol. 18, no. 2, Public Library of Science, 2023, p. e0279838, doi:10.1371/journal.pone.0279838. short: J.C. Mckerral, M. Kleshnina, V. Ejov, L. Bartle, J.G. Mitchell, J.A. Filar, PLoS One 18 (2023) e0279838. date_created: 2023-03-05T23:01:05Z date_published: 2023-02-27T00:00:00Z date_updated: 2023-10-17T12:53:30Z day: '27' ddc: - '000' department: - _id: KrCh doi: 10.1371/journal.pone.0279838 external_id: isi: - '000996122900022' pmid: - '36848357' file: - access_level: open_access checksum: 798ed5739a4117b03173e5d56e0534c9 content_type: application/pdf creator: cchlebak date_created: 2023-03-07T10:26:45Z date_updated: 2023-03-07T10:26:45Z file_id: '12712' file_name: 2023_PLOSOne_Mckerral.pdf file_size: 1257003 relation: main_file success: 1 file_date_updated: 2023-03-07T10:26:45Z fulldoi: https://doi.org/10.1371/journal.pone.0279838 has_accepted_license: '1' intvolume: ' 18' isi: 1 issue: '2' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: e0279838 pmid: 1 publication: PLoS One publication_identifier: eissn: - 1932-6203 publication_status: published publisher: Public Library of Science quality_controlled: '1' scopus_import: '1' status: public title: Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur equations tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 18 year: '2023' ... --- _id: '12833' abstract: - lang: eng text: 'The input to the token swapping problem is a graph with vertices v1, v2, . . . , vn, and n tokens with labels 1,2, . . . , n, one on each vertex. The goal is to get token i to vertex vi for all i= 1, . . . , n using a minimum number of swaps, where a swap exchanges the tokens on the endpoints of an edge.Token swapping on a tree, also known as “sorting with a transposition tree,” is not known to be in P nor NP-complete. We present some partial results: 1. An optimum swap sequence may need to perform a swap on a leaf vertex that has the correct token (a “happy leaf”), disproving a conjecture of Vaughan. 2. Any algorithm that fixes happy leaves—as all known approximation algorithms for the problem do—has approximation factor at least 4/3. Furthermore, the two best-known 2-approximation algorithms have approximation factor exactly 2. 3. A generalized problem—weighted coloured token swapping—is NP-complete on trees, but solvable in polynomial time on paths and stars. In this version, tokens and vertices have colours, and colours have weights. The goal is to get every token to a vertex of the same colour, and the cost of a swap is the sum of the weights of the two tokens involved.' acknowledgement: "This work was begun at the University of Waterloo and was partially supported by the Natural Sciences and Engineering Council of Canada (NSERC).\r\n" article_number: '9' article_processing_charge: No article_type: original arxiv: 1 author: - first_name: Ahmad full_name: Biniaz, Ahmad last_name: Biniaz - first_name: Kshitij full_name: Jain, Kshitij last_name: Jain - first_name: Anna full_name: Lubiw, Anna last_name: Lubiw - first_name: Zuzana full_name: Masárová, Zuzana id: 45CFE238-F248-11E8-B48F-1D18A9856A87 last_name: Masárová orcid: 0000-0002-6660-1322 - first_name: Tillmann full_name: Miltzow, Tillmann last_name: Miltzow - first_name: Debajyoti full_name: Mondal, Debajyoti last_name: Mondal - first_name: Anurag Murty full_name: Naredla, Anurag Murty last_name: Naredla - first_name: Josef full_name: Tkadlec, Josef id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87 last_name: Tkadlec orcid: 0000-0002-1097-9684 - first_name: Alexi full_name: Turcotte, Alexi last_name: Turcotte citation: ama: Biniaz A, Jain K, Lubiw A, et al. Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. 2023;24(2). doi:10.46298/DMTCS.8383 apa: Biniaz, A., Jain, K., Lubiw, A., Masárová, Z., Miltzow, T., Mondal, D., … Turcotte, A. (2023). Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. EPI Sciences. https://doi.org/10.46298/DMTCS.8383 chicago: Biniaz, Ahmad, Kshitij Jain, Anna Lubiw, Zuzana Masárová, Tillmann Miltzow, Debajyoti Mondal, Anurag Murty Naredla, Josef Tkadlec, and Alexi Turcotte. “Token Swapping on Trees.” Discrete Mathematics and Theoretical Computer Science. EPI Sciences, 2023. https://doi.org/10.46298/DMTCS.8383. ieee: A. Biniaz et al., “Token swapping on trees,” Discrete Mathematics and Theoretical Computer Science, vol. 24, no. 2. EPI Sciences, 2023. ista: Biniaz A, Jain K, Lubiw A, Masárová Z, Miltzow T, Mondal D, Naredla AM, Tkadlec J, Turcotte A. 2023. Token swapping on trees. Discrete Mathematics and Theoretical Computer Science. 24(2), 9. mla: Biniaz, Ahmad, et al. “Token Swapping on Trees.” Discrete Mathematics and Theoretical Computer Science, vol. 24, no. 2, 9, EPI Sciences, 2023, doi:10.46298/DMTCS.8383. short: A. Biniaz, K. Jain, A. Lubiw, Z. Masárová, T. Miltzow, D. Mondal, A.M. Naredla, J. Tkadlec, A. Turcotte, Discrete Mathematics and Theoretical Computer Science 24 (2023). date_created: 2023-04-16T22:01:08Z date_published: 2023-01-18T00:00:00Z date_updated: 2025-01-20T14:05:09Z day: '18' ddc: - '000' department: - _id: KrCh - _id: HeEd - _id: UlWa doi: 10.46298/DMTCS.8383 external_id: arxiv: - '1903.06981' file: - access_level: open_access checksum: 439102ea4f6e2aeefd7107dfb9ccf532 content_type: application/pdf creator: dernst date_created: 2023-04-17T08:10:28Z date_updated: 2023-04-17T08:10:28Z file_id: '12844' file_name: 2022_DMTCS_Biniaz.pdf file_size: 2072197 relation: main_file success: 1 file_date_updated: 2023-04-17T08:10:28Z fulldoi: https://doi.org/10.46298/DMTCS.8383 has_accepted_license: '1' intvolume: ' 24' issue: '2' language: - iso: eng month: '01' oa: 1 oa_version: Published Version publication: Discrete Mathematics and Theoretical Computer Science publication_identifier: eissn: - 1365-8050 issn: - 1462-7264 publication_status: published publisher: EPI Sciences quality_controlled: '1' related_material: record: - id: '7950' relation: earlier_version status: public scopus_import: '1' status: public title: Token swapping on trees tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 24 year: '2023' ... --- _id: '12861' abstract: - lang: eng text: The field of indirect reciprocity investigates how social norms can foster cooperation when individuals continuously monitor and assess each other’s social interactions. By adhering to certain social norms, cooperating individuals can improve their reputation and, in turn, receive benefits from others. Eight social norms, known as the “leading eight," have been shown to effectively promote the evolution of cooperation as long as information is public and reliable. These norms categorize group members as either ’good’ or ’bad’. In this study, we examine a scenario where individuals instead assign nuanced reputation scores to each other, and only cooperate with those whose reputation exceeds a certain threshold. We find both analytically and through simulations that such quantitative assessments are error-correcting, thus facilitating cooperation in situations where information is private and unreliable. Moreover, our results identify four specific norms that are robust to such conditions, and may be relevant for helping to sustain cooperation in natural populations. acknowledgement: 'This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.). L.S. received additional partial support by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), and also thanks the support by the Stochastic Analysis and Application Research Center (SAARC) under National Research Foundation of Korea grant NRF-2019R1A5A1028324. The authors additionally thank Stefan Schmid for providing access to his lab infrastructure at the University of Vienna for the purpose of collecting simulation data.' article_number: '2086' article_processing_charge: No article_type: original author: - first_name: Laura full_name: Schmid, Laura id: 38B437DE-F248-11E8-B48F-1D18A9856A87 last_name: Schmid orcid: 0000-0002-6978-7329 - first_name: Farbod full_name: Ekbatani, Farbod last_name: Ekbatani - first_name: Christian full_name: Hilbe, Christian id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87 last_name: Hilbe orcid: 0000-0001-5116-955X - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: Schmid L, Ekbatani F, Hilbe C, Chatterjee K. Quantitative assessment can stabilize indirect reciprocity under imperfect information. Nature Communications. 2023;14. doi:10.1038/s41467-023-37817-x apa: Schmid, L., Ekbatani, F., Hilbe, C., & Chatterjee, K. (2023). Quantitative assessment can stabilize indirect reciprocity under imperfect information. Nature Communications. Springer Nature. https://doi.org/10.1038/s41467-023-37817-x chicago: Schmid, Laura, Farbod Ekbatani, Christian Hilbe, and Krishnendu Chatterjee. “Quantitative Assessment Can Stabilize Indirect Reciprocity under Imperfect Information.” Nature Communications. Springer Nature, 2023. https://doi.org/10.1038/s41467-023-37817-x. ieee: L. Schmid, F. Ekbatani, C. Hilbe, and K. Chatterjee, “Quantitative assessment can stabilize indirect reciprocity under imperfect information,” Nature Communications, vol. 14. Springer Nature, 2023. ista: Schmid L, Ekbatani F, Hilbe C, Chatterjee K. 2023. Quantitative assessment can stabilize indirect reciprocity under imperfect information. Nature Communications. 14, 2086. mla: Schmid, Laura, et al. “Quantitative Assessment Can Stabilize Indirect Reciprocity under Imperfect Information.” Nature Communications, vol. 14, 2086, Springer Nature, 2023, doi:10.1038/s41467-023-37817-x. short: L. Schmid, F. Ekbatani, C. Hilbe, K. Chatterjee, Nature Communications 14 (2023). date_created: 2023-04-23T22:01:03Z date_published: 2023-04-12T00:00:00Z date_updated: 2025-04-15T06:26:15Z day: '12' ddc: - '000' department: - _id: KrCh doi: 10.1038/s41467-023-37817-x ec_funded: 1 external_id: isi: - '001003644100020' pmid: - '37045828' file: - access_level: open_access checksum: a4b3b7b36fbef068cabf4fb99501fef6 content_type: application/pdf creator: dernst date_created: 2023-04-25T09:13:53Z date_updated: 2023-04-25T09:13:53Z file_id: '12868' file_name: 2023_NatureComm_Schmid.pdf file_size: 1786475 relation: main_file success: 1 file_date_updated: 2023-04-25T09:13:53Z fulldoi: https://doi.org/10.1038/s41467-023-37817-x has_accepted_license: '1' intvolume: ' 14' isi: 1 language: - iso: eng month: '04' oa: 1 oa_version: Published Version pmid: 1 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: Formal methods for the design and analysis of complex systems publication: Nature Communications publication_identifier: eissn: - 2041-1723 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Quantitative assessment can stabilize indirect reciprocity under imperfect information tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 volume: 14 year: '2023' ...