---
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
license: https://creativecommons.org/licenses/by/4.0/
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_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: repository
OA_type: gold
_id: '21668'
abstract:
- lang: eng
text: "This artifact allows to review and reproduce the experiments from the paper
*A Revised Practitioner's Guide to MDP Model Checking Algorithms*.\r\nThe package
contains all original logfiles and derived data used to generate the plots as
in the paper. Furthermore, the artifact contains the model checking tools `Storm`
and `mcsta` in the version exercised in the paper, the used Docker container,
as well as benchmark instances and execution scripts to reproduce the experiments.\r\n\r\nSee
also the artifact of the conference paper: https://zenodo.org/records/7509474"
article_processing_charge: No
author:
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- first_name: Sebastian
full_name: Junges, Sebastian
last_name: Junges
- first_name: Tim
full_name: Quatmann, Tim
last_name: Quatmann
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
citation:
ama: Hartmanns A, Junges S, Quatmann T, Weininger M. Benchmark data for the revised
practitioner’s guide to MDP model checking algorithms. 2025. doi:10.5281/ZENODO.14500423
apa: Hartmanns, A., Junges, S., Quatmann, T., & Weininger, M. (2025). Benchmark
data for the revised practitioner’s guide to MDP model checking algorithms. Zenodo.
https://doi.org/10.5281/ZENODO.14500423
chicago: Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger.
“Benchmark Data for the Revised Practitioner’s Guide to MDP Model Checking Algorithms.”
Zenodo, 2025. https://doi.org/10.5281/ZENODO.14500423.
ieee: A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “Benchmark data for
the revised practitioner’s guide to MDP model checking algorithms.” Zenodo, 2025.
ista: Hartmanns A, Junges S, Quatmann T, Weininger M. 2025. Benchmark data for the
revised practitioner’s guide to MDP model checking algorithms, Zenodo, 10.5281/ZENODO.14500423.
mla: Hartmanns, Arnd, et al. Benchmark Data for the Revised Practitioner’s Guide
to MDP Model Checking Algorithms. Zenodo, 2025, doi:10.5281/ZENODO.14500423.
short: A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, (2025).
date_created: 2026-04-07T09:47:22Z
date_published: 2025-03-07T00:00:00Z
date_updated: 2026-04-07T09:52:55Z
day: '07'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.5281/ZENODO.14500423
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/ZENODO.14500423
month: '03'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '21661'
relation: used_for_analysis_in
status: public
status: public
title: Benchmark data for the revised practitioner's guide to MDP model checking algorithms
type: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19375'
abstract:
- lang: eng
text: "Despite the advances in probabilistic model checking, the scalability of
the verification methods remains limited. In particular, the state space often
becomes extremely large when instantiating parameterized Markov decision processes
(MDPs) even with moderate values. Synthesizing policies for such huge MDPs is
beyond the reach of available tools. We propose a learning-based approach to obtain
a reasonable policy for such huge MDPs.\r\n\r\nThe idea is to generalize optimal
policies obtained by model-checking small instances to larger ones using decision-tree
learning. Consequently, our method bypasses the need for explicit state-space
exploration of large models, providing a practical solution to the state-space
explosion problem. We demonstrate the efficacy of our approach by performing extensive
experimentation on the relevant models from the quantitative verification benchmark
set. The experimental results indicate that our policies perform well, even when
the size of the model is orders of magnitude beyond the reach of state-of-the-art
analysis tools."
acknowledgement: This research was funded in part by the DFG project 427755713 GOPro,
the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021)
of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement
101034413 (IST-BRIDGE).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Muqsit
full_name: Azeem, Muqsit
last_name: Azeem
- first_name: Debraj
full_name: Chakraborty, Debraj
last_name: Chakraborty
- first_name: Sudeep
full_name: Kanav, Sudeep
last_name: Kanav
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Mohammadsadegh
full_name: Mohagheghi, Mohammadsadegh
last_name: Mohagheghi
- first_name: Stefanie
full_name: Mohr, Stefanie
last_name: Mohr
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
citation:
ama: 'Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized
Markov decision processes via decision-tree learning and generalization. In: 26th
International Conference on Verification, Model Checking, and Abstract Interpretation.
Vol 15530. Springer Nature; 2025:97-120. doi:10.1007/978-3-031-82703-7_5'
apa: 'Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr,
S., & Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov
decision processes via decision-tree learning and generalization. In 26th International
Conference on Verification, Model Checking, and Abstract Interpretation (Vol.
15530, pp. 97–120). Denver, CO, United States: Springer Nature. https://doi.org/10.1007/978-3-031-82703-7_5'
chicago: Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh
Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis
for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.”
In 26th International Conference on Verification, Model Checking, and Abstract
Interpretation, 15530:97–120. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-82703-7_5.
ieee: M. Azeem et al., “1–2–3–Go! Policy synthesis for parameterized Markov
decision processes via decision-tree learning and generalization,” in 26th
International Conference on Verification, Model Checking, and Abstract Interpretation,
Denver, CO, United States, 2025, vol. 15530, pp. 97–120.
ista: 'Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger
M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes
via decision-tree learning and generalization. 26th International Conference on
Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification,
Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.'
mla: Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov
Decision Processes via Decision-Tree Learning and Generalization.” 26th International
Conference on Verification, Model Checking, and Abstract Interpretation, vol.
15530, Springer Nature, 2025, pp. 97–120, doi:10.1007/978-3-031-82703-7_5.
short: M. Azeem, D. Chakraborty, S. Kanav, J. Kretinsky, M. Mohagheghi, S. Mohr,
M. Weininger, in:, 26th International Conference on Verification, Model Checking,
and Abstract Interpretation, Springer Nature, 2025, pp. 97–120.
conference:
end_date: 2025-01-21
location: Denver, CO, United States
name: 'VMCAI: Verification, Model Checking, and Abstract Interpretation'
start_date: 2025-01-20
date_created: 2025-03-09T23:01:29Z
date_published: 2025-01-23T00:00:00Z
date_updated: 2025-09-30T10:46:54Z
day: '23'
department:
- _id: KrCh
doi: 10.1007/978-3-031-82703-7_5
ec_funded: 1
external_id:
arxiv:
- '2410.18293'
isi:
- '001446577100005'
intvolume: ' 15530'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2410.18293
month: '01'
oa: 1
oa_version: Preprint
page: 97-120
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 26th International Conference on Verification, Model Checking, and Abstract
Interpretation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031827020'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree
learning and generalization
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15530
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19445'
abstract:
- lang: eng
text: "In reconfiguration, we are given two solutions to a graph problem, such as
Vertex Cover or Dominating Set, with each solution represented by a placement
of tokens on vertices of the graph. Our task is to reconfigure one into the other
using small steps while ensuring the intermediate configurations of tokens are
also valid solutions. The two commonly studied settings are Token Jumping and
Token Sliding, which allows moving a single token to an arbitrary or an adjacent
vertex, respectively.\r\n\r\nWe introduce new rules that generalize Token Jumping,
parameterized by the number of tokens allowed to move at once and by the maximum
distance of each move. Our main contribution is identifying minimal rules that
allow reconfiguring any possible given solution into any other for Independent
Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide
an efficient algorithm that finds a corresponding reconfiguration sequence.\r\n\r\nWe
further focus on the rule that allows each token to move to an adjacent vertex
in a single step. This natural variant turns out to be the minimal rule that guarantees
reconfigurability for Vertex Cover. We determine the computational complexity
of deciding whether a (shortest) reconfiguration sequence exists under this rule
for the three studied problems. While reachability for Vertex Cover is shown to
be in P, finding a shortest sequence is shown to be NP-complete. For Independent
Set and Dominating Set, even reachability is shown to be PSPACE-complete."
acknowledgement: J. M. Křišťan acknowledges the support of the Czech Science Foundation
Grant No. 24-12046S. This work was supported by the Grant Agency of the Czech Technical
University in Prague, grant No. SGS23/205/OHK3/3T/18. J. Svoboda acknowledges the
support of the ERC CoG 863818 (ForM-SMArt) grant.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Jan Matyáš
full_name: Křišťan, Jan Matyáš
last_name: Křišťan
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Křišťan JM, Svoboda J. Reconfiguration using generalized token jumping. In:
19th International Conference and Workshops on Algorithms and Computation.
Vol 15411. Springer Nature; 2025:244-265. doi:10.1007/978-981-96-2845-2_16'
apa: 'Křišťan, J. M., & Svoboda, J. (2025). Reconfiguration using generalized
token jumping. In 19th International Conference and Workshops on Algorithms
and Computation (Vol. 15411, pp. 244–265). Chengdu, China: Springer Nature.
https://doi.org/10.1007/978-981-96-2845-2_16'
chicago: Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized
Token Jumping.” In 19th International Conference and Workshops on Algorithms
and Computation, 15411:244–65. Springer Nature, 2025. https://doi.org/10.1007/978-981-96-2845-2_16.
ieee: J. M. Křišťan and J. Svoboda, “Reconfiguration using generalized token jumping,”
in 19th International Conference and Workshops on Algorithms and Computation,
Chengdu, China, 2025, vol. 15411, pp. 244–265.
ista: 'Křišťan JM, Svoboda J. 2025. Reconfiguration using generalized token jumping.
19th International Conference and Workshops on Algorithms and Computation. WALCOM:
International Conference and Workshops on Algorithms and Computation, LNCS, vol.
15411, 244–265.'
mla: Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized
Token Jumping.” 19th International Conference and Workshops on Algorithms and
Computation, vol. 15411, Springer Nature, 2025, pp. 244–65, doi:10.1007/978-981-96-2845-2_16.
short: J.M. Křišťan, J. Svoboda, in:, 19th International Conference and Workshops
on Algorithms and Computation, Springer Nature, 2025, pp. 244–265.
conference:
end_date: 2025-03-02
location: Chengdu, China
name: 'WALCOM: International Conference and Workshops on Algorithms and Computation'
start_date: 2025-02-28
date_created: 2025-03-23T23:01:27Z
date_published: 2025-02-20T00:00:00Z
date_updated: 2025-09-30T11:14:33Z
day: '20'
department:
- _id: KrCh
doi: 10.1007/978-981-96-2845-2_16
ec_funded: 1
external_id:
arxiv:
- '2411.12582'
isi:
- '001537885900016'
intvolume: ' 15411'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2411.12582
month: '02'
oa: 1
oa_version: Preprint
page: 244-265
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 19th International Conference and Workshops on Algorithms and Computation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9789819628445'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reconfiguration using generalized token jumping
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15411
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19499'
abstract:
- lang: eng
text: Quantum hardware is inherently fragile and noisy. We find that the accuracy
of traditional quantum error correction algorithms can be improved depending on
the hardware. Given different hardware specifications, we automatically synthesize
hardware-optimal algorithms for parity correction, qubit resetting, and GHZ (Greenberger–Horne–Zeilinger)
state preparation. Using stochastic techniques from computer science, our method
presents a computational tool to compute exact accuracy guarantees and synthesize
optimal algorithms that are often different from traditional ones. We also show
that improvements can be gained with respect to the Qiskit transpiler as we compute
the hardware-optimal qubit mapping for the GHZ state-preparation problem.
acknowledgement: We thank the reviewers. In particular, they inspired us to analyze
the reset and state-preparation problems, to compute optimal qubit mappings, and
to apply our method to a quantum error correction scheme that includes both bitflip
and phaseflip corrections. We also thank Raimundo Saona and Marek Chalupa for their
time spent in insightful discussions. This research was partially supported by the
European Research Council CoG 863818 (ForM-SMArt) grant.
article_number: e2419273122
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Muroya Lei S, Chatterjee K, Henzinger TA. Hardware-optimal quantum algorithms.
Proceedings of the National Academy of Sciences. 2025;122(12). doi:10.1073/pnas.2419273122
apa: Muroya Lei, S., Chatterjee, K., & Henzinger, T. A. (2025). Hardware-optimal
quantum algorithms. Proceedings of the National Academy of Sciences. National
Academy of Sciences. https://doi.org/10.1073/pnas.2419273122
chicago: Muroya Lei, Stefanie, Krishnendu Chatterjee, and Thomas A Henzinger. “Hardware-Optimal
Quantum Algorithms.” Proceedings of the National Academy of Sciences. National
Academy of Sciences, 2025. https://doi.org/10.1073/pnas.2419273122.
ieee: S. Muroya Lei, K. Chatterjee, and T. A. Henzinger, “Hardware-optimal quantum
algorithms,” Proceedings of the National Academy of Sciences, vol. 122,
no. 12. National Academy of Sciences, 2025.
ista: Muroya Lei S, Chatterjee K, Henzinger TA. 2025. Hardware-optimal quantum algorithms.
Proceedings of the National Academy of Sciences. 122(12), e2419273122.
mla: Muroya Lei, Stefanie, et al. “Hardware-Optimal Quantum Algorithms.” Proceedings
of the National Academy of Sciences, vol. 122, no. 12, e2419273122, National
Academy of Sciences, 2025, doi:10.1073/pnas.2419273122.
short: S. Muroya Lei, K. Chatterjee, T.A. Henzinger, Proceedings of the National
Academy of Sciences 122 (2025).
corr_author: '1'
date_created: 2025-04-06T22:01:32Z
date_published: 2025-03-25T00:00:00Z
date_updated: 2026-04-28T13:41:14Z
day: '25'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1073/pnas.2419273122
ec_funded: 1
external_id:
isi:
- '001459435600001'
pmid:
- '40106357'
file:
- access_level: open_access
checksum: 83501b8a65ee5fdd3f5604fc28eddc22
content_type: application/pdf
creator: dernst
date_created: 2025-04-07T11:42:22Z
date_updated: 2025-04-07T11:42:22Z
file_id: '19524'
file_name: 2025_PNAS_Muroya.pdf
file_size: 6805668
relation: main_file
success: 1
file_date_updated: 2025-04-07T11:42:22Z
has_accepted_license: '1'
intvolume: ' 122'
isi: 1
issue: '12'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '03'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the National Academy of Sciences
publication_identifier:
eissn:
- 1091-6490
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/smml1996/algorithm_synthesis
- description: News on ISTA website
relation: press_release
url: https://ista.ac.at/en/news/hardware-optimal-quantum-algorithms/
scopus_import: '1'
status: public
title: Hardware-optimal quantum algorithms
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 122
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '19508'
abstract:
- lang: eng
text: We consider random two-player zero-sum dynamic games with perfect information
on a class of infinite directed graphs. Starting from a fixed vertex, the players
take turns to move a token along the edges of the graph. Every vertex is assigned
a payoff known in advance by both players. Every time the token visits a vertex,
Player 2 pays Player 1 the corresponding payoff. We consider a distribution over
such games by assigning i.i.d. payoffs to the vertices. On the one hand, for acyclic
directed graphs of bounded degree and sub-exponential expansion, we show that,
when the duration of the game tends to infinity, the value converges almost surely
to a constant at an exponential rate dominated in terms of the expansion. On the
other hand, for the infinite d-ary tree (that does not fall into the previous
class of graphs), we show convergence at a double-exponential rate.
acknowledgement: Open access funding provided by Institute of Science and Technology
(IST Austria). This work was supported by the French Agence Nationale de la Recherche
(ANR) under references ANR-21-CE40-0020 (CONVERGENCE project) and ANR-20-CE40-0002
(GrHyDy), by Fondecyt grant 1220174, by ANID Chile grant ACT210005, and by the ERC
CoG 863818 (ForM-SMArt) grant. This collaboration was mainly conducted during a
1-year visit of Bruno Ziliotto to the Center for Mathematical Modeling (CMM) at
University of Chile in 2023, under the IRL program of CNRS. This work was supported
by Fondation CFM pour la Recherche. This paper has also been funded by the Agence
Nationale de la Recherche under grant ANR-17-EURE-0010 (Investissements d’Avenir
program).
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Luc
full_name: Attia, Luc
last_name: Attia
- first_name: Lyuben
full_name: Lichev, Lyuben
id: 9aa8388e-d003-11ee-8458-c4c1d7447977
last_name: Lichev
- first_name: Dieter
full_name: Mitsche, Dieter
last_name: Mitsche
- 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: Bruno
full_name: Ziliotto, Bruno
last_name: Ziliotto
citation:
ama: Attia L, Lichev L, Mitsche D, Saona Urmeneta RJ, Ziliotto B. Random zero-sum
dynamic games on infinite directed graphs. Dynamic Games and Applications.
2025;15:1517-1535. doi:10.1007/s13235-025-00636-4
apa: Attia, L., Lichev, L., Mitsche, D., Saona Urmeneta, R. J., & Ziliotto,
B. (2025). Random zero-sum dynamic games on infinite directed graphs. Dynamic
Games and Applications. Springer Nature. https://doi.org/10.1007/s13235-025-00636-4
chicago: Attia, Luc, Lyuben Lichev, Dieter Mitsche, Raimundo J Saona Urmeneta, and
Bruno Ziliotto. “Random Zero-Sum Dynamic Games on Infinite Directed Graphs.” Dynamic
Games and Applications. Springer Nature, 2025. https://doi.org/10.1007/s13235-025-00636-4.
ieee: L. Attia, L. Lichev, D. Mitsche, R. J. Saona Urmeneta, and B. Ziliotto, “Random
zero-sum dynamic games on infinite directed graphs,” Dynamic Games and Applications,
vol. 15. Springer Nature, pp. 1517–1535, 2025.
ista: Attia L, Lichev L, Mitsche D, Saona Urmeneta RJ, Ziliotto B. 2025. Random
zero-sum dynamic games on infinite directed graphs. Dynamic Games and Applications.
15, 1517–1535.
mla: Attia, Luc, et al. “Random Zero-Sum Dynamic Games on Infinite Directed Graphs.”
Dynamic Games and Applications, vol. 15, Springer Nature, 2025, pp. 1517–35,
doi:10.1007/s13235-025-00636-4.
short: L. Attia, L. Lichev, D. Mitsche, R.J. Saona Urmeneta, B. Ziliotto, Dynamic
Games and Applications 15 (2025) 1517–1535.
corr_author: '1'
date_created: 2025-04-06T22:01:32Z
date_published: 2025-11-01T00:00:00Z
date_updated: 2026-04-07T12:31:21Z
day: '01'
ddc:
- '000'
department:
- _id: MaKw
- _id: KrCh
doi: 10.1007/s13235-025-00636-4
ec_funded: 1
external_id:
isi:
- '001449708900001'
file:
- access_level: open_access
checksum: b3a1b7eef40c9ac2acf3fef563081694
content_type: application/pdf
creator: dernst
date_created: 2025-12-30T08:13:04Z
date_updated: 2025-12-30T08:13:04Z
file_id: '20891'
file_name: 2025_DynGamesAppl_Attia.pdf
file_size: 570994
relation: main_file
success: 1
file_date_updated: 2025-12-30T08:13:04Z
has_accepted_license: '1'
intvolume: ' 15'
isi: 1
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: 1517-1535
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Dynamic Games and Applications
publication_identifier:
eissn:
- 2153-0793
issn:
- 2153-0785
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20234'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Random zero-sum dynamic games on infinite directed graphs
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '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'
...
---
OA_place: repository
OA_type: green
_id: '19667'
abstract:
- lang: eng
text: The problem of checking satisfiability of linear real arithmetic (LRA) and
non-linear real arithmetic (NRA) formulas has broad applications, in particular,
they are at the heart of logic-related applications such as logic for artificial
intelligence, program analysis, etc. While there has been much work on checking
satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability
of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck
in the existing methods is a computationally expensive quantifier elimination
step. In this work, we propose a novel method for efficient quantifier elimination
in quantified LRA and NRA formulas. We propose a template-based Skolemization
approach, where we automatically synthesize linear/polynomial Skolem functions
in order to eliminate quantifiers in the formula. The key technical ingredient
in our approach are Positivstellensätze theorems from algebraic geometry, which
allow for an efficient manipulation of polynomial inequalities. Our method offers
a range of appealing theoretical properties combined with a strong practical performance.
On the theory side, our method is sound, semi-complete, and runs in subexponential
time and polynomial space, as opposed to existing sound and complete quantifier
elimination methods that run in doubly-exponential time and at least exponential
space. On the practical side, our experiments show superior performance compared
to state of the art SMT solvers in terms of the number of solved instances and
runtime, both on LRA and on NRA benchmarks.
acknowledgement: This work was partially funded by ERC CoG 863818 (ForM-SMArt) and
Austrian Science Fund (FWF) 10.55776/COE12.
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
orcid: 0009-0007-5253-9170
- first_name: Harshit J.
full_name: Motwani, Harshit J.
last_name: Motwani
- 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 E, Karrabi M, Motwani HJ, Seeliger M, Zikelic D.
Quantified linear and polynomial arithmetic satisfiability via template-based
skolemization. In: Proceedings of the 39th AAAI Conference on Artificial Intelligence.
Vol 39. Association for the Advancement of Artificial Intelligence; 2025:11158-11166.
doi:10.1609/aaai.v39i11.33213'
apa: 'Chatterjee, K., Goharshady, E., Karrabi, M., Motwani, H. J., Seeliger, M.,
& Zikelic, D. (2025). Quantified linear and polynomial arithmetic satisfiability
via template-based skolemization. In Proceedings of the 39th AAAI Conference
on Artificial Intelligence (Vol. 39, pp. 11158–11166). Philadelphia, PA, United
States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v39i11.33213'
chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Harshit J. Motwani,
Maximilian Seeliger, and Dorde Zikelic. “Quantified Linear and Polynomial Arithmetic
Satisfiability via Template-Based Skolemization.” In Proceedings of the 39th
AAAI Conference on Artificial Intelligence, 39:11158–66. Association for the
Advancement of Artificial Intelligence, 2025. https://doi.org/10.1609/aaai.v39i11.33213.
ieee: K. Chatterjee, E. Goharshady, M. Karrabi, H. J. Motwani, M. Seeliger, and
D. Zikelic, “Quantified linear and polynomial arithmetic satisfiability via template-based
skolemization,” in Proceedings of the 39th AAAI Conference on Artificial Intelligence,
Philadelphia, PA, United States, 2025, vol. 39, no. 11, pp. 11158–11166.
ista: 'Chatterjee K, Goharshady E, Karrabi M, Motwani HJ, Seeliger M, Zikelic D.
2025. Quantified linear and polynomial arithmetic satisfiability via template-based
skolemization. Proceedings of the 39th AAAI Conference on Artificial Intelligence.
AAAI: Conference on Artificial Intelligence vol. 39, 11158–11166.'
mla: Chatterjee, Krishnendu, et al. “Quantified Linear and Polynomial Arithmetic
Satisfiability via Template-Based Skolemization.” Proceedings of the 39th AAAI
Conference on Artificial Intelligence, vol. 39, no. 11, Association for the
Advancement of Artificial Intelligence, 2025, pp. 11158–66, doi:10.1609/aaai.v39i11.33213.
short: K. Chatterjee, E. Goharshady, M. Karrabi, H.J. Motwani, M. Seeliger, D. Zikelic,
in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association
for the Advancement of Artificial Intelligence, 2025, pp. 11158–11166.
conference:
end_date: 2025-03-04
location: Philadelphia, PA, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2025-02-25
corr_author: '1'
date_created: 2025-05-11T22:02:39Z
date_published: 2025-04-11T00:00:00Z
date_updated: 2026-02-16T12:24:47Z
day: '11'
department:
- _id: KrCh
doi: 10.1609/aaai.v39i11.33213
ec_funded: 1
external_id:
arxiv:
- '2412.16226'
intvolume: ' 39'
issue: '11'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2412.16226
month: '04'
oa: 1
oa_version: Preprint
page: 11158-11166
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'
scopus_import: '1'
status: public
title: Quantified linear and polynomial arithmetic satisfiability via template-based
skolemization
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 39
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19669'
abstract:
- lang: eng
text: 'We consider a class of optimization problems defined by a system of linear
equations with min and max operators. This class of optimization problems has
been studied under restrictive conditions, such as, (C1) the halting or stability
condition; (C2) the non-negative coefficients condition; (C3) the sum upto 1 condition;
and (C4) the only min or only max operator condition. Several seminal results
in the literature focus on special cases. For example, turn-based stochastic games
correspond to conditions C2 and C3; and Markov decision process to conditions
C2, C3, and C4. However, the systematic computational complexity study of all
the cases has not been explored, which we address in this work. Some highlights
of our results are: with conditions C2 and C4, and with conditions C3 and C4,
the problem is NP-complete, whereas with condition C1 only, the problem is in
UP intersects coUP. Finally, we establish the computational complexity of the
decision problem of checking the respective conditions.'
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant and the Austrian Science Fund (FWF) 10.55776/COE12 grant.
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: Ruichen
full_name: Luo, Ruichen
id: b391db08-1ffe-11ee-8b67-d18ddcfb5a14
last_name: Luo
- first_name: Raimundo J
full_name: Saona Urmeneta, Raimundo J
id: BD1DF4C4-D767-11E9-B658-BC13E6697425
last_name: Saona Urmeneta
orcid: 0000-0001-5103-038X
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Chatterjee K, Luo R, Saona Urmeneta RJ, Svoboda J. Linear equations with min
and max operators: Computational complexity. In: Proceedings of the 39th AAAI
Conference on Artificial Intelligence. Vol 39. Association for the Advancement
of Artificial Intelligence; 2025:11150-11157. doi:10.1609/aaai.v39i11.33212'
apa: 'Chatterjee, K., Luo, R., Saona Urmeneta, R. J., & Svoboda, J. (2025).
Linear equations with min and max operators: Computational complexity. In Proceedings
of the 39th AAAI Conference on Artificial Intelligence (Vol. 39, pp. 11150–11157).
Philadelphia, PA, United States: Association for the Advancement of Artificial
Intelligence. https://doi.org/10.1609/aaai.v39i11.33212'
chicago: 'Chatterjee, Krishnendu, Ruichen Luo, Raimundo J Saona Urmeneta, and Jakub
Svoboda. “Linear Equations with Min and Max Operators: Computational Complexity.”
In Proceedings of the 39th AAAI Conference on Artificial Intelligence,
39:11150–57. Association for the Advancement of Artificial Intelligence, 2025.
https://doi.org/10.1609/aaai.v39i11.33212.'
ieee: 'K. Chatterjee, R. Luo, R. J. Saona Urmeneta, and J. Svoboda, “Linear equations
with min and max operators: Computational complexity,” in Proceedings of the
39th AAAI Conference on Artificial Intelligence, Philadelphia, PA, United
States, 2025, vol. 39, no. 11, pp. 11150–11157.'
ista: 'Chatterjee K, Luo R, Saona Urmeneta RJ, Svoboda J. 2025. Linear equations
with min and max operators: Computational complexity. Proceedings of the 39th
AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence
vol. 39, 11150–11157.'
mla: 'Chatterjee, Krishnendu, et al. “Linear Equations with Min and Max Operators:
Computational Complexity.” Proceedings of the 39th AAAI Conference on Artificial
Intelligence, vol. 39, no. 11, Association for the Advancement of Artificial
Intelligence, 2025, pp. 11150–57, doi:10.1609/aaai.v39i11.33212.'
short: K. Chatterjee, R. Luo, R.J. Saona Urmeneta, J. Svoboda, in:, Proceedings
of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2025, pp. 11150–11157.
conference:
end_date: 2025-03-04
location: Philadelphia, PA, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2025-02-25
corr_author: '1'
date_created: 2025-05-11T22:02:40Z
date_published: 2025-04-11T00:00:00Z
date_updated: 2025-05-12T09:42:09Z
day: '11'
department:
- _id: KrCh
doi: 10.1609/aaai.v39i11.33212
ec_funded: 1
external_id:
arxiv:
- '2412.12228'
intvolume: ' 39'
issue: '11'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2412.12228
month: '04'
oa: 1
oa_version: Preprint
page: 11150-11157
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'
scopus_import: '1'
status: public
title: 'Linear equations with min and max operators: Computational complexity'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 39
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19740'
abstract:
- lang: eng
text: Two standard models for probabilistic systems are Markov chains (MCs) and
Markov decision processes (MDPs). Classic objectives for such probabilistic models
for control and planning problems are reachability and stochastic shortest path.
The widely studied algorithmic approach for these problems is the Value Iteration
(VI) algorithm which iteratively applies local updates called Bellman updates.
There are many practical approaches for VI in the literature but they all require
exponentially many Bellman updates for MCs in the worst case. A preprocessing
step is an algorithm that is discrete, graph-theoretical, and requires linear
space. An important open question is whether, after a polynomial-time preprocessing,
VI can be achieved with sub-exponentially many Bellman updates. In this work,
we present a new approach for VI based on guessing values. Our theoretical contributions
are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm
after which, along with guessing values, VI requires only subexponentially many
Bellman updates. Second, we present an improved analysis of the speed of convergence
of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our
new approach. Experimental results show that our approach provides a considerable
improvement over existing VI-based approaches on several benchmark examples from
the literature.
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant and Austrian Science Fund (FWF) 10.55776/COE12 grant.
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: Mahdi
full_name: Jafariraviz, Mahdi
last_name: Jafariraviz
- first_name: Raimundo J
full_name: Saona Urmeneta, Raimundo J
id: BD1DF4C4-D767-11E9-B658-BC13E6697425
last_name: Saona Urmeneta
orcid: 0000-0001-5103-038X
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. Value iteration
with guessing for Markov chains and Markov decision processes. In: 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 15697. Springer Nature; 2025:217-236. doi:10.1007/978-3-031-90653-4_11'
apa: 'Chatterjee, K., Jafariraviz, M., Saona Urmeneta, R. J., & Svoboda, J.
(2025). Value iteration with guessing for Markov chains and Markov decision processes.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15697, pp. 217–236). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90653-4_11'
chicago: Chatterjee, Krishnendu, Mahdi Jafariraviz, Raimundo J Saona Urmeneta, and
Jakub Svoboda. “Value Iteration with Guessing for Markov Chains and Markov Decision
Processes.” In 31st International Conference on Tools and Algorithms for the
Construction and Analysis of Systems, 15697:217–36. Springer Nature, 2025.
https://doi.org/10.1007/978-3-031-90653-4_11.
ieee: K. Chatterjee, M. Jafariraviz, R. J. Saona Urmeneta, and J. Svoboda, “Value
iteration with guessing for Markov chains and Markov decision processes,” in 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Hamilton, ON, Canada, 2025, vol. 15697, pp. 217–236.
ista: 'Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. 2025. Value iteration
with guessing for Markov chains and Markov decision processes. 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 15697, 217–236.'
mla: Chatterjee, Krishnendu, et al. “Value Iteration with Guessing for Markov Chains
and Markov Decision Processes.” 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, vol. 15697, Springer
Nature, 2025, pp. 217–36, doi:10.1007/978-3-031-90653-4_11.
short: K. Chatterjee, M. Jafariraviz, R.J. Saona Urmeneta, J. Svoboda, in:, 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Springer Nature, 2025, pp. 217–236.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:06Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T07:35:06Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90653-4_11
ec_funded: 1
external_id:
arxiv:
- '2505.06769'
file:
- access_level: open_access
checksum: 45da6efbcbed20aada16c48c8e55e2d6
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T07:31:12Z
date_updated: 2025-06-02T07:31:12Z
file_id: '19767'
file_name: 2025_TACAS_Chatterjee.pdf
file_size: 557481
relation: main_file
success: 1
file_date_updated: 2025-06-02T07:31:12Z
has_accepted_license: '1'
intvolume: ' 15697'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 217-236
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906527'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Value iteration with guessing for Markov chains and 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: 15697
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19742'
abstract:
- lang: eng
text: Statistical model checking estimates probabilities and expectations of interest
in probabilistic system models by using random simulations. Its results come with
statistical guarantees. However, many tools use unsound statistical methods that
produce incorrect results more often than they claim. In this paper, we provide
a comprehensive overview of tools and their correctness, as well as of sound methods
available for estimating probabilities from the literature. For expected rewards,
we investigate how to bound the path reward distribution to apply sound statistical
methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz
inequality that has not been used in SMC so far. We prove that even reachability
rewards can be bounded in theory, and formalise the concept of limit-PAC procedures
for a practical solution. The modes SMC tool implements our methods and recommendations,
which we use to experimentally confirm our results.
acknowledgement: This work was supported by 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 perspicuous-computing.science, project ID 389792660), by the
European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie
grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED),
by the EU under NextGenerationEU projects D53D23008400006 (Smartitude) under MUR
PRIN 2022 and PE00000014 (SERICS) under MUR PNRR, by the Interreg North Sea project
STORM_SAFE, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Carlos E.
full_name: Budde, Carlos E.
last_name: Budde
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- 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
- first_name: Patrick
full_name: Wienhöft, Patrick
last_name: Wienhöft
citation:
ama: 'Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical
model checking for probabilities and expected rewards. In: 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 15696. Springer Nature; 2025:167-190. doi:10.1007/978-3-031-90643-5_9'
apa: 'Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., & Wienhöft,
P. (2025). Sound statistical model checking for probabilities and expected rewards.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90643-5_9'
chicago: Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger,
and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and
Expected Rewards.” In 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, 15696:167–90. Springer Nature,
2025. https://doi.org/10.1007/978-3-031-90643-5_9.
ieee: C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft,
“Sound statistical model checking for probabilities and expected rewards,” in
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190.
ista: 'Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound
statistical model checking for probabilities and expected rewards. 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 15696, 167–190.'
mla: Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities
and Expected Rewards.” 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, vol. 15696, Springer Nature,
2025, pp. 167–90, doi:10.1007/978-3-031-90643-5_9.
short: C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:,
31st International Conference on Tools and Algorithms for the Construction and
Analysis of Systems, Springer Nature, 2025, pp. 167–190.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
date_created: 2025-05-25T22:17:08Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T09:45:41Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90643-5_9
ec_funded: 1
external_id:
arxiv:
- '2411.00559'
file:
- access_level: open_access
checksum: d45856b503b1dd4f8f14c3566327225b
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T09:35:42Z
date_updated: 2025-06-02T09:35:42Z
file_id: '19770'
file_name: 2025_TACAS_Budde.pdf
file_size: 711271
relation: main_file
success: 1
file_date_updated: 2025-06-02T09:35:42Z
has_accepted_license: '1'
intvolume: ' 15696'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 167-190
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906428'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '19769'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Sound statistical model checking for probabilities and expected rewards
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: 15696
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19743'
abstract:
- lang: eng
text: The possibility of errors in human-engineered formal verification software,
such as model checkers, poses a serious threat to the purpose of these tools.
An established approach to mitigate this problem are certificates—lightweight,
easy-to-check proofs of the verification results. In this paper, we develop novel
certificates for model checking of Markov decision processes (MDPs) with quantitative
reachability and expected reward properties. Our approach is conceptually simple
and relies almost exclusively on elementary fixed point theory. Our certificates
work for arbitrary finite MDPs and can be readily computed with little overhead
using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL
and provide a formally verified certificate checker. Moreover, we augment existing
algorithms in the probabilistic model checker Storm with the ability to produce
certificates and demonstrate practical applicability by conducting the first formal
certification of the reference results in the Quantitative Verification Benchmark
Set.
acknowledgement: This project has received funding from the ERC CoG 863818 (ForM-SMArt),
the Austrian Science Fund (FWF) 10.55776/COE12, a KI-Starter grant from the Ministerium
für Kultur und Wissenschaft NRW, the DFG RTG 378803395 (ConVeY), the EU’s Horizon
2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement
Nos. 101034413 (IST-BRIDGE) and 101008233 (MISSION), and the DFG RTG 2236 (UnRAVeL).
Experiments were performed with computing resources granted by RWTH Aachen University
under project rwth1632.
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: Tim
full_name: Quatmann, Tim
last_name: Quatmann
- first_name: Maximilian
full_name: Schäffeler, Maximilian
last_name: Schäffeler
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
- first_name: Tobias
full_name: Winkler, Tobias
last_name: Winkler
- first_name: Daniel
full_name: Zilken, Daniel
id: d8ebc24a-3f98-11f0-9044-8296d4f39ab3
last_name: Zilken
citation:
ama: 'Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D.
Fixed point certificates for reachability and expected rewards in MDPs. In: 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. Vol 15697. Springer Nature; 2025:130-151. doi:10.1007/978-3-031-90653-4_7'
apa: 'Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T.,
& Zilken, D. (2025). Fixed point certificates for reachability and expected
rewards in MDPs. In 31st International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (Vol. 15697, pp. 130–151). Hamilton,
ON, Canada: Springer Nature. https://doi.org/10.1007/978-3-031-90653-4_7'
chicago: Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian
Weininger, Tobias Winkler, and Daniel Zilken. “Fixed Point Certificates for Reachability
and Expected Rewards in MDPs.” In 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, 15697:130–51. Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-90653-4_7.
ieee: K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D.
Zilken, “Fixed point certificates for reachability and expected rewards in MDPs,”
in 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15697, pp. 130–151.
ista: 'Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D.
2025. Fixed point certificates for reachability and expected rewards in MDPs.
31st International Conference on Tools and Algorithms for the Construction and
Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, LNCS, vol. 15697, 130–151.'
mla: Chatterjee, Krishnendu, et al. “Fixed Point Certificates for Reachability and
Expected Rewards in MDPs.” 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, vol. 15697, Springer Nature,
2025, pp. 130–51, doi:10.1007/978-3-031-90653-4_7.
short: K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken,
in:, 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2025, pp. 130–151.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:09Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T10:55:34Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90653-4_7
ec_funded: 1
external_id:
arxiv:
- '2501.11467'
file:
- access_level: open_access
checksum: 64b7f46ef05649b87b827248045c7645
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T10:49:52Z
date_updated: 2025-06-02T10:49:52Z
file_id: '19772'
file_name: 2025_TACAS_ChatterjeeKrish.pdf
file_size: 732136
relation: main_file
success: 1
file_date_updated: 2025-06-02T10:49:52Z
has_accepted_license: '1'
intvolume: ' 15697'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 130-151
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: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906527'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '19771'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Fixed point certificates for reachability and expected rewards in MDPs
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: 15697
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19744'
abstract:
- lang: eng
text: We consider the problem of refuting equivalence of probabilistic programs,
i.e., the problem of proving that two probabilistic programs induce different
output distributions. We study this problem in the context of programs with conditioning
(i.e., with observe and score statements), where the output distribution is conditioned
by the event that all the observe statements along a run evaluate to true, and
where the probability densities of different runs may be updated via the score
statements. Building on a recent work on programs without conditioning, we present
a new equivalence refutation method for programs with conditioning. Our method
is based on weighted restarting, a novel transformation of probabilistic programs
with conditioning to the output equivalent probabilistic programs without conditioning
that we introduce in this work. Our method is the first to be both a) fully automated,
and b) providing provably correct answers. We demonstrate the applicability of
our method on a set of programs from the probabilistic inference literature.
acknowledgement: This work was partially supported by ERC CoG 863818 (ForM-SMArt)
and Austrian Science Fund (FWF) 10.55776/COE12. Petr Novotný is supported by the
Czech Science Foundation grant no. GA23-06963S.
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: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady E, Novotný P, Zikelic D. Refuting equivalence in
probabilistic programs with conditioning. In: 31st International Conference
on Tools and Algorithms for the Construction and Analysis of Systems. Vol
15697. Springer Nature; 2025:279-300. doi:10.1007/978-3-031-90653-4_14'
apa: 'Chatterjee, K., Goharshady, E., Novotný, P., & Zikelic, D. (2025). Refuting
equivalence in probabilistic programs with conditioning. In 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 15697, pp. 279–300). Hamilton, ON, Canada: Springer Nature. https://doi.org/10.1007/978-3-031-90653-4_14'
chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic.
“Refuting Equivalence in Probabilistic Programs with Conditioning.” In 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, 15697:279–300. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90653-4_14.
ieee: K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Refuting equivalence
in probabilistic programs with conditioning,” in 31st International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, Hamilton,
ON, Canada, 2025, vol. 15697, pp. 279–300.
ista: 'Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2025. Refuting equivalence
in probabilistic programs with conditioning. 31st International Conference on
Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697,
279–300.'
mla: Chatterjee, Krishnendu, et al. “Refuting Equivalence in Probabilistic Programs
with Conditioning.” 31st International Conference on Tools and Algorithms for
the Construction and Analysis of Systems, vol. 15697, Springer Nature, 2025,
pp. 279–300, doi:10.1007/978-3-031-90653-4_14.
short: K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, in:, 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Springer Nature, 2025, pp. 279–300.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:10Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T11:16:13Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90653-4_14
ec_funded: 1
external_id:
arxiv:
- '2501.06579'
file:
- access_level: open_access
checksum: 7dcd85e7e753bfa994c10b3cf9ebc185
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T11:13:49Z
date_updated: 2025-06-02T11:13:49Z
file_id: '19773'
file_name: 2025_TACAS_Chatterjee_Goharshadi.pdf
file_size: 532181
relation: main_file
success: 1
file_date_updated: 2025-06-02T11:13:49Z
has_accepted_license: '1'
intvolume: ' 15697'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 279-300
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906527'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Refuting equivalence in probabilistic programs with conditioning
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: 15697
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19769'
abstract:
- lang: eng
text: "Artifact to reproduce the experimental results presented in the article \"Sound
Statistical Model Checking for Probabilities and Expected Rewards\" by Carlos
E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick
Wienhöft (TACAS 2025).\r\n\r\nThe contents include all data and software (formal
models, software tools, Python & bash scripts) used in the experimental evaluation
presented in sections 3, 4, and 6 of the article. Detailed instructions on how
to reproduce the results are bundled in the artifact."
article_processing_charge: No
author:
- first_name: Carlos
full_name: Budde, Carlos
last_name: Budde
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- 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
- first_name: Patrick
full_name: Wienhöft, Patrick
last_name: Wienhöft
citation:
ama: Budde C, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical
model checking for probabilities and expected rewards (experimental reproduction
package). 2025. doi:10.5281/ZENODO.14602066
apa: Budde, C., Hartmanns, A., Meggendorfer, T., Weininger, M., & Wienhöft,
P. (2025). Sound statistical model checking for probabilities and expected rewards
(experimental reproduction package). Zenodo. https://doi.org/10.5281/ZENODO.14602066
chicago: Budde, Carlos, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger,
and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and
Expected Rewards (Experimental Reproduction Package).” Zenodo, 2025. https://doi.org/10.5281/ZENODO.14602066.
ieee: C. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft, “Sound
statistical model checking for probabilities and expected rewards (experimental
reproduction package).” Zenodo, 2025.
ista: Budde C, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound
statistical model checking for probabilities and expected rewards (experimental
reproduction package), Zenodo, 10.5281/ZENODO.14602066.
mla: Budde, Carlos, et al. Sound Statistical Model Checking for Probabilities
and Expected Rewards (Experimental Reproduction Package). Zenodo, 2025, doi:10.5281/ZENODO.14602066.
short: C. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, (2025).
date_created: 2025-06-02T09:37:14Z
date_published: 2025-01-07T00:00:00Z
date_updated: 2025-06-02T09:45:41Z
day: '07'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.5281/ZENODO.14602066
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/ZENODO.14602066
month: '01'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '19742'
relation: used_in_publication
status: public
status: public
title: Sound statistical model checking for probabilities and expected rewards (experimental
reproduction package)
type: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19771'
abstract:
- lang: eng
text: "This artifact allows to review and reproduce the Isabelle proofs and practical
experiments from the paper *Fixed Point Certificates for Reachability and Expected
Rewards in MDPs*.\r\nThe contents are two-fold:\r\nFirst, the artifact contains
a formally verified certificate checker for the certificates presented in the
paper.\r\nThe formal Isabelle/HOL proofs of the background theory can be inspected,
checked by Isabelle and the code extraction can be retraced.\r\n\r\nSecond, the
artifact contains a modified version of the model checking tool `Storm` with support
for certificate generation. Together with the provided scripts and benchmark files,
this allows to reproduce the experiments from the paper.\r\nAn appropriate subset
of the experiments is given to allow a review in a timely manner. In addition,
original logfiles from our experiments are provided, allowing a detailed inspection.\r\n\r\nThe
package includes convenient installation scripts for [the TACAS 2023 VM](https://doi.org/10.5281/zenodo.7113223)
(based on Ubuntu 22.04).\r\nA native installation on Linux or macOS systems (including
the newer ARM-based machines) is also possible."
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: Tim
full_name: Quatmann, Tim
last_name: Quatmann
- first_name: Maximilian
full_name: Schäffeler, Maximilian
last_name: Schäffeler
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
- first_name: Tobias
full_name: Winkler, Tobias
last_name: Winkler
- first_name: Daniel
full_name: Zilken, Daniel
id: d8ebc24a-3f98-11f0-9044-8296d4f39ab3
last_name: Zilken
citation:
ama: 'Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D.
Artifact: Fixed point certificates for reachability and expected rewards in MDPs.
2025. doi:10.5281/ZENODO.14626585'
apa: 'Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T.,
& Zilken, D. (2025). Artifact: Fixed point certificates for reachability and
expected rewards in MDPs. Zenodo. https://doi.org/10.5281/ZENODO.14626585'
chicago: 'Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian
Weininger, Tobias Winkler, and Daniel Zilken. “Artifact: Fixed Point Certificates
for Reachability and Expected Rewards in MDPs.” Zenodo, 2025. https://doi.org/10.5281/ZENODO.14626585.'
ieee: 'K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and
D. Zilken, “Artifact: Fixed point certificates for reachability and expected rewards
in MDPs.” Zenodo, 2025.'
ista: 'Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D.
2025. Artifact: Fixed point certificates for reachability and expected rewards
in MDPs, Zenodo, 10.5281/ZENODO.14626585.'
mla: 'Chatterjee, Krishnendu, et al. Artifact: Fixed Point Certificates for Reachability
and Expected Rewards in MDPs. Zenodo, 2025, doi:10.5281/ZENODO.14626585.'
short: K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken,
(2025).
date_created: 2025-06-02T10:13:24Z
date_published: 2025-01-09T00:00:00Z
date_updated: 2025-06-02T10:55:35Z
day: '09'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.5281/ZENODO.14626585
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/ZENODO.14626585
month: '01'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '19743'
relation: used_in_publication
status: public
status: public
title: 'Artifact: Fixed point certificates for reachability and expected rewards in
MDPs'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '19843'
abstract:
- lang: eng
text: 'Social dilemmas are collective-action problems where individual interests
are at odds with group interests. Such dilemmas occur frequently at all scales
of human interactions. When dealing with collective-action problems, people often
act reciprocally. They adjust their behavior to match the previous behavior of
the recipient. The literature distinguishes two kinds of reciprocity. According
to direct reciprocity, individuals react to their immediate experiences with the
recipient. They are more likely to cooperate if the recipient previously cooperated
with them. According to indirect reciprocity, individuals react to the recipient’s
general behavior, irrespectively of whether or not they benefited directly. In
practice, the two kinds of reciprocity are often intertwined; people typically
base their decisions on both direct experiences and indirect observations. Yet
only recently have researchers begun to explore how the two kinds of reciprocity
interact. So far, this research only addresses a single type of social dilemma,
the donation game, where the effects of individual behaviors are independent.
Instead, here we allow for all pairwise social dilemmas. By applying novel techniques
to generalize the theory of zero-determinant strategies, we establish an important
proof of principle: In all social dilemmas, socially optimal outcomes can be sustained
as an equilibrium, using either direct or indirect reciprocity, or arbitrary mixtures
thereof. These results neither require games to be repeated infinitely often,
nor that individual opinions are synchronized. In this way, we considerably generalize
the scope of models of reciprocity, and we build further bridges between the literatures
on direct and indirect reciprocity.'
acknowledgement: 'This work was supported by the European Research Council CoG 863818
(ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529:
E-DIRECT (to C.H.).'
article_number: pgaf154
article_processing_charge: Yes
article_type: original
author:
- first_name: Valentin
full_name: Hübner, Valentin
id: 2c8aa207-dc7d-11ea-9b2f-f22972ecd910
last_name: Hübner
orcid: 0009-0001-5009-4987
- first_name: Laura
full_name: Schmid, Laura
id: 38B437DE-F248-11E8-B48F-1D18A9856A87
last_name: Schmid
orcid: 0000-0002-6978-7329
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Hübner V, Schmid L, Hilbe C, Chatterjee K. Stable strategies of direct and
indirect reciprocity across all social dilemmas. PNAS Nexus. 2025;4(5).
doi:10.1093/pnasnexus/pgaf154
apa: Hübner, V., Schmid, L., Hilbe, C., & Chatterjee, K. (2025). Stable strategies
of direct and indirect reciprocity across all social dilemmas. PNAS Nexus.
Oxford University Press. https://doi.org/10.1093/pnasnexus/pgaf154
chicago: Hübner, Valentin, Laura Schmid, Christian Hilbe, and Krishnendu Chatterjee.
“Stable Strategies of Direct and Indirect Reciprocity across All Social Dilemmas.”
PNAS Nexus. Oxford University Press, 2025. https://doi.org/10.1093/pnasnexus/pgaf154.
ieee: V. Hübner, L. Schmid, C. Hilbe, and K. Chatterjee, “Stable strategies of direct
and indirect reciprocity across all social dilemmas,” PNAS Nexus, vol.
4, no. 5. Oxford University Press, 2025.
ista: Hübner V, Schmid L, Hilbe C, Chatterjee K. 2025. Stable strategies of direct
and indirect reciprocity across all social dilemmas. PNAS Nexus. 4(5), pgaf154.
mla: Hübner, Valentin, et al. “Stable Strategies of Direct and Indirect Reciprocity
across All Social Dilemmas.” PNAS Nexus, vol. 4, no. 5, pgaf154, Oxford
University Press, 2025, doi:10.1093/pnasnexus/pgaf154.
short: V. Hübner, L. Schmid, C. Hilbe, K. Chatterjee, PNAS Nexus 4 (2025).
corr_author: '1'
date_created: 2025-06-15T22:01:30Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2026-04-07T12:30:56Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1093/pnasnexus/pgaf154
ec_funded: 1
external_id:
pmid:
- '40417077'
file:
- access_level: open_access
checksum: efd6648db3fc3ea0cdd7155d667e5f11
content_type: application/pdf
creator: dernst
date_created: 2025-06-23T08:09:50Z
date_updated: 2025-06-23T08:09:50Z
file_id: '19867'
file_name: 2025_PNASNexus_Huebner.pdf
file_size: 2551195
relation: main_file
success: 1
file_date_updated: 2025-06-23T08:09:50Z
has_accepted_license: '1'
intvolume: ' 4'
issue: '5'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc/4.0/
month: '05'
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: PNAS Nexus
publication_identifier:
eissn:
- 2752-6542
publication_status: published
publisher: Oxford University Press
quality_controlled: '1'
related_material:
record:
- id: '19903'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Stable strategies of direct and indirect reciprocity across all social dilemmas
tmp:
image: /images/cc_by_nc.png
legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
short: CC BY-NC (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4
year: '2025'
...