---
OA_place: publisher
OA_type: gold
PlanS_conform: '1'
_id: '22102'
abstract:
- lang: eng
text: 'Differential privacy (DP) has established itself as one of the standards
for ensuring privacy of individual data. However, reasoning about DP is a challenging
and error-prone task, hence methods for formal verification and refutation of
DP properties have received significant interest in recent years. In this work,
we present a novel method for automated formal refutation of є-DP. Our method
refutes є-DP by searching for a pair of inputs together with a non-negative function
over outputs whose expected value on these two inputs differs by a significant
amount. The two inputs and the non-negative function over outputs are computed
simultaneously, by utilizing upper expectation supermartingales and lower expectation
submartingales from probabilistic program analysis, which we leverage to introduce
a sound and complete proof rule for є-DP refutation. To the best of our knowledge,
our method is the first method for є-DP refutation to offer the following four
desirable features: (1) it is fully automated, (2) it is applicable to stochastic
mechanisms with sampling instructions from both discrete and continuous distributions,
(3) it provides soundness guarantees, and (4) it provides semi-completeness guarantees.
Our experiments show that our prototype tool SuperDP achieves superior performance
compared to the state of the art and manages to refute є-DP for a number of challenging
examples collected from the literature, including ones that were out of the reach
of prior methods.'
acknowledgement: "The authors would like to thank Petr Novotný for valuable discussions
that helped shape this work.\r\nThis research was supported by the Singapore Ministry
of Education (MOE) Academic Research\r\nFund (AcRF) Tier 1 grant (Proposal ID: 25-SIS-SMU-009),
Vienna Science and Technology Fund\r\n(WWTF), State of Lower Austria [Grant ID 10.47379/ICT25017],
ERC CoG 863818 (ForM-SMArt),\r\nand Austrian Science Fund (FWF) 10.55776/COE12."
article_number: '218'
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady E, Zikelic D. SuperDP: Differential privacy refutation
via supermartingales. Proceedings of the ACM on Programming Languages.
2026;10(PLDI). doi:10.1145/3808296'
apa: 'Chatterjee, K., Goharshady, E., & Zikelic, D. (2026). SuperDP: Differential
privacy refutation via supermartingales. Proceedings of the ACM on Programming
Languages. Association for Computing Machinery. https://doi.org/10.1145/3808296'
chicago: 'Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP:
Differential Privacy Refutation via Supermartingales.” Proceedings of the ACM
on Programming Languages. Association for Computing Machinery, 2026. https://doi.org/10.1145/3808296.'
ieee: 'K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential privacy
refutation via supermartingales,” Proceedings of the ACM on Programming Languages,
vol. 10, no. PLDI. Association for Computing Machinery, 2026.'
ista: 'Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy
refutation via supermartingales. Proceedings of the ACM on Programming Languages.
10(PLDI), 218.'
mla: 'Chatterjee, Krishnendu, et al. “SuperDP: Differential Privacy Refutation via
Supermartingales.” Proceedings of the ACM on Programming Languages, vol.
10, no. PLDI, 218, Association for Computing Machinery, 2026, doi:10.1145/3808296.'
short: K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming
Languages 10 (2026).
corr_author: '1'
das_tickbox: '1'
dataavailabilitystatement: "The artifact supporting the findings of this study, which
includes the underlying datasets, software\r\ncode, and experiments, is publicly
available in Zenodo https://zenodo.org/records/19399862."
date_created: 2026-06-21T22:02:59Z
date_published: 2026-06-08T00:00:00Z
date_updated: 2026-06-24T06:39:37Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3808296
ec_funded: 1
external_id:
arxiv:
- '2603.26215'
file:
- access_level: open_access
checksum: 994bf21d6269dabccf1e1091e02962c5
content_type: application/pdf
creator: dernst
date_created: 2026-06-24T06:19:56Z
date_updated: 2026-06-24T06:19:56Z
file_id: '22135'
file_name: 2026_ProcACMProgrammingLanguages_Chatterjee.pdf
file_size: 858595
relation: main_file
success: 1
file_date_updated: 2026-06-24T06:19:56Z
has_accepted_license: '1'
intvolume: ' 10'
issue: PLDI
keyword:
- Static Program Analysis
- Differential Privacy
- Probabilistic Programming
- Martingales
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '22134'
relation: research_data
status: public
researchdata_availability: yes
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'SuperDP: Differential privacy refutation via supermartingales'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '22134'
abstract:
- lang: eng
text: This artifact provides the source code, benchmarks, and scripts necessary
to build and reproduce the experimental results for `SuperDP` (Accepted at PLDI
2026). It also includes instructions for running the tool on user-provided inputs.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady E, Zikelic D. SuperDP: Differential Privacy Refutation
via Supermartingales. 2026. doi:10.5281/ZENODO.18930113'
apa: 'Chatterjee, K., Goharshady, E., & Zikelic, D. (2026). SuperDP: Differential
Privacy Refutation via Supermartingales. Zenodo. https://doi.org/10.5281/ZENODO.18930113'
chicago: 'Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP:
Differential Privacy Refutation via Supermartingales.” Zenodo, 2026. https://doi.org/10.5281/ZENODO.18930113.'
ieee: 'K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential Privacy
Refutation via Supermartingales.” Zenodo, 2026.'
ista: 'Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential Privacy
Refutation via Supermartingales, Zenodo, 10.5281/ZENODO.18930113.'
mla: 'Chatterjee, Krishnendu, et al. SuperDP: Differential Privacy Refutation
via Supermartingales. Zenodo, 2026, doi:10.5281/ZENODO.18930113.'
short: K. Chatterjee, E. Goharshady, D. Zikelic, (2026).
corr_author: '1'
date_created: 2026-06-24T06:25:29Z
date_published: 2026-03-09T00:00:00Z
date_updated: 2026-06-24T06:39:38Z
day: '09'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.5281/ZENODO.18930113
has_accepted_license: '1'
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/ZENODO.18930113
month: '03'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '22102'
relation: used_in_publication
status: public
status: public
title: 'SuperDP: Differential Privacy Refutation via Supermartingales'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '21717'
abstract:
- lang: eng
text: Robust Markov Decision Processes (RMDPs) generalize classical MDPs that consider
uncertainties in transition probabilities by defining a set of possible transition
functions. An objective is a set of runs (or infinite trajectories) of the RMDP,
and the value for an objective is the maximal probability that the agent can guarantee
against the adversarial environment. We consider (a) reachability objectives,
where given a target set of states, the goal is to eventually arrive at one of
them; and (b) parity objectives, which are a canonical representation for ω-regular
objectives. The qualitative analysis problem asks whether the objective can be
ensured with probability 1. In this work, we study the qualitative problem for
reachability and parity objectives on RMDPs without making any assumption over
the structures of the RMDPs, e.g., unichain or aperiodic. Our contributions are
twofold. We first present efficient algorithms with oracle access to uncertainty
sets that solve qualitative problems of reachability and parity objectives. We
then report experimental results demonstrating the effectiveness of our oracle-based
approach on classical RMDP examples from the literature scaling up to thousands
of states.
acknowledgement: This work was supported by ERC CoG 863818 (ForMSMArt) and Austrian
Science Fund (FWF) 10.55776/COE12. We also thank Hossein Zakerinia for his helpful
feedback.
article_processing_charge: No
arxiv: 1
author:
- first_name: Ali
full_name: Asadi, Ali
id: 02d96aae-000e-11ec-b801-cadd0a5eefbb
last_name: Asadi
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
orcid: 0009-0007-5253-9170
- first_name: Ali
full_name: Shafiee, Ali
id: 2783031a-7378-11f0-b2d0-f17f1db2ebad
last_name: Shafiee
citation:
ama: 'Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. Qualitative analysis
of ω-regular objectives on robust MDPs. In: Proceedings of the 40th AAAI Conference
on Artificial Intelligence. Vol 40. Association for the Advancement of Artificial
Intelligence; 2026:36137-36145. doi:10.1609/aaai.v40i43.40931'
apa: 'Asadi, A., Chatterjee, K., Goharshady, E., Karrabi, M., & Shafiee, A.
(2026). Qualitative analysis of ω-regular objectives on robust MDPs. In Proceedings
of the 40th AAAI Conference on Artificial Intelligence (Vol. 40, pp. 36137–36145).
Singapore, Singapore: Association for the Advancement of Artificial Intelligence.
https://doi.org/10.1609/aaai.v40i43.40931'
chicago: Asadi, Ali, Krishnendu Chatterjee, Ehsan Goharshady, Mehrdad Karrabi, and
Ali Shafiee. “Qualitative Analysis of ω-Regular Objectives on Robust MDPs.” In
Proceedings of the 40th AAAI Conference on Artificial Intelligence, 40:36137–45.
Association for the Advancement of Artificial Intelligence, 2026. https://doi.org/10.1609/aaai.v40i43.40931.
ieee: A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, and A. Shafiee, “Qualitative
analysis of ω-regular objectives on robust MDPs,” in Proceedings of the 40th
AAAI Conference on Artificial Intelligence, Singapore, Singapore, 2026, vol.
40, no. 43, pp. 36137–36145.
ista: 'Asadi A, Chatterjee K, Goharshady E, Karrabi M, Shafiee A. 2026. Qualitative
analysis of ω-regular objectives on robust MDPs. Proceedings of the 40th AAAI
Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence
vol. 40, 36137–36145.'
mla: Asadi, Ali, et al. “Qualitative Analysis of ω-Regular Objectives on Robust
MDPs.” Proceedings of the 40th AAAI Conference on Artificial Intelligence,
vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026,
pp. 36137–45, doi:10.1609/aaai.v40i43.40931.
short: A. Asadi, K. Chatterjee, E. Goharshady, M. Karrabi, A. Shafiee, in:, Proceedings
of the 40th AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2026, pp. 36137–36145.
conference:
end_date: 2026-01-27
location: Singapore, Singapore
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2026-01-20
date_created: 2026-04-12T22:01:50Z
date_published: 2026-03-14T00:00:00Z
date_updated: 2026-05-04T11:38:56Z
day: '14'
department:
- _id: KrCh
- _id: GradSch
doi: 10.1609/aaai.v40i43.40931
ec_funded: 1
external_id:
arxiv:
- '2505.04539'
intvolume: ' 40'
issue: '43'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2505.04539
month: '03'
oa: 1
oa_version: Preprint
page: 36137-36145
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 40th AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: Qualitative analysis of ω-regular objectives on robust MDPs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 40
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '21722'
abstract:
- lang: eng
text: 'Partially observable Markov decision processes (POMDPs) are a central model
for uncertainty in sequential decision making. The most basic objective is the
reachability objective, where a target set must be eventually visited, and the
more general parity objectives can model all omega-regular specifications. For
such objectives, the computational analysis problems are the following: (a) qualitative
analysis that asks whether the objective can be satisfied with probability 1 (almost-sure
winning) or probability arbitrarily close to 1 (limit-sure winning); and (b) quantitative
analysis that asks for the approximation of the optimal probability of satisfying
the objective. For general POMDPs, almost-sure analysis for reachability objectives
is EXPTIME-complete, but limit-sure and quantitative analyses for reachability
objectives are undecidable; almost-sure, limit-sure, and quantitative analyses
for parity objectives are all undecidable. A special class of POMDPs, called revealing
POMDPs, has been studied recently in several works, and for this subclass the
almost-sure analysis for parity objectives was shown to be EXPTIME-complete. In
this work, we show that for revealing POMDPs the limit-sure analysis for parity
objectives is EXPTIME-complete, and even the quantitative analysis for parity
objectives can be achieved in EXPTIME.'
acknowledgement: "This work was partially supported by the ANRT under the French CIFRE
Ph.D program in collaboration between NyxAir and Paris-Dauphine University (Contract:
CIFRE N° 2022/0513), by the French Agence Nationale de la Recherche (ANR) under
reference ANR-21-CE40-\r\n0020 (CONVERGENCE project), by Austrian Science Fund (FWF)
10.55776/COE12, and by the ERC CoG 863818 (ForM-SMArt) grant."
article_processing_charge: No
arxiv: 1
author:
- first_name: Ali
full_name: Asadi, Ali
id: 02d96aae-000e-11ec-b801-cadd0a5eefbb
last_name: Asadi
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: David
full_name: Lurie, David
id: 579a6c20-34cf-11f1-acbd-8c2f19cdb4da
last_name: Lurie
- first_name: Raimundo J
full_name: Saona Urmeneta, Raimundo J
id: BD1DF4C4-D767-11E9-B658-BC13E6697425
last_name: Saona Urmeneta
orcid: 0000-0001-5103-038X
citation:
ama: 'Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. Revealing POMDPs: Qualitative
and quantitative analysis for parity objectives. In: Proceedings of the AAAI
Conference on Artificial Intelligence. Vol 40. Association for the Advancement
of Artificial Intelligence; 2026:36146-36154. doi:10.1609/aaai.v40i43.40932'
apa: 'Asadi, A., Chatterjee, K., Lurie, D., & Saona Urmeneta, R. J. (2026).
Revealing POMDPs: Qualitative and quantitative analysis for parity objectives.
In Proceedings of the AAAI Conference on Artificial Intelligence (Vol.
40, pp. 36146–36154). Singapore, Singapore: Association for the Advancement of
Artificial Intelligence. https://doi.org/10.1609/aaai.v40i43.40932'
chicago: 'Asadi, Ali, Krishnendu Chatterjee, David Lurie, and Raimundo J Saona Urmeneta.
“Revealing POMDPs: Qualitative and Quantitative Analysis for Parity Objectives.”
In Proceedings of the AAAI Conference on Artificial Intelligence, 40:36146–54.
Association for the Advancement of Artificial Intelligence, 2026. https://doi.org/10.1609/aaai.v40i43.40932.'
ieee: 'A. Asadi, K. Chatterjee, D. Lurie, and R. J. Saona Urmeneta, “Revealing POMDPs:
Qualitative and quantitative analysis for parity objectives,” in Proceedings
of the AAAI Conference on Artificial Intelligence, Singapore, Singapore, 2026,
vol. 40, no. 43, pp. 36146–36154.'
ista: 'Asadi A, Chatterjee K, Lurie D, Saona Urmeneta RJ. 2026. Revealing POMDPs:
Qualitative and quantitative analysis for parity objectives. Proceedings of the
AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence
vol. 40, 36146–36154.'
mla: 'Asadi, Ali, et al. “Revealing POMDPs: Qualitative and Quantitative Analysis
for Parity Objectives.” Proceedings of the AAAI Conference on Artificial Intelligence,
vol. 40, no. 43, Association for the Advancement of Artificial Intelligence, 2026,
pp. 36146–54, doi:10.1609/aaai.v40i43.40932.'
short: A. Asadi, K. Chatterjee, D. Lurie, R.J. Saona Urmeneta, in:, Proceedings
of the AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2026, pp. 36146–36154.
conference:
end_date: 2026-01-27
location: Singapore, Singapore
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2026-01-20
corr_author: '1'
date_created: 2026-04-12T22:01:52Z
date_published: 2026-03-14T00:00:00Z
date_updated: 2026-05-04T11:44:14Z
day: '14'
department:
- _id: KrCh
doi: 10.1609/aaai.v40i43.40932
ec_funded: 1
external_id:
arxiv:
- '2511.13134'
intvolume: ' 40'
issue: '43'
language:
- iso: eng
main_file_link:
- url: https://doi.org/10.48550/arXiv.2511.13134
month: '03'
oa_version: Preprint
page: 36146-36154
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Revealing POMDPs: Qualitative and quantitative analysis for parity objectives'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 40
year: '2026'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '22101'
abstract:
- lang: eng
text: "Evolutionary biology examines how the genetic and phenotypic composition\r\nof
populations changes over time. An important goal is to determine the\r\nfixation
probability of a single advantageous mutant that arises in a homogeneous\r\npopulation
of N residents. Many real populations experience environmental\r\ngradients that
cause mutations to be beneficial in some spatial\r\nregions but harmful in others.
Here, we study the fixation probability of a\r\nmutant placed on a simple one-dimensional
spatial structure that experiences\r\nsuch a gradient. The mutant’s fitness varies
linearly from1 − s to 1 + s, whereas\r\nthe resident fitness is constant and equal
to 1. The existing literature suggests\r\nthat such heterogeneity in the mutant’s
fitness should lead to a decrease in its\r\nfixation probability. However, in
this work, we find that small, non-negligible\r\ngradients (s < 1=√N) substantially
increase the fixation probability,while larger\r\ngradients (s > (log N)/√N) substantially
decrease it.Moreover, we quantify the\r\nstrength of this phenomenon analytically
and we precisely delimit the range of\r\nthe gradients for which it occurs. Our
computer simulations closely match\r\nthose findings. Altogether, our results
indicate that subjecting a simple\r\npopulation structure to natural environmental
conditions can produce strong\r\ncounterintuitive effects."
acknowledgement: "J.S. and K.C. were supported by the European Research Council (ERC)\r\nCoG
863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/\r\nCOE12. J.T. was
supported by GAČR grant 25-17377S and by Charles\r\nUniv. projects UNCE 24/SCI/008
and PRIMUS 24/SCI/012."
article_number: '5325'
article_processing_charge: Yes
article_type: original
author:
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Hossein
full_name: Nemati, Hossein
last_name: Nemati
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Kamran
full_name: Kaveh, Kamran
last_name: Kaveh
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Svoboda J, Nemati H, Tkadlec J, Kaveh K, Chatterjee K. The effect of the fitness
gradient on fixation probability. Nature Communications. 2026;17. doi:10.1038/s41467-026-71777-2
apa: Svoboda, J., Nemati, H., Tkadlec, J., Kaveh, K., & Chatterjee, K. (2026).
The effect of the fitness gradient on fixation probability. Nature Communications.
Springer Nature. https://doi.org/10.1038/s41467-026-71777-2
chicago: Svoboda, Jakub, Hossein Nemati, Josef Tkadlec, Kamran Kaveh, and Krishnendu
Chatterjee. “The Effect of the Fitness Gradient on Fixation Probability.” Nature
Communications. Springer Nature, 2026. https://doi.org/10.1038/s41467-026-71777-2.
ieee: J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, and K. Chatterjee, “The effect
of the fitness gradient on fixation probability,” Nature Communications,
vol. 17. Springer Nature, 2026.
ista: Svoboda J, Nemati H, Tkadlec J, Kaveh K, Chatterjee K. 2026. The effect of
the fitness gradient on fixation probability. Nature Communications. 17, 5325.
mla: Svoboda, Jakub, et al. “The Effect of the Fitness Gradient on Fixation Probability.”
Nature Communications, vol. 17, 5325, Springer Nature, 2026, doi:10.1038/s41467-026-71777-2.
short: J. Svoboda, H. Nemati, J. Tkadlec, K. Kaveh, K. Chatterjee, Nature Communications
17 (2026).
corr_author: '1'
das_tickbox: '0'
dataavailabilitystatement: Correspondence and requests for materials should be addressed
to Krishnendu Chatterjee.
date_created: 2026-06-21T22:02:59Z
date_published: 2026-12-01T00:00:00Z
date_updated: 2026-06-24T07:53:53Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/s41467-026-71777-2
ec_funded: 1
external_id:
pmid:
- '41997932'
file:
- access_level: open_access
checksum: b660048bb271f24d6763803e247d5c32
content_type: application/pdf
creator: dernst
date_created: 2026-06-24T06:50:24Z
date_updated: 2026-06-24T06:50:24Z
file_id: '22136'
file_name: 2026_NatureComm_Svoboda.pdf
file_size: 1068919
relation: main_file
success: 1
file_date_updated: 2026-06-24T06:50:24Z
has_accepted_license: '1'
intvolume: ' 17'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Nature Communications
publication_identifier:
eissn:
- 2041-1723
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: yes
title: The effect of the fitness gradient on fixation probability
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 17
year: '2026'
...
---
APC_amount: 3003,56 EUR
OA_place: publisher
OA_type: hybrid
_id: '20857'
abstract:
- lang: eng
text: 'Evolutionary games provide a flexible mathematical framework for many problems
in biology and social evolution. Prisoners’ dilemma, and in particular, the important
special case of donation games, represents social dilemmas where cooperation is
mutually beneficial, yet defection is preferred by selfish agents. In evolutionary
games on networks, the agents interact over a population structure. The existence
of population structures that promote cooperative behavior is a fascinating and
active research topic. Previous research establishes structures promoting cooperation
in the limit of weak selection where the benefit-to-cost ratio β exceeds 1.5.
The existence of such structures for medium and strong selection for 1 < ß < 2
and for weak selection for 1 < ß < 1.5 has been a long-standing open question.
First, we answer the open questions in the affirmative: For every selection strength
and every ß > 1, we construct networks promoting cooperation. Second, we present
a robustness result with respect to β and selection strength: Our structures promote
cooperation for a range of these parameter values rather than specific parameter
values. Finally, we supplement our theoretical results with simulation results
on small population structures that show the effectiveness of our construction
over well-studied population structures.'
acknowledgement: J.S. and K.C. were supported by the European Research Council CoG
863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12.
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Svoboda J, Chatterjee K. Promoters of cooperation in evolutionary games. Proceedings
of the National Academy of Sciences. 2025;122(51):e2524109122. doi:10.1073/pnas.2524109122
apa: Svoboda, J., & Chatterjee, K. (2025). Promoters of cooperation in evolutionary
games. Proceedings of the National Academy of Sciences. National Academy
of Sciences. https://doi.org/10.1073/pnas.2524109122
chicago: Svoboda, Jakub, and Krishnendu Chatterjee. “Promoters of Cooperation in
Evolutionary Games.” Proceedings of the National Academy of Sciences. National
Academy of Sciences, 2025. https://doi.org/10.1073/pnas.2524109122.
ieee: J. Svoboda and K. Chatterjee, “Promoters of cooperation in evolutionary games,”
Proceedings of the National Academy of Sciences, vol. 122, no. 51. National
Academy of Sciences, p. e2524109122, 2025.
ista: Svoboda J, Chatterjee K. 2025. Promoters of cooperation in evolutionary games.
Proceedings of the National Academy of Sciences. 122(51), e2524109122.
mla: Svoboda, Jakub, and Krishnendu Chatterjee. “Promoters of Cooperation in Evolutionary
Games.” Proceedings of the National Academy of Sciences, vol. 122, no.
51, National Academy of Sciences, 2025, p. e2524109122, doi:10.1073/pnas.2524109122.
short: J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences
122 (2025) e2524109122.
corr_author: '1'
date_created: 2025-12-28T23:01:26Z
date_published: 2025-12-15T00:00:00Z
date_updated: 2026-05-20T08:13:17Z
day: '15'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1073/pnas.2524109122
ec_funded: 1
external_id:
pmid:
- '41397136'
file:
- access_level: open_access
checksum: dd50b62a1efc28c0133fe9c11dbee53c
content_type: application/pdf
creator: dernst
date_created: 2025-12-29T09:36:50Z
date_updated: 2025-12-29T09:36:50Z
file_id: '20860'
file_name: 2025_PNAS_Svoboda.pdf
file_size: 2308124
relation: main_file
success: 1
file_date_updated: 2025-12-29T09:36:50Z
has_accepted_license: '1'
intvolume: ' 122'
issue: '51'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: e2524109122
pmid: 1
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the National Academy of Sciences
publication_identifier:
eissn:
- 1091-6490
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
scopus_import: '1'
status: public
title: Promoters of cooperation in evolutionary games
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 122
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '21268'
abstract:
- lang: eng
text: "We consider multiple-environment Markov decision processes (MEMDP), which
consist of a finite set of MDPs over the same state space, representing different
scenarios of transition structure and probability. The value of a strategy is
the probability to satisfy the objective, here a parity objective, in the worst-case
scenario, and the value of an MEMDP is the supremum of the values achievable by
a strategy.\r\nWe show that deciding whether the value is 1 is a PSPACE-complete
problem, and even in P when the number of environments is fixed, along with new
insights to the almost-sure winning problem, which is to decide if there exists
a strategy with value 1. Pure strategies are sufficient for theses problems, whereas
randomization is necessary in general when the value is smaller than 1. We present
an algorithm to approximate the value, running in double exponential space. Our
results are in contrast to the related model of partially-observable MDPs where
all these problems are known to be undecidable."
acknowledgement: "Krishnendu Chatterjee: ERC CoG 863818 (ForM-SMArt) and Austrian
Science Fund\r\n(FWF) 10.55776/COE12. Jean-François Raskin: PDR Weave project FORM-LEARN-POMDP
funded by FNRS and DFG, and the support of the Fondation ULB. Ocan Sankur: ANR BisoUS
(ANR-22-CE48-0012) and ANR EpiRL (ANR-22-CE23-0029)."
alternative_title:
- LIPIcs
article_number: '150'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Jean-Francois
full_name: Raskin, Jean-Francois
last_name: Raskin
- first_name: Ocan
full_name: Sankur, Ocan
last_name: Sankur
citation:
ama: 'Chatterjee K, Doyen L, Raskin J-F, Sankur O. The value problem for multiple-environment
MDPs with parity objective. In: 52nd International Colloquium on Automata,
Languages, and Programming. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2025. doi:10.4230/LIPIcs.ICALP.2025.150'
apa: 'Chatterjee, K., Doyen, L., Raskin, J.-F., & Sankur, O. (2025). The value
problem for multiple-environment MDPs with parity objective. In 52nd International
Colloquium on Automata, Languages, and Programming. Aarhus, Denmark: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2025.150'
chicago: Chatterjee, Krishnendu, Laurent Doyen, Jean-Francois Raskin, and Ocan Sankur.
“The Value Problem for Multiple-Environment MDPs with Parity Objective.” In 52nd
International Colloquium on Automata, Languages, and Programming. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPIcs.ICALP.2025.150.
ieee: K. Chatterjee, L. Doyen, J.-F. Raskin, and O. Sankur, “The value problem for
multiple-environment MDPs with parity objective,” in 52nd International Colloquium
on Automata, Languages, and Programming, Aarhus, Denmark, 2025.
ista: 'Chatterjee K, Doyen L, Raskin J-F, Sankur O. 2025. The value problem for
multiple-environment MDPs with parity objective. 52nd International Colloquium
on Automata, Languages, and Programming. ICALP: Automata, Languages and Programming,
LIPIcs, , 150.'
mla: Chatterjee, Krishnendu, et al. “The Value Problem for Multiple-Environment
MDPs with Parity Objective.” 52nd International Colloquium on Automata, Languages,
and Programming, 150, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025,
doi:10.4230/LIPIcs.ICALP.2025.150.
short: K. Chatterjee, L. Doyen, J.-F. Raskin, O. Sankur, in:, 52nd International
Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025.
conference:
end_date: 2025-07-11
location: Aarhus, Denmark
name: 'ICALP: Automata, Languages and Programming'
start_date: 2025-07-08
corr_author: '1'
date_created: 2026-02-17T07:49:17Z
date_published: 2025-07-30T00:00:00Z
date_updated: 2026-02-18T07:53:26Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2025.150
ec_funded: 1
external_id:
arxiv:
- '2504.15960'
file:
- access_level: open_access
checksum: 4477a7fd4fbf0ba6c8e9b15683b5a6b8
content_type: application/pdf
creator: dernst
date_created: 2026-02-18T07:50:56Z
date_updated: 2026-02-18T07:50:56Z
file_id: '21313'
file_name: 2025_LIPIcs_Chatterjee.pdf
file_size: 1075724
relation: main_file
success: 1
file_date_updated: 2026-02-18T07:50:56Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 52nd International Colloquium on Automata, Languages, and Programming
publication_identifier:
isbn:
- '9783959773720'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: The value problem for multiple-environment MDPs with parity objective
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '21281'
abstract:
- lang: eng
text: "A strategy profile in a multi-player game is a Nash equilibrium if no player
can unilaterally deviate to achieve a strictly better payoff. A profile is an
ε-Nash equilibrium if no player can gain more than ε by unilaterally deviating
from their strategy. In this work, we use ε-Nash equilibria to approximate the
computation of Nash equilibria. Specifically, we focus on turn-based, multiplayer
stochastic games played on graphs, where players are restricted to stationary
strategies - strategies that use randomness but not memory.\r\nThe problem of
deciding the constrained existence of stationary Nash equilibria - where each
player’s payoff must lie within a given interval - is known to be ∃ℝ-complete
in such a setting (Hansen and Sølvsten, 2020). We extend this line of work to
stationary ε-Nash equilibria and present an algorithm that solves the following
promise problem: given a game with a Nash equilibrium satisfying the constraints,
compute an ε-Nash equilibrium that ε-satisfies those same constraints - satisfies
the constraints up to an ε additive error. Our algorithm runs in FNP^NP time.\r\nTo
achieve this, we first show that if a constrained Nash equilibrium exists, then
one exists where the non-zero probabilities are at least an inverse of a double-exponential
in the input. We further prove that such a strategy can be encoded using floating-point
representations, as in the work of Frederiksen and Miltersen (2013), which finally
gives us our FNP^NP algorithm. \r\nWe further show that the decision version of
the promise problem is NP-hard. Finally, we show a partial tightness result by
proving a lower bound for such techniques: if a constrained Nash equilibrium exists,
then there must be one where the probabilities in the strategies are double-exponentially
small."
acknowledgement: "This work is a part of project VAMOS that has received funding from
the European\r\nResearch Council (ERC), grant agreement No 101020093.\r\n"
alternative_title:
- LIPIcs
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Ali
full_name: Asadi, Ali
id: 02d96aae-000e-11ec-b801-cadd0a5eefbb
last_name: Asadi
- first_name: Leonard
full_name: Brice, Leonard
last_name: Brice
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Asadi A, Brice L, Chatterjee K, Thejaswini KS. ε-stationary Nash equilibria
in multi-player stochastic graph games. In: 45th Annual Conference on Foundations
of Software Technology and Theoretical Computer Science. Vol 360. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2025:9:1-9:17. doi:10.4230/lipics.fsttcs.2025.9'
apa: 'Asadi, A., Brice, L., Chatterjee, K., & Thejaswini, K. S. (2025). ε-stationary
Nash equilibria in multi-player stochastic graph games. In 45th Annual Conference
on Foundations of Software Technology and Theoretical Computer Science (Vol.
360, p. 9:1-9:17). Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/lipics.fsttcs.2025.9'
chicago: Asadi, Ali, Leonard Brice, Krishnendu Chatterjee, and K. S. Thejaswini.
“ε-Stationary Nash Equilibria in Multi-Player Stochastic Graph Games.” In 45th
Annual Conference on Foundations of Software Technology and Theoretical Computer
Science, 360:9:1-9:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025. https://doi.org/10.4230/lipics.fsttcs.2025.9.
ieee: A. Asadi, L. Brice, K. Chatterjee, and K. S. Thejaswini, “ε-stationary Nash
equilibria in multi-player stochastic graph games,” in 45th Annual Conference
on Foundations of Software Technology and Theoretical Computer Science, Pilani,
India, 2025, vol. 360, p. 9:1-9:17.
ista: 'Asadi A, Brice L, Chatterjee K, Thejaswini KS. 2025. ε-stationary Nash equilibria
in multi-player stochastic graph games. 45th Annual Conference on Foundations
of Software Technology and Theoretical Computer Science. FSTTCS: Conference on
Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol.
360, 9:1-9:17.'
mla: Asadi, Ali, et al. “ε-Stationary Nash Equilibria in Multi-Player Stochastic
Graph Games.” 45th Annual Conference on Foundations of Software Technology
and Theoretical Computer Science, vol. 360, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025, p. 9:1-9:17, doi:10.4230/lipics.fsttcs.2025.9.
short: A. Asadi, L. Brice, K. Chatterjee, K.S. Thejaswini, in:, 45th Annual Conference
on Foundations of Software Technology and Theoretical Computer Science, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 9:1-9:17.
conference:
end_date: 2025-12-19
location: Pilani, India
name: 'FSTTCS: Conference on Foundations of Software Technology and Theoretical
Computer Science'
start_date: 2025-12-17
corr_author: '1'
date_created: 2026-02-17T08:27:14Z
date_published: 2025-12-09T00:00:00Z
date_updated: 2026-02-19T09:39:15Z
day: '09'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
doi: 10.4230/lipics.fsttcs.2025.9
ec_funded: 1
external_id:
arxiv:
- '2508.15356'
file:
- access_level: open_access
checksum: a66343e3ccc4a9cc5bc699c03d5764ff
content_type: application/pdf
creator: dernst
date_created: 2026-02-18T09:13:25Z
date_updated: 2026-02-18T09:13:25Z
file_id: '21316'
file_name: 2025_FSTTCS_Asadi.pdf
file_size: 1054007
relation: main_file
success: 1
file_date_updated: 2026-02-18T09:13:25Z
has_accepted_license: '1'
intvolume: ' 360'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: 9:1-9:17
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 45th Annual Conference on Foundations of Software Technology and Theoretical
Computer Science
publication_identifier:
isbn:
- '9783959774062'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
status: public
title: ε-stationary Nash equilibria in multi-player stochastic graph games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 360
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '21412'
abstract:
- lang: eng
text: "Payment channel networks (PCNs) are a promising technology that alleviates
blockchain scalability by shifting the transaction load from the blockchain to
the PCN. Nevertheless, the network topology has to be carefully designed to maximise
the transaction throughput in PCNs. Additionally, users in PCNs also have to make
optimal decisions on which transactions to forward and which to reject to prolong
the lifetime of their channels. In this work, we consider an input sequence of
transactions over p parties. Each transaction consists of a transaction size,
source, and target, and can be either accepted or rejected (entailing a cost).
The goal is to design a PCN topology among the p cooperating parties, along with
the channel capacities, and then output a decision for each transaction in the
sequence to minimise the cost of creating and augmenting channels, as well as
the cost of rejecting transactions. Our main contribution is an \U0001D4AA(p)
approximation algorithm for the problem with p parties. We further show that with
some assumptions on the distribution of transactions, we can reduce the approximation
ratio to \U0001D4AA(√p). We complement our theoretical analysis with an empirical
study of our assumptions and approach in the context of the Lightning Network."
acknowledgement: "Chatterjee, Krishnendu: European Research Council CoG 863818 (ForM-SMArt)
and Austrian Science Fund 10.55776/COE12.\r\nKřišťan, Jan Matyáš: Czech Science
Foundation Grant no. 24-12046S.\r\nSchmid, Stefan: German Research Foundation (DFG)
project ReNO (SPP 2378) from 2023-2027.\r\nSvoboda, Jakub: European Research Council
CoG 863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.\r\nYeo, Michelle:
MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms)."
alternative_title:
- LIPIcs
article_number: '23'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Jan Matyáš
full_name: Křišťan, Jan Matyáš
last_name: Křišťan
- first_name: Stefan
full_name: Schmid, Stefan
last_name: Schmid
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Michelle X
full_name: Yeo, Michelle X
id: 2D82B818-F248-11E8-B48F-1D18A9856A87
last_name: Yeo
orcid: 0009-0001-3676-4809
citation:
ama: 'Chatterjee K, Křišťan JM, Schmid S, Svoboda J, Yeo MX. Boosting payment channel
network liquidity with topology optimization and transaction selection. In: 39th
International Symposium on Distributed Computing. Vol 356. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.DISC.2025.23'
apa: 'Chatterjee, K., Křišťan, J. M., Schmid, S., Svoboda, J., & Yeo, M. X.
(2025). Boosting payment channel network liquidity with topology optimization
and transaction selection. In 39th International Symposium on Distributed Computing
(Vol. 356). Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.DISC.2025.23'
chicago: Chatterjee, Krishnendu, Jan Matyáš Křišťan, Stefan Schmid, Jakub Svoboda,
and Michelle X Yeo. “Boosting Payment Channel Network Liquidity with Topology
Optimization and Transaction Selection.” In 39th International Symposium on
Distributed Computing, Vol. 356. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025. https://doi.org/10.4230/LIPIcs.DISC.2025.23.
ieee: K. Chatterjee, J. M. Křišťan, S. Schmid, J. Svoboda, and M. X. Yeo, “Boosting
payment channel network liquidity with topology optimization and transaction selection,”
in 39th International Symposium on Distributed Computing, Berlin, Germany,
2025, vol. 356.
ista: 'Chatterjee K, Křišťan JM, Schmid S, Svoboda J, Yeo MX. 2025. Boosting payment
channel network liquidity with topology optimization and transaction selection.
39th International Symposium on Distributed Computing. DISC: Symposium on Distributed
Computing, LIPIcs, vol. 356, 23.'
mla: Chatterjee, Krishnendu, et al. “Boosting Payment Channel Network Liquidity
with Topology Optimization and Transaction Selection.” 39th International Symposium
on Distributed Computing, vol. 356, 23, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025, doi:10.4230/LIPIcs.DISC.2025.23.
short: K. Chatterjee, J.M. Křišťan, S. Schmid, J. Svoboda, M.X. Yeo, in:, 39th International
Symposium on Distributed Computing, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025.
conference:
end_date: 2025-10-31
location: Berlin, Germany
name: 'DISC: Symposium on Distributed Computing'
start_date: 2025-10-27
date_created: 2026-03-08T23:01:46Z
date_published: 2025-10-22T00:00:00Z
date_updated: 2026-03-09T11:52:58Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.DISC.2025.23
ec_funded: 1
external_id:
arxiv:
- '2508.14524'
file:
- access_level: open_access
checksum: 8e3d1594365df60163d9df22158a37b1
content_type: application/pdf
creator: dernst
date_created: 2026-03-09T11:51:59Z
date_updated: 2026-03-09T11:51:59Z
file_id: '21418'
file_name: 2025_DISC_Chatterjee.pdf
file_size: 1130069
relation: main_file
success: 1
file_date_updated: 2026-03-09T11:51:59Z
has_accepted_license: '1'
intvolume: ' 356'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/1484.pdf
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 39th International Symposium on Distributed Computing
publication_identifier:
isbn:
- '9783959774024'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Boosting payment channel network liquidity with topology optimization and transaction
selection
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 356
year: '2025'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
PlanS_conform: '1'
_id: '21413'
abstract:
- lang: eng
text: "We present a general framework for applying learning algorithms and heuristical
guidance to the verification of Markov decision processes (MDPs).\r\nThe primary
goal of our techniques is to improve performance by avoiding an exhaustive exploration
of the state space, instead focussing on particularly relevant areas of the system,
guided by heuristics. Our work builds on the previous results of Br{á}zdil et
al., significantly extending it as well as refining several details and fixing
errors.\r\nThe presented framework focuses on probabilistic reachability, which
is a core problem in verification, and is instantiated in two distinct scenarios.\r\nThe
first assumes that full knowledge of the MDP is available, in particular precise
transition probabilities. It performs a heuristic-driven partial exploration of
the model, yielding precise lower and upper bounds on the required probability.
The second tackles the case where we may only sample the MDP without knowing the
exact transition dynamics. Here, we obtain probabilistic guarantees, again in
terms of both the lower and upper bounds, which provides efficient stopping criteria
for the approximation. In particular, the latter is an extension of statistical
model-checking (SMC) for unbounded properties in MDPs. In contrast to other related
approaches, we do not restrict our attention to time-bounded (finite-horizon)
or discounted properties, nor assume any particular structural properties of the
MDP."
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement AdG-267989 (QUAREM)*, AdG-246967 (VERIWARE)*, StG-279307
(Graph Games)*\r\n, CoG-863818 (ForM-SMArt), and AdG-834115 (FUN2MODEL), by the
EU FP7 project HIERATIC*, by the German Research Foundation (DFG) project 427755713
(GOPro), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE)* , S11407-N23
(RiSE)*\r\n, and P23499-N23* , by the Czech Science Foundation grant No P202/12/P612*
and GA23-06963S, by the MUNI Award in Science and Humanities (MUNI/I/1757/2021)
of the Grant\r\nAgency of Masaryk University, by EPSRC project EP/K038575/1*, and
by the Microsoft faculty fellows award*. A preliminary version of this article appeared
at ATVA 2014 [33]. The * indicates funding that supported that version."
article_number: '10'
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Marta
full_name: Kwiatkowska, Marta
last_name: Kwiatkowska
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Mateusz
full_name: Ujma, Mateusz
last_name: Ujma
citation:
ama: Brázdil T, Chatterjee K, Chmelik M, et al. Learning algorithms for verification
of Markov decision processes. TheoretiCS. 2025;4. doi:10.46298/theoretics.25.10
apa: Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska,
M., … Ujma, M. (2025). Learning algorithms for verification of Markov decision
processes. TheoretiCS. TheoretiCS Foundation. https://doi.org/10.46298/theoretics.25.10
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt,
Jan Kretinsky, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, and Mateusz
Ujma. “Learning Algorithms for Verification of Markov Decision Processes.” TheoretiCS.
TheoretiCS Foundation, 2025. https://doi.org/10.46298/theoretics.25.10.
ieee: T. Brázdil et al., “Learning algorithms for verification of Markov
decision processes,” TheoretiCS, vol. 4. TheoretiCS Foundation, 2025.
ista: Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M,
Meggendorfer T, Parker D, Ujma M. 2025. Learning algorithms for verification of
Markov decision processes. TheoretiCS. 4, 10.
mla: Brázdil, Tomáš, et al. “Learning Algorithms for Verification of Markov Decision
Processes.” TheoretiCS, vol. 4, 10, TheoretiCS Foundation, 2025, doi:10.46298/theoretics.25.10.
short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska,
T. Meggendorfer, D. Parker, M. Ujma, TheoretiCS 4 (2025).
date_created: 2026-03-08T23:01:46Z
date_published: 2025-04-01T00:00:00Z
date_updated: 2026-03-09T11:43:38Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.46298/theoretics.25.10
ec_funded: 1
external_id:
arxiv:
- '2403.09184'
file:
- access_level: open_access
checksum: 2ccf563ae577ee08d82baf752292ca7b
content_type: application/pdf
creator: dernst
date_created: 2026-03-09T11:39:59Z
date_updated: 2026-03-09T11:39:59Z
file_id: '21417'
file_name: 2026_TheoretiCS_Brazdil.pdf
file_size: 861607
relation: main_file
success: 1
file_date_updated: 2026-03-09T11:39:59Z
has_accepted_license: '1'
intvolume: ' 4'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
publication: TheoretiCS
publication_identifier:
eissn:
- 2751-4838
publication_status: published
publisher: TheoretiCS Foundation
quality_controlled: '1'
scopus_import: '1'
status: public
title: Learning algorithms for verification of Markov decision processes
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4
year: '2025'
...
---
OA_type: closed access
_id: '18529'
abstract:
- lang: eng
text: Temporal networks are obtained from time-dependent interactions among individuals,
whereas the interactions can be emails, phone calls, face-to-face meetings, or
work collaboration. In this article, a temporal game framework is established,
in which interactions among rational individuals are embedded into two-player
games in a time-dependent manner. This allows studying the time-dependent complexity
and variability of interactions, and the way they affect prosocial behaviors.
Based on this simple mathematical model, it is found that the level of cooperation
is promoted when the time of collaboration is equally limited for every individual.
This observation is confirmed by a series of systematic human experiments on over
1,400 subjects, forming a foundation for comprehensively describing human temporal
interactions in collaboration. The research results reveal an important incentive
for human cooperation, leading to a better understanding of a fascinating aspect
of human nature in society.
article_processing_charge: No
article_type: original
author:
- first_name: Yichao
full_name: Zhang, Yichao
last_name: Zhang
- first_name: Jiasheng
full_name: Wang, Jiasheng
last_name: Wang
- first_name: Guanghui
full_name: Wen, Guanghui
last_name: Wen
- first_name: Jihong
full_name: Guan, Jihong
last_name: Guan
- first_name: Shuigeng
full_name: Zhou, Shuigeng
last_name: Zhou
- first_name: Guanrong
full_name: Chen, Guanrong
last_name: Chen
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Matjaz
full_name: Perc, Matjaz
last_name: Perc
citation:
ama: Zhang Y, Wang J, Wen G, et al. Limitation of time promotes cooperation in structured
collaboration systems. IEEE Transactions on Network Science and Engineering.
2025;12(1):4-12. doi:10.1109/TNSE.2024.3481434
apa: Zhang, Y., Wang, J., Wen, G., Guan, J., Zhou, S., Chen, G., … Perc, M. (2025).
Limitation of time promotes cooperation in structured collaboration systems. IEEE
Transactions on Network Science and Engineering. IEEE. https://doi.org/10.1109/TNSE.2024.3481434
chicago: Zhang, Yichao, Jiasheng Wang, Guanghui Wen, Jihong Guan, Shuigeng Zhou,
Guanrong Chen, Krishnendu Chatterjee, and Matjaz Perc. “Limitation of Time Promotes
Cooperation in Structured Collaboration Systems.” IEEE Transactions on Network
Science and Engineering. IEEE, 2025. https://doi.org/10.1109/TNSE.2024.3481434.
ieee: Y. Zhang et al., “Limitation of time promotes cooperation in structured
collaboration systems,” IEEE Transactions on Network Science and Engineering,
vol. 12, no. 1. IEEE, pp. 4–12, 2025.
ista: Zhang Y, Wang J, Wen G, Guan J, Zhou S, Chen G, Chatterjee K, Perc M. 2025.
Limitation of time promotes cooperation in structured collaboration systems. IEEE
Transactions on Network Science and Engineering. 12(1), 4–12.
mla: Zhang, Yichao, et al. “Limitation of Time Promotes Cooperation in Structured
Collaboration Systems.” IEEE Transactions on Network Science and Engineering,
vol. 12, no. 1, IEEE, 2025, pp. 4–12, doi:10.1109/TNSE.2024.3481434.
short: Y. Zhang, J. Wang, G. Wen, J. Guan, S. Zhou, G. Chen, K. Chatterjee, M. Perc,
IEEE Transactions on Network Science and Engineering 12 (2025) 4–12.
date_created: 2024-11-10T23:02:00Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2025-02-27T12:35:48Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/TNSE.2024.3481434
external_id:
isi:
- '001385382200040'
intvolume: ' 12'
isi: 1
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 4-12
publication: IEEE Transactions on Network Science and Engineering
publication_identifier:
eissn:
- 2327-4697
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Limitation of time promotes cooperation in structured collaboration systems
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 12
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '19074'
abstract:
- lang: eng
text: 'The public goods game is among the most studied metaphors of cooperation
in groups. In this game, individuals can use their endowments to make contributions
towards a good that benefits everyone. Each individual, however, is tempted to
free-ride on the contributions of others. Herein, we study repeated public goods
games among asymmetric players. Previous work has explored to which extent asymmetry
allows for full cooperation, such that players contribute their full endowment
each round. However, by design that work focusses on equilibria where individuals
make the same contribution each round. Instead, here we consider players whose
contributions along the equilibrium path can change from one round to the next.
We do so for three different models – one without any budget constraints, one
with endowment constraints, and one in which individuals can save their current
endowment to be used in subsequent rounds. In each case, we explore two key quantities:
the welfare and the resource efficiency that can be achieved in equilibrium. Welfare
corresponds to the sum of all players’ payoffs. Resource efficiency relates this
welfare to the total contributions made by the players. Compared to constant contribution
sequences, we find that time-dependent contributions can improve resource efficiency
across all three models. Moreover, they can improve the players’ welfare in the
model with savings.'
acknowledgement: 'This work was supported by the European Research Council CoG 863818
(ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529:
E-DIRECT (to C.H.), the European Union’s Horizon 2020 research and innovation programme
under the Marie Skłodowska-Curie Grant Agreement #754411 and the French Agence Nationale
de la Recherche (under the Investissement d’Avenir programme, ANR-17-EURE-0010),
and ARC SRIEAS Grant SR200100005 Securing Antarctica’s Environmental Future (to
M.K.). Open access funding provided by Institute of Science and Technology (IST
Austria).'
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Valentin
full_name: Hübner, Valentin
id: 2c8aa207-dc7d-11ea-9b2f-f22972ecd910
last_name: Hübner
orcid: 0009-0001-5009-4987
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Manuel
full_name: Staab, Manuel
last_name: Staab
- first_name: Maria
full_name: Kleshnina, Maria
id: 4E21749C-F248-11E8-B48F-1D18A9856A87
last_name: Kleshnina
orcid: 0000-0002-5518-8317
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Hübner V, Hilbe C, Staab M, Kleshnina M, Chatterjee K. Time-dependent strategies
in repeated asymmetric public goods games. Dynamic Games and Applications.
2025;15:1617-1645. doi:10.1007/s13235-025-00627-5
apa: Hübner, V., Hilbe, C., Staab, M., Kleshnina, M., & Chatterjee, K. (2025).
Time-dependent strategies in repeated asymmetric public goods games. Dynamic
Games and Applications. Springer Nature. https://doi.org/10.1007/s13235-025-00627-5
chicago: Hübner, Valentin, Christian Hilbe, Manuel Staab, Maria Kleshnina, and Krishnendu
Chatterjee. “Time-Dependent Strategies in Repeated Asymmetric Public Goods Games.”
Dynamic Games and Applications. Springer Nature, 2025. https://doi.org/10.1007/s13235-025-00627-5.
ieee: V. Hübner, C. Hilbe, M. Staab, M. Kleshnina, and K. Chatterjee, “Time-dependent
strategies in repeated asymmetric public goods games,” Dynamic Games and Applications,
vol. 15. Springer Nature, pp. 1617–1645, 2025.
ista: Hübner V, Hilbe C, Staab M, Kleshnina M, Chatterjee K. 2025. Time-dependent
strategies in repeated asymmetric public goods games. Dynamic Games and Applications.
15, 1617–1645.
mla: Hübner, Valentin, et al. “Time-Dependent Strategies in Repeated Asymmetric
Public Goods Games.” Dynamic Games and Applications, vol. 15, Springer
Nature, 2025, pp. 1617–45, doi:10.1007/s13235-025-00627-5.
short: V. Hübner, C. Hilbe, M. Staab, M. Kleshnina, K. Chatterjee, Dynamic Games
and Applications 15 (2025) 1617–1645.
corr_author: '1'
date_created: 2025-02-23T23:01:57Z
date_published: 2025-11-01T00:00:00Z
date_updated: 2026-04-07T12:30:56Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s13235-025-00627-5
ec_funded: 1
external_id:
isi:
- '001415587800001'
file:
- access_level: open_access
checksum: de0a412cbb7d98bf5e6a551c26acbefa
content_type: application/pdf
creator: dernst
date_created: 2025-12-30T08:01:35Z
date_updated: 2025-12-30T08:01:35Z
file_id: '20888'
file_name: 2025_DynGamesAppl_Huebner.pdf
file_size: 1126178
relation: main_file
success: 1
file_date_updated: 2025-12-30T08:01:35Z
has_accepted_license: '1'
intvolume: ' 15'
isi: 1
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: 1617-1645
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: Dynamic Games and Applications
publication_identifier:
eissn:
- 2153-0793
issn:
- 2153-0785
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '19903'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Time-dependent strategies in repeated asymmetric public goods games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19499'
abstract:
- lang: eng
text: Quantum hardware is inherently fragile and noisy. We find that the accuracy
of traditional quantum error correction algorithms can be improved depending on
the hardware. Given different hardware specifications, we automatically synthesize
hardware-optimal algorithms for parity correction, qubit resetting, and GHZ (Greenberger–Horne–Zeilinger)
state preparation. Using stochastic techniques from computer science, our method
presents a computational tool to compute exact accuracy guarantees and synthesize
optimal algorithms that are often different from traditional ones. We also show
that improvements can be gained with respect to the Qiskit transpiler as we compute
the hardware-optimal qubit mapping for the GHZ state-preparation problem.
acknowledgement: We thank the reviewers. In particular, they inspired us to analyze
the reset and state-preparation problems, to compute optimal qubit mappings, and
to apply our method to a quantum error correction scheme that includes both bitflip
and phaseflip corrections. We also thank Raimundo Saona and Marek Chalupa for their
time spent in insightful discussions. This research was partially supported by the
European Research Council CoG 863818 (ForM-SMArt) grant.
article_number: e2419273122
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Muroya Lei S, Chatterjee K, Henzinger TA. Hardware-optimal quantum algorithms.
Proceedings of the National Academy of Sciences. 2025;122(12). doi:10.1073/pnas.2419273122
apa: Muroya Lei, S., Chatterjee, K., & Henzinger, T. A. (2025). Hardware-optimal
quantum algorithms. Proceedings of the National Academy of Sciences. National
Academy of Sciences. https://doi.org/10.1073/pnas.2419273122
chicago: Muroya Lei, Stefanie, Krishnendu Chatterjee, and Thomas A Henzinger. “Hardware-Optimal
Quantum Algorithms.” Proceedings of the National Academy of Sciences. National
Academy of Sciences, 2025. https://doi.org/10.1073/pnas.2419273122.
ieee: S. Muroya Lei, K. Chatterjee, and T. A. Henzinger, “Hardware-optimal quantum
algorithms,” Proceedings of the National Academy of Sciences, vol. 122,
no. 12. National Academy of Sciences, 2025.
ista: Muroya Lei S, Chatterjee K, Henzinger TA. 2025. Hardware-optimal quantum algorithms.
Proceedings of the National Academy of Sciences. 122(12), e2419273122.
mla: Muroya Lei, Stefanie, et al. “Hardware-Optimal Quantum Algorithms.” Proceedings
of the National Academy of Sciences, vol. 122, no. 12, e2419273122, National
Academy of Sciences, 2025, doi:10.1073/pnas.2419273122.
short: S. Muroya Lei, K. Chatterjee, T.A. Henzinger, Proceedings of the National
Academy of Sciences 122 (2025).
corr_author: '1'
date_created: 2025-04-06T22:01:32Z
date_published: 2025-03-25T00:00:00Z
date_updated: 2026-04-28T13:41:14Z
day: '25'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1073/pnas.2419273122
ec_funded: 1
external_id:
isi:
- '001459435600001'
pmid:
- '40106357'
file:
- access_level: open_access
checksum: 83501b8a65ee5fdd3f5604fc28eddc22
content_type: application/pdf
creator: dernst
date_created: 2025-04-07T11:42:22Z
date_updated: 2025-04-07T11:42:22Z
file_id: '19524'
file_name: 2025_PNAS_Muroya.pdf
file_size: 6805668
relation: main_file
success: 1
file_date_updated: 2025-04-07T11:42:22Z
has_accepted_license: '1'
intvolume: ' 122'
isi: 1
issue: '12'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the National Academy of Sciences
publication_identifier:
eissn:
- 1091-6490
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/smml1996/algorithm_synthesis
- description: News on ISTA website
relation: press_release
url: https://ista.ac.at/en/news/hardware-optimal-quantum-algorithms/
scopus_import: '1'
status: public
title: Hardware-optimal quantum algorithms
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 122
year: '2025'
...
---
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: '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: '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
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'
...