--- OA_place: publisher OA_type: gold PlanS_conform: '1' _id: '22102' abstract: - lang: eng text: 'Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of є-DP. Our method refutes є-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for є-DP refutation. To the best of our knowledge, our method is the first method for є-DP refutation to offer the following four desirable features: (1) it is fully automated, (2) it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3) it provides soundness guarantees, and (4) it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute є-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.' acknowledgement: "The authors would like to thank Petr Novotný for valuable discussions that helped shape this work.\r\nThis research was supported by the Singapore Ministry of Education (MOE) Academic Research\r\nFund (AcRF) Tier 1 grant (Proposal ID: 25-SIS-SMU-009), Vienna Science and Technology Fund\r\n(WWTF), State of Lower Austria [Grant ID 10.47379/ICT25017], ERC CoG 863818 (ForM-SMArt),\r\nand Austrian Science Fund (FWF) 10.55776/COE12." article_number: '218' 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: Ehsan full_name: Kafshdar Goharshadi, Ehsan id: 103b4fa0-896a-11ed-bdf8-87b697bef40d last_name: Kafshdar Goharshadi orcid: 0000-0002-8595-0587 - 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, Zikelic D. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 2026;10(PLDI). doi:10.1145/3808296' apa: 'Chatterjee, K., Goharshady, E., & Zikelic, D. (2026). SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3808296' chicago: 'Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2026. https://doi.org/10.1145/3808296.' ieee: 'K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential privacy refutation via supermartingales,” Proceedings of the ACM on Programming Languages, vol. 10, no. PLDI. Association for Computing Machinery, 2026.' ista: 'Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 10(PLDI), 218.' mla: 'Chatterjee, Krishnendu, et al. “SuperDP: Differential Privacy Refutation via Supermartingales.” Proceedings of the ACM on Programming Languages, vol. 10, no. PLDI, 218, Association for Computing Machinery, 2026, doi:10.1145/3808296.' short: K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming Languages 10 (2026). corr_author: '1' das_tickbox: '1' dataavailabilitystatement: "The artifact supporting the findings of this study, which includes the underlying datasets, software\r\ncode, and experiments, is publicly available in Zenodo https://zenodo.org/records/19399862." date_created: 2026-06-21T22:02:59Z date_published: 2026-06-08T00:00:00Z date_updated: 2026-06-24T06:39:37Z day: '08' ddc: - '000' department: - _id: KrCh doi: 10.1145/3808296 ec_funded: 1 external_id: arxiv: - '2603.26215' file: - access_level: open_access checksum: 994bf21d6269dabccf1e1091e02962c5 content_type: application/pdf creator: dernst date_created: 2026-06-24T06:19:56Z date_updated: 2026-06-24T06:19:56Z file_id: '22135' file_name: 2026_ProcACMProgrammingLanguages_Chatterjee.pdf file_size: 858595 relation: main_file success: 1 file_date_updated: 2026-06-24T06:19:56Z has_accepted_license: '1' intvolume: ' 10' issue: PLDI keyword: - Static Program Analysis - Differential Privacy - Probabilistic Programming - Martingales 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' related_material: record: - id: '22134' relation: research_data status: public researchdata_availability: yes scopus_import: '1' status: public supplementarymaterial: no title: 'SuperDP: Differential privacy refutation via supermartingales' 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: 10 year: '2026' ... --- OA_place: repository OA_type: green _id: '22134' abstract: - lang: eng text: This artifact provides the source code, benchmarks, and scripts necessary to build and reproduce the experimental results for `SuperDP` (Accepted at PLDI 2026). It also includes instructions for running the tool on user-provided inputs. 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: Ehsan full_name: Kafshdar Goharshadi, Ehsan id: 103b4fa0-896a-11ed-bdf8-87b697bef40d last_name: Kafshdar Goharshadi orcid: 0000-0002-8595-0587 - 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, Zikelic D. SuperDP: Differential Privacy Refutation via Supermartingales. 2026. doi:10.5281/ZENODO.18930113' apa: 'Chatterjee, K., Goharshady, E., & Zikelic, D. (2026). SuperDP: Differential Privacy Refutation via Supermartingales. Zenodo. https://doi.org/10.5281/ZENODO.18930113' chicago: 'Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” Zenodo, 2026. https://doi.org/10.5281/ZENODO.18930113.' ieee: 'K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential Privacy Refutation via Supermartingales.” Zenodo, 2026.' ista: 'Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential Privacy Refutation via Supermartingales, Zenodo, 10.5281/ZENODO.18930113.' mla: 'Chatterjee, Krishnendu, et al. SuperDP: Differential Privacy Refutation via Supermartingales. Zenodo, 2026, doi:10.5281/ZENODO.18930113.' short: K. Chatterjee, E. Goharshady, D. Zikelic, (2026). corr_author: '1' date_created: 2026-06-24T06:25:29Z date_published: 2026-03-09T00:00:00Z date_updated: 2026-06-24T06:39:38Z day: '09' ddc: - '000' department: - _id: KrCh doi: 10.5281/ZENODO.18930113 has_accepted_license: '1' main_file_link: - open_access: '1' url: https://doi.org/10.5281/ZENODO.18930113 month: '03' oa: 1 oa_version: Published Version publisher: Zenodo related_material: record: - id: '22102' relation: used_in_publication status: public status: public title: 'SuperDP: Differential Privacy Refutation via Supermartingales' 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: '2026' ... --- OA_place: publisher OA_type: gold _id: '21411' abstract: - lang: eng text: "To achieve fast recovery from link failures, most modern communication networks feature fully\r\ndecentralized fast re-routing mechanisms. These re-routing mechanisms rely on pre-installed static re-routing rules at the nodes (the routers), which depend only on local failure information, namely on the failed links incident to the node. Ideally, a network is perfectly resilient: the re-routing rules ensure that packets are always successfully routed to their destinations as long as the source and the destination are still physically connected in the underlying network after the failures. Unfortunately, there are examples where achieving perfect resilience is not possible. Surprisingly, only very little is known about the algorithmic aspect of when and how perfect resilience can be achieved. We investigate the computational complexity of analyzing such local fast re-routing mechanisms. Our main result is a negative one: we show that even checking whether a given set of static re-routing rules ensures perfect resilience is coNP-complete. Additionally, we investigate other fundamental variations of the problem. In particular, we show that our coNP-completeness proof also applies to scenarios where the re-routing rules have specific patterns (known as skipping in the literature). On the positive side, for scenarios where nodes do not have information about the link from which a packet arrived (the so-called in-port), we present a linear-time algorithm to realize perfect resilience whenever possible (which we show can also be determined in linear time). " acknowledgement: "Matthias Bentert: ERC Horizon 2020 research and innovation programme (grant agreement\r\nNo. 819416) and ERC Consolidator grant AdjustNet (agreement No. 864228).\r\nEsra Ceylan: German Research Foundation (DFG) project ReNO, Schwerpunktprogramm:\r\nResilienz in Vernetzten Welten – Beherrschen von Fehlern, Überlast, Angriffen und dem\r\nUnbekannten (SPP 2378).\r\nStefan Schmid: German Research Foundation (DFG) project ReNO, Schwerpunktprogramm:\r\nResilienz in Vernetzten Welten – Beherrschen von Fehlern, Überlast, Angriffen und dem\r\nUnbekannten (SPP 2378)." alternative_title: - LIPIcs article_number: '31' article_processing_charge: No author: - first_name: Matthias full_name: Bentert, Matthias last_name: Bentert - first_name: Esra full_name: Ceylan, Esra last_name: Ceylan - 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: Stefan full_name: Schmid, Stefan last_name: Schmid - first_name: Jiří full_name: Srba, Jiří last_name: Srba citation: ama: 'Bentert M, Ceylan E, Hübner V, Schmid S, Srba J. Fast re-routing in networks: On the complexity of perfect resilience. In: 29th International Conference on Principles of Distributed Systems. Vol 361. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.OPODIS.2025.31' apa: 'Bentert, M., Ceylan, E., Hübner, V., Schmid, S., & Srba, J. (2026). Fast re-routing in networks: On the complexity of perfect resilience. In 29th International Conference on Principles of Distributed Systems (Vol. 361). Iaşi, Romania: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.OPODIS.2025.31' chicago: 'Bentert, Matthias, Esra Ceylan, Valentin Hübner, Stefan Schmid, and Jiří Srba. “Fast Re-Routing in Networks: On the Complexity of Perfect Resilience.” In 29th International Conference on Principles of Distributed Systems, Vol. 361. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.OPODIS.2025.31.' ieee: 'M. Bentert, E. Ceylan, V. Hübner, S. Schmid, and J. Srba, “Fast re-routing in networks: On the complexity of perfect resilience,” in 29th International Conference on Principles of Distributed Systems, Iaşi, Romania, 2026, vol. 361.' ista: 'Bentert M, Ceylan E, Hübner V, Schmid S, Srba J. 2026. Fast re-routing in networks: On the complexity of perfect resilience. 29th International Conference on Principles of Distributed Systems. OPODIS: Conference on Principles of Distributed Systems, LIPIcs, vol. 361, 31.' mla: 'Bentert, Matthias, et al. “Fast Re-Routing in Networks: On the Complexity of Perfect Resilience.” 29th International Conference on Principles of Distributed Systems, vol. 361, 31, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.OPODIS.2025.31.' short: M. Bentert, E. Ceylan, V. Hübner, S. Schmid, J. Srba, in:, 29th International Conference on Principles of Distributed Systems, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. conference: end_date: 2025-12-05 location: Iaşi, Romania name: 'OPODIS: Conference on Principles of Distributed Systems' start_date: 2025-12-03 date_created: 2026-03-08T23:01:46Z date_published: 2026-01-07T00:00:00Z date_updated: 2026-03-09T12:36:11Z day: '07' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.OPODIS.2025.31 file: - access_level: open_access checksum: a7af114da7c38d2338b4edb922eb27f1 content_type: application/pdf creator: dernst date_created: 2026-03-09T12:33:58Z date_updated: 2026-03-09T12:33:58Z file_id: '21419' file_name: 2026_OPODIS_Bentert.pdf file_size: 1041334 relation: main_file success: 1 file_date_updated: 2026-03-09T12:33:58Z has_accepted_license: '1' intvolume: ' 361' language: - iso: eng month: '01' oa: 1 oa_version: Published Version publication: 29th International Conference on Principles of Distributed Systems publication_identifier: eissn: - 1868-8969 isbn: - '9783959774093' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' status: public title: 'Fast re-routing in networks: On the complexity of perfect resilience' 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 361 year: '2026' ... --- OA_place: publisher OA_type: hybrid _id: '21661' abstract: - lang: eng text: Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) are key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear programme, solvable in polynomial time. In this paper, we give a detailed overview of today’s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners—tool builders and users alike. acknowledgement: "This research was funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie grant agreements 101008233 (MISSION)\r\nand 101034413 (IST-BRIDGE), by the Interreg North Sea project STORM_SAFE, by a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, by NWO VENI grant no. 639.021.754, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632." article_processing_charge: Yes (in subscription journal) article_type: original author: - first_name: Arnd full_name: Hartmanns, Arnd last_name: Hartmanns - first_name: Sebastian full_name: Junges, Sebastian last_name: Junges - first_name: Tim full_name: Quatmann, Tim last_name: Quatmann - first_name: Maximilian full_name: Weininger, Maximilian id: 02ab0197-cc70-11ed-ab61-918e71f56881 last_name: Weininger orcid: 0000-0002-0163-2152 citation: ama: Hartmanns A, Junges S, Quatmann T, Weininger M. The revised practitioner’s guide to MDP model checking algorithms. International Journal on Software Tools for Technology Transfer. 2026. doi:10.1007/s10009-026-00848-y apa: Hartmanns, A., Junges, S., Quatmann, T., & Weininger, M. (2026). The revised practitioner’s guide to MDP model checking algorithms. International Journal on Software Tools for Technology Transfer. Springer Nature. https://doi.org/10.1007/s10009-026-00848-y chicago: Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” International Journal on Software Tools for Technology Transfer. Springer Nature, 2026. https://doi.org/10.1007/s10009-026-00848-y. ieee: A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “The revised practitioner’s guide to MDP model checking algorithms,” International Journal on Software Tools for Technology Transfer. Springer Nature, 2026. ista: Hartmanns A, Junges S, Quatmann T, Weininger M. 2026. The revised practitioner’s guide to MDP model checking algorithms. International Journal on Software Tools for Technology Transfer. mla: Hartmanns, Arnd, et al. “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” International Journal on Software Tools for Technology Transfer, Springer Nature, 2026, doi:10.1007/s10009-026-00848-y. short: A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, International Journal on Software Tools for Technology Transfer (2026). date_created: 2026-04-05T22:01:32Z date_published: 2026-03-09T00:00:00Z date_updated: 2026-04-07T09:52:54Z day: '09' ddc: - '000' department: - _id: KrCh doi: 10.1007/s10009-026-00848-y ec_funded: 1 has_accepted_license: '1' keyword: - Quantitative model checking - Markov decision process - Linear programming - Value iteration - Policy iteration language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.1007/s10009-026-00848-y month: '03' oa: 1 oa_version: Published Version project: - _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c call_identifier: H2020 grant_number: '101034413' name: 'IST-BRIDGE: International postdoctoral program' publication: International Journal on Software Tools for Technology Transfer publication_identifier: eissn: - 1433-2787 issn: - 1433-2779 publication_status: epub_ahead publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '21668' relation: software status: public scopus_import: '1' status: public title: The revised practitioner’s guide to MDP model checking 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: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2026' ... --- OA_place: repository OA_type: green _id: '21717' abstract: - lang: eng text: Robust Markov Decision Processes (RMDPs) generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for ω-regular objectives. The qualitative analysis problem asks whether the objective can be ensured with probability 1. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. Our contributions are twofold. We first present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives. We then report experimental results demonstrating the effectiveness of our oracle-based approach on classical RMDP examples from the literature scaling up to thousands of states. acknowledgement: This work was supported by ERC CoG 863818 (ForMSMArt) and Austrian Science Fund (FWF) 10.55776/COE12. We also thank Hossein Zakerinia for his helpful feedback. 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: 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: Ali full_name: Shafiee, Ali id: 2783031a-7378-11f0-b2d0-f17f1db2ebad last_name: Shafiee citation: ama: 'Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. Qualitative analysis of ω-regular objectives on robust MDPs. In: Proceedings of the 40th AAAI Conference on Artificial Intelligence. Vol 40. Association for the Advancement of Artificial Intelligence; 2026:36137-36145. doi:10.1609/aaai.v40i43.40931' apa: 'Asadi, A., Chatterjee, K., Goharshady, E., Karrabi, M., & Shafiee, A. (2026). Qualitative analysis of ω-regular objectives on robust MDPs. In Proceedings of the 40th AAAI Conference on Artificial Intelligence (Vol. 40, pp. 36137–36145). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v40i43.40931' chicago: Asadi, Ali, Krishnendu Chatterjee, Ehsan Goharshady, Mehrdad Karrabi, and Ali Shafiee. “Qualitative Analysis of ω-Regular Objectives on Robust MDPs.” In Proceedings of the 40th AAAI Conference on Artificial Intelligence, 40:36137–45. Association for the Advancement of Artificial Intelligence, 2026. https://doi.org/10.1609/aaai.v40i43.40931. ieee: A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, and A. Shafiee, “Qualitative analysis of ω-regular objectives on robust MDPs,” in Proceedings of the 40th AAAI Conference on Artificial Intelligence, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36137–36145. ista: 'Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. 2026. Qualitative analysis of ω-regular objectives on robust MDPs. Proceedings of the 40th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 40, 36137–36145.' mla: Asadi, Ali, et al. “Qualitative Analysis of ω-Regular Objectives on Robust MDPs.” Proceedings of the 40th AAAI Conference on Artificial Intelligence, vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–45, doi:10.1609/aaai.v40i43.40931. short: A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, A. Shafiee, in:, Proceedings of the 40th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2026, pp. 36137–36145. conference: end_date: 2026-01-27 location: Singapore, Singapore name: 'AAAI: Conference on Artificial Intelligence' start_date: 2026-01-20 date_created: 2026-04-12T22:01:50Z date_published: 2026-03-14T00:00:00Z date_updated: 2026-05-04T11:38:56Z day: '14' department: - _id: KrCh - _id: GradSch doi: 10.1609/aaai.v40i43.40931 ec_funded: 1 external_id: arxiv: - '2505.04539' intvolume: ' 40' issue: '43' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2505.04539 month: '03' oa: 1 oa_version: Preprint page: 36137-36145 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 40th AAAI Conference on Artificial Intelligence publication_identifier: eissn: - 2374-3468 issn: - 2159-5399 publication_status: published publisher: Association for the Advancement of Artificial Intelligence quality_controlled: '1' scopus_import: '1' status: public title: Qualitative analysis of ω-regular objectives on robust MDPs type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 40 year: '2026' ... --- OA_place: repository OA_type: green _id: '21722' abstract: - lang: eng text: 'Partially observable Markov decision processes (POMDPs) are a central model for uncertainty in sequential decision making. The most basic objective is the reachability objective, where a target set must be eventually visited, and the more general parity objectives can model all omega-regular specifications. For such objectives, the computational analysis problems are the following: (a) qualitative analysis that asks whether the objective can be satisfied with probability 1 (almost-sure winning) or probability arbitrarily close to 1 (limit-sure winning); and (b) quantitative analysis that asks for the approximation of the optimal probability of satisfying the objective. For general POMDPs, almost-sure analysis for reachability objectives is EXPTIME-complete, but limit-sure and quantitative analyses for reachability objectives are undecidable; almost-sure, limit-sure, and quantitative analyses for parity objectives are all undecidable. A special class of POMDPs, called revealing POMDPs, has been studied recently in several works, and for this subclass the almost-sure analysis for parity objectives was shown to be EXPTIME-complete. In this work, we show that for revealing POMDPs the limit-sure analysis for parity objectives is EXPTIME-complete, and even the quantitative analysis for parity objectives can be achieved in EXPTIME.' acknowledgement: "This work was partially supported by the ANRT under the French CIFRE Ph.D program in collaboration between NyxAir and Paris-Dauphine University (Contract: CIFRE N° 2022/0513), by the French Agence Nationale de la Recherche (ANR) under reference ANR-21-CE40-\r\n0020 (CONVERGENCE project), by Austrian Science Fund (FWF) 10.55776/COE12, and by the ERC CoG 863818 (ForM-SMArt) grant." 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: David full_name: Lurie, David id: 579a6c20-34cf-11f1-acbd-8c2f19cdb4da last_name: Lurie - 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 citation: ama: 'Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. In: Proceedings of the AAAI Conference on Artificial Intelligence. Vol 40. Association for the Advancement of Artificial Intelligence; 2026:36146-36154. doi:10.1609/aaai.v40i43.40932' apa: 'Asadi, A., Chatterjee, K., Lurie, D., & Saona Urmeneta, R. J. (2026). Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. In Proceedings of the AAAI Conference on Artificial Intelligence (Vol. 40, pp. 36146–36154). Singapore, Singapore: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v40i43.40932' chicago: 'Asadi, Ali, Krishnendu Chatterjee, David Lurie, and Raimundo J Saona Urmeneta. “Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives.” In Proceedings of the AAAI Conference on Artificial Intelligence, 40:36146–54. Association for the Advancement of Artificial Intelligence, 2026. https://doi.org/10.1609/aaai.v40i43.40932.' ieee: 'A. Asadi, K. Chatterjee, D. Lurie, and R. J. Saona Urmeneta, “Revealing POMDPs: Qualitative and quantitative analysis for parity objectives,” in Proceedings of the AAAI Conference on Artificial Intelligence, Singapore, Singapore, 2026, vol. 40, no. 43, pp. 36146–36154.' ista: 'Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. 2026. Revealing POMDPs: Qualitative and quantitative analysis for parity objectives. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 40, 36146–36154.' mla: 'Asadi, Ali, et al. “Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives.” Proceedings of the AAAI Conference on Artificial Intelligence, vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026, pp. 36146–54, doi:10.1609/aaai.v40i43.40932.' short: A. Asadi, K. Chatterjee, D. Lurie, R.J. Saona Urmeneta, in:, Proceedings of the AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2026, pp. 36146–36154. conference: end_date: 2026-01-27 location: Singapore, Singapore name: 'AAAI: Conference on Artificial Intelligence' start_date: 2026-01-20 corr_author: '1' date_created: 2026-04-12T22:01:52Z date_published: 2026-03-14T00:00:00Z date_updated: 2026-05-04T11:44:14Z day: '14' department: - _id: KrCh doi: 10.1609/aaai.v40i43.40932 ec_funded: 1 external_id: arxiv: - '2511.13134' intvolume: ' 40' issue: '43' language: - iso: eng main_file_link: - url: https://doi.org/10.48550/arXiv.2511.13134 month: '03' oa_version: Preprint page: 36146-36154 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 AAAI Conference on Artificial Intelligence publication_identifier: eissn: - 2374-3468 issn: - 2159-5399 publication_status: published publisher: Association for the Advancement of Artificial Intelligence quality_controlled: '1' scopus_import: '1' status: public title: 'Revealing POMDPs: Qualitative and quantitative analysis for parity objectives' type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 40 year: '2026' ... --- DOAJ_listed: '1' OA_place: publisher OA_type: gold _id: '22101' abstract: - lang: eng text: "Evolutionary biology examines how the genetic and phenotypic composition\r\nof populations changes over time. An important goal is to determine the\r\nfixation probability of a single advantageous mutant that arises in a homogeneous\r\npopulation of N residents. Many real populations experience environmental\r\ngradients that cause mutations to be beneficial in some spatial\r\nregions but harmful in others. Here, we study the fixation probability of a\r\nmutant placed on a simple one-dimensional spatial structure that experiences\r\nsuch a gradient. The mutant’s fitness varies linearly from1 − s to 1 + s, whereas\r\nthe resident fitness is constant and equal to 1. The existing literature suggests\r\nthat such heterogeneity in the mutant’s fitness should lead to a decrease in its\r\nfixation probability. However, in this work, we find that small, non-negligible\r\ngradients (s < 1=√N) substantially increase the fixation probability,while larger\r\ngradients (s > (log N)/√N) substantially decrease it.Moreover, we quantify the\r\nstrength of this phenomenon analytically and we precisely delimit the range of\r\nthe gradients for which it occurs. Our computer simulations closely match\r\nthose findings. Altogether, our results indicate that subjecting a simple\r\npopulation structure to natural environmental conditions can produce strong\r\ncounterintuitive effects." acknowledgement: "J.S. and K.C. were supported by the European Research Council (ERC)\r\nCoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/\r\nCOE12. J.T. was supported by GAČR grant 25-17377S and by Charles\r\nUniv. projects UNCE 24/SCI/008 and PRIMUS 24/SCI/012." article_number: '5325' 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: Hossein full_name: Nemati, Hossein last_name: Nemati - first_name: Josef full_name: Tkadlec, Josef id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87 last_name: Tkadlec orcid: 0000-0002-1097-9684 - first_name: Kamran full_name: Kaveh, Kamran last_name: Kaveh - 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, Nemati H, Tkadlec J, Kaveh K, Chatterjee K. The effect of the fitness gradient on fixation probability. Nature Communications. 2026;17. doi:10.1038/s41467-026-71777-2 apa: Svoboda, J., Nemati, H., Tkadlec, J., Kaveh, K., & Chatterjee, K. (2026). The effect of the fitness gradient on fixation probability. Nature Communications. Springer Nature. https://doi.org/10.1038/s41467-026-71777-2 chicago: Svoboda, Jakub, Hossein Nemati, Josef Tkadlec, Kamran Kaveh, and Krishnendu Chatterjee. “The Effect of the Fitness Gradient on Fixation Probability.” Nature Communications. Springer Nature, 2026. https://doi.org/10.1038/s41467-026-71777-2. ieee: J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, and K. Chatterjee, “The effect of the fitness gradient on fixation probability,” Nature Communications, vol. 17. Springer Nature, 2026. ista: Svoboda J, Nemati H, Tkadlec J, Kaveh K, Chatterjee K. 2026. The effect of the fitness gradient on fixation probability. Nature Communications. 17, 5325. mla: Svoboda, Jakub, et al. “The Effect of the Fitness Gradient on Fixation Probability.” Nature Communications, vol. 17, 5325, Springer Nature, 2026, doi:10.1038/s41467-026-71777-2. short: J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, K. Chatterjee, Nature Communications 17 (2026). corr_author: '1' das_tickbox: '0' dataavailabilitystatement: Correspondence and requests for materials should be addressed to Krishnendu Chatterjee. date_created: 2026-06-21T22:02:59Z date_published: 2026-12-01T00:00:00Z date_updated: 2026-06-24T07:53:53Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.1038/s41467-026-71777-2 ec_funded: 1 external_id: pmid: - '41997932' file: - access_level: open_access checksum: b660048bb271f24d6763803e247d5c32 content_type: application/pdf creator: dernst date_created: 2026-06-24T06:50:24Z date_updated: 2026-06-24T06:50:24Z file_id: '22136' file_name: 2026_NatureComm_Svoboda.pdf file_size: 1068919 relation: main_file success: 1 file_date_updated: 2026-06-24T06:50:24Z has_accepted_license: '1' intvolume: ' 17' language: - iso: eng 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: Nature Communications publication_identifier: eissn: - 2041-1723 publication_status: published publisher: Springer Nature quality_controlled: '1' researchdata_availability: no scopus_import: '1' status: public supplementarymaterial: yes title: The effect of the fitness gradient on fixation probability 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 17 year: '2026' ... --- APC_amount: 3003,56 EUR OA_place: publisher OA_type: hybrid _id: '20857' abstract: - lang: eng text: 'Evolutionary games provide a flexible mathematical framework for many problems in biology and social evolution. Prisoners’ dilemma, and in particular, the important special case of donation games, represents social dilemmas where cooperation is mutually beneficial, yet defection is preferred by selfish agents. In evolutionary games on networks, the agents interact over a population structure. The existence of population structures that promote cooperative behavior is a fascinating and active research topic. Previous research establishes structures promoting cooperation in the limit of weak selection where the benefit-to-cost ratio β exceeds 1.5. The existence of such structures for medium and strong selection for 1 < ß < 2 and for weak selection for 1 < ß < 1.5 has been a long-standing open question. First, we answer the open questions in the affirmative: For every selection strength and every ß > 1, we construct networks promoting cooperation. Second, we present a robustness result with respect to β and selection strength: Our structures promote cooperation for a range of these parameter values rather than specific parameter values. Finally, we supplement our theoretical results with simulation results on small population structures that show the effectiveness of our construction over well-studied population structures.' acknowledgement: J.S. and K.C. were supported by the European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12. article_processing_charge: Yes (in subscription journal) 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. Promoters of cooperation in evolutionary games. Proceedings of the National Academy of Sciences. 2025;122(51):e2524109122. doi:10.1073/pnas.2524109122 apa: Svoboda, J., & Chatterjee, K. (2025). Promoters of cooperation in evolutionary games. Proceedings of the National Academy of Sciences. National Academy of Sciences. https://doi.org/10.1073/pnas.2524109122 chicago: Svoboda, Jakub, and Krishnendu Chatterjee. “Promoters of Cooperation in Evolutionary Games.” Proceedings of the National Academy of Sciences. National Academy of Sciences, 2025. https://doi.org/10.1073/pnas.2524109122. ieee: J. Svoboda and K. Chatterjee, “Promoters of cooperation in evolutionary games,” Proceedings of the National Academy of Sciences, vol. 122, no. 51. National Academy of Sciences, p. e2524109122, 2025. ista: Svoboda J, Chatterjee K. 2025. Promoters of cooperation in evolutionary games. Proceedings of the National Academy of Sciences. 122(51), e2524109122. mla: Svoboda, Jakub, and Krishnendu Chatterjee. “Promoters of Cooperation in Evolutionary Games.” Proceedings of the National Academy of Sciences, vol. 122, no. 51, National Academy of Sciences, 2025, p. e2524109122, doi:10.1073/pnas.2524109122. short: J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences 122 (2025) e2524109122. corr_author: '1' date_created: 2025-12-28T23:01:26Z date_published: 2025-12-15T00:00:00Z date_updated: 2026-05-20T08:13:17Z day: '15' ddc: - '000' department: - _id: KrCh doi: 10.1073/pnas.2524109122 ec_funded: 1 external_id: pmid: - '41397136' file: - access_level: open_access checksum: dd50b62a1efc28c0133fe9c11dbee53c content_type: application/pdf creator: dernst date_created: 2025-12-29T09:36:50Z date_updated: 2025-12-29T09:36:50Z file_id: '20860' file_name: 2025_PNAS_Svoboda.pdf file_size: 2308124 relation: main_file success: 1 file_date_updated: 2025-12-29T09:36:50Z has_accepted_license: '1' intvolume: ' 122' issue: '51' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: e2524109122 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 publication_identifier: eissn: - 1091-6490 publication_status: published publisher: National Academy of Sciences quality_controlled: '1' scopus_import: '1' status: public title: Promoters of cooperation in evolutionary 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 122 year: '2025' ... --- OA_place: publisher OA_type: gold _id: '21268' abstract: - lang: eng text: "We consider multiple-environment Markov decision processes (MEMDP), which consist of a finite set of MDPs over the same state space, representing different scenarios of transition structure and probability. The value of a strategy is the probability to satisfy the objective, here a parity objective, in the worst-case scenario, and the value of an MEMDP is the supremum of the values achievable by a strategy.\r\nWe show that deciding whether the value is 1 is a PSPACE-complete problem, and even in P when the number of environments is fixed, along with new insights to the almost-sure winning problem, which is to decide if there exists a strategy with value 1. Pure strategies are sufficient for theses problems, whereas randomization is necessary in general when the value is smaller than 1. We present an algorithm to approximate the value, running in double exponential space. Our results are in contrast to the related model of partially-observable MDPs where all these problems are known to be undecidable." acknowledgement: "Krishnendu Chatterjee: ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund\r\n(FWF) 10.55776/COE12. Jean-François Raskin: PDR Weave project FORM-LEARN-POMDP funded by FNRS and DFG, and the support of the Fondation ULB. Ocan Sankur: ANR BisoUS (ANR-22-CE48-0012) and ANR EpiRL (ANR-22-CE23-0029)." alternative_title: - LIPIcs article_number: '150' 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: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Jean-Francois full_name: Raskin, Jean-Francois last_name: Raskin - first_name: Ocan full_name: Sankur, Ocan last_name: Sankur citation: ama: 'Chatterjee K, Doyen L, Raskin J-F, Sankur O. The value problem for multiple-environment MDPs with parity objective. In: 52nd International Colloquium on Automata, Languages, and Programming. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.ICALP.2025.150' apa: 'Chatterjee, K., Doyen, L., Raskin, J.-F., & Sankur, O. (2025). The value problem for multiple-environment MDPs with parity objective. In 52nd International Colloquium on Automata, Languages, and Programming. Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2025.150' chicago: Chatterjee, Krishnendu, Laurent Doyen, Jean-Francois Raskin, and Ocan Sankur. “The Value Problem for Multiple-Environment MDPs with Parity Objective.” In 52nd International Colloquium on Automata, Languages, and Programming. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPIcs.ICALP.2025.150. ieee: K. Chatterjee, L. Doyen, J.-F. Raskin, and O. Sankur, “The value problem for multiple-environment MDPs with parity objective,” in 52nd International Colloquium on Automata, Languages, and Programming, Aarhus, Denmark, 2025. ista: 'Chatterjee K, Doyen L, Raskin J-F, Sankur O. 2025. The value problem for multiple-environment MDPs with parity objective. 52nd International Colloquium on Automata, Languages, and Programming. ICALP: Automata, Languages and Programming, LIPIcs, , 150.' mla: Chatterjee, Krishnendu, et al. “The Value Problem for Multiple-Environment MDPs with Parity Objective.” 52nd International Colloquium on Automata, Languages, and Programming, 150, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:10.4230/LIPIcs.ICALP.2025.150. short: K. Chatterjee, L. Doyen, J.-F. Raskin, O. Sankur, in:, 52nd International Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. conference: end_date: 2025-07-11 location: Aarhus, Denmark name: 'ICALP: Automata, Languages and Programming' start_date: 2025-07-08 corr_author: '1' date_created: 2026-02-17T07:49:17Z date_published: 2025-07-30T00:00:00Z date_updated: 2026-02-18T07:53:26Z day: '30' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.ICALP.2025.150 ec_funded: 1 external_id: arxiv: - '2504.15960' file: - access_level: open_access checksum: 4477a7fd4fbf0ba6c8e9b15683b5a6b8 content_type: application/pdf creator: dernst date_created: 2026-02-18T07:50:56Z date_updated: 2026-02-18T07:50:56Z file_id: '21313' file_name: 2025_LIPIcs_Chatterjee.pdf file_size: 1075724 relation: main_file success: 1 file_date_updated: 2026-02-18T07:50:56Z has_accepted_license: '1' language: - iso: eng month: '07' 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: 52nd International Colloquium on Automata, Languages, and Programming publication_identifier: isbn: - '9783959773720' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' status: public title: The value problem for multiple-environment MDPs with parity objective 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2025' ... --- OA_place: publisher OA_type: gold _id: '21281' abstract: - lang: eng text: "A strategy profile in a multi-player game is a Nash equilibrium if no player can unilaterally deviate to achieve a strictly better payoff. A profile is an ε-Nash equilibrium if no player can gain more than ε by unilaterally deviating from their strategy. In this work, we use ε-Nash equilibria to approximate the computation of Nash equilibria. Specifically, we focus on turn-based, multiplayer stochastic games played on graphs, where players are restricted to stationary strategies - strategies that use randomness but not memory.\r\nThe problem of deciding the constrained existence of stationary Nash equilibria - where each player’s payoff must lie within a given interval - is known to be ∃ℝ-complete in such a setting (Hansen and Sølvsten, 2020). We extend this line of work to stationary ε-Nash equilibria and present an algorithm that solves the following promise problem: given a game with a Nash equilibrium satisfying the constraints, compute an ε-Nash equilibrium that ε-satisfies those same constraints - satisfies the constraints up to an ε additive error. Our algorithm runs in FNP^NP time.\r\nTo achieve this, we first show that if a constrained Nash equilibrium exists, then one exists where the non-zero probabilities are at least an inverse of a double-exponential in the input. We further prove that such a strategy can be encoded using floating-point representations, as in the work of Frederiksen and Miltersen (2013), which finally gives us our FNP^NP algorithm. \r\nWe further show that the decision version of the promise problem is NP-hard. Finally, we show a partial tightness result by proving a lower bound for such techniques: if a constrained Nash equilibrium exists, then there must be one where the probabilities in the strategies are double-exponentially small." acknowledgement: "This work is a part of project VAMOS that has received funding from the European\r\nResearch Council (ERC), grant agreement No 101020093.\r\n" alternative_title: - LIPIcs article_processing_charge: Yes arxiv: 1 author: - first_name: Ali full_name: Asadi, Ali id: 02d96aae-000e-11ec-b801-cadd0a5eefbb last_name: Asadi - first_name: Leonard full_name: Brice, Leonard last_name: Brice - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: K. S. full_name: Thejaswini, K. S. id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753 last_name: Thejaswini citation: ama: 'Asadi A, Brice L, Chatterjee K, Thejaswini KS. ε-stationary Nash equilibria in multi-player stochastic graph games. In: 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Vol 360. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025:9:1-9:17. doi:10.4230/lipics.fsttcs.2025.9' apa: 'Asadi, A., Brice, L., Chatterjee, K., & Thejaswini, K. S. (2025). ε-stationary Nash equilibria in multi-player stochastic graph games. In 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science (Vol. 360, p. 9:1-9:17). Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/lipics.fsttcs.2025.9' chicago: Asadi, Ali, Leonard Brice, Krishnendu Chatterjee, and K. S. Thejaswini. “ε-Stationary Nash Equilibria in Multi-Player Stochastic Graph Games.” In 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 360:9:1-9:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/lipics.fsttcs.2025.9. ieee: A. Asadi, L. Brice, K. Chatterjee, and K. S. Thejaswini, “ε-stationary Nash equilibria in multi-player stochastic graph games,” in 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Pilani, India, 2025, vol. 360, p. 9:1-9:17. ista: 'Asadi A, Brice L, Chatterjee K, Thejaswini KS. 2025. ε-stationary Nash equilibria in multi-player stochastic graph games. 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 360, 9:1-9:17.' mla: Asadi, Ali, et al. “ε-Stationary Nash Equilibria in Multi-Player Stochastic Graph Games.” 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 360, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 9:1-9:17, doi:10.4230/lipics.fsttcs.2025.9. short: A. Asadi, L. Brice, K. Chatterjee, K.S. Thejaswini, in:, 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 9:1-9:17. conference: end_date: 2025-12-19 location: Pilani, India name: 'FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science' start_date: 2025-12-17 corr_author: '1' date_created: 2026-02-17T08:27:14Z date_published: 2025-12-09T00:00:00Z date_updated: 2026-02-19T09:39:15Z day: '09' ddc: - '000' department: - _id: KrCh - _id: GradSch doi: 10.4230/lipics.fsttcs.2025.9 ec_funded: 1 external_id: arxiv: - '2508.15356' file: - access_level: open_access checksum: a66343e3ccc4a9cc5bc699c03d5764ff content_type: application/pdf creator: dernst date_created: 2026-02-18T09:13:25Z date_updated: 2026-02-18T09:13:25Z file_id: '21316' file_name: 2025_FSTTCS_Asadi.pdf file_size: 1054007 relation: main_file success: 1 file_date_updated: 2026-02-18T09:13:25Z has_accepted_license: '1' intvolume: ' 360' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: 9:1-9:17 project: - _id: 62781420-2b32-11ec-9570-8d9b63373d4d call_identifier: H2020 grant_number: '101020093' name: Vigilant Algorithmic Monitoring of Software publication: 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science publication_identifier: isbn: - '9783959774062' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' status: public title: ε-stationary Nash equilibria in multi-player stochastic graph 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: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 360 year: '2025' ... --- OA_place: publisher OA_type: gold _id: '21320' abstract: - lang: eng text: "Prophet inequalities are a central object of study in optimal stopping theory. In the iid model, a gambler sees values in an online fashion, sampled independently from a given distribution. Upon observing each value, the gambler either accepts it as a reward, or irrevocably rejects it and proceeds to observe the next value. The goal of the gambler, who cannot see the future, is to maximise the expected value of the reward while competing against the expectation of a prophet (the offline maximum). In other words, one seeks to maximise the gambler-to-prophet ratio of the expectations. \r\nThis model has been studied with infinite, finite and unknown number of values. When the gambler faces a random number of values, the model is said to have a random horizon. We consider the model in which the gambler is given a priori knowledge of the horizon’s distribution. Alijani et al. (2020) designed a single-threshold algorithm achieving a ratio of 1/2 when the random horizon has an increasing hazard rate and is independent of the values. We prove that with a single threshold, a ratio of 1/2 is actually achievable for several larger classes of horizon distributions, with the largest being known as the \U0001D4A2 class in reliability theory. Moreover, we show that this does not extend to its dual, the ̅\U0001D4A2 class (which includes the decreasing hazard rate class), while it can be extended to low-variance horizons. Finally, we construct the first example of a family of horizons, for which multiple thresholds are necessary to achieve a nonzero ratio. We establish that the Secretary Problem optimal stopping rule provides one such algorithm, paving the way towards the study of the model beyond single-threshold algorithms." acknowledgement: 'We would like to thank José Correa for his precious advice, Bruno Ziliotto and Vasilis Livanos for early conversations. Giambartolomei, Giordano: EPSRC grants EP/W005573/1 and EP/X021696/1. Mallmann-Trenn, Frederik: EPSRC grant EP/W005573/1. Saona, Raimundo: ERC grant CoG 863818 (ForM-SMArt), ANID Chile grant ACT210005, French Agence Nationale de la Recherche (ANR) grant ANR-21-CE40-0020 (CONVERGENCE), and Austrian Science Fund (FWF) grant 10.55776/COE12.' alternative_title: - LIPIcs article_processing_charge: No arxiv: 1 author: - first_name: Giordano full_name: Giambartolomei, Giordano last_name: Giambartolomei - first_name: Frederik full_name: Mallmann-Trenn, Frederik last_name: Mallmann-Trenn - 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 citation: ama: 'Giambartolomei G, Mallmann-Trenn F, Saona Urmeneta RJ. IID prophet inequality with random horizon: Going beyond increasing hazard rates. In: 52nd International Colloquium on Automata, Languages, and Programming. Vol 334. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.ICALP.2025.87' apa: 'Giambartolomei, G., Mallmann-Trenn, F., & Saona Urmeneta, R. J. (2025). IID prophet inequality with random horizon: Going beyond increasing hazard rates. In 52nd International Colloquium on Automata, Languages, and Programming (Vol. 334). Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2025.87' chicago: 'Giambartolomei, Giordano, Frederik Mallmann-Trenn, and Raimundo J Saona Urmeneta. “IID Prophet Inequality with Random Horizon: Going beyond Increasing Hazard Rates.” In 52nd International Colloquium on Automata, Languages, and Programming, Vol. 334. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPIcs.ICALP.2025.87.' ieee: 'G. Giambartolomei, F. Mallmann-Trenn, and R. J. Saona Urmeneta, “IID prophet inequality with random horizon: Going beyond increasing hazard rates,” in 52nd International Colloquium on Automata, Languages, and Programming, Aarhus, Denmark, 2025, vol. 334.' ista: 'Giambartolomei G, Mallmann-Trenn F, Saona Urmeneta RJ. 2025. IID prophet inequality with random horizon: Going beyond increasing hazard rates. 52nd International Colloquium on Automata, Languages, and Programming. ICALP: Automata, Languages and Programming, LIPIcs, vol. 334.' mla: 'Giambartolomei, Giordano, et al. “IID Prophet Inequality with Random Horizon: Going beyond Increasing Hazard Rates.” 52nd International Colloquium on Automata, Languages, and Programming, vol. 334, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:10.4230/LIPIcs.ICALP.2025.87.' short: G. Giambartolomei, F. Mallmann-Trenn, R.J. Saona Urmeneta, in:, 52nd International Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. conference: end_date: 2025-07-11 location: Aarhus, Denmark name: 'ICALP: Automata, Languages and Programming' start_date: 2025-07-08 date_created: 2026-02-18T10:44:14Z date_published: 2025-06-30T00:00:00Z date_updated: 2026-02-19T07:43:29Z day: '30' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.ICALP.2025.87 ec_funded: 1 external_id: arxiv: - '2407.11752' file: - access_level: open_access checksum: 960110956c26a5cefadde8e47888bfbe content_type: application/pdf creator: dernst date_created: 2026-02-19T07:41:55Z date_updated: 2026-02-19T07:41:55Z file_id: '21331' file_name: 2025_ICALP_Giambartolomei.pdf file_size: 876167 relation: main_file success: 1 file_date_updated: 2026-02-19T07:41:55Z has_accepted_license: '1' intvolume: ' 334' 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: 52nd International Colloquium on Automata, Languages, and Programming publication_identifier: isbn: - '9783959773720' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' status: public title: 'IID prophet inequality with random horizon: Going beyond increasing hazard rates' 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 334 year: '2025' ... --- OA_place: publisher OA_type: gold _id: '21412' abstract: - lang: eng text: "Payment channel networks (PCNs) are a promising technology that alleviates blockchain scalability by shifting the transaction load from the blockchain to the PCN. Nevertheless, the network topology has to be carefully designed to maximise the transaction throughput in PCNs. Additionally, users in PCNs also have to make optimal decisions on which transactions to forward and which to reject to prolong the lifetime of their channels. In this work, we consider an input sequence of transactions over p parties. Each transaction consists of a transaction size, source, and target, and can be either accepted or rejected (entailing a cost). The goal is to design a PCN topology among the p cooperating parties, along with the channel capacities, and then output a decision for each transaction in the sequence to minimise the cost of creating and augmenting channels, as well as the cost of rejecting transactions. Our main contribution is an \U0001D4AA(p) approximation algorithm for the problem with p parties. We further show that with some assumptions on the distribution of transactions, we can reduce the approximation ratio to \U0001D4AA(√p). We complement our theoretical analysis with an empirical study of our assumptions and approach in the context of the Lightning Network." acknowledgement: "Chatterjee, Krishnendu: European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.\r\nKřišťan, Jan Matyáš: Czech Science Foundation Grant no. 24-12046S.\r\nSchmid, Stefan: German Research Foundation (DFG) project ReNO (SPP 2378) from 2023-2027.\r\nSvoboda, Jakub: European Research Council CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.\r\nYeo, Michelle: MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms)." alternative_title: - LIPIcs article_number: '23' 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: Jan Matyáš full_name: Křišťan, Jan Matyáš last_name: Křišťan - 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: 'Chatterjee K, Křišťan JM, Schmid S, Svoboda J, Yeo MX. Boosting payment channel network liquidity with topology optimization and transaction selection. In: 39th International Symposium on Distributed Computing. Vol 356. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.DISC.2025.23' apa: 'Chatterjee, K., Křišťan, J. M., Schmid, S., Svoboda, J., & Yeo, M. X. (2025). Boosting payment channel network liquidity with topology optimization and transaction selection. In 39th International Symposium on Distributed Computing (Vol. 356). Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.DISC.2025.23' chicago: Chatterjee, Krishnendu, Jan Matyáš Křišťan, Stefan Schmid, Jakub Svoboda, and Michelle X Yeo. “Boosting Payment Channel Network Liquidity with Topology Optimization and Transaction Selection.” In 39th International Symposium on Distributed Computing, Vol. 356. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPIcs.DISC.2025.23. ieee: K. Chatterjee, J. M. Křišťan, S. Schmid, J. Svoboda, and M. X. Yeo, “Boosting payment channel network liquidity with topology optimization and transaction selection,” in 39th International Symposium on Distributed Computing, Berlin, Germany, 2025, vol. 356. ista: 'Chatterjee K, Křišťan JM, Schmid S, Svoboda J, Yeo MX. 2025. Boosting payment channel network liquidity with topology optimization and transaction selection. 39th International Symposium on Distributed Computing. DISC: Symposium on Distributed Computing, LIPIcs, vol. 356, 23.' mla: Chatterjee, Krishnendu, et al. “Boosting Payment Channel Network Liquidity with Topology Optimization and Transaction Selection.” 39th International Symposium on Distributed Computing, vol. 356, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:10.4230/LIPIcs.DISC.2025.23. short: K. Chatterjee, J.M. Křišťan, S. Schmid, J. Svoboda, M.X. Yeo, in:, 39th International Symposium on Distributed Computing, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. conference: end_date: 2025-10-31 location: Berlin, Germany name: 'DISC: Symposium on Distributed Computing' start_date: 2025-10-27 date_created: 2026-03-08T23:01:46Z date_published: 2025-10-22T00:00:00Z date_updated: 2026-03-09T11:52:58Z day: '22' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.DISC.2025.23 ec_funded: 1 external_id: arxiv: - '2508.14524' file: - access_level: open_access checksum: 8e3d1594365df60163d9df22158a37b1 content_type: application/pdf creator: dernst date_created: 2026-03-09T11:51:59Z date_updated: 2026-03-09T11:51:59Z file_id: '21418' file_name: 2025_DISC_Chatterjee.pdf file_size: 1130069 relation: main_file success: 1 file_date_updated: 2026-03-09T11:51:59Z has_accepted_license: '1' intvolume: ' 356' language: - iso: eng main_file_link: - open_access: '1' url: https://eprint.iacr.org/2025/1484.pdf month: '10' 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: 39th International Symposium on Distributed Computing publication_identifier: isbn: - '9783959774024' issn: - 1868-8969 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' scopus_import: '1' status: public title: Boosting payment channel network liquidity with topology optimization and transaction selection 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 356 year: '2025' ... --- DOAJ_listed: '1' OA_place: publisher OA_type: gold PlanS_conform: '1' _id: '21413' abstract: - lang: eng text: "We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs).\r\nThe primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors.\r\nThe presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios.\r\nThe first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP." acknowledgement: "This research was funded in part by the European Research Council (ERC) under grant agreement AdG-267989 (QUAREM)*, AdG-246967 (VERIWARE)*, StG-279307 (Graph Games)*\r\n, CoG-863818 (ForM-SMArt), and AdG-834115 (FUN2MODEL), by the EU FP7 project HIERATIC*, by the German Research Foundation (DFG) project 427755713 (GOPro), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE)* , S11407-N23 (RiSE)*\r\n, and P23499-N23* , by the Czech Science Foundation grant No P202/12/P612* and GA23-06963S, by the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant\r\nAgency of Masaryk University, by EPSRC project EP/K038575/1*, and by the Microsoft faculty fellows award*. A preliminary version of this article appeared at ATVA 2014 [33]. The * indicates funding that supported that version." article_number: '10' article_processing_charge: Yes article_type: original arxiv: 1 author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Marta full_name: Kwiatkowska, Marta last_name: Kwiatkowska - 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: Mateusz full_name: Ujma, Mateusz last_name: Ujma citation: ama: Brázdil T, Chatterjee K, Chmelik M, et al. Learning algorithms for verification of Markov decision processes. TheoretiCS. 2025;4. doi:10.46298/theoretics.25.10 apa: Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2025). Learning algorithms for verification of Markov decision processes. TheoretiCS. TheoretiCS Foundation. https://doi.org/10.46298/theoretics.25.10 chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, and Mateusz Ujma. “Learning Algorithms for Verification of Markov Decision Processes.” TheoretiCS. TheoretiCS Foundation, 2025. https://doi.org/10.46298/theoretics.25.10. ieee: T. Brázdil et al., “Learning algorithms for verification of Markov decision processes,” TheoretiCS, vol. 4. TheoretiCS Foundation, 2025. ista: Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Meggendorfer T, Parker D, Ujma M. 2025. Learning algorithms for verification of Markov decision processes. TheoretiCS. 4, 10. mla: Brázdil, Tomáš, et al. “Learning Algorithms for Verification of Markov Decision Processes.” TheoretiCS, vol. 4, 10, TheoretiCS Foundation, 2025, doi:10.46298/theoretics.25.10. short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, T. Meggendorfer, D. Parker, M. Ujma, TheoretiCS 4 (2025). date_created: 2026-03-08T23:01:46Z date_published: 2025-04-01T00:00:00Z date_updated: 2026-03-09T11:43:38Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.46298/theoretics.25.10 ec_funded: 1 external_id: arxiv: - '2403.09184' file: - access_level: open_access checksum: 2ccf563ae577ee08d82baf752292ca7b content_type: application/pdf creator: dernst date_created: 2026-03-09T11:39:59Z date_updated: 2026-03-09T11:39:59Z file_id: '21417' file_name: 2026_TheoretiCS_Brazdil.pdf file_size: 861607 relation: main_file success: 1 file_date_updated: 2026-03-09T11:39:59Z has_accepted_license: '1' intvolume: ' 4' language: - iso: eng month: '04' oa: 1 oa_version: Published Version project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 25F2ACDE-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Rigorous Systems Engineering - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification publication: TheoretiCS publication_identifier: eissn: - 2751-4838 publication_status: published publisher: TheoretiCS Foundation quality_controlled: '1' scopus_import: '1' status: public title: Learning algorithms for verification of Markov decision processes 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: 4 year: '2025' ... --- OA_place: repository OA_type: gold _id: '21668' abstract: - lang: eng text: "This artifact allows to review and reproduce the experiments from the paper *A Revised Practitioner's Guide to MDP Model Checking Algorithms*.\r\nThe package contains all original logfiles and derived data used to generate the plots as in the paper. Furthermore, the artifact contains the model checking tools `Storm` and `mcsta` in the version exercised in the paper, the used Docker container, as well as benchmark instances and execution scripts to reproduce the experiments.\r\n\r\nSee also the artifact of the conference paper: https://zenodo.org/records/7509474" article_processing_charge: No author: - first_name: Arnd full_name: Hartmanns, Arnd last_name: Hartmanns - first_name: Sebastian full_name: Junges, Sebastian last_name: Junges - first_name: Tim full_name: Quatmann, Tim last_name: Quatmann - first_name: Maximilian full_name: Weininger, Maximilian id: 02ab0197-cc70-11ed-ab61-918e71f56881 last_name: Weininger orcid: 0000-0002-0163-2152 citation: ama: Hartmanns A, Junges S, Quatmann T, Weininger M. Benchmark data for the revised practitioner’s guide to MDP model checking algorithms. 2025. doi:10.5281/ZENODO.14500423 apa: Hartmanns, A., Junges, S., Quatmann, T., & Weininger, M. (2025). Benchmark data for the revised practitioner’s guide to MDP model checking algorithms. Zenodo. https://doi.org/10.5281/ZENODO.14500423 chicago: Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. “Benchmark Data for the Revised Practitioner’s Guide to MDP Model Checking Algorithms.” Zenodo, 2025. https://doi.org/10.5281/ZENODO.14500423. ieee: A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “Benchmark data for the revised practitioner’s guide to MDP model checking algorithms.” Zenodo, 2025. ista: Hartmanns A, Junges S, Quatmann T, Weininger M. 2025. Benchmark data for the revised practitioner’s guide to MDP model checking algorithms, Zenodo, 10.5281/ZENODO.14500423. mla: Hartmanns, Arnd, et al. Benchmark Data for the Revised Practitioner’s Guide to MDP Model Checking Algorithms. Zenodo, 2025, doi:10.5281/ZENODO.14500423. short: A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, (2025). date_created: 2026-04-07T09:47:22Z date_published: 2025-03-07T00:00:00Z date_updated: 2026-04-07T09:52:55Z day: '07' ddc: - '000' department: - _id: KrCh doi: 10.5281/ZENODO.14500423 main_file_link: - open_access: '1' url: https://doi.org/10.5281/ZENODO.14500423 month: '03' oa: 1 oa_version: Published Version publisher: Zenodo related_material: record: - id: '21661' relation: used_for_analysis_in status: public status: public title: Benchmark data for the revised practitioner's guide to MDP model checking algorithms type: research_data_reference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2025' ... --- _id: '17037' abstract: - lang: eng text: Zero-sum stochastic games are parameterized by payoffs, transitions, and possibly a discount rate. In this article, we study how the main solution concepts, the discounted and undiscounted values, vary when these parameters are perturbed. We focus on the marginal values, introduced by Mills in 1956 in the context of matrix games—that is, the directional derivatives of the value along any fixed perturbation. We provide a formula for the marginal values of a discounted stochastic game. Further, under mild assumptions on the perturbation, we provide a formula for their limit as the discount rate vanishes and for the marginal values of an undiscounted stochastic game. We also show, via an example, that the two latter differ in general. acknowledgement: This work was supported by Fondation CFM pour la Recherche; the European Research Council [Grant ERC-CoG-863818 (ForM-SMArt)]; and Agence Nationale de la Recherche [Grant ANR-21-CE40-0020]. article_processing_charge: No article_type: original author: - first_name: Luc full_name: Attia, Luc last_name: Attia - first_name: Miquel full_name: Oliu-Barton, Miquel last_name: Oliu-Barton - 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 citation: ama: Attia L, Oliu-Barton M, Saona Urmeneta RJ. Marginal values of a stochastic game. Mathematics of Operations Research. 2025;50(1):482-505. doi:10.1287/moor.2023.0297 apa: Attia, L., Oliu-Barton, M., & Saona Urmeneta, R. J. (2025). Marginal values of a stochastic game. Mathematics of Operations Research. Institute for Operations Research and the Management Sciences. https://doi.org/10.1287/moor.2023.0297 chicago: Attia, Luc, Miquel Oliu-Barton, and Raimundo J Saona Urmeneta. “Marginal Values of a Stochastic Game.” Mathematics of Operations Research. Institute for Operations Research and the Management Sciences, 2025. https://doi.org/10.1287/moor.2023.0297. ieee: L. Attia, M. Oliu-Barton, and R. J. Saona Urmeneta, “Marginal values of a stochastic game,” Mathematics of Operations Research, vol. 50, no. 1. Institute for Operations Research and the Management Sciences, pp. 482–505, 2025. ista: Attia L, Oliu-Barton M, Saona Urmeneta RJ. 2025. Marginal values of a stochastic game. Mathematics of Operations Research. 50(1), 482–505. mla: Attia, Luc, et al. “Marginal Values of a Stochastic Game.” Mathematics of Operations Research, vol. 50, no. 1, Institute for Operations Research and the Management Sciences, 2025, pp. 482–505, doi:10.1287/moor.2023.0297. short: L. Attia, M. Oliu-Barton, R.J. Saona Urmeneta, Mathematics of Operations Research 50 (2025) 482–505. date_created: 2024-05-22T11:41:14Z date_published: 2025-02-01T00:00:00Z date_updated: 2026-04-07T12:31:21Z day: '01' department: - _id: GradSch - _id: KrCh doi: 10.1287/moor.2023.0297 ec_funded: 1 external_id: isi: - '001184648000001' intvolume: ' 50' isi: 1 issue: '1' language: - iso: eng month: '02' oa_version: None page: 482-505 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: Mathematics of Operations Research publication_identifier: eissn: - 1526-5471 issn: - 0364-765X publication_status: published publisher: Institute for Operations Research and the Management Sciences quality_controlled: '1' related_material: record: - id: '20234' relation: dissertation_contains status: public scopus_import: '1' status: public title: Marginal values of a stochastic game type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 50 year: '2025' ... --- OA_type: closed access _id: '18529' abstract: - lang: eng text: Temporal networks are obtained from time-dependent interactions among individuals, whereas the interactions can be emails, phone calls, face-to-face meetings, or work collaboration. In this article, a temporal game framework is established, in which interactions among rational individuals are embedded into two-player games in a time-dependent manner. This allows studying the time-dependent complexity and variability of interactions, and the way they affect prosocial behaviors. Based on this simple mathematical model, it is found that the level of cooperation is promoted when the time of collaboration is equally limited for every individual. This observation is confirmed by a series of systematic human experiments on over 1,400 subjects, forming a foundation for comprehensively describing human temporal interactions in collaboration. The research results reveal an important incentive for human cooperation, leading to a better understanding of a fascinating aspect of human nature in society. article_processing_charge: No article_type: original author: - first_name: Yichao full_name: Zhang, Yichao last_name: Zhang - first_name: Jiasheng full_name: Wang, Jiasheng last_name: Wang - first_name: Guanghui full_name: Wen, Guanghui last_name: Wen - first_name: Jihong full_name: Guan, Jihong last_name: Guan - first_name: Shuigeng full_name: Zhou, Shuigeng last_name: Zhou - first_name: Guanrong full_name: Chen, Guanrong last_name: Chen - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Matjaz full_name: Perc, Matjaz last_name: Perc citation: ama: Zhang Y, Wang J, Wen G, et al. Limitation of time promotes cooperation in structured collaboration systems. IEEE Transactions on Network Science and Engineering. 2025;12(1):4-12. doi:10.1109/TNSE.2024.3481434 apa: Zhang, Y., Wang, J., Wen, G., Guan, J., Zhou, S., Chen, G., … Perc, M. (2025). Limitation of time promotes cooperation in structured collaboration systems. IEEE Transactions on Network Science and Engineering. IEEE. https://doi.org/10.1109/TNSE.2024.3481434 chicago: Zhang, Yichao, Jiasheng Wang, Guanghui Wen, Jihong Guan, Shuigeng Zhou, Guanrong Chen, Krishnendu Chatterjee, and Matjaz Perc. “Limitation of Time Promotes Cooperation in Structured Collaboration Systems.” IEEE Transactions on Network Science and Engineering. IEEE, 2025. https://doi.org/10.1109/TNSE.2024.3481434. ieee: Y. Zhang et al., “Limitation of time promotes cooperation in structured collaboration systems,” IEEE Transactions on Network Science and Engineering, vol. 12, no. 1. IEEE, pp. 4–12, 2025. ista: Zhang Y, Wang J, Wen G, Guan J, Zhou S, Chen G, Chatterjee K, Perc M. 2025. Limitation of time promotes cooperation in structured collaboration systems. IEEE Transactions on Network Science and Engineering. 12(1), 4–12. mla: Zhang, Yichao, et al. “Limitation of Time Promotes Cooperation in Structured Collaboration Systems.” IEEE Transactions on Network Science and Engineering, vol. 12, no. 1, IEEE, 2025, pp. 4–12, doi:10.1109/TNSE.2024.3481434. short: Y. Zhang, J. Wang, G. Wen, J. Guan, S. Zhou, G. Chen, K. Chatterjee, M. Perc, IEEE Transactions on Network Science and Engineering 12 (2025) 4–12. date_created: 2024-11-10T23:02:00Z date_published: 2025-01-01T00:00:00Z date_updated: 2025-02-27T12:35:48Z day: '01' department: - _id: KrCh doi: 10.1109/TNSE.2024.3481434 external_id: isi: - '001385382200040' intvolume: ' 12' isi: 1 issue: '1' language: - iso: eng month: '01' oa_version: None page: 4-12 publication: IEEE Transactions on Network Science and Engineering publication_identifier: eissn: - 2327-4697 publication_status: published publisher: IEEE quality_controlled: '1' scopus_import: '1' status: public title: Limitation of time promotes cooperation in structured collaboration systems type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 12 year: '2025' ... --- OA_place: publisher OA_type: hybrid PlanS_conform: '1' _id: '19074' abstract: - lang: eng text: 'The public goods game is among the most studied metaphors of cooperation in groups. In this game, individuals can use their endowments to make contributions towards a good that benefits everyone. Each individual, however, is tempted to free-ride on the contributions of others. Herein, we study repeated public goods games among asymmetric players. Previous work has explored to which extent asymmetry allows for full cooperation, such that players contribute their full endowment each round. However, by design that work focusses on equilibria where individuals make the same contribution each round. Instead, here we consider players whose contributions along the equilibrium path can change from one round to the next. We do so for three different models – one without any budget constraints, one with endowment constraints, and one in which individuals can save their current endowment to be used in subsequent rounds. In each case, we explore two key quantities: the welfare and the resource efficiency that can be achieved in equilibrium. Welfare corresponds to the sum of all players’ payoffs. Resource efficiency relates this welfare to the total contributions made by the players. Compared to constant contribution sequences, we find that time-dependent contributions can improve resource efficiency across all three models. Moreover, they can improve the players’ welfare in the model with savings.' acknowledgement: 'This work was supported by the European Research Council CoG 863818 (ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529: E-DIRECT (to C.H.), the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement #754411 and the French Agence Nationale de la Recherche (under the Investissement d’Avenir programme, ANR-17-EURE-0010), and ARC SRIEAS Grant SR200100005 Securing Antarctica’s Environmental Future (to M.K.). Open access funding provided by Institute of Science and Technology (IST Austria).' article_processing_charge: Yes (via OA deal) article_type: original 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: Christian full_name: Hilbe, Christian id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87 last_name: Hilbe orcid: 0000-0001-5116-955X - first_name: Manuel full_name: Staab, Manuel last_name: Staab - first_name: Maria full_name: Kleshnina, Maria id: 4E21749C-F248-11E8-B48F-1D18A9856A87 last_name: Kleshnina orcid: 0000-0002-5518-8317 - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: Hübner V, Hilbe C, Staab M, Kleshnina M, Chatterjee K. Time-dependent strategies in repeated asymmetric public goods games. Dynamic Games and Applications. 2025;15:1617-1645. doi:10.1007/s13235-025-00627-5 apa: Hübner, V., Hilbe, C., Staab, M., Kleshnina, M., & Chatterjee, K. (2025). Time-dependent strategies in repeated asymmetric public goods games. Dynamic Games and Applications. Springer Nature. https://doi.org/10.1007/s13235-025-00627-5 chicago: Hübner, Valentin, Christian Hilbe, Manuel Staab, Maria Kleshnina, and Krishnendu Chatterjee. “Time-Dependent Strategies in Repeated Asymmetric Public Goods Games.” Dynamic Games and Applications. Springer Nature, 2025. https://doi.org/10.1007/s13235-025-00627-5. ieee: V. Hübner, C. Hilbe, M. Staab, M. Kleshnina, and K. Chatterjee, “Time-dependent strategies in repeated asymmetric public goods games,” Dynamic Games and Applications, vol. 15. Springer Nature, pp. 1617–1645, 2025. ista: Hübner V, Hilbe C, Staab M, Kleshnina M, Chatterjee K. 2025. Time-dependent strategies in repeated asymmetric public goods games. Dynamic Games and Applications. 15, 1617–1645. mla: Hübner, Valentin, et al. “Time-Dependent Strategies in Repeated Asymmetric Public Goods Games.” Dynamic Games and Applications, vol. 15, Springer Nature, 2025, pp. 1617–45, doi:10.1007/s13235-025-00627-5. short: V. Hübner, C. Hilbe, M. Staab, M. Kleshnina, K. Chatterjee, Dynamic Games and Applications 15 (2025) 1617–1645. corr_author: '1' date_created: 2025-02-23T23:01:57Z date_published: 2025-11-01T00:00:00Z date_updated: 2026-04-07T12:30:56Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.1007/s13235-025-00627-5 ec_funded: 1 external_id: isi: - '001415587800001' file: - access_level: open_access checksum: de0a412cbb7d98bf5e6a551c26acbefa content_type: application/pdf creator: dernst date_created: 2025-12-30T08:01:35Z date_updated: 2025-12-30T08:01:35Z file_id: '20888' file_name: 2025_DynGamesAppl_Huebner.pdf file_size: 1126178 relation: main_file success: 1 file_date_updated: 2025-12-30T08:01:35Z has_accepted_license: '1' intvolume: ' 15' isi: 1 language: - iso: eng month: '11' oa: 1 oa_version: Published Version page: 1617-1645 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' - _id: 260C2330-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '754411' name: ISTplus - Postdoctoral Fellowships publication: Dynamic Games and Applications publication_identifier: eissn: - 2153-0793 issn: - 2153-0785 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '19903' relation: dissertation_contains status: public scopus_import: '1' status: public title: Time-dependent strategies in repeated asymmetric public goods 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 15 year: '2025' ... --- OA_place: repository OA_type: green _id: '19375' abstract: - lang: eng text: "Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs.\r\n\r\nThe idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools." acknowledgement: This research was funded in part by the DFG project 427755713 GOPro, the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement 101034413 (IST-BRIDGE). alternative_title: - LNCS article_processing_charge: No arxiv: 1 author: - first_name: Muqsit full_name: Azeem, Muqsit last_name: Azeem - first_name: Debraj full_name: Chakraborty, Debraj last_name: Chakraborty - first_name: Sudeep full_name: Kanav, Sudeep last_name: Kanav - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Mohammadsadegh full_name: Mohagheghi, Mohammadsadegh last_name: Mohagheghi - first_name: Stefanie full_name: Mohr, Stefanie last_name: Mohr - first_name: Maximilian full_name: Weininger, Maximilian id: 02ab0197-cc70-11ed-ab61-918e71f56881 last_name: Weininger citation: ama: 'Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In: 26th International Conference on Verification, Model Checking, and Abstract Interpretation. Vol 15530. Springer Nature; 2025:97-120. doi:10.1007/978-3-031-82703-7_5' apa: 'Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr, S., & Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In 26th International Conference on Verification, Model Checking, and Abstract Interpretation (Vol. 15530, pp. 97–120). Denver, CO, United States: Springer Nature. https://doi.org/10.1007/978-3-031-82703-7_5' chicago: Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” In 26th International Conference on Verification, Model Checking, and Abstract Interpretation, 15530:97–120. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-82703-7_5. ieee: M. Azeem et al., “1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization,” in 26th International Conference on Verification, Model Checking, and Abstract Interpretation, Denver, CO, United States, 2025, vol. 15530, pp. 97–120. ista: 'Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. 26th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.' mla: Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” 26th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 15530, Springer Nature, 2025, pp. 97–120, doi:10.1007/978-3-031-82703-7_5. short: M. Azeem, D. Chakraborty, S. Kanav, J. Kretinsky, M. Mohagheghi, S. Mohr, M. Weininger, in:, 26th International Conference on Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2025, pp. 97–120. conference: end_date: 2025-01-21 location: Denver, CO, United States name: 'VMCAI: Verification, Model Checking, and Abstract Interpretation' start_date: 2025-01-20 date_created: 2025-03-09T23:01:29Z date_published: 2025-01-23T00:00:00Z date_updated: 2025-09-30T10:46:54Z day: '23' department: - _id: KrCh doi: 10.1007/978-3-031-82703-7_5 ec_funded: 1 external_id: arxiv: - '2410.18293' isi: - '001446577100005' intvolume: ' 15530' isi: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2410.18293 month: '01' oa: 1 oa_version: Preprint page: 97-120 project: - _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c call_identifier: H2020 grant_number: '101034413' name: 'IST-BRIDGE: International postdoctoral program' publication: 26th International Conference on Verification, Model Checking, and Abstract Interpretation publication_identifier: eissn: - 1611-3349 isbn: - '9783031827020' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 15530 year: '2025' ... --- OA_place: repository OA_type: green _id: '19445' abstract: - lang: eng text: "In reconfiguration, we are given two solutions to a graph problem, such as Vertex Cover or Dominating Set, with each solution represented by a placement of tokens on vertices of the graph. Our task is to reconfigure one into the other using small steps while ensuring the intermediate configurations of tokens are also valid solutions. The two commonly studied settings are Token Jumping and Token Sliding, which allows moving a single token to an arbitrary or an adjacent vertex, respectively.\r\n\r\nWe introduce new rules that generalize Token Jumping, parameterized by the number of tokens allowed to move at once and by the maximum distance of each move. Our main contribution is identifying minimal rules that allow reconfiguring any possible given solution into any other for Independent Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide an efficient algorithm that finds a corresponding reconfiguration sequence.\r\n\r\nWe further focus on the rule that allows each token to move to an adjacent vertex in a single step. This natural variant turns out to be the minimal rule that guarantees reconfigurability for Vertex Cover. We determine the computational complexity of deciding whether a (shortest) reconfiguration sequence exists under this rule for the three studied problems. While reachability for Vertex Cover is shown to be in P, finding a shortest sequence is shown to be NP-complete. For Independent Set and Dominating Set, even reachability is shown to be PSPACE-complete." acknowledgement: J. M. Křišťan acknowledges the support of the Czech Science Foundation Grant No. 24-12046S. This work was supported by the Grant Agency of the Czech Technical University in Prague, grant No. SGS23/205/OHK3/3T/18. J. Svoboda acknowledges the support of the ERC CoG 863818 (ForM-SMArt) grant. alternative_title: - LNCS article_processing_charge: No arxiv: 1 author: - first_name: Jan Matyáš full_name: Křišťan, Jan Matyáš last_name: Křišťan - first_name: Jakub full_name: Svoboda, Jakub id: 130759D2-D7DD-11E9-87D2-DE0DE6697425 last_name: Svoboda orcid: 0000-0002-1419-3267 citation: ama: 'Křišťan JM, Svoboda J. Reconfiguration using generalized token jumping. In: 19th International Conference and Workshops on Algorithms and Computation. Vol 15411. Springer Nature; 2025:244-265. doi:10.1007/978-981-96-2845-2_16' apa: 'Křišťan, J. M., & Svoboda, J. (2025). Reconfiguration using generalized token jumping. In 19th International Conference and Workshops on Algorithms and Computation (Vol. 15411, pp. 244–265). Chengdu, China: Springer Nature. https://doi.org/10.1007/978-981-96-2845-2_16' chicago: Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized Token Jumping.” In 19th International Conference and Workshops on Algorithms and Computation, 15411:244–65. Springer Nature, 2025. https://doi.org/10.1007/978-981-96-2845-2_16. ieee: J. M. Křišťan and J. Svoboda, “Reconfiguration using generalized token jumping,” in 19th International Conference and Workshops on Algorithms and Computation, Chengdu, China, 2025, vol. 15411, pp. 244–265. ista: 'Křišťan JM, Svoboda J. 2025. Reconfiguration using generalized token jumping. 19th International Conference and Workshops on Algorithms and Computation. WALCOM: International Conference and Workshops on Algorithms and Computation, LNCS, vol. 15411, 244–265.' mla: Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized Token Jumping.” 19th International Conference and Workshops on Algorithms and Computation, vol. 15411, Springer Nature, 2025, pp. 244–65, doi:10.1007/978-981-96-2845-2_16. short: J.M. Křišťan, J. Svoboda, in:, 19th International Conference and Workshops on Algorithms and Computation, Springer Nature, 2025, pp. 244–265. conference: end_date: 2025-03-02 location: Chengdu, China name: 'WALCOM: International Conference and Workshops on Algorithms and Computation' start_date: 2025-02-28 date_created: 2025-03-23T23:01:27Z date_published: 2025-02-20T00:00:00Z date_updated: 2025-09-30T11:14:33Z day: '20' department: - _id: KrCh doi: 10.1007/978-981-96-2845-2_16 ec_funded: 1 external_id: arxiv: - '2411.12582' isi: - '001537885900016' intvolume: ' 15411' isi: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2411.12582 month: '02' oa: 1 oa_version: Preprint page: 244-265 project: - _id: 0599E47C-7A3F-11EA-A408-12923DDC885E call_identifier: H2020 grant_number: '863818' name: 'Formal Methods for Stochastic Models: Algorithms and Applications' publication: 19th International Conference and Workshops on Algorithms and Computation publication_identifier: eissn: - 1611-3349 isbn: - '9789819628445' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' scopus_import: '1' status: public title: Reconfiguration using generalized token jumping type: conference user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 15411 year: '2025' ... --- OA_place: publisher OA_type: hybrid _id: '19499' abstract: - lang: eng text: Quantum hardware is inherently fragile and noisy. We find that the accuracy of traditional quantum error correction algorithms can be improved depending on the hardware. Given different hardware specifications, we automatically synthesize hardware-optimal algorithms for parity correction, qubit resetting, and GHZ (Greenberger–Horne–Zeilinger) state preparation. Using stochastic techniques from computer science, our method presents a computational tool to compute exact accuracy guarantees and synthesize optimal algorithms that are often different from traditional ones. We also show that improvements can be gained with respect to the Qiskit transpiler as we compute the hardware-optimal qubit mapping for the GHZ state-preparation problem. acknowledgement: We thank the reviewers. In particular, they inspired us to analyze the reset and state-preparation problems, to compute optimal qubit mappings, and to apply our method to a quantum error correction scheme that includes both bitflip and phaseflip corrections. We also thank Raimundo Saona and Marek Chalupa for their time spent in insightful discussions. This research was partially supported by the European Research Council CoG 863818 (ForM-SMArt) grant. article_number: e2419273122 article_processing_charge: Yes (in subscription journal) article_type: original author: - first_name: Stefanie full_name: Muroya Lei, Stefanie id: a376de31-8972-11ed-ae7b-d0251c13c8ff last_name: Muroya Lei - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: ama: Muroya Lei S, Chatterjee K, Henzinger TA. Hardware-optimal quantum algorithms. Proceedings of the National Academy of Sciences. 2025;122(12). doi:10.1073/pnas.2419273122 apa: Muroya Lei, S., Chatterjee, K., & Henzinger, T. A. (2025). Hardware-optimal quantum algorithms. Proceedings of the National Academy of Sciences. National Academy of Sciences. https://doi.org/10.1073/pnas.2419273122 chicago: Muroya Lei, Stefanie, Krishnendu Chatterjee, and Thomas A Henzinger. “Hardware-Optimal Quantum Algorithms.” Proceedings of the National Academy of Sciences. National Academy of Sciences, 2025. https://doi.org/10.1073/pnas.2419273122. ieee: S. Muroya Lei, K. Chatterjee, and T. A. Henzinger, “Hardware-optimal quantum algorithms,” Proceedings of the National Academy of Sciences, vol. 122, no. 12. National Academy of Sciences, 2025. ista: Muroya Lei S, Chatterjee K, Henzinger TA. 2025. Hardware-optimal quantum algorithms. Proceedings of the National Academy of Sciences. 122(12), e2419273122. mla: Muroya Lei, Stefanie, et al. “Hardware-Optimal Quantum Algorithms.” Proceedings of the National Academy of Sciences, vol. 122, no. 12, e2419273122, National Academy of Sciences, 2025, doi:10.1073/pnas.2419273122. short: S. Muroya Lei, K. Chatterjee, T.A. Henzinger, Proceedings of the National Academy of Sciences 122 (2025). corr_author: '1' date_created: 2025-04-06T22:01:32Z date_published: 2025-03-25T00:00:00Z date_updated: 2026-04-28T13:41:14Z day: '25' ddc: - '000' department: - _id: KrCh - _id: ToHe doi: 10.1073/pnas.2419273122 ec_funded: 1 external_id: isi: - '001459435600001' pmid: - '40106357' file: - access_level: open_access checksum: 83501b8a65ee5fdd3f5604fc28eddc22 content_type: application/pdf creator: dernst date_created: 2025-04-07T11:42:22Z date_updated: 2025-04-07T11:42:22Z file_id: '19524' file_name: 2025_PNAS_Muroya.pdf file_size: 6805668 relation: main_file success: 1 file_date_updated: 2025-04-07T11:42:22Z has_accepted_license: '1' intvolume: ' 122' isi: 1 issue: '12' language: - iso: eng month: '03' 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 publication_identifier: eissn: - 1091-6490 issn: - 0027-8424 publication_status: published publisher: National Academy of Sciences quality_controlled: '1' related_material: link: - relation: software url: https://github.com/smml1996/algorithm_synthesis - description: News on ISTA website relation: press_release url: https://ista.ac.at/en/news/hardware-optimal-quantum-algorithms/ scopus_import: '1' status: public title: Hardware-optimal quantum algorithms 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: ba8df636-2132-11f1-aed0-ed93e2281fdd volume: 122 year: '2025' ...