---
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'
...
---
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
_id: '19965'
abstract:
- lang: eng
text: Multiagent learning is challenging when agents face mixed-motivation interactions,
where conflicts of interest arise as agents independently try to optimize their
respective outcomes. Recent advancements in evolutionary game theory have identified
a class of “zero-determinant” strategies, which confer an agent with significant
unilateral control over outcomes in repeated games. Building on these insights,
we present a comprehensive generalization of zero-determinant strategies to stochastic
games, encompassing dynamic environments. We propose an algorithm that allows
an agent to discover strategies enforcing predetermined linear (or approximately
linear) payoff relationships. Of particular interest is the relationship in which
both payoffs are equal, which serves as a proxy for fairness in symmetric games.
We demonstrate that an agent can discover strategies enforcing such relationships
through experience alone, without coordinating with an opponent. In finding and
using such a strategy, an agent (“enforcer”) can incentivize optimal and equitable
outcomes, circumventing potential exploitation. In particular, from the opponent’s
viewpoint, the enforcer transforms a mixed-motivation problem into a cooperative
problem, paving the way for more collaboration and fairness in multiagent systems.
acknowledgement: 'We gratefully acknowledge the support from the European Research
Council (Starting Grant 850529: E-DIRECT) and the Max Planck Society (C.H.), the
European Research Council (Consolidator Grant 863818: ForM-SMArt) (K.C.), the Shanghai
Pujiang Program (No. 23PJ1405500) (Q.S.), the Army Research Office (Grant No. W911NF-18-1-0325)
(N.E.L.), and the John Templeton Foundation (Grant No. 62281) (J.B.P.).'
article_number: e2319927121
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Alex
full_name: Mcavoy, Alex
last_name: Mcavoy
- first_name: Udari Madhushani
full_name: Sehwag, Udari Madhushani
last_name: Sehwag
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfram
full_name: Barfuss, Wolfram
last_name: Barfuss
- first_name: Qi
full_name: Su, Qi
last_name: Su
- first_name: Naomi Ehrich
full_name: Leonard, Naomi Ehrich
last_name: Leonard
- first_name: Joshua B.
full_name: Plotkin, Joshua B.
last_name: Plotkin
citation:
ama: Mcavoy A, Sehwag UM, Hilbe C, et al. Unilateral incentive alignment in two-agent
stochastic games. Proceedings of the National Academy of Sciences. 2025;122(25).
doi:10.1073/pnas.2319927121
apa: Mcavoy, A., Sehwag, U. M., Hilbe, C., Chatterjee, K., Barfuss, W., Su, Q.,
… Plotkin, J. B. (2025). Unilateral incentive alignment in two-agent stochastic
games. Proceedings of the National Academy of Sciences. National Academy
of Sciences. https://doi.org/10.1073/pnas.2319927121
chicago: Mcavoy, Alex, Udari Madhushani Sehwag, Christian Hilbe, Krishnendu Chatterjee,
Wolfram Barfuss, Qi Su, Naomi Ehrich Leonard, and Joshua B. Plotkin. “Unilateral
Incentive Alignment in Two-Agent Stochastic Games.” Proceedings of the National
Academy of Sciences. National Academy of Sciences, 2025. https://doi.org/10.1073/pnas.2319927121.
ieee: A. Mcavoy et al., “Unilateral incentive alignment in two-agent stochastic
games,” Proceedings of the National Academy of Sciences, vol. 122, no.
25. National Academy of Sciences, 2025.
ista: Mcavoy A, Sehwag UM, Hilbe C, Chatterjee K, Barfuss W, Su Q, Leonard NE, Plotkin
JB. 2025. Unilateral incentive alignment in two-agent stochastic games. Proceedings
of the National Academy of Sciences. 122(25), e2319927121.
mla: Mcavoy, Alex, et al. “Unilateral Incentive Alignment in Two-Agent Stochastic
Games.” Proceedings of the National Academy of Sciences, vol. 122, no.
25, e2319927121, National Academy of Sciences, 2025, doi:10.1073/pnas.2319927121.
short: A. Mcavoy, U.M. Sehwag, C. Hilbe, K. Chatterjee, W. Barfuss, Q. Su, N.E.
Leonard, J.B. Plotkin, Proceedings of the National Academy of Sciences 122 (2025).
date_created: 2025-07-06T22:01:23Z
date_published: 2025-06-24T00:00:00Z
date_updated: 2025-09-30T13:47:14Z
day: '24'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1073/pnas.2319927121
ec_funded: 1
external_id:
isi:
- '001522351900001'
pmid:
- '40523172'
file:
- access_level: open_access
checksum: 3b35befd959a3e37aa9080a64a6afaf3
content_type: application/pdf
creator: dernst
date_created: 2025-07-08T05:52:26Z
date_updated: 2025-07-08T05:52:26Z
file_id: '19972'
file_name: 2025_PNAS_McAvoy.pdf
file_size: 29525932
relation: main_file
success: 1
file_date_updated: 2025-07-08T05:52:26Z
has_accepted_license: '1'
intvolume: ' 122'
isi: 1
issue: '25'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '06'
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'
scopus_import: '1'
status: public
title: Unilateral incentive alignment in two-agent stochastic games
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 122
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20053'
abstract:
- lang: eng
text: "Liquid democracy is a transitive vote delegation mechanism over voting graphs.
It enables each voter to delegate their vote(s) to another better-informed voter,
with the goal of collectively making a better decision. The question of whether
liquid democracy outperforms direct voting has been previously studied in the
context of local delegation mechanisms (where voters can only delegate to someone
in their neighbourhood) and binary decision problems. It has previously been shown
that it is impossible for local delegation mechanisms to outperform direct voting
in general graphs. This raises the question: for which classes of graphs do local
delegation mechanisms yield good results?\r\nIn this work, we analyse (1) properties
of specific graphs and (2) properties of local delegation mechanisms on these
graphs, determining where local delegation actually outperforms direct voting.
We show that a critical graph property enabling liquid democracy is that the voting
outcome of local delegation mechanisms preserves a sufficient amount of variance,
thereby avoiding situations where delegation falls behind direct voting1. These
insights allow us to prove our main results, namely that there exist local delegation
mechanisms that perform no worse and in fact quantitatively better than direct
voting in natural graph topologies like complete, random d-regular, and bounded
degree graphs, lending a more nuanced perspective to previous impossibility results."
acknowledgement: This work was partially supported by MOE-T2EP20122-0014 (DataDriven
Distributed Algorithms), German Research Foundation (DFG) project ReNO (SPP 2378)
from 2023-2027, ERC CoG 863818 (ForMSMArt) and Austrian Science Fund (FWF) 10.55776/COE12.
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: Seth
full_name: Gilbert, Seth
last_name: Gilbert
- 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, Gilbert S, Schmid S, Svoboda J, Yeo MX. When is liquid democracy
possible?: On the manipulation of variance. In: Proceedings of the ACM Symposium
on Principles of Distributed Computing. Association for Computing Machinery;
2025:241-251. doi:10.1145/3732772.3733544'
apa: 'Chatterjee, K., Gilbert, S., Schmid, S., Svoboda, J., & Yeo, M. X. (2025).
When is liquid democracy possible?: On the manipulation of variance. In Proceedings
of the ACM Symposium on Principles of Distributed Computing (pp. 241–251).
Huatulco, Mexico: Association for Computing Machinery. https://doi.org/10.1145/3732772.3733544'
chicago: 'Chatterjee, Krishnendu, Seth Gilbert, Stefan Schmid, Jakub Svoboda, and
Michelle X Yeo. “When Is Liquid Democracy Possible?: On the Manipulation of Variance.”
In Proceedings of the ACM Symposium on Principles of Distributed Computing,
241–51. Association for Computing Machinery, 2025. https://doi.org/10.1145/3732772.3733544.'
ieee: 'K. Chatterjee, S. Gilbert, S. Schmid, J. Svoboda, and M. X. Yeo, “When is
liquid democracy possible?: On the manipulation of variance,” in Proceedings
of the ACM Symposium on Principles of Distributed Computing, Huatulco, Mexico,
2025, pp. 241–251.'
ista: 'Chatterjee K, Gilbert S, Schmid S, Svoboda J, Yeo MX. 2025. When is liquid
democracy possible?: On the manipulation of variance. Proceedings of the ACM Symposium
on Principles of Distributed Computing. PODC: Symposium on Principles of Distributed
Computing, 241–251.'
mla: 'Chatterjee, Krishnendu, et al. “When Is Liquid Democracy Possible?: On the
Manipulation of Variance.” Proceedings of the ACM Symposium on Principles of
Distributed Computing, Association for Computing Machinery, 2025, pp. 241–51,
doi:10.1145/3732772.3733544.'
short: K. Chatterjee, S. Gilbert, S. Schmid, J. Svoboda, M.X. Yeo, in:, Proceedings
of the ACM Symposium on Principles of Distributed Computing, Association for Computing
Machinery, 2025, pp. 241–251.
conference:
end_date: 2025-06-20
location: Huatulco, Mexico
name: 'PODC: Symposium on Principles of Distributed Computing'
start_date: 2025-06-16
corr_author: '1'
date_created: 2025-07-21T08:18:26Z
date_published: 2025-06-13T00:00:00Z
date_updated: 2026-02-16T11:46:51Z
day: '13'
ddc:
- '000'
department:
- _id: KrCh
- _id: KrPi
doi: 10.1145/3732772.3733544
ec_funded: 1
external_id:
isi:
- '001525534800030'
file:
- access_level: open_access
checksum: cd628fe54d96e9fc6cc789bb8145422b
content_type: application/pdf
creator: dernst
date_created: 2025-08-05T07:15:31Z
date_updated: 2025-08-05T07:15:31Z
file_id: '20122'
file_name: 2025_PODC_Chatterjee.pdf
file_size: 783297
relation: main_file
success: 1
file_date_updated: 2025-08-05T07:15:31Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/745
month: '06'
oa: 1
oa_version: Published Version
page: 241-251
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 Symposium on Principles of Distributed Computing
publication_identifier:
isbn:
- '9798400718854'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
status: public
title: 'When is liquid democracy possible?: On the manipulation of variance'
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'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
PlanS_conform: '1'
_id: '20254'
abstract:
- lang: eng
text: 'We examine population structures for their ability to maintain diversity
in neutral evolution. We use the general framework of evolutionary graph theory
and consider birth–death (bd) and death–birth (db) updating. The population is
of size N. Initially all individuals represent different types. The basic question
is: what is the time TN until one type takes over the population? This time is
known as consensus time in computer science and as total coalescent time in evolutionary
biology. For the complete graph, it is known that TN is quadratic in N for db
and bd. For the cycle, we prove that TN is cubic in N for db and bd. For the star,
we prove that TN is cubic for bd and quasilinear (N log N) for db. For the double
star, we show that TN is quartic for bd. We derive upper and lower bounds for
all undirected graphs for bd and db. We also show the Pareto front of graphs (of
size N = 8) that maintain diversity the longest for bd and db. Further, we show
that some graphs that quickly homogenize can maintain high levels of diversity
longer than graphs that slowly homogenize. For directed graphs, we give simple
contracting star-like structures that have superexponential time scales for maintaining
diversity.'
acknowledgement: J.S. and K.C. were supported by the European Research Council CoG
863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12. J.T. was supported
by GAČR grant 25-17377S and by Charles Univ. projects UNCE 24/SCI/008 and PRIMUS
24/SCI/012.
article_number: pgaf252
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: David A.
full_name: Brewster, David A.
last_name: Brewster
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Dylan
full_name: Roscow, Dylan
last_name: Roscow
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Martin A.
full_name: Nowak, Martin A.
last_name: Nowak
citation:
ama: Brewster DA, Svoboda J, Roscow D, Chatterjee K, Tkadlec J, Nowak MA. Maintaining
diversity in structured populations. PNAS Nexus. 2025;4(8). doi:10.1093/pnasnexus/pgaf252
apa: Brewster, D. A., Svoboda, J., Roscow, D., Chatterjee, K., Tkadlec, J., &
Nowak, M. A. (2025). Maintaining diversity in structured populations. PNAS
Nexus. Oxford University Press. https://doi.org/10.1093/pnasnexus/pgaf252
chicago: Brewster, David A., Jakub Svoboda, Dylan Roscow, Krishnendu Chatterjee,
Josef Tkadlec, and Martin A. Nowak. “Maintaining Diversity in Structured Populations.”
PNAS Nexus. Oxford University Press, 2025. https://doi.org/10.1093/pnasnexus/pgaf252.
ieee: D. A. Brewster, J. Svoboda, D. Roscow, K. Chatterjee, J. Tkadlec, and M. A.
Nowak, “Maintaining diversity in structured populations,” PNAS Nexus, vol.
4, no. 8. Oxford University Press, 2025.
ista: Brewster DA, Svoboda J, Roscow D, Chatterjee K, Tkadlec J, Nowak MA. 2025.
Maintaining diversity in structured populations. PNAS Nexus. 4(8), pgaf252.
mla: Brewster, David A., et al. “Maintaining Diversity in Structured Populations.”
PNAS Nexus, vol. 4, no. 8, pgaf252, Oxford University Press, 2025, doi:10.1093/pnasnexus/pgaf252.
short: D.A. Brewster, J. Svoboda, D. Roscow, K. Chatterjee, J. Tkadlec, M.A. Nowak,
PNAS Nexus 4 (2025).
date_created: 2025-08-31T22:01:32Z
date_published: 2025-08-01T00:00:00Z
date_updated: 2026-02-16T12:23:19Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1093/pnasnexus/pgaf252
ec_funded: 1
external_id:
arxiv:
- '2503.09841'
file:
- access_level: open_access
checksum: 8a5e82c6f842e3220ec96028c9374b69
content_type: application/pdf
creator: dernst
date_created: 2025-09-03T06:20:08Z
date_updated: 2025-09-03T06:20:08Z
file_id: '20280'
file_name: 2025_PNASNexus_Brewster.pdf
file_size: 1086419
relation: main_file
success: 1
file_date_updated: 2025-09-03T06:20:08Z
has_accepted_license: '1'
intvolume: ' 4'
issue: '8'
language:
- iso: eng
month: '08'
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: PNAS Nexus
publication_identifier:
eissn:
- 2752-6542
publication_status: published
publisher: Oxford University Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Maintaining diversity in structured populations
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: publisher
OA_type: diamond
_id: '20297'
abstract:
- lang: eng
text: "A standard model that arises in several applications in sequential decision-making
is partially observable Markov decision processes (POMDPs) where a decision-making
agent interacts with an uncertain environment. A basic objective in POMDPs is
the reachability objective, where given a target set of states, the goal is to
eventually arrive at one of them.\r\n\r\nThe limit-sure problem asks whether reachability
can be ensured with probability arbitrarily close to 1. In general, the limit-sure
reachability problem for POMDPs is undecidable. However, in many practical cases,
the most relevant question is the existence of policies with a small amount of
memory. In this work, we study the limit-sure reachability problem for POMDPs
with a fixed amount of memory. We establish that the computational complexity
of the problem is NP-complete."
acknowledgement: This research was partially supported by Austrian Science Fund (FWF)
10.55776/COE12, the support of the French Agence Nationale de la Recherche (ANR)
under reference ANR-21-CE40-0020 (CONVERGENCE project), and the ERC CoG 863818 (ForM-SMArt)
grant.
alternative_title:
- PMLR
article_processing_charge: No
arxiv: 1
author:
- first_name: Ali
full_name: Asadi, Ali
id: 02d96aae-000e-11ec-b801-cadd0a5eefbb
last_name: Asadi
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Raimundo J
full_name: Saona Urmeneta, Raimundo J
id: BD1DF4C4-D767-11E9-B658-BC13E6697425
last_name: Saona Urmeneta
orcid: 0000-0001-5103-038X
- first_name: Ali
full_name: Shafiee, Ali
id: 2783031a-7378-11f0-b2d0-f17f1db2ebad
last_name: Shafiee
citation:
ama: 'Asadi A, Chatterjee K, Saona Urmeneta RJ, Shafiee A. Limit-sure reachability
for small memory policies in POMDPs is NP-complete. In: The 41st Conference
on Uncertainty in Artificial Intelligence. Vol 286. ML Research Press; 2025:238-247.'
apa: 'Asadi, A., Chatterjee, K., Saona Urmeneta, R. J., & Shafiee, A. (2025).
Limit-sure reachability for small memory policies in POMDPs is NP-complete. In
The 41st Conference on Uncertainty in Artificial Intelligence (Vol. 286,
pp. 238–247). Rio de Janeiro, Brazil: ML Research Press.'
chicago: Asadi, Ali, Krishnendu Chatterjee, Raimundo J Saona Urmeneta, and Ali Shafiee.
“Limit-Sure Reachability for Small Memory Policies in POMDPs Is NP-Complete.”
In The 41st Conference on Uncertainty in Artificial Intelligence, 286:238–47.
ML Research Press, 2025.
ieee: A. Asadi, K. Chatterjee, R. J. Saona Urmeneta, and A. Shafiee, “Limit-sure
reachability for small memory policies in POMDPs is NP-complete,” in The 41st
Conference on Uncertainty in Artificial Intelligence, Rio de Janeiro, Brazil,
2025, vol. 286, pp. 238–247.
ista: 'Asadi A, Chatterjee K, Saona Urmeneta RJ, Shafiee A. 2025. Limit-sure reachability
for small memory policies in POMDPs is NP-complete. The 41st Conference on Uncertainty
in Artificial Intelligence. UAI: Conference on Uncertainty in Artificial Intelligence,
PMLR, vol. 286, 238–247.'
mla: Asadi, Ali, et al. “Limit-Sure Reachability for Small Memory Policies in POMDPs
Is NP-Complete.” The 41st Conference on Uncertainty in Artificial Intelligence,
vol. 286, ML Research Press, 2025, pp. 238–47.
short: A. Asadi, K. Chatterjee, R.J. Saona Urmeneta, A. Shafiee, in:, The 41st Conference
on Uncertainty in Artificial Intelligence, ML Research Press, 2025, pp. 238–247.
conference:
end_date: 2025-07-25
location: Rio de Janeiro, Brazil
name: 'UAI: Conference on Uncertainty in Artificial Intelligence'
start_date: 2025-07-21
corr_author: '1'
date_created: 2025-09-07T22:01:34Z
date_published: 2025-07-01T00:00:00Z
date_updated: 2025-09-09T08:21:45Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
ec_funded: 1
external_id:
arxiv:
- '2412.00941'
file:
- access_level: open_access
checksum: 1a37ebe7ba73ab6985765bf0d17a0acc
content_type: application/pdf
creator: dernst
date_created: 2025-09-09T08:19:41Z
date_updated: 2025-09-09T08:19:41Z
file_id: '20315'
file_name: 2025_UAI_AsadiAli.pdf
file_size: 307458
relation: main_file
success: 1
file_date_updated: 2025-09-09T08:19:41Z
has_accepted_license: '1'
intvolume: ' 286'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 238-247
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: The 41st Conference on Uncertainty in Artificial Intelligence
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Limit-sure reachability for small memory policies in POMDPs is NP-complete
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: 286
year: '2025'
...
---
OA_place: publisher
OA_type: diamond
_id: '20299'
abstract:
- lang: eng
text: "Deterministic Markov Decision Processes (DMDPs) are a mathematical framework
for decision-making where the outcomes and future possible actions are deterministically
determined by the current action taken. DMDPs can be viewed as a finite directed
weighted graph, where in each step, the controller chooses an outgoing edge. An
objective is a measurable function on runs (or infinite trajectories) of the DMDP,
and the value for an objective is the maximal cumulative reward (or weight) that
the controller can guarantee. We consider the classical mean-payoff (aka limit-average)
objective, which is a basic and fundamental objective.\r\n\r\nHoward's policy
iteration algorithm is a popular method for solving DMDPs with mean-payoff objectives.
Although Howard's algorithm performs well in practice, as experimental studies
suggested, the best known upper bound is exponential and the current known lower
bound is as follows: For the input size I, the algorithm requires (math formular)
iterations, where (math formular) hides the poly-logarithmic factors, i.e., the
current lower bound on iterations is sub-linear with respect to the input size.
Our main result is an improved lower bound for this fundamental algorithm where
we show that for the input size I, the algorithm requires (math formular) iterations."
acknowledgement: "This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant and Austrian Science Fund (FWF) 10.55776/COE12.\r\n"
alternative_title:
- PMLR
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: Jakob
full_name: De Raaij, Jakob
last_name: De Raaij
citation:
ama: 'Asadi A, Chatterjee K, De Raaij J. Lower bound on Howard policy iteration
for deterministic Markov Decision Processes. In: The 41st Conference on Uncertainty
in Artificial Intelligence. Vol 286. ML Research Press; 2025:223-232.'
apa: 'Asadi, A., Chatterjee, K., & De Raaij, J. (2025). Lower bound on Howard
policy iteration for deterministic Markov Decision Processes. In The 41st Conference
on Uncertainty in Artificial Intelligence (Vol. 286, pp. 223–232). Rio de
Janeiro, Brazil: ML Research Press.'
chicago: Asadi, Ali, Krishnendu Chatterjee, and Jakob De Raaij. “Lower Bound on
Howard Policy Iteration for Deterministic Markov Decision Processes.” In The
41st Conference on Uncertainty in Artificial Intelligence, 286:223–32. ML
Research Press, 2025.
ieee: A. Asadi, K. Chatterjee, and J. De Raaij, “Lower bound on Howard policy iteration
for deterministic Markov Decision Processes,” in The 41st Conference on Uncertainty
in Artificial Intelligence, Rio de Janeiro, Brazil, 2025, vol. 286, pp. 223–232.
ista: 'Asadi A, Chatterjee K, De Raaij J. 2025. Lower bound on Howard policy iteration
for deterministic Markov Decision Processes. The 41st Conference on Uncertainty
in Artificial Intelligence. UAI: Conference on Uncertainty in Artificial Intelligence,
PMLR, vol. 286, 223–232.'
mla: Asadi, Ali, et al. “Lower Bound on Howard Policy Iteration for Deterministic
Markov Decision Processes.” The 41st Conference on Uncertainty in Artificial
Intelligence, vol. 286, ML Research Press, 2025, pp. 223–32.
short: A. Asadi, K. Chatterjee, J. De Raaij, in:, The 41st Conference on Uncertainty
in Artificial Intelligence, ML Research Press, 2025, pp. 223–232.
conference:
end_date: 2025-07-25
location: Rio de Janeiro, Brazil
name: 'UAI: Conference on Uncertainty in Artificial Intelligence'
start_date: 2025-07-21
corr_author: '1'
date_created: 2025-09-07T22:01:34Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2025-09-09T06:31:20Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
ec_funded: 1
external_id:
arxiv:
- '2506.12254'
file:
- access_level: open_access
checksum: 4180c81bb6ed3b4f5c7a8e48d06520c6
content_type: application/pdf
creator: dernst
date_created: 2025-09-09T06:27:59Z
date_updated: 2025-09-09T06:27:59Z
file_id: '20313'
file_name: 2025_UAI_Asadi.pdf
file_size: 317097
relation: main_file
success: 1
file_date_updated: 2025-09-09T06:27:59Z
has_accepted_license: '1'
intvolume: ' 286'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 223-232
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: The 41st Conference on Uncertainty in Artificial Intelligence
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Lower bound on Howard policy iteration for deterministic 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: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 286
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20302'
abstract:
- lang: eng
text: "LocalSGD and SCAFFOLD are widely used methods in distributed stochastic optimization,
with numerous applications in machine learning, large-scale data processing, and
federated learning. However, rigorously establishing their theoretical advantages
over simpler methods, such as minibatch SGD (MbSGD), has proven challenging, as
existing analyses often rely on strong assumptions, unrealistic premises, or overly
restrictive scenarios.\r\n\r\nIn this work, we revisit the convergence properties
of LocalSGD and SCAFFOLD under a variety of existing or weaker conditions, including
gradient similarity, Hessian similarity, weak convexity, and Lipschitz continuity
of the Hessian. Our analysis shows that (i) LocalSGD achieves faster convergence
compared to MbSGD for weakly convex functions without requiring stronger gradient
similarity assumptions; (ii) LocalSGD benefits significantly from higher-order
similarity and smoothness; and (iii) SCAFFOLD demonstrates faster convergence
than MbSGD for a broader class of non-quadratic functions. These theoretical insights
provide a clearer understanding of the conditions under which LocalSGD and SCAFFOLD
outperform MbSGD."
acknowledgement: "The authors thank for the helpful discussions with Eduard Gorbunov,
Kumar Kshitij Patel, Anton\r\nRodomanov, and Ali Zindari during the preparation
of this work. This work was partially done during the first author’s stays at CISPA
and at MBZUAI. The first author also acknowledges ERC CoG 863818 (ForM-SMArt) and
Austrian Science Fund (FWF) 10.55776/COE12."
alternative_title:
- PMLR
article_processing_charge: No
arxiv: 1
author:
- first_name: Ruichen
full_name: Luo, Ruichen
id: b391db08-1ffe-11ee-8b67-d18ddcfb5a14
last_name: Luo
- first_name: Sebastian U.
full_name: Stich, Sebastian U.
last_name: Stich
- first_name: Samuel
full_name: Horváth, Samuel
last_name: Horváth
- first_name: Martin
full_name: Takáč, Martin
last_name: Takáč
citation:
ama: 'Luo R, Stich SU, Horváth S, Takáč M. Revisiting LocalSGD and SCAFFOLD: Improved
rates and missing analysis. In: The 28th International Conference on Artificial
Intelligence and Statistics. Vol 258. ML Research Press; 2025:2539-2547.'
apa: 'Luo, R., Stich, S. U., Horváth, S., & Takáč, M. (2025). Revisiting LocalSGD
and SCAFFOLD: Improved rates and missing analysis. In The 28th International
Conference on Artificial Intelligence and Statistics (Vol. 258, pp. 2539–2547).
Mai Khao, Thailand: ML Research Press.'
chicago: 'Luo, Ruichen, Sebastian U. Stich, Samuel Horváth, and Martin Takáč. “Revisiting
LocalSGD and SCAFFOLD: Improved Rates and Missing Analysis.” In The 28th International
Conference on Artificial Intelligence and Statistics, 258:2539–47. ML Research
Press, 2025.'
ieee: 'R. Luo, S. U. Stich, S. Horváth, and M. Takáč, “Revisiting LocalSGD and SCAFFOLD:
Improved rates and missing analysis,” in The 28th International Conference
on Artificial Intelligence and Statistics, Mai Khao, Thailand, 2025, vol.
258, pp. 2539–2547.'
ista: 'Luo R, Stich SU, Horváth S, Takáč M. 2025. Revisiting LocalSGD and SCAFFOLD:
Improved rates and missing analysis. The 28th International Conference on Artificial
Intelligence and Statistics. AISTATS: Conference on Artificial Intelligence and
Statistics, PMLR, vol. 258, 2539–2547.'
mla: 'Luo, Ruichen, et al. “Revisiting LocalSGD and SCAFFOLD: Improved Rates and
Missing Analysis.” The 28th International Conference on Artificial Intelligence
and Statistics, vol. 258, ML Research Press, 2025, pp. 2539–47.'
short: R. Luo, S.U. Stich, S. Horváth, M. Takáč, in:, The 28th International Conference
on Artificial Intelligence and Statistics, ML Research Press, 2025, pp. 2539–2547.
conference:
end_date: 2025-05-05
location: Mai Khao, Thailand
name: 'AISTATS: Conference on Artificial Intelligence and Statistics'
start_date: 2025-05-03
date_created: 2025-09-07T22:01:35Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-09-09T07:17:08Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '2501.04443'
intvolume: ' 258'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2501.04443
month: '05'
oa: 1
oa_version: Preprint
page: 2539-2547
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: The 28th International Conference on Artificial Intelligence and Statistics
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 258
year: '2025'
...
---
_id: '20610'
abstract:
- lang: eng
text: "Markov decision processes (MDPs) are a fundamental model of decision making
which exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally,
verification assumes exact knowledge of the probabilities that govern the behaviour
of an MDP. However, this assumption often is unrealistic, e.g. when modelling
cyber-physical systems or biological processes. There, we can employ statistical
model checking (SMC) to obtain an estimate of the MDP’s value (e.g. the maximal
probability of reaching a goal state) that is close to the true value with high
confidence (probably approximately correct). Model-based SMC algorithms sample
the MDP and build a model of it by estimating all transition probabilities, essentially
for every transition answering the question: “What are the odds?” However, so
far the statistical methods employed by state-of-the-art SMC verification algorithms
are quite naive or even compromise the correctness guarantees.\r\n\r\nOur first
contribution is to survey, categorize, and analyse statistical methods, identifying
those few that are most efficient and that provide suitable guarantees for the
verification setting. Secondly, we propose improvements that exploit structural
knowledge of the MDP. Both contributions generalize to many types of problem statements
as they are largely independent of the setting. Moreover, our experimental evaluation
shows that they lead to significant gains, reducing the number of samples that
an SMC algorithm has to collect by up to two orders of magnitude."
acknowledgement: This work was supported by the European Union’s Horizon 2020 research
and innovation programme under the Marie Sklodowska-Curie grant agreement No 10103441,
the ERC Starting Grant DEUCE (101077178) and the DFG through the Cluster of Excellence
EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy)
and the DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
- first_name: Patrick
full_name: Wienhöft, Patrick
last_name: Wienhöft
citation:
ama: 'Meggendorfer T, Weininger M, Wienhöft P. What are the odds? Improving statistical
model checking of Markov decision processes. In: Second International Joint
Conference on QEST+FORMATS. Vol 16143. Springer Nature; 2025:195-218. doi:10.1007/978-3-032-05792-1_11'
apa: 'Meggendorfer, T., Weininger, M., & Wienhöft, P. (2025). What are the odds?
Improving statistical model checking of Markov decision processes. In Second
International Joint Conference on QEST+FORMATS (Vol. 16143, pp. 195–218).
Aarhus, Denmark: Springer Nature. https://doi.org/10.1007/978-3-032-05792-1_11'
chicago: Meggendorfer, Tobias, Maximilian Weininger, and Patrick Wienhöft. “What
Are the Odds? Improving Statistical Model Checking of Markov Decision Processes.”
In Second International Joint Conference on QEST+FORMATS, 16143:195–218.
Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05792-1_11.
ieee: T. Meggendorfer, M. Weininger, and P. Wienhöft, “What are the odds? Improving
statistical model checking of Markov decision processes,” in Second International
Joint Conference on QEST+FORMATS, Aarhus, Denmark, 2025, vol. 16143, pp. 195–218.
ista: 'Meggendorfer T, Weininger M, Wienhöft P. 2025. What are the odds? Improving
statistical model checking of Markov decision processes. Second International
Joint Conference on QEST+FORMATS. QEST-FORMATS: International Conference on Quantitative
Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, LNCS,
vol. 16143, 195–218.'
mla: Meggendorfer, Tobias, et al. “What Are the Odds? Improving Statistical Model
Checking of Markov Decision Processes.” Second International Joint Conference
on QEST+FORMATS, vol. 16143, Springer Nature, 2025, pp. 195–218, doi:10.1007/978-3-032-05792-1_11.
short: T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Second International Joint
Conference on QEST+FORMATS, Springer Nature, 2025, pp. 195–218.
conference:
end_date: 2025-08-28
location: Aarhus, Denmark
name: 'QEST-FORMATS: International Conference on Quantitative Evaluation of Systems
and Formal Modeling and Analysis of Timed Systems'
start_date: 2025-08-26
date_created: 2025-11-09T23:01:34Z
date_published: 2025-10-02T00:00:00Z
date_updated: 2025-11-10T08:06:27Z
day: '02'
department:
- _id: KrCh
doi: 10.1007/978-3-032-05792-1_11
ec_funded: 1
intvolume: ' 16143'
language:
- iso: eng
month: '10'
oa_version: None
page: 195-218
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Second International Joint Conference on QEST+FORMATS
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032057914'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: What are the odds? Improving statistical model checking of Markov decision
processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16143
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20648'
abstract:
- lang: eng
text: Polynomial quantified entailments with existentially and universally quantified
variables arise in many problems of verification and program analysis. We present
PolyQEnt which is a tool for solving polynomial quantified entailments in which
variables on both sides of the implication are real valued or unbounded integers.
Our tool provides a unified framework for polynomial quantified entailment problems
that arise in several papers in the literature. Our experimental evaluation over
a wide range of benchmarks shows the applicability of the tool as well as its
benefits as opposed to simply using existing SMT solvers to solve such constraints.
acknowledgement: 'This work was supported by the following grants: ERC CoG 863818
(ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, ERC StG 101222524 (SPES),
the Ethereum Foundation Research Grant FY24-1793, and the Singapore Ministry of
Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SISSMU-100).'
alternative_title:
- LNCS
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: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Ehsan
full_name: 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: Milad
full_name: Saadat, Milad
last_name: Saadat
- first_name: Maximilian
full_name: Seeliger, Maximilian
last_name: Seeliger
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady AK, Goharshady E, et al. PolyQEnt: A polynomial quantified
entailment solver. In: 23rd International Symposium on Automated Technology
for Verification and Analysis. Vol 16145. Springer Nature; 2025:411-424. doi:10.1007/978-3-032-08707-2_19'
apa: 'Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., Saadat, M.,
Seeliger, M., & Zikelic, D. (2025). PolyQEnt: A polynomial quantified entailment
solver. In 23rd International Symposium on Automated Technology for Verification
and Analysis (Vol. 16145, pp. 411–424). Bengaluru, India: Springer Nature.
https://doi.org/10.1007/978-3-032-08707-2_19'
chicago: 'Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad
Karrabi, Milad Saadat, Maximilian Seeliger, and Dorde Zikelic. “PolyQEnt: A Polynomial
Quantified Entailment Solver.” In 23rd International Symposium on Automated
Technology for Verification and Analysis, 16145:411–24. Springer Nature, 2025.
https://doi.org/10.1007/978-3-032-08707-2_19.'
ieee: 'K. Chatterjee et al., “PolyQEnt: A polynomial quantified entailment
solver,” in 23rd International Symposium on Automated Technology for Verification
and Analysis, Bengaluru, India, 2025, vol. 16145, pp. 411–424.'
ista: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger
M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd
International Symposium on Automated Technology for Verification and Analysis.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424.'
mla: 'Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment
Solver.” 23rd International Symposium on Automated Technology for Verification
and Analysis, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:10.1007/978-3-032-08707-2_19.'
short: K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, M. Saadat, M.
Seeliger, D. Zikelic, in:, 23rd International Symposium on Automated Technology
for Verification and Analysis, Springer Nature, 2025, pp. 411–424.
conference:
end_date: 2025-10-31
location: Bengaluru, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2025-10-27
corr_author: '1'
date_created: 2025-11-16T23:01:24Z
date_published: 2025-10-26T00:00:00Z
date_updated: 2025-11-24T13:11:10Z
day: '26'
department:
- _id: KrCh
doi: 10.1007/978-3-032-08707-2_19
ec_funded: 1
external_id:
arxiv:
- '2408.03796'
intvolume: ' 16145'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2408.03796
month: '10'
oa: 1
oa_version: Preprint
page: 411-424
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 23rd International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032087065'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'PolyQEnt: A polynomial quantified entailment solver'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16145
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20688'
abstract:
- lang: eng
text: 'We consider two-player zero-sum concurrent stochastic games (CSGs) played
on graphs with reachability and safety objectives. These include degenerate classes
such as Markov decision processes or turn-based stochastic games, which can be
solved by linear or quadratic programming; however, in practice, value iteration
(VI) outperforms the other approaches and is the most implemented method. Similarly,
for CSGs, this practical performance makes VI an attractive alternative to the
standard theoretical solution via the existential theory of reals.VI starts with
an under-approximation of the sought values for each state and iteratively updates
them, traditionally terminating once two consecutive approximations are ϵ-close.
However, this stopping criterion lacks guarantees on the precision of the approximation,
which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs:
it complements standard VI with a converging sequence of over-approximations and
terminates once the over- and under-approximations are ϵ-close.'
acknowledgement: This research was funded in part by the German Research Foundation
(DFG) project 427755713 GOPro, the MUNI Award in Science and Humanities (MUNI/I/1757/2021)
of the Grant Agency of Masaryk University, the European Union’s Horizon 2020 research
and innovation programme under the Marie Sklodowska-Curie grant agreement No 101034413,
and the ERC Starting Grant DEUCE (101077178).
article_processing_charge: No
arxiv: 1
author:
- first_name: Marta
full_name: Grobelna, Marta
last_name: Grobelna
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
citation:
ama: 'Grobelna M, Kretinsky J, Weininger M. Stopping criteria for value iteration
on concurrent stochastic reachability and safety games. In: 2025 40th Annual
ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2025:568-580. doi:10.1109/lics65433.2025.00049'
apa: 'Grobelna, M., Kretinsky, J., & Weininger, M. (2025). Stopping criteria
for value iteration on concurrent stochastic reachability and safety games. In
2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 568–580).
Singapore, Singapore: IEEE. https://doi.org/10.1109/lics65433.2025.00049'
chicago: Grobelna, Marta, Jan Kretinsky, and Maximilian Weininger. “Stopping Criteria
for Value Iteration on Concurrent Stochastic Reachability and Safety Games.” In
2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, 568–80.
IEEE, 2025. https://doi.org/10.1109/lics65433.2025.00049.
ieee: M. Grobelna, J. Kretinsky, and M. Weininger, “Stopping criteria for value
iteration on concurrent stochastic reachability and safety games,” in 2025
40th Annual ACM/IEEE Symposium on Logic in Computer Science, Singapore, Singapore,
2025, pp. 568–580.
ista: 'Grobelna M, Kretinsky J, Weininger M. 2025. Stopping criteria for value iteration
on concurrent stochastic reachability and safety games. 2025 40th Annual ACM/IEEE
Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 568–580.'
mla: Grobelna, Marta, et al. “Stopping Criteria for Value Iteration on Concurrent
Stochastic Reachability and Safety Games.” 2025 40th Annual ACM/IEEE Symposium
on Logic in Computer Science, IEEE, 2025, pp. 568–80, doi:10.1109/lics65433.2025.00049.
short: M. Grobelna, J. Kretinsky, M. Weininger, in:, 2025 40th Annual ACM/IEEE Symposium
on Logic in Computer Science, IEEE, 2025, pp. 568–580.
conference:
end_date: 2025-06-26
location: Singapore, Singapore
name: 'LICS: Logic in Computer Science'
start_date: 2025-06-23
corr_author: '1'
date_created: 2025-11-24T14:23:49Z
date_published: 2025-10-09T00:00:00Z
date_updated: 2025-11-26T07:34:19Z
day: '09'
department:
- _id: KrCh
doi: 10.1109/lics65433.2025.00049
ec_funded: 1
external_id:
arxiv:
- '2505.21087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2505.21087
month: '10'
oa: 1
oa_version: Preprint
page: 568-580
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
eisbn:
- '9798331579005'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stopping criteria for value iteration on concurrent stochastic reachability
and safety games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20689'
abstract:
- lang: eng
text: This paper studies the expected value of multiplicative rewards, where rewards
obtained in each step are multiplied (instead of the usual addition), in Markov
chains (MCs) and Markov decision processes (MDPs). One of the key differences
to additive rewards is that the expected value may diverge to ∞ not only due to
recurrent, but also due to transient states.For MCs, computing the value is shown
to be possible in polynomial time given an oracle for the comparison of succinctly
represented integers (CSRI), which is only known to be solvable in polynomial
time subject to number-theoretic conjectures. Interestingly, distinguishing whether
the value is ∞ or 0 is at least as hard as CSRI, while determining if it is one
of these two can be done in polynomial time. In MDPs, the optimal value can be
computed in polynomial space. Further refined complexity results and results on
the complexity of optimal schedulers are presented. The techniques developed for
MDPs additionally allow to solve the multiplicative variant of the stochastic
shortest path problem. Finally, for MCs and MDPs where an absorbing state is reached
almost surely, all considered problems are solvable in polynomial time.
acknowledgement: "This work was partly funded by the ERC CoG 863818 (ForM-SMArt),
the Austrian Science Fund (FWF) 10.55776/COE12, the DFG Grant 389792660 as part
of TRR 248 (Foundations of Perspicuous Software Systems), the Cluster of Excellence
EXC 2050/1 (CeTI, project ID\r\n390696704, as part of Germany’s Excellence Strategy),
and by the BMBF (Federal Ministry of Education and Research) in DAAD project 57616814
(SECAI, School of Embedded and\r\nComposite AI) as part of the program Konrad Zuse
Schools of Excellence in Artificial Intelligence."
article_processing_charge: No
arxiv: 1
author:
- first_name: Christel
full_name: Baier, Christel
last_name: Baier
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Jakob
full_name: Piribauer, Jakob
last_name: Piribauer
citation:
ama: 'Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Multiplicative rewards
in Markovian models. In: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer
Science. IEEE; 2025:499-512. doi:10.1109/lics65433.2025.00044'
apa: 'Baier, C., Chatterjee, K., Meggendorfer, T., & Piribauer, J. (2025). Multiplicative
rewards in Markovian models. In 2025 40th Annual ACM/IEEE Symposium on Logic
in Computer Science (pp. 499–512). Singapore, Singapore: IEEE. https://doi.org/10.1109/lics65433.2025.00044'
chicago: Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob
Piribauer. “Multiplicative Rewards in Markovian Models.” In 2025 40th Annual
ACM/IEEE Symposium on Logic in Computer Science, 499–512. IEEE, 2025. https://doi.org/10.1109/lics65433.2025.00044.
ieee: C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Multiplicative
rewards in Markovian models,” in 2025 40th Annual ACM/IEEE Symposium on Logic
in Computer Science, Singapore, Singapore, 2025, pp. 499–512.
ista: 'Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2025. Multiplicative
rewards in Markovian models. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer
Science. LICS: Logic in Computer Science, 499–512.'
mla: Baier, Christel, et al. “Multiplicative Rewards in Markovian Models.” 2025
40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp.
499–512, doi:10.1109/lics65433.2025.00044.
short: C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, in:, 2025 40th Annual
ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp. 499–512.
conference:
end_date: 2025-06-26
location: Singapore, Singapore
name: 'LICS: Logic in Computer Science'
start_date: 2025-06-23
corr_author: '1'
date_created: 2025-11-24T14:24:00Z
date_published: 2025-10-09T00:00:00Z
date_updated: 2025-11-25T07:59:25Z
day: '09'
department:
- _id: KrCh
doi: 10.1109/lics65433.2025.00044
ec_funded: 1
external_id:
arxiv:
- '2504.18277'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2504.18277
month: '10'
oa: 1
oa_version: Preprint
page: 499-512
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
eisbn:
- '9798331579005'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Multiplicative rewards in Markovian models
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20690'
abstract:
- lang: eng
text: 'Cumulative prospect theory (CPT) is the first theory for decision-making
under uncertainty that combines full theoretical soundness and empirically realistic
features [1], [Page 2]. While CPT was originally considered in one-shot settings
for risk-aware decision-making, we consider CPT in sequential decision-making.
The most fundamental and well-studied models for sequential decision-making are
Markov chains (MCs), and their generalization Markov decision processes (MDPs).
The complexity theoretic study of MCs and MDPs with CPT is a fundamental problem
that has not been addressed in the literature.Our contributions are as follows:
First, we present an alternative viewpoint for the CPT-value of MCs and MDPs.
This allows us to establish a connection with multi-objective reachability analysis
and conclude the strategy complexity result that memoryless randomized strategies
are necessary and sufficient for optimality. Second, based on this connection,
we provide an algorithm for computing the CPT-value in MDPs with infinite-horizon
objectives. We show that the problem is in EXPTIME and fixed-parameter tractable.
Moreover, we provide a polynomial-time algorithm for the special case of MCs.'
acknowledgement: "This project has received funding from the Fonds de la Recherche
Scientifique - FNRS under grant No. T.0027.21, the Belgian National Lottery; the
ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12; the
DFG project 427755713, GOPro, and the DFG research training group GRK 2428 Continuous
Verification of Cyber-Physical Systems\r\n(ConVeY); the EU’s Horizon 2020 research
and innovation programmes under the Marie Sklodowska-Curie grant agreement No. 101034413
(IST-BRIDGE) and the ERC Starting Grant DEUCE (101077178)."
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas
full_name: Brihaye, Thomas
last_name: Brihaye
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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
orcid: 0000-0002-0163-2152
citation:
ama: 'Brihaye T, Chatterjee K, Mohr S, Weininger M. Risk-aware Markov decision processes
using cumulative prospect theory. In: 2025 40th Annual ACM/IEEE Symposium on
Logic in Computer Science. IEEE; 2025:458-471. doi:10.1109/lics65433.2025.00041'
apa: 'Brihaye, T., Chatterjee, K., Mohr, S., & Weininger, M. (2025). Risk-aware
Markov decision processes using cumulative prospect theory. In 2025 40th Annual
ACM/IEEE Symposium on Logic in Computer Science (pp. 458–471). Singapore,
Singapore: IEEE. https://doi.org/10.1109/lics65433.2025.00041'
chicago: Brihaye, Thomas, Krishnendu Chatterjee, Stefanie Mohr, and Maximilian Weininger.
“Risk-Aware Markov Decision Processes Using Cumulative Prospect Theory.” In 2025
40th Annual ACM/IEEE Symposium on Logic in Computer Science, 458–71. IEEE,
2025. https://doi.org/10.1109/lics65433.2025.00041.
ieee: T. Brihaye, K. Chatterjee, S. Mohr, and M. Weininger, “Risk-aware Markov decision
processes using cumulative prospect theory,” in 2025 40th Annual ACM/IEEE Symposium
on Logic in Computer Science, Singapore, Singapore, 2025, pp. 458–471.
ista: 'Brihaye T, Chatterjee K, Mohr S, Weininger M. 2025. Risk-aware Markov decision
processes using cumulative prospect theory. 2025 40th Annual ACM/IEEE Symposium
on Logic in Computer Science. LICS: Logic in Computer Science, 458–471.'
mla: Brihaye, Thomas, et al. “Risk-Aware Markov Decision Processes Using Cumulative
Prospect Theory.” 2025 40th Annual ACM/IEEE Symposium on Logic in Computer
Science, IEEE, 2025, pp. 458–71, doi:10.1109/lics65433.2025.00041.
short: T. Brihaye, K. Chatterjee, S. Mohr, M. Weininger, in:, 2025 40th Annual ACM/IEEE
Symposium on Logic in Computer Science, IEEE, 2025, pp. 458–471.
conference:
end_date: 2025-06-26
location: Singapore, Singapore
name: 'LICS: Logic in Computer Science'
start_date: 2025-06-23
corr_author: '1'
date_created: 2025-11-24T14:43:47Z
date_published: 2025-10-09T00:00:00Z
date_updated: 2025-11-25T07:59:49Z
day: '09'
department:
- _id: KrCh
doi: 10.1109/lics65433.2025.00041
ec_funded: 1
external_id:
arxiv:
- '2505.09514'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2505.09514
month: '10'
oa: 1
oa_version: Preprint
page: 458-471
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
eisbn:
- '9798331579005'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Risk-aware Markov decision processes using cumulative prospect theory
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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: repository
OA_type: green
_id: '19600'
abstract:
- lang: eng
text: In this work, we explore route discovery in private payment channel networks.
We first determine what “ideal" privacy for a routing protocol means in this setting.
We observe that protocols achieving this strong privacy definition exist by leveraging
Multi-Party Computation but they are inherently inefficient as they must involve
the entire network. We then present protocols with weaker privacy guarantees but
much better efficiency (involving only a small fraction of the nodes). The core
idea is that both sender and receiver gossip a message which propagates through
the network, and the moment any node in the network receives both messages, a
path is found. In our first protocol the message is always sent to all neighbouring
nodes with a delay proportional to the fees of that edge. In our second protocol
the message is only sent to one neighbour chosen randomly with a probability proportional
to its degree. We additionally propose a more realistic notion of privacy in order
to measure the privacy leakage of our protocols in practice. Our realistic notion
of privacy challenges an adversary that join the network with a fixed budget to
create channels to guess the sender and receiver of a transaction upon receiving
messages from our protocols. Simulations of our protocols on the Lightning network
topology (for random transactions and uniform fees) show that 1) forming edges
with high degree nodes is a more effective attack strategy for the adversary,
2) there is a tradeoff between the number of nodes involved in our protocols (privacy)
and the optimality of the discovered path, and 3) our protocols involve a very
small fraction of the network on average.
acknowledgement: This work was supported in part by the ERC CoG 863818 (ForM-SMArt),
Austrian Science Fund (FWF) 10.55776/COE12, and MOE-T2EP20122-0014 (Data-Driven
Distributed Algorithms) grants.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Zeta
full_name: Avarikioti, Zeta
last_name: Avarikioti
- first_name: Mahsa
full_name: Bastankhah, Mahsa
last_name: Bastankhah
- first_name: Mohammad Ali
full_name: Maddah-Ali, Mohammad Ali
last_name: Maddah-Ali
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
- first_name: 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: 'Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX.
Route discovery in private payment channel networks. In: Computer Security.
ESORICS 2024 International Workshops. Vol 15263. Springer Nature; 2025:207-223.
doi:10.1007/978-3-031-82349-7_15'
apa: 'Avarikioti, Z., Bastankhah, M., Maddah-Ali, M. A., Pietrzak, K. Z., Svoboda,
J., & Yeo, M. X. (2025). Route discovery in private payment channel networks.
In Computer Security. ESORICS 2024 International Workshops (Vol. 15263,
pp. 207–223). Bydgoszcz, Poland: Springer Nature. https://doi.org/10.1007/978-3-031-82349-7_15'
chicago: Avarikioti, Zeta, Mahsa Bastankhah, Mohammad Ali Maddah-Ali, Krzysztof
Z Pietrzak, Jakub Svoboda, and Michelle X Yeo. “Route Discovery in Private Payment
Channel Networks.” In Computer Security. ESORICS 2024 International Workshops,
15263:207–23. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-82349-7_15.
ieee: Z. Avarikioti, M. Bastankhah, M. A. Maddah-Ali, K. Z. Pietrzak, J. Svoboda,
and M. X. Yeo, “Route discovery in private payment channel networks,” in Computer
Security. ESORICS 2024 International Workshops, Bydgoszcz, Poland, 2025, vol.
15263, pp. 207–223.
ista: 'Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX.
2025. Route discovery in private payment channel networks. Computer Security.
ESORICS 2024 International Workshops. ESORICS: European Symposium on Research
in Computer Security, LNCS, vol. 15263, 207–223.'
mla: Avarikioti, Zeta, et al. “Route Discovery in Private Payment Channel Networks.”
Computer Security. ESORICS 2024 International Workshops, vol. 15263, Springer
Nature, 2025, pp. 207–23, doi:10.1007/978-3-031-82349-7_15.
short: Z. Avarikioti, M. Bastankhah, M.A. Maddah-Ali, K.Z. Pietrzak, J. Svoboda,
M.X. Yeo, in:, Computer Security. ESORICS 2024 International Workshops, Springer
Nature, 2025, pp. 207–223.
conference:
end_date: 2024-09-20
location: Bydgoszcz, Poland
name: 'ESORICS: European Symposium on Research in Computer Security'
start_date: 2024-09-16
date_created: 2025-04-20T22:01:28Z
date_published: 2025-04-01T00:00:00Z
date_updated: 2025-11-05T07:52:35Z
day: '01'
department:
- _id: KrPi
- _id: KrCh
doi: 10.1007/978-3-031-82349-7_15
ec_funded: 1
intvolume: ' 15263'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2021/1539
month: '04'
oa: 1
oa_version: Submitted Version
page: 207-223
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Computer Security. ESORICS 2024 International Workshops
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031823480'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Route discovery in private payment channel networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15263
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19666'
abstract:
- lang: eng
text: Markov decision processes (MDP) are a well-established model for sequential
decision-making in the presence of probabilities. In *robust* MDP (RMDP), every
action is associated with an *uncertainty set* of probability distributions, modelling
that transition probabilities are not known precisely. Based on the known theoretical
connection to stochastic games, we provide a framework for solving RMDPs that
is generic, reliable, and efficient. It is *generic* both with respect to the
model, allowing for a wide range of uncertainty sets, including but not limited
to intervals, L1- or L2-balls, and polytopes; and with respect to the objective,
including long-run average reward, undiscounted total reward, and stochastic shortest
path. It is *reliable*, as our approach not only converges in the limit, but provides
precision guarantees at any time during the computation. It is *efficient* because
-- in contrast to state-of-the-art approaches -- it avoids explicitly constructing
the underlying stochastic game. Consequently, our prototype implementation outperforms
existing tools by several orders of magnitude and can solve RMDPs with a million
states in under a minute.
acknowledgement: "This project has received funding from the European Union’s Horizon
2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement
No. 101034413,\r\nthe ERC CoG 863818 (ForM-SMArt), and the DFG through the Cluster
of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence
Strategy) and the TRR 248 (see https://perspicuous-computing.science, project ID
389792660)."
article_processing_charge: No
arxiv: 1
author:
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
- first_name: Patrick
full_name: Wienhöft, Patrick
last_name: Wienhöft
citation:
ama: 'Meggendorfer T, Weininger M, Wienhöft P. Solving robust Markov decision processes:
Generic, reliable, efficient. In: Proceedings of the 39th AAAI Conference on
Artificial Intelligence. Vol 39. Association for the Advancement of Artificial
Intelligence; 2025:26631-26641. doi:10.1609/aaai.v39i25.34865'
apa: 'Meggendorfer, T., Weininger, M., & Wienhöft, P. (2025). Solving robust
Markov decision processes: Generic, reliable, efficient. In Proceedings of
the 39th AAAI Conference on Artificial Intelligence (Vol. 39, pp. 26631–26641).
Philadelphia, PA, United States: Association for the Advancement of Artificial
Intelligence. https://doi.org/10.1609/aaai.v39i25.34865'
chicago: 'Meggendorfer, Tobias, Maximilian Weininger, and Patrick Wienhöft. “Solving
Robust Markov Decision Processes: Generic, Reliable, Efficient.” In Proceedings
of the 39th AAAI Conference on Artificial Intelligence, 39:26631–41. Association
for the Advancement of Artificial Intelligence, 2025. https://doi.org/10.1609/aaai.v39i25.34865.'
ieee: 'T. Meggendorfer, M. Weininger, and P. Wienhöft, “Solving robust Markov decision
processes: Generic, reliable, efficient,” in Proceedings of the 39th AAAI Conference
on Artificial Intelligence, Philadelphia, PA, United States, 2025, vol. 39,
no. 25, pp. 26631–26641.'
ista: 'Meggendorfer T, Weininger M, Wienhöft P. 2025. Solving robust Markov decision
processes: Generic, reliable, efficient. Proceedings of the 39th AAAI Conference
on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39,
26631–26641.'
mla: 'Meggendorfer, Tobias, et al. “Solving Robust Markov Decision Processes: Generic,
Reliable, Efficient.” Proceedings of the 39th AAAI Conference on Artificial
Intelligence, vol. 39, no. 25, Association for the Advancement of Artificial
Intelligence, 2025, pp. 26631–41, doi:10.1609/aaai.v39i25.34865.'
short: T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Proceedings of the 39th
AAAI Conference on Artificial Intelligence, Association for the Advancement of
Artificial Intelligence, 2025, pp. 26631–26641.
conference:
end_date: 2025-03-04
location: Philadelphia, PA, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2025-02-25
date_created: 2025-05-11T22:02:39Z
date_published: 2025-04-11T00:00:00Z
date_updated: 2026-02-16T12:25:05Z
day: '11'
department:
- _id: KrCh
doi: 10.1609/aaai.v39i25.34865
ec_funded: 1
external_id:
arxiv:
- '2412.10185'
intvolume: ' 39'
issue: '25'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2412.10185
month: '04'
oa: 1
oa_version: Preprint
page: 26631-26641
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 39th 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'
related_material:
link:
- relation: software
url: https://doi.org/10.5281/zenodo.14385449
scopus_import: '1'
status: public
title: 'Solving robust Markov decision processes: Generic, reliable, efficient'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 39
year: '2025'
...