---
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: 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'
...
---
OA_place: repository
OA_type: green
_id: '22134'
abstract:
- lang: eng
text: This artifact provides the source code, benchmarks, and scripts necessary
to build and reproduce the experimental results for `SuperDP` (Accepted at PLDI
2026). It also includes instructions for running the tool on user-provided inputs.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady E, Zikelic D. SuperDP: Differential Privacy Refutation
via Supermartingales. 2026. doi:10.5281/ZENODO.18930113'
apa: 'Chatterjee, K., Goharshady, E., & Zikelic, D. (2026). SuperDP: Differential
Privacy Refutation via Supermartingales. Zenodo. https://doi.org/10.5281/ZENODO.18930113'
chicago: 'Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP:
Differential Privacy Refutation via Supermartingales.” Zenodo, 2026. https://doi.org/10.5281/ZENODO.18930113.'
ieee: 'K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential Privacy
Refutation via Supermartingales.” Zenodo, 2026.'
ista: 'Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential Privacy
Refutation via Supermartingales, Zenodo, 10.5281/ZENODO.18930113.'
mla: 'Chatterjee, Krishnendu, et al. SuperDP: Differential Privacy Refutation
via Supermartingales. Zenodo, 2026, doi:10.5281/ZENODO.18930113.'
short: K. Chatterjee, E. Goharshady, D. Zikelic, (2026).
corr_author: '1'
date_created: 2026-06-24T06:25:29Z
date_published: 2026-03-09T00:00:00Z
date_updated: 2026-09-16T07:36:13Z
day: '09'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.5281/ZENODO.18930113
fulldoi: https://doi.org/10.5281/ZENODO.18930113
has_accepted_license: '1'
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/ZENODO.18930113
month: '03'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '22102'
relation: used_in_publication
status: public
status: public
title: 'SuperDP: Differential Privacy Refutation via Supermartingales'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2026'
...
---
OA_place: publisher
OA_type: gold
_id: '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: 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: '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: '18160'
abstract:
- lang: eng
text: 'Markov decision processes (MDPs) provide a standard framework for sequential
decision making under uncertainty. However, MDPs do not take uncertainty in transition
probabilities into account. Robust Markov decision processes (RMDPs) address this
shortcoming of MDPs by assigning to each transition an uncertainty set rather
than a single probability value. In this work, we consider polytopic RMDPs in
which all uncertainty sets are polytopes and study the problem of solving long-run
average reward polytopic RMDPs. We present a novel perspective on this problem
and show that it can be reduced to solving long-run average reward turn-based
stochastic games with finite state and action spaces. This reduction allows us
to derive several important consequences that were hitherto not known to hold
for polytopic RMDPs. First, we derive new computational complexity bounds for
solving long-run average reward polytopic RMDPs, showing for the first time that
the threshold decision problem for them is in NP∩CONP and that they admit a randomized
algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic
Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run
average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is
much more efficient in solving long-run average reward polytopic RMDPs compared
to state-of-the-art methods based on value iteration. '
acknowledgement: "This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt)
and the Czech Science Foundation\r\ngrant no. GA23-06963S."
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: 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, Karrabi M, Novotný P, Zikelic D. Solving long-run
average reward robust MDPs via stochastic games. In: 33rd International Joint
Conference on Artificial Intelligence. International Joint Conferences on
Artificial Intelligence; 2024:6707-6715. doi:10.24963/ijcai.2024/741'
apa: 'Chatterjee, K., Goharshady, E., Karrabi, M., Novotný, P., & Zikelic, D.
(2024). Solving long-run average reward robust MDPs via stochastic games. In 33rd
International Joint Conference on Artificial Intelligence (pp. 6707–6715).
Jeju, South Korea: International Joint Conferences on Artificial Intelligence.
https://doi.org/10.24963/ijcai.2024/741'
chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Petr Novotný,
and Dorde Zikelic. “Solving Long-Run Average Reward Robust MDPs via Stochastic
Games.” In 33rd International Joint Conference on Artificial Intelligence,
6707–15. International Joint Conferences on Artificial Intelligence, 2024. https://doi.org/10.24963/ijcai.2024/741.
ieee: K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, and D. Zikelic, “Solving
long-run average reward robust MDPs via stochastic games,” in 33rd International
Joint Conference on Artificial Intelligence, Jeju, South Korea, 2024, pp.
6707–6715.
ista: 'Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving
long-run average reward robust MDPs via stochastic games. 33rd International Joint
Conference on Artificial Intelligence. IJCAI: International Joint Conference on
Artificial Intelligence, 6707–6715.'
mla: Chatterjee, Krishnendu, et al. “Solving Long-Run Average Reward Robust MDPs
via Stochastic Games.” 33rd International Joint Conference on Artificial Intelligence,
International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–15,
doi:10.24963/ijcai.2024/741.
short: K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, D. Zikelic, in:, 33rd
International Joint Conference on Artificial Intelligence, International Joint
Conferences on Artificial Intelligence, 2024, pp. 6707–6715.
conference:
end_date: 2024-08-09
location: Jeju, South Korea
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2024-08-03
corr_author: '1'
das_tickbox: '0'
date_created: 2024-09-29T22:01:39Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2026-10-16T08:07:05Z
day: '01'
department:
- _id: KrCh
doi: 10.24963/ijcai.2024/741
ec_funded: 1
external_id:
arxiv:
- '2312.13912'
fulldoi: https://doi.org/10.24963/ijcai.2024/741
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2312.13912
month: '09'
oa: 1
oa_version: Preprint
page: 6707-6715
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 33rd International Joint Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781956792041'
issn:
- 1045-0823
publication_status: published
publisher: International Joint Conferences on Artificial Intelligence
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Solving long-run average reward robust MDPs via stochastic games
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
---
OA_place: publisher
OA_type: hybrid
_id: '17283'
abstract:
- lang: eng
text: 'We consider the problems of statically refuting equivalence and similarity
of output distributions defined by a pair of probabilistic programs. Equivalence
and similarity are two fundamental relational properties of probabilistic programs
that are essential for their correctness both in implementation and in compilation.
In this work, we present a new method for static equivalence and similarity refutation.
Our method refutes equivalence and similarity by computing a function over program
outputs whose expected value with respect to the output distributions of two programs
is different. The function is computed simultaneously with an upper expectation
supermartingale and a lower expectation submartingale for the two programs, which
we show to together provide a formal certificate for refuting equivalence and
similarity. To the best of our knowledge, our method is the first approach to
relational program analysis to offer the combination of the following desirable
features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic
programs, and (3) it provides formal guarantees on the correctness of its results.
We implement a prototype of our method and our experiments demonstrate the effectiveness
of our method to refute equivalence and similarity for a number of examples collected
from the literature.'
acknowledgement: "This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant. Petr Novotný\r\nis supported by the Czech Science Foundation grant no. GA23-06963S.\r\n"
article_number: '232'
article_processing_charge: Yes (via OA deal)
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: 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. Equivalence and similarity
refutation for probabilistic programs. Proceedings of the ACM on Programming
Languages. 2024;8. doi:10.1145/3656462
apa: Chatterjee, K., Goharshady, E., Novotný, P., & Zikelic, D. (2024). Equivalence
and similarity refutation for probabilistic programs. Proceedings of the ACM
on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3656462
chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic.
“Equivalence and Similarity Refutation for Probabilistic Programs.” Proceedings
of the ACM on Programming Languages. Association for Computing Machinery,
2024. https://doi.org/10.1145/3656462.
ieee: K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Equivalence and
similarity refutation for probabilistic programs,” Proceedings of the ACM on
Programming Languages, vol. 8. Association for Computing Machinery, 2024.
ista: Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2024. Equivalence and similarity
refutation for probabilistic programs. Proceedings of the ACM on Programming Languages.
8, 232.
mla: Chatterjee, Krishnendu, et al. “Equivalence and Similarity Refutation for Probabilistic
Programs.” Proceedings of the ACM on Programming Languages, vol. 8, 232,
Association for Computing Machinery, 2024, doi:10.1145/3656462.
short: K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, Proceedings of the
ACM on Programming Languages 8 (2024).
corr_author: '1'
das_tickbox: '0'
date_created: 2024-07-21T22:01:01Z
date_published: 2024-06-20T00:00:00Z
date_updated: 2026-10-16T08:08:51Z
day: '20'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
doi: 10.1145/3656462
ec_funded: 1
external_id:
arxiv:
- '2404.03430'
file:
- access_level: open_access
checksum: 8cbf220f284a4a87d093db5320c5afdd
content_type: application/pdf
creator: dernst
date_created: 2024-07-22T07:17:14Z
date_updated: 2024-07-22T07:17:14Z
file_id: '17290'
file_name: 2024_ACMProgLang_Chatterjee.pdf
file_size: 355421
relation: main_file
success: 1
file_date_updated: 2024-07-22T07:17:14Z
fulldoi: https://doi.org/10.1145/3656462
has_accepted_license: '1'
intvolume: ' 8'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Equivalence and similarity refutation for probabilistic programs
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 8
year: '2024'
...
---
_id: '10414'
abstract:
- lang: eng
text: 'We consider the almost-sure (a.s.) termination problem for probabilistic
programs, which are a stochastic extension of classical imperative programs. Lexicographic
ranking functions provide a sound and practical approach for termination of non-probabilistic
programs, and their extension to probabilistic programs is achieved via lexicographic
ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous
work have a limitation that impedes their automation: all of their components
have to be non-negative in all reachable states. This might result in LexRSM not
existing even for simple terminating programs. Our contributions are twofold:
First, we introduce a generalization of LexRSMs which allows for some components
to be negative. This standard feature of non-probabilistic termination proofs
was hitherto not known to be sound in the probabilistic setting, as the soundness
proof requires a careful analysis of the underlying stochastic process. Second,
we present polynomial-time algorithms using our generalized LexRSMs for proving
a.s. termination in broad classes of linear-arithmetic programs.'
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt),
the Czech Science Foundation grant No. GJ19-15134Y, and the European Union’s Horizon
2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement
No. 665385.
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: Jiří
full_name: Zárevúcky, Jiří
last_name: Zárevúcky
- 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, Zárevúcky J, Zikelic D. On lexicographic
proof rules for probabilistic termination. In: 24th International Symposium
on Formal Methods. Vol 13047. Springer Nature; 2021:619-639. doi:10.1007/978-3-030-90870-6_33'
apa: 'Chatterjee, K., Goharshady, E., Novotný, P., Zárevúcky, J., & Zikelic,
D. (2021). On lexicographic proof rules for probabilistic termination. In 24th
International Symposium on Formal Methods (Vol. 13047, pp. 619–639). Virtual:
Springer Nature. https://doi.org/10.1007/978-3-030-90870-6_33'
chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, Jiří Zárevúcky,
and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.”
In 24th International Symposium on Formal Methods, 13047:619–39. Springer
Nature, 2021. https://doi.org/10.1007/978-3-030-90870-6_33.
ieee: K. Chatterjee, E. Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On
lexicographic proof rules for probabilistic termination,” in 24th International
Symposium on Formal Methods, Virtual, 2021, vol. 13047, pp. 619–639.
ista: 'Chatterjee K, Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2021. On lexicographic
proof rules for probabilistic termination. 24th International Symposium on Formal
Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.'
mla: Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic
Termination.” 24th International Symposium on Formal Methods, vol. 13047,
Springer Nature, 2021, pp. 619–39, doi:10.1007/978-3-030-90870-6_33.
short: K. Chatterjee, E. Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, in:,
24th International Symposium on Formal Methods, Springer Nature, 2021, pp. 619–639.
conference:
end_date: 2021-11-26
location: Virtual
name: 'FM: Formal Methods'
start_date: 2021-11-20
date_created: 2021-12-05T23:01:45Z
date_published: 2021-11-10T00:00:00Z
date_updated: 2026-04-07T13:27:55Z
day: '10'
department:
- _id: KrCh
doi: 10.1007/978-3-030-90870-6_33
ec_funded: 1
external_id:
arxiv:
- '2108.02188'
isi:
- '000758218600033'
fulldoi: https://doi.org/10.1007/978-3-030-90870-6_33
intvolume: ' 13047'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2108.02188
month: '11'
oa: 1
oa_version: Preprint
page: 619-639
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: 24th International Symposium on Formal Methods
publication_identifier:
eisbn:
- 978-3-030-90870-6
eissn:
- 1611-3349
isbn:
- 9-783-0309-0869-0
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14778'
relation: later_version
status: public
- id: '14539'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: On lexicographic proof rules for probabilistic termination
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13047
year: '2021'
...