---
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-09-16T07:27:43Z
day: '14'
department:
- _id: KrCh
- _id: GradSch
doi: 10.1609/aaai.v40i43.40931
ec_funded: 1
external_id:
arxiv:
- '2505.04539'
fulldoi: https://doi.org/10.1609/aaai.v40i43.40931
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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-09-16T07:28:33Z
day: '14'
department:
- _id: KrCh
doi: 10.1609/aaai.v40i43.40932
ec_funded: 1
external_id:
arxiv:
- '2511.13134'
fulldoi: https://doi.org/10.1609/aaai.v40i43.40932
intvolume: ' 40'
issue: '43'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2511.13134
month: '03'
oa: 1
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Revealing POMDPs: Qualitative and quantitative analysis for parity objectives'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 40
year: '2026'
...
---
OA_place: publisher
OA_type: gold
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. ACM. 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. ACM, 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. ACM, 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, ACM, 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-09-16T07:36:14Z
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
fulldoi: https://doi.org/10.1145/3808296
has_accepted_license: '1'
intvolume: ' 10'
issue: PLDI
keyword:
- Static Program Analysis
- Differential Privacy
- Probabilistic Programming
- Martingales
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: ACM
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'
...
---
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: '1'
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-09-16T07:36:49Z
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
fulldoi: https://doi.org/10.1038/s41467-026-71777-2
has_accepted_license: '1'
intvolume: ' 17'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '12'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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'
...
---
OA_place: publisher
OA_type: gold
_id: '22920'
abstract:
- lang: eng
text: "Two-player games on graphs are a classical framework for analyzing strategic
decision making. In turn-based games, two players move a token along the edges
of the graph, and the right to move the token is determined by the current vertex.
In traditional bidding games - referred to as pure bidding games - the right to
move the token is determined at each step through bidding; here we consider Richman
bidding, where the winning player of a bid pays the losing player. The winner
is decided based on a temporal or quantitative specification evaluated over the
resulting infinite play.\r\nIn this work, we combine turn-based games and pure
bidding games into generalized bidding games, with player-1 vertices, player-2
vertices, and bidding vertices. This natural and simple generalization of bidding
games has far-reaching consequences. First, we show that, as a model, generalized
bidding games are more expressive than pure bidding games, and we provide several
applications. Second, and most importantly, we show that generalized Richman bidding
games are structurally equivalent to simple stochastic games, a well-studied model:
they are linearly interreducible to each other. As was previously known, the special
case of pure Richman bidding games corresponds to random-turn games. In other
words, generalized bidding games extend pure bidding games in the same way that
simple stochastic games extend random-turn games. We use this connection to solve
generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff
and discounted-sum) specifications. From a computational perspective, we establish
that generalized bidding games with parity and mean-payoff specifications retain
the best known upper bounds for turn-based games and pure bidding games, namely
NP∩coNP.\r\nFinally, we study a repair problem that asks whether bidding vertices
can be assigned \"owners\" so as to bring the threshold budget required to win
the game below a given target. This problem has direct applications in compositional
policy synthesis for multi-objective settings, and we show it to be NP-complete."
acknowledgement: "The research was partially supported by Austrian Science Fund (FWF)
10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), ERC-2020-AdG
101020093\r\n(VAMOS), and the RYC2024-049116-I grant funded by MICIU/AEI/10.13039/501100011033
and\r\nESF+.\r\n"
alternative_title:
- LIPIcs
article_number: 13:1-13:20
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- 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: Pavol
full_name: Kebis, Pavol
id: 2e0132b3-4e98-11ef-b275-cf7281c2802a
last_name: Kebis
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. Generalized bidding
games: Where bidding and stochastic games meet. In: 37th International Conference
on Concurrency Theory. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2026. doi:10.4230/LIPIcs.CONCUR.2026.13'
apa: 'Asadi, A., Henzinger, T. A., Goharshady, E., Kebis, P., & Mallik, K. (2026).
Generalized bidding games: Where bidding and stochastic games meet. In 37th
International Conference on Concurrency Theory (Vol. 391). Liverpool, United
Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2026.13'
chicago: 'Asadi, Ali, Thomas A Henzinger, Ehsan Goharshady, Pavol Kebis, and Kaushik
Mallik. “Generalized Bidding Games: Where Bidding and Stochastic Games Meet.”
In 37th International Conference on Concurrency Theory, Vol. 391. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.CONCUR.2026.13.'
ieee: 'A. Asadi, T. A. Henzinger, E. Goharshady, P. Kebis, and K. Mallik, “Generalized
bidding games: Where bidding and stochastic games meet,” in 37th International
Conference on Concurrency Theory, Liverpool, United Kingdom, 2026, vol. 391.'
ista: 'Asadi A, Henzinger TA, Goharshady E, Kebis P, Mallik K. 2026. Generalized
bidding games: Where bidding and stochastic games meet. 37th International Conference
on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol.
391, 13:1-13:20.'
mla: 'Asadi, Ali, et al. “Generalized Bidding Games: Where Bidding and Stochastic
Games Meet.” 37th International Conference on Concurrency Theory, vol.
391, 13:1-13:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.CONCUR.2026.13.'
short: A. Asadi, T.A. Henzinger, E. Goharshady, P. Kebis, K. Mallik, in:, 37th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2026.
conference:
end_date: 2026-09-04
location: Liverpool, United Kingdom
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2026-09-01
corr_author: '1'
das_tickbox: '0'
date_created: 2026-09-13T22:01:53Z
date_published: 2026-08-24T00:00:00Z
date_updated: 2026-09-17T09:44:41Z
day: '24'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2026.13
ec_funded: 1
external_id:
arxiv:
- '2606.29420'
file:
- access_level: open_access
checksum: de9af748d78fa42c173f68a71cbbd8d9
content_type: application/pdf
creator: dernst
date_created: 2026-09-17T09:43:28Z
date_updated: 2026-09-17T09:43:28Z
file_id: '22946'
file_name: 2026_LIPIcsCONCUR_Asadi.pdf
file_size: 1175682
relation: main_file
success: 1
file_date_updated: 2026-09-17T09:43:28Z
fulldoi: https://doi.org/10.4230/LIPIcs.CONCUR.2026.13
has_accepted_license: '1'
intvolume: ' 391'
keyword:
- Bidding Games
- Stochastic Games
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Concurrency Theory
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959774475'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: yes
title: 'Generalized bidding games: Where bidding and stochastic games meet'
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: 391
year: '2026'
...
---
OA_place: publisher
OA_type: gold
_id: '22919'
abstract:
- lang: eng
text: 'Reachability is the most fundamental logical objective, yet it is notoriously
difficult to learn in reinforcement learning settings: even for Markov decision
processes, PAC learning of reachability is impossible without additional assumptions.
This difficulty also holds in turn-based stochastic games (TBSGs), where two adversarial
players interact on a finite state space. In this work, we consider turn-based
stochastic games with reachability objectives. For such settings, adversarial
learning, in which players are adversarial even in the learning phase, is impossible.
Therefore, the goal is to consider learning, in which both players learn the unknown
model together. In this spirit, previous literature on PAC learning in TBSGs considers
(a) public information shared by both players; and (b) centralized learning, which
means that players share the same learning algorithm. In this work, our contribution
is two-fold. First, we relax these strong assumptions and ensure learning: (i)
with private information not shared with the other player; and (ii) decentralized
learning where the players do not share the same learning algorithm. To the best
of our knowledge, this work is the first positive result for decentralized and
private information learning of TBSGs with reachability objectives. Second, we
introduce a game-theoretic generalization of the Expected Conditional Distance
(ECD) parameter, which measures the expected length of reaching the target set.
We establish a polynomial-sample complexity bound with respect to the number of
states, actions, ECD parameter, and inverses of error tolerance and failure probability.'
acknowledgement: "The research was partially supported by Austrian Science Fund (FWF)
10.55776/COE12,\r\nERC CoG 863818 (ForM-SMArt), FWF-2022-SFB F8502 (SPyCoDe), and
ERC-2020-AdG 101020093\r\n(VAMOS) grants."
alternative_title:
- LIPIcs
article_number: 12:1-12:23
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: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Pavol
full_name: Kebis, Pavol
id: 2e0132b3-4e98-11ef-b275-cf7281c2802a
last_name: Kebis
citation:
ama: 'Asadi A, Chatterjee K, Kebis P. PAC learning in turn-based stochastic games
with reachability objectives: A decentralized private approach via expected conditional
distance. In: 37th International Conference on Concurrency Theory. Vol
391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.CONCUR.2026.12'
apa: 'Asadi, A., Chatterjee, K., & Kebis, P. (2026). PAC learning in turn-based
stochastic games with reachability objectives: A decentralized private approach
via expected conditional distance. In 37th International Conference on Concurrency
Theory (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2026.12'
chicago: 'Asadi, Ali, Krishnendu Chatterjee, and Pavol Kebis. “PAC Learning in Turn-Based
Stochastic Games with Reachability Objectives: A Decentralized Private Approach
via Expected Conditional Distance.” In 37th International Conference on Concurrency
Theory, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.
https://doi.org/10.4230/LIPIcs.CONCUR.2026.12.'
ieee: 'A. Asadi, K. Chatterjee, and P. Kebis, “PAC learning in turn-based stochastic
games with reachability objectives: A decentralized private approach via expected
conditional distance,” in 37th International Conference on Concurrency Theory,
Liverpool, United Kingdom, 2026, vol. 391.'
ista: 'Asadi A, Chatterjee K, Kebis P. 2026. PAC learning in turn-based stochastic
games with reachability objectives: A decentralized private approach via expected
conditional distance. 37th International Conference on Concurrency Theory. CONCUR:
Conference on Concurrency Theory, LIPIcs, vol. 391, 12:1-12:23.'
mla: 'Asadi, Ali, et al. “PAC Learning in Turn-Based Stochastic Games with Reachability
Objectives: A Decentralized Private Approach via Expected Conditional Distance.”
37th International Conference on Concurrency Theory, vol. 391, 12:1-12:23,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.CONCUR.2026.12.'
short: A. Asadi, K. Chatterjee, P. Kebis, in:, 37th International Conference on
Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.
conference:
end_date: 2026-09-04
location: Liverpool, United Kingdom
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2026-09-01
corr_author: '1'
das_tickbox: '0'
date_created: 2026-09-13T22:01:53Z
date_published: 2026-08-24T00:00:00Z
date_updated: 2026-09-17T09:51:25Z
day: '24'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2026.12
ec_funded: 1
external_id:
arxiv:
- '2607.14877'
file:
- access_level: open_access
checksum: 2e6c55b65d9d7ce436a6f59e81d7ba17
content_type: application/pdf
creator: dernst
date_created: 2026-09-17T09:50:00Z
date_updated: 2026-09-17T09:50:00Z
file_id: '22947'
file_name: 2026_LIPIcsCONCUR_Asadi2.pdf
file_size: 959234
relation: main_file
success: 1
file_date_updated: 2026-09-17T09:50:00Z
fulldoi: https://doi.org/10.4230/LIPIcs.CONCUR.2026.12
has_accepted_license: '1'
intvolume: ' 391'
keyword:
- formal methods
- games and logic
- logical aspects of AI
- model checking
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Concurrency Theory
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959774475'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: yes
title: 'PAC learning in turn-based stochastic games with reachability objectives:
A decentralized private approach via expected conditional distance'
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: 391
year: '2026'
...
---
OA_place: publisher
OA_type: gold
_id: '22922'
abstract:
- lang: eng
text: In this note, we recall the history and our motivation behind the development
of Strategy Logic and we discuss some of the work that ensued from its introduction.
acknowledgement: " Krishnendu Chatterjee: Supported in part by the Austrian Science
Fund (FWF) COE\r\ngrant 10.55776/COE12 and the ERC CoG 863818 (ForM-SMArt).\r\nThomas
A. Henzinger: Supported in part by the ERC AdG 101020093 (VAMOS) and the FWF\r\nSFB
grant F8502 (SPyCoDe).\r\nNir Piterman: Supported in part by the Swedish research
council (VR) project no. 2025-05419 and\r\nthe Wallenberg AI, Autonomous Systems
and Software Program (WASP) funded by the Knut and\r\nAlice Wallenberg Foundation.\r\nAcknowledgements
We thank the jury that our paper introducing Strategy Logic at the Conference\r\non
Concurrency Theory (CONCUR) 2007 [10] was chosen for a CONCUR Test-of-Time Award
at\r\nCONCUR 2026."
alternative_title:
- LIPIcs
article_number: 6:1-6:7
article_processing_charge: Yes
author:
- 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
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Chatterjee K, Henzinger TA, Piterman N. A look back at strategy logic. In:
37th International Conference on Concurrency Theory. Vol 391. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.CONCUR.2026.6'
apa: 'Chatterjee, K., Henzinger, T. A., & Piterman, N. (2026). A look back at
strategy logic. In 37th International Conference on Concurrency Theory
(Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2026.6'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Nir Piterman. “A Look Back
at Strategy Logic.” In 37th International Conference on Concurrency Theory,
Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.CONCUR.2026.6.
ieee: K. Chatterjee, T. A. Henzinger, and N. Piterman, “A look back at strategy
logic,” in 37th International Conference on Concurrency Theory, Liverpool,
United Kingdom, 2026, vol. 391.
ista: 'Chatterjee K, Henzinger TA, Piterman N. 2026. A look back at strategy logic.
37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency
Theory, LIPIcs, vol. 391, 6:1-6:7.'
mla: Chatterjee, Krishnendu, et al. “A Look Back at Strategy Logic.” 37th International
Conference on Concurrency Theory, vol. 391, 6:1-6:7, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2026, doi:10.4230/LIPIcs.CONCUR.2026.6.
short: K. Chatterjee, T.A. Henzinger, N. Piterman, in:, 37th International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.
conference:
end_date: 2026-09-04
location: Liverpool, United Kingdom
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2026-09-01
corr_author: '1'
das_tickbox: '0'
date_created: 2026-09-13T22:01:54Z
date_published: 2026-08-24T00:00:00Z
date_updated: 2026-09-22T05:54:30Z
day: '24'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2026.6
ec_funded: 1
file:
- access_level: open_access
checksum: f3995df175701f56a702bdb012e4f710
content_type: application/pdf
creator: dernst
date_created: 2026-09-22T05:53:16Z
date_updated: 2026-09-22T05:53:16Z
file_id: '22977'
file_name: 2026_LIPIcsCONCUR_Chatterjee.pdf
file_size: 517651
relation: main_file
success: 1
file_date_updated: 2026-09-22T05:53:16Z
fulldoi: https://doi.org/10.4230/LIPIcs.CONCUR.2026.6
has_accepted_license: '1'
intvolume: ' 391'
keyword:
- Strategy Logic
- Games
- Automata
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: 37th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959774475'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: A look back at strategy logic
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: 391
year: '2026'
...
---
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
orcid: 0000-0002-0163-2152
- 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: 2026-09-16T06:57:17Z
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
fulldoi: https://doi.org/10.1007/978-3-031-90653-4_7
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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: '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: 2026-09-16T06:56:56Z
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
fulldoi: https://doi.org/10.1007/978-3-031-90653-4_11
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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: '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: 2026-09-16T06:57:43Z
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
fulldoi: https://doi.org/10.1007/978-3-031-90653-4_14
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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: '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-09-16T06:55:21Z
day: '11'
department:
- _id: KrCh
doi: 10.1609/aaai.v39i11.33213
ec_funded: 1
external_id:
arxiv:
- '2412.16226'
fulldoi: https://doi.org/10.1609/aaai.v39i11.33213
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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: 2026-09-16T06:55:47Z
day: '11'
department:
- _id: KrCh
doi: 10.1609/aaai.v39i11.33212
ec_funded: 1
external_id:
arxiv:
- '2412.12228'
fulldoi: https://doi.org/10.1609/aaai.v39i11.33212
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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
_id: '19903'
abstract:
- lang: eng
text: "Cooperation, that is, one person paying a cost for another's benefit, is
a fundamental principle without which no form of society could exist. The extent
to which humans cooperate with each other is also an essential feature that differentiates
them from other animals. Cooperation occurs even in the absence of altruistic
motivations, when it is selfishly incentivised by the expectation of a future
reward. For example, many economic interactions are well described that way. This
kind of cooperation requires that people exhibit reciprocal behaviour that acts
as a mechanism that rewards cooperation.\r\nWith game-theoretic models, it is
possible to formally study potential such mechanisms and under what conditions
they can exist. This thesis contributes to this effort by analysing recently introduced
models of cooperation that advance on previous work by taking into account the
potential for pre-existing inequality among cooperating individuals as well as
the different forms that reciprocity can take.\r\nIndividuals may differ both
intrinsically, in their abilities, as well as extrinsically, in the amount of
resources they have available. Allowing for such differences in a model of cooperation
helps to understand how inequality affects the potential for, and outcomes of,
cooperation among unequals. In this thesis, it is shown that in the presence of
intrinsic inequality, a similar unequal distribution of resources can increase
the potential for cooperation. This effect is stronger the smaller the group is
in which cooperation takes place. It is also shown that under particular assumptions,
if the unequal members of a group vary the size of their contributions to a cooperative
effort over time, they can thereby increase their efficiency and improve the collective
outcome.\r\nCooperative behaviour in a two-person interaction can be rewarded
either by direct reciprocation whenever the same two people interact again, or
indirectly by a third party who observed the interaction. In the latter case of
indirect reciprocity, individuals are proximally rewarded by a good reputation,
which ultimately translates to being rewarded with cooperative behaviour by others.
This mechanism can enable selfishly motivated cooperation even in circumstances
where individuals are unlikely to meet again, akin to how money facilitates trade.
While these two forms of reciprocity have mostly been studied in isolation, this
thesis analyses both direct and indirect reciprocity in a general model in order
to compare their relative effectiveness under different circumstances. The contribution
of this thesis is an extension of previous work regarding a specific kind of interaction,
whose parameters allow for convenient mathematical analysis, to the most general
set of possible interactions."
acknowledgement: "The research for this thesis was supported by the European Research
Council\r\n(grant agreements No. 863818 and No. 850529), the European Union’s Horizon
2020 research and innovation programme (Marie Skłodowska-Curie grant agreement No.
754411),\r\nthe Austrian Science Fund (grant DOI 10.55776/COE12), the French Agence
Nationale\r\nde la Recherche under the Programme d’investissements d’avenir (project
reference 17-\r\nEURE-0010) and the Australian Government through the Australian
Research Council\r\n(grant No. SR200100005, “Securing Antarctica’s Environmental
Future”)."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Valentin
full_name: Hübner, Valentin
id: 2c8aa207-dc7d-11ea-9b2f-f22972ecd910
last_name: Hübner
orcid: 0009-0001-5009-4987
citation:
ama: Hübner V. Reciprocity and inequality in social dilemmas. 2025. doi:10.15479/AT-ISTA-19903
apa: Hübner, V. (2025). Reciprocity and inequality in social dilemmas. Institute
of Science and Technology Austria. https://doi.org/10.15479/AT-ISTA-19903
chicago: Hübner, Valentin. “Reciprocity and Inequality in Social Dilemmas.” Institute
of Science and Technology Austria, 2025. https://doi.org/10.15479/AT-ISTA-19903.
ieee: V. Hübner, “Reciprocity and inequality in social dilemmas,” Institute of Science
and Technology Austria, 2025.
ista: Hübner V. 2025. Reciprocity and inequality in social dilemmas. Institute of
Science and Technology Austria.
mla: Hübner, Valentin. Reciprocity and Inequality in Social Dilemmas. Institute
of Science and Technology Austria, 2025, doi:10.15479/AT-ISTA-19903.
short: V. Hübner, Reciprocity and Inequality in Social Dilemmas, Institute of Science
and Technology Austria, 2025.
corr_author: '1'
date_created: 2025-06-25T13:50:10Z
date_published: 2025-06-25T00:00:00Z
date_updated: 2026-09-16T06:58:24Z
day: '25'
ddc:
- '519'
degree_awarded: PhD
department:
- _id: GradSch
- _id: KrCh
doi: 10.15479/AT-ISTA-19903
doi_confirm: '1'
ec_funded: 1
file:
- access_level: closed
checksum: 794c02f8c82ca59ba6dda3bd7eed871a
content_type: application/x-xz
creator: vhuebner
date_created: 2025-06-25T13:38:07Z
date_updated: 2025-06-25T13:38:07Z
file_id: '19905'
file_name: Thesis Valentin Hübner source.tar.xz
file_size: 6192760
relation: source_file
- access_level: open_access
checksum: ac56063d81c81e40322b6ff5a8c4912e
content_type: application/pdf
creator: vhuebner
date_created: 2025-07-09T13:37:00Z
date_updated: 2025-07-09T13:37:00Z
file_id: '19976'
file_name: Thesis Valentin Hübner.pdf
file_size: 4837864
relation: main_file
file_date_updated: 2025-07-09T13:37:00Z
fulldoi: https://doi.org/10.15479/AT-ISTA-19903
has_accepted_license: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc/4.0/
month: '06'
oa: 1
oa_version: Published Version
page: '157'
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
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '19843'
relation: part_of_dissertation
status: public
- id: '15083'
relation: part_of_dissertation
status: public
- id: '19074'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
title: Reciprocity and inequality in 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: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: publisher
_id: '20138'
abstract:
- lang: eng
text: "The evolution shapes the world around us.\r\nNot only in biology, where the
fittest individuals spread their genes but also in physics and social dynamics,
the evolutionary forces determine the development of a state of matter or public
opinions.\r\nMany models describe these dynamics.\r\nThis thesis examines the
role of the structure in the models of selection.\r\nThe population structure
is represented as a graph or a network, and each vertex is occupied by one individual.\r\nEvery
individual has a type and fitness that represents the reproductive potential and
depends on the type, occupied vertex, and the arrangement of the neighbors.\r\nThe
evolution is modeled in discrete steps; in one step, one individual is replaced
by a neighbor selected randomly with the influence of fitness.\r\n\r\n\r\n\r\nThe
role of the networks is widely examined in the literature.\r\nThe structures that
promote the spread of the desired type compared to the structureless case are
called amplifiers.\r\nThe existence of amplifiers in various settings is an intensively
studied topic, and in some settings, the amplifiers have been identified.\r\nMoreover,
there are other important questions about the number of steps until one type spreads
over the whole network (fixation time), the computational complexity, and the
questions about the robustness of these processes.\r\n\r\n\r\nThis thesis explores
the role of structure in evolution from many perspectives.\r\nFirst, it introduces
different models and various choices that can be made in the models of evolution.\r\nIt
highlights the role of the structure in the real world and how this is reflected
in these models.\r\nThen, it describes the previous results and open problems.\r\nSecond,
the thesis describes an amplifier for two variants of the Moran process: one with
a constant birth rate and the other with a constant death rate.\r\nThis is an
important contribution to the robustness of the amplification.\r\nThird, the thesis
determines the complexity of spatial games.\r\nThese are processes where the fitness
comes from a game, and the strength of selection is high.\r\nIt shows that determining
the fate of cooperation in these games is a PSPACE-complete problem.\r\nFourth,
the thesis describes the amplifier of cooperation for spatial games.\r\nThis is
the first amplifier in this setting.\r\nFifth, the thesis examines the coexistence
in the Moran process with environmental heterogeneity.\r\nIn this setting, the
fitness depends not only on the type of the individual but also on the occupied
vertex.\r\nThe chapter determines the relationship between the interactions of
vertices of different types and the coexistence time.\r\nSixth, the thesis examines
the social balance on networks and proposes a stochastic dynamic partially aware
of the state of the graph, which reaches a balanced position quickly.\r\nFinally,
the thesis presents conclusions and outlines the directions for future work.\r\n\r\n\r\n"
acknowledgement: "This work was supported by the European Research Council CoG 863818
(ForMSMArt) and Austrian Science Fund 10.55776/COE12.\r\n"
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: Svoboda J. Structural properties of games on graphs. 2025. doi:10.15479/AT-ISTA-20138
apa: Svoboda, J. (2025). Structural properties of games on graphs. Institute
of Science and Technology Austria. https://doi.org/10.15479/AT-ISTA-20138
chicago: Svoboda, Jakub. “Structural Properties of Games on Graphs.” Institute of
Science and Technology Austria, 2025. https://doi.org/10.15479/AT-ISTA-20138.
ieee: J. Svoboda, “Structural properties of games on graphs,” Institute of Science
and Technology Austria, 2025.
ista: Svoboda J. 2025. Structural properties of games on graphs. Institute of Science
and Technology Austria.
mla: Svoboda, Jakub. Structural Properties of Games on Graphs. Institute
of Science and Technology Austria, 2025, doi:10.15479/AT-ISTA-20138.
short: J. Svoboda, Structural Properties of Games on Graphs, Institute of Science
and Technology Austria, 2025.
corr_author: '1'
das_tickbox: '1'
date_created: 2025-08-05T14:33:59Z
date_published: 2025-08-05T00:00:00Z
date_updated: 2026-09-16T06:59:33Z
day: '05'
ddc:
- '000'
- '519'
degree_awarded: PhD
department:
- _id: GradSch
- _id: KrCh
doi: 10.15479/AT-ISTA-20138
doi_confirm: '1'
ec_funded: 1
file:
- access_level: open_access
checksum: c6c4df9777f4537940de7ab392ad57e2
content_type: application/pdf
creator: jsvoboda
date_created: 2025-08-14T09:54:43Z
date_updated: 2025-08-14T09:54:43Z
file_id: '20177'
file_name: 2025_Svoboda_Jakub_Thesis.pdf
file_size: 5927291
relation: main_file
success: 1
- access_level: closed
checksum: 485e9f9822821bc03666d245d80aaa08
content_type: application/zip
creator: jsvoboda
date_created: 2025-08-14T09:55:20Z
date_updated: 2025-08-21T11:48:39Z
file_id: '20178'
file_name: 2025_Svoboda_Jakub_Thesis.zip
file_size: 6731815
relation: source_file
file_date_updated: 2025-08-21T11:48:39Z
fulldoi: https://doi.org/10.15479/AT-ISTA-20138
has_accepted_license: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-sa/4.0/
month: '08'
oa: 1
oa_version: Published Version
page: '167'
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publisher_comment: "Chapter 4 is copyrighted by CC BY-NC-ND\r\n4.0, which prohibits
derivatives. Chapter 6 is copyrighted: Copyright (2025) by the American\r\nPhysical
Society. For a copy, redistribution, or modification needs to be permitted by the\r\nAmerican
Physical Society.\r\n"
related_material:
record:
- id: '12787'
relation: part_of_dissertation
status: public
- id: '12101'
relation: part_of_dissertation
status: public
- id: '12257'
relation: part_of_dissertation
status: public
- id: '15297'
relation: part_of_dissertation
status: public
- id: '18703'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
title: Structural properties of games on graphs
tmp:
image: /images/cc_by_nc_sa.png
legal_code_url: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC
BY-NC-SA 4.0)
short: CC BY-NC-SA (4.0)
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: publisher
OA_type: diamond
_id: '20299'
abstract:
- lang: eng
text: "Deterministic Markov Decision Processes (DMDPs) are a mathematical framework
for decision-making where the outcomes and future possible actions are deterministically
determined by the current action taken. DMDPs can be viewed as a finite directed
weighted graph, where in each step, the controller chooses an outgoing edge. An
objective is a measurable function on runs (or infinite trajectories) of the DMDP,
and the value for an objective is the maximal cumulative reward (or weight) that
the controller can guarantee. We consider the classical mean-payoff (aka limit-average)
objective, which is a basic and fundamental objective.\r\n\r\nHoward's policy
iteration algorithm is a popular method for solving DMDPs with mean-payoff objectives.
Although Howard's algorithm performs well in practice, as experimental studies
suggested, the best known upper bound is exponential and the current known lower
bound is as follows: For the input size I, the algorithm requires (math formular)
iterations, where (math formular) hides the poly-logarithmic factors, i.e., the
current lower bound on iterations is sub-linear with respect to the input size.
Our main result is an improved lower bound for this fundamental algorithm where
we show that for the input size I, the algorithm requires (math formular) iterations."
acknowledgement: "This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant and Austrian Science Fund (FWF) 10.55776/COE12.\r\n"
alternative_title:
- PMLR
article_processing_charge: No
arxiv: 1
author:
- first_name: Ali
full_name: Asadi, Ali
id: 02d96aae-000e-11ec-b801-cadd0a5eefbb
last_name: Asadi
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Jakob
full_name: De Raaij, Jakob
last_name: De Raaij
citation:
ama: 'Asadi A, Chatterjee K, De Raaij J. Lower bound on Howard policy iteration
for deterministic Markov Decision Processes. In: The 41st Conference on Uncertainty
in Artificial Intelligence. Vol 286. ML Research Press; 2025:223-232.'
apa: 'Asadi, A., Chatterjee, K., & De Raaij, J. (2025). Lower bound on Howard
policy iteration for deterministic Markov Decision Processes. In The 41st Conference
on Uncertainty in Artificial Intelligence (Vol. 286, pp. 223–232). Rio de
Janeiro, Brazil: ML Research Press.'
chicago: Asadi, Ali, Krishnendu Chatterjee, and Jakob De Raaij. “Lower Bound on
Howard Policy Iteration for Deterministic Markov Decision Processes.” In The
41st Conference on Uncertainty in Artificial Intelligence, 286:223–32. ML
Research Press, 2025.
ieee: A. Asadi, K. Chatterjee, and J. De Raaij, “Lower bound on Howard policy iteration
for deterministic Markov Decision Processes,” in The 41st Conference on Uncertainty
in Artificial Intelligence, Rio de Janeiro, Brazil, 2025, vol. 286, pp. 223–232.
ista: 'Asadi A, Chatterjee K, De Raaij J. 2025. Lower bound on Howard policy iteration
for deterministic Markov Decision Processes. The 41st Conference on Uncertainty
in Artificial Intelligence. UAI: Conference on Uncertainty in Artificial Intelligence,
PMLR, vol. 286, 223–232.'
mla: Asadi, Ali, et al. “Lower Bound on Howard Policy Iteration for Deterministic
Markov Decision Processes.” The 41st Conference on Uncertainty in Artificial
Intelligence, vol. 286, ML Research Press, 2025, pp. 223–32.
short: A. Asadi, K. Chatterjee, J. De Raaij, in:, The 41st Conference on Uncertainty
in Artificial Intelligence, ML Research Press, 2025, pp. 223–232.
conference:
end_date: 2025-07-25
location: Rio de Janeiro, Brazil
name: 'UAI: Conference on Uncertainty in Artificial Intelligence'
start_date: 2025-07-21
corr_author: '1'
date_created: 2025-09-07T22:01:34Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2026-09-16T07:01:05Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
ec_funded: 1
external_id:
arxiv:
- '2506.12254'
file:
- access_level: open_access
checksum: 4180c81bb6ed3b4f5c7a8e48d06520c6
content_type: application/pdf
creator: dernst
date_created: 2025-09-09T06:27:59Z
date_updated: 2025-09-09T06:27:59Z
file_id: '20313'
file_name: 2025_UAI_Asadi.pdf
file_size: 317097
relation: main_file
success: 1
file_date_updated: 2025-09-09T06:27:59Z
has_accepted_license: '1'
intvolume: ' 286'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 223-232
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: The 41st Conference on Uncertainty in Artificial Intelligence
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Lower bound on Howard policy iteration for deterministic Markov Decision Processes
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 286
year: '2025'
...
---
OA_place: publisher
OA_type: diamond
_id: '20297'
abstract:
- lang: eng
text: "A standard model that arises in several applications in sequential decision-making
is partially observable Markov decision processes (POMDPs) where a decision-making
agent interacts with an uncertain environment. A basic objective in POMDPs is
the reachability objective, where given a target set of states, the goal is to
eventually arrive at one of them.\r\n\r\nThe limit-sure problem asks whether reachability
can be ensured with probability arbitrarily close to 1. In general, the limit-sure
reachability problem for POMDPs is undecidable. However, in many practical cases,
the most relevant question is the existence of policies with a small amount of
memory. In this work, we study the limit-sure reachability problem for POMDPs
with a fixed amount of memory. We establish that the computational complexity
of the problem is NP-complete."
acknowledgement: This research was partially supported by Austrian Science Fund (FWF)
10.55776/COE12, the support of the French Agence Nationale de la Recherche (ANR)
under reference ANR-21-CE40-0020 (CONVERGENCE project), and the ERC CoG 863818 (ForM-SMArt)
grant.
alternative_title:
- PMLR
article_processing_charge: No
arxiv: 1
author:
- first_name: Ali
full_name: Asadi, Ali
id: 02d96aae-000e-11ec-b801-cadd0a5eefbb
last_name: Asadi
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Raimundo J
full_name: Saona Urmeneta, Raimundo J
id: BD1DF4C4-D767-11E9-B658-BC13E6697425
last_name: Saona Urmeneta
orcid: 0000-0001-5103-038X
- first_name: Ali
full_name: Shafiee, Ali
id: 2783031a-7378-11f0-b2d0-f17f1db2ebad
last_name: Shafiee
citation:
ama: 'Asadi A, Chatterjee K, Saona Urmeneta RJ, Shafiee A. Limit-sure reachability
for small memory policies in POMDPs is NP-complete. In: The 41st Conference
on Uncertainty in Artificial Intelligence. Vol 286. ML Research Press; 2025:238-247.'
apa: 'Asadi, A., Chatterjee, K., Saona Urmeneta, R. J., & Shafiee, A. (2025).
Limit-sure reachability for small memory policies in POMDPs is NP-complete. In
The 41st Conference on Uncertainty in Artificial Intelligence (Vol. 286,
pp. 238–247). Rio de Janeiro, Brazil: ML Research Press.'
chicago: Asadi, Ali, Krishnendu Chatterjee, Raimundo J Saona Urmeneta, and Ali Shafiee.
“Limit-Sure Reachability for Small Memory Policies in POMDPs Is NP-Complete.”
In The 41st Conference on Uncertainty in Artificial Intelligence, 286:238–47.
ML Research Press, 2025.
ieee: A. Asadi, K. Chatterjee, R. J. Saona Urmeneta, and A. Shafiee, “Limit-sure
reachability for small memory policies in POMDPs is NP-complete,” in The 41st
Conference on Uncertainty in Artificial Intelligence, Rio de Janeiro, Brazil,
2025, vol. 286, pp. 238–247.
ista: 'Asadi A, Chatterjee K, Saona Urmeneta RJ, Shafiee A. 2025. Limit-sure reachability
for small memory policies in POMDPs is NP-complete. The 41st Conference on Uncertainty
in Artificial Intelligence. UAI: Conference on Uncertainty in Artificial Intelligence,
PMLR, vol. 286, 238–247.'
mla: Asadi, Ali, et al. “Limit-Sure Reachability for Small Memory Policies in POMDPs
Is NP-Complete.” The 41st Conference on Uncertainty in Artificial Intelligence,
vol. 286, ML Research Press, 2025, pp. 238–47.
short: A. Asadi, K. Chatterjee, R.J. Saona Urmeneta, A. Shafiee, in:, The 41st Conference
on Uncertainty in Artificial Intelligence, ML Research Press, 2025, pp. 238–247.
conference:
end_date: 2025-07-25
location: Rio de Janeiro, Brazil
name: 'UAI: Conference on Uncertainty in Artificial Intelligence'
start_date: 2025-07-21
corr_author: '1'
date_created: 2025-09-07T22:01:34Z
date_published: 2025-07-01T00:00:00Z
date_updated: 2026-09-16T07:03:02Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
ec_funded: 1
external_id:
arxiv:
- '2412.00941'
file:
- access_level: open_access
checksum: 1a37ebe7ba73ab6985765bf0d17a0acc
content_type: application/pdf
creator: dernst
date_created: 2025-09-09T08:19:41Z
date_updated: 2025-09-09T08:19:41Z
file_id: '20315'
file_name: 2025_UAI_AsadiAli.pdf
file_size: 307458
relation: main_file
success: 1
file_date_updated: 2025-09-09T08:19:41Z
has_accepted_license: '1'
intvolume: ' 286'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 238-247
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: The 41st Conference on Uncertainty in Artificial Intelligence
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Limit-sure reachability for small memory policies in POMDPs is NP-complete
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 286
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20302'
abstract:
- lang: eng
text: "LocalSGD and SCAFFOLD are widely used methods in distributed stochastic optimization,
with numerous applications in machine learning, large-scale data processing, and
federated learning. However, rigorously establishing their theoretical advantages
over simpler methods, such as minibatch SGD (MbSGD), has proven challenging, as
existing analyses often rely on strong assumptions, unrealistic premises, or overly
restrictive scenarios.\r\n\r\nIn this work, we revisit the convergence properties
of LocalSGD and SCAFFOLD under a variety of existing or weaker conditions, including
gradient similarity, Hessian similarity, weak convexity, and Lipschitz continuity
of the Hessian. Our analysis shows that (i) LocalSGD achieves faster convergence
compared to MbSGD for weakly convex functions without requiring stronger gradient
similarity assumptions; (ii) LocalSGD benefits significantly from higher-order
similarity and smoothness; and (iii) SCAFFOLD demonstrates faster convergence
than MbSGD for a broader class of non-quadratic functions. These theoretical insights
provide a clearer understanding of the conditions under which LocalSGD and SCAFFOLD
outperform MbSGD."
acknowledgement: "The authors thank for the helpful discussions with Eduard Gorbunov,
Kumar Kshitij Patel, Anton\r\nRodomanov, and Ali Zindari during the preparation
of this work. This work was partially done during the first author’s stays at CISPA
and at MBZUAI. The first author also acknowledges ERC CoG 863818 (ForM-SMArt) and
Austrian Science Fund (FWF) 10.55776/COE12."
alternative_title:
- PMLR
article_processing_charge: No
arxiv: 1
author:
- first_name: Ruichen
full_name: Luo, Ruichen
id: b391db08-1ffe-11ee-8b67-d18ddcfb5a14
last_name: Luo
- first_name: Sebastian U.
full_name: Stich, Sebastian U.
last_name: Stich
- first_name: Samuel
full_name: Horváth, Samuel
last_name: Horváth
- first_name: Martin
full_name: Takáč, Martin
last_name: Takáč
citation:
ama: 'Luo R, Stich SU, Horváth S, Takáč M. Revisiting LocalSGD and SCAFFOLD: Improved
rates and missing analysis. In: The 28th International Conference on Artificial
Intelligence and Statistics. Vol 258. ML Research Press; 2025:2539-2547.'
apa: 'Luo, R., Stich, S. U., Horváth, S., & Takáč, M. (2025). Revisiting LocalSGD
and SCAFFOLD: Improved rates and missing analysis. In The 28th International
Conference on Artificial Intelligence and Statistics (Vol. 258, pp. 2539–2547).
Mai Khao, Thailand: ML Research Press.'
chicago: 'Luo, Ruichen, Sebastian U. Stich, Samuel Horváth, and Martin Takáč. “Revisiting
LocalSGD and SCAFFOLD: Improved Rates and Missing Analysis.” In The 28th International
Conference on Artificial Intelligence and Statistics, 258:2539–47. ML Research
Press, 2025.'
ieee: 'R. Luo, S. U. Stich, S. Horváth, and M. Takáč, “Revisiting LocalSGD and SCAFFOLD:
Improved rates and missing analysis,” in The 28th International Conference
on Artificial Intelligence and Statistics, Mai Khao, Thailand, 2025, vol.
258, pp. 2539–2547.'
ista: 'Luo R, Stich SU, Horváth S, Takáč M. 2025. Revisiting LocalSGD and SCAFFOLD:
Improved rates and missing analysis. The 28th International Conference on Artificial
Intelligence and Statistics. AISTATS: Conference on Artificial Intelligence and
Statistics, PMLR, vol. 258, 2539–2547.'
mla: 'Luo, Ruichen, et al. “Revisiting LocalSGD and SCAFFOLD: Improved Rates and
Missing Analysis.” The 28th International Conference on Artificial Intelligence
and Statistics, vol. 258, ML Research Press, 2025, pp. 2539–47.'
short: R. Luo, S.U. Stich, S. Horváth, M. Takáč, in:, The 28th International Conference
on Artificial Intelligence and Statistics, ML Research Press, 2025, pp. 2539–2547.
conference:
end_date: 2025-05-05
location: Mai Khao, Thailand
name: 'AISTATS: Conference on Artificial Intelligence and Statistics'
start_date: 2025-05-03
date_created: 2025-09-07T22:01:35Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2026-09-16T07:01:32Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '2501.04443'
intvolume: ' 258'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2501.04443
month: '05'
oa: 1
oa_version: Preprint
page: 2539-2547
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: The 28th International Conference on Artificial Intelligence and Statistics
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Revisiting LocalSGD and SCAFFOLD: Improved rates and missing analysis'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 258
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20648'
abstract:
- lang: eng
text: Polynomial quantified entailments with existentially and universally quantified
variables arise in many problems of verification and program analysis. We present
PolyQEnt which is a tool for solving polynomial quantified entailments in which
variables on both sides of the implication are real valued or unbounded integers.
Our tool provides a unified framework for polynomial quantified entailment problems
that arise in several papers in the literature. Our experimental evaluation over
a wide range of benchmarks shows the applicability of the tool as well as its
benefits as opposed to simply using existing SMT solvers to solve such constraints.
acknowledgement: 'This work was supported by the following grants: ERC CoG 863818
(ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, ERC StG 101222524 (SPES),
the Ethereum Foundation Research Grant FY24-1793, and the Singapore Ministry of
Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SISSMU-100).'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
orcid: 0009-0007-5253-9170
- first_name: Milad
full_name: Saadat, Milad
last_name: Saadat
- first_name: Maximilian
full_name: Seeliger, Maximilian
last_name: Seeliger
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady AK, Goharshady E, et al. PolyQEnt: A polynomial quantified
entailment solver. In: 23rd International Symposium on Automated Technology
for Verification and Analysis. Vol 16145. Springer Nature; 2025:411-424. doi:10.1007/978-3-032-08707-2_19'
apa: 'Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., Saadat, M.,
Seeliger, M., & Zikelic, D. (2025). PolyQEnt: A polynomial quantified entailment
solver. In 23rd International Symposium on Automated Technology for Verification
and Analysis (Vol. 16145, pp. 411–424). Bengaluru, India: Springer Nature.
https://doi.org/10.1007/978-3-032-08707-2_19'
chicago: 'Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad
Karrabi, Milad Saadat, Maximilian Seeliger, and Dorde Zikelic. “PolyQEnt: A Polynomial
Quantified Entailment Solver.” In 23rd International Symposium on Automated
Technology for Verification and Analysis, 16145:411–24. Springer Nature, 2025.
https://doi.org/10.1007/978-3-032-08707-2_19.'
ieee: 'K. Chatterjee et al., “PolyQEnt: A polynomial quantified entailment
solver,” in 23rd International Symposium on Automated Technology for Verification
and Analysis, Bengaluru, India, 2025, vol. 16145, pp. 411–424.'
ista: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger
M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd
International Symposium on Automated Technology for Verification and Analysis.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424.'
mla: 'Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment
Solver.” 23rd International Symposium on Automated Technology for Verification
and Analysis, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:10.1007/978-3-032-08707-2_19.'
short: K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, M. Saadat, M.
Seeliger, D. Zikelic, in:, 23rd International Symposium on Automated Technology
for Verification and Analysis, Springer Nature, 2025, pp. 411–424.
conference:
end_date: 2025-10-31
location: Bengaluru, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2025-10-27
corr_author: '1'
date_created: 2025-11-16T23:01:24Z
date_published: 2025-10-26T00:00:00Z
date_updated: 2026-09-16T07:03:56Z
day: '26'
department:
- _id: KrCh
doi: 10.1007/978-3-032-08707-2_19
ec_funded: 1
external_id:
arxiv:
- '2408.03796'
fulldoi: https://doi.org/10.1007/978-3-032-08707-2_19
intvolume: ' 16145'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2408.03796
month: '10'
oa: 1
oa_version: Preprint
page: 411-424
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: 23rd International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032087065'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'PolyQEnt: A polynomial quantified entailment solver'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16145
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20690'
abstract:
- lang: eng
text: 'Cumulative prospect theory (CPT) is the first theory for decision-making
under uncertainty that combines full theoretical soundness and empirically realistic
features [1], [Page 2]. While CPT was originally considered in one-shot settings
for risk-aware decision-making, we consider CPT in sequential decision-making.
The most fundamental and well-studied models for sequential decision-making are
Markov chains (MCs), and their generalization Markov decision processes (MDPs).
The complexity theoretic study of MCs and MDPs with CPT is a fundamental problem
that has not been addressed in the literature.Our contributions are as follows:
First, we present an alternative viewpoint for the CPT-value of MCs and MDPs.
This allows us to establish a connection with multi-objective reachability analysis
and conclude the strategy complexity result that memoryless randomized strategies
are necessary and sufficient for optimality. Second, based on this connection,
we provide an algorithm for computing the CPT-value in MDPs with infinite-horizon
objectives. We show that the problem is in EXPTIME and fixed-parameter tractable.
Moreover, we provide a polynomial-time algorithm for the special case of MCs.'
acknowledgement: "This project has received funding from the Fonds de la Recherche
Scientifique - FNRS under grant No. T.0027.21, the Belgian National Lottery; the
ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12; the
DFG project 427755713, GOPro, and the DFG research training group GRK 2428 Continuous
Verification of Cyber-Physical Systems\r\n(ConVeY); the EU’s Horizon 2020 research
and innovation programmes under the Marie Sklodowska-Curie grant agreement No. 101034413
(IST-BRIDGE) and the ERC Starting Grant DEUCE (101077178)."
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas
full_name: Brihaye, Thomas
last_name: Brihaye
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Stefanie
full_name: Mohr, Stefanie
last_name: Mohr
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
citation:
ama: 'Brihaye T, Chatterjee K, Mohr S, Weininger M. Risk-aware Markov decision processes
using cumulative prospect theory. In: 2025 40th Annual ACM/IEEE Symposium on
Logic in Computer Science. IEEE; 2025:458-471. doi:10.1109/lics65433.2025.00041'
apa: 'Brihaye, T., Chatterjee, K., Mohr, S., & Weininger, M. (2025). Risk-aware
Markov decision processes using cumulative prospect theory. In 2025 40th Annual
ACM/IEEE Symposium on Logic in Computer Science (pp. 458–471). Singapore,
Singapore: IEEE. https://doi.org/10.1109/lics65433.2025.00041'
chicago: Brihaye, Thomas, Krishnendu Chatterjee, Stefanie Mohr, and Maximilian Weininger.
“Risk-Aware Markov Decision Processes Using Cumulative Prospect Theory.” In 2025
40th Annual ACM/IEEE Symposium on Logic in Computer Science, 458–71. IEEE,
2025. https://doi.org/10.1109/lics65433.2025.00041.
ieee: T. Brihaye, K. Chatterjee, S. Mohr, and M. Weininger, “Risk-aware Markov decision
processes using cumulative prospect theory,” in 2025 40th Annual ACM/IEEE Symposium
on Logic in Computer Science, Singapore, Singapore, 2025, pp. 458–471.
ista: 'Brihaye T, Chatterjee K, Mohr S, Weininger M. 2025. Risk-aware Markov decision
processes using cumulative prospect theory. 2025 40th Annual ACM/IEEE Symposium
on Logic in Computer Science. LICS: Logic in Computer Science, 458–471.'
mla: Brihaye, Thomas, et al. “Risk-Aware Markov Decision Processes Using Cumulative
Prospect Theory.” 2025 40th Annual ACM/IEEE Symposium on Logic in Computer
Science, IEEE, 2025, pp. 458–71, doi:10.1109/lics65433.2025.00041.
short: T. Brihaye, K. Chatterjee, S. Mohr, M. Weininger, in:, 2025 40th Annual ACM/IEEE
Symposium on Logic in Computer Science, IEEE, 2025, pp. 458–471.
conference:
end_date: 2025-06-26
location: Singapore, Singapore
name: 'LICS: Logic in Computer Science'
start_date: 2025-06-23
corr_author: '1'
date_created: 2025-11-24T14:43:47Z
date_published: 2025-10-09T00:00:00Z
date_updated: 2026-09-16T07:05:13Z
day: '09'
department:
- _id: KrCh
doi: 10.1109/lics65433.2025.00041
ec_funded: 1
external_id:
arxiv:
- '2505.09514'
fulldoi: https://doi.org/10.1109/lics65433.2025.00041
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2505.09514
month: '10'
oa: 1
oa_version: Preprint
page: 458-471
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
eisbn:
- '9798331579005'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Risk-aware Markov decision processes using cumulative prospect theory
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20689'
abstract:
- lang: eng
text: This paper studies the expected value of multiplicative rewards, where rewards
obtained in each step are multiplied (instead of the usual addition), in Markov
chains (MCs) and Markov decision processes (MDPs). One of the key differences
to additive rewards is that the expected value may diverge to ∞ not only due to
recurrent, but also due to transient states.For MCs, computing the value is shown
to be possible in polynomial time given an oracle for the comparison of succinctly
represented integers (CSRI), which is only known to be solvable in polynomial
time subject to number-theoretic conjectures. Interestingly, distinguishing whether
the value is ∞ or 0 is at least as hard as CSRI, while determining if it is one
of these two can be done in polynomial time. In MDPs, the optimal value can be
computed in polynomial space. Further refined complexity results and results on
the complexity of optimal schedulers are presented. The techniques developed for
MDPs additionally allow to solve the multiplicative variant of the stochastic
shortest path problem. Finally, for MCs and MDPs where an absorbing state is reached
almost surely, all considered problems are solvable in polynomial time.
acknowledgement: "This work was partly funded by the ERC CoG 863818 (ForM-SMArt),
the Austrian Science Fund (FWF) 10.55776/COE12, the DFG Grant 389792660 as part
of TRR 248 (Foundations of Perspicuous Software Systems), the Cluster of Excellence
EXC 2050/1 (CeTI, project ID\r\n390696704, as part of Germany’s Excellence Strategy),
and by the BMBF (Federal Ministry of Education and Research) in DAAD project 57616814
(SECAI, School of Embedded and\r\nComposite AI) as part of the program Konrad Zuse
Schools of Excellence in Artificial Intelligence."
article_processing_charge: No
arxiv: 1
author:
- first_name: Christel
full_name: Baier, Christel
last_name: Baier
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Jakob
full_name: Piribauer, Jakob
last_name: Piribauer
citation:
ama: 'Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Multiplicative rewards
in Markovian models. In: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer
Science. IEEE; 2025:499-512. doi:10.1109/lics65433.2025.00044'
apa: 'Baier, C., Chatterjee, K., Meggendorfer, T., & Piribauer, J. (2025). Multiplicative
rewards in Markovian models. In 2025 40th Annual ACM/IEEE Symposium on Logic
in Computer Science (pp. 499–512). Singapore, Singapore: IEEE. https://doi.org/10.1109/lics65433.2025.00044'
chicago: Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob
Piribauer. “Multiplicative Rewards in Markovian Models.” In 2025 40th Annual
ACM/IEEE Symposium on Logic in Computer Science, 499–512. IEEE, 2025. https://doi.org/10.1109/lics65433.2025.00044.
ieee: C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Multiplicative
rewards in Markovian models,” in 2025 40th Annual ACM/IEEE Symposium on Logic
in Computer Science, Singapore, Singapore, 2025, pp. 499–512.
ista: 'Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2025. Multiplicative
rewards in Markovian models. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer
Science. LICS: Logic in Computer Science, 499–512.'
mla: Baier, Christel, et al. “Multiplicative Rewards in Markovian Models.” 2025
40th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp.
499–512, doi:10.1109/lics65433.2025.00044.
short: C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, in:, 2025 40th Annual
ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2025, pp. 499–512.
conference:
end_date: 2025-06-26
location: Singapore, Singapore
name: 'LICS: Logic in Computer Science'
start_date: 2025-06-23
corr_author: '1'
date_created: 2025-11-24T14:24:00Z
date_published: 2025-10-09T00:00:00Z
date_updated: 2026-09-16T07:05:41Z
day: '09'
department:
- _id: KrCh
doi: 10.1109/lics65433.2025.00044
ec_funded: 1
external_id:
arxiv:
- '2504.18277'
fulldoi: https://doi.org/10.1109/lics65433.2025.00044
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2504.18277
month: '10'
oa: 1
oa_version: Preprint
page: 499-512
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
eisbn:
- '9798331579005'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Multiplicative rewards in Markovian models
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...