---
_id: '17402'
abstract:
- lang: eng
text: We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification
of probabilistic systems. We extend the previous version by adding support for
stochastic games, based on a recent unified framework for sound value iteration
algorithms. Thereby, PET2 is the first tool implementing a sound and efficient
approach for solving stochastic games with objectives of the type reachability/safety
and mean payoff. We complement this approach by developing and implementing a
partial-exploration based variant for all three objectives. Our experimental evaluation
shows that PET2 offers the most efficient partial-exploration based algorithm
and is the most viable tool on SGs, even outperforming unsound tools.
acknowledgement: M. Weininger has received funding from the EU’s Horizon 2020 research
and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101034413.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
citation:
ama: 'Meggendorfer T, Weininger M. Playing games with your PET: Extending the Partial
Exploration Tool to stochastic games. In: 36th International Conference on
Computer Aided Verification. Vol 14683. Springer Nature; 2024:359-372. doi:10.1007/978-3-031-65633-0_16'
apa: 'Meggendorfer, T., & Weininger, M. (2024). Playing games with your PET:
Extending the Partial Exploration Tool to stochastic games. In 36th International
Conference on Computer Aided Verification (Vol. 14683, pp. 359–372). Montreal,
Canada: Springer Nature. https://doi.org/10.1007/978-3-031-65633-0_16'
chicago: 'Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your
PET: Extending the Partial Exploration Tool to Stochastic Games.” In 36th International
Conference on Computer Aided Verification, 14683:359–72. Springer Nature,
2024. https://doi.org/10.1007/978-3-031-65633-0_16.'
ieee: 'T. Meggendorfer and M. Weininger, “Playing games with your PET: Extending
the Partial Exploration Tool to stochastic games,” in 36th International Conference
on Computer Aided Verification, Montreal, Canada, 2024, vol. 14683, pp. 359–372.'
ista: 'Meggendorfer T, Weininger M. 2024. Playing games with your PET: Extending
the Partial Exploration Tool to stochastic games. 36th International Conference
on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 14683,
359–372.'
mla: 'Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET:
Extending the Partial Exploration Tool to Stochastic Games.” 36th International
Conference on Computer Aided Verification, vol. 14683, Springer Nature, 2024,
pp. 359–72, doi:10.1007/978-3-031-65633-0_16.'
short: T. Meggendorfer, M. Weininger, in:, 36th International Conference on Computer
Aided Verification, Springer Nature, 2024, pp. 359–372.
conference:
end_date: 2024-07-27
location: Montreal, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2024-07-24
corr_author: '1'
date_created: 2024-08-09T11:24:54Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2025-09-08T08:53:55Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-65633-0_16
ec_funded: 1
external_id:
arxiv:
- '2405.03885'
isi:
- '001307897000016'
file:
- access_level: open_access
checksum: c888231d0a47b55786b7b4c0f02216bb
content_type: application/pdf
creator: dernst
date_created: 2024-08-12T08:39:12Z
date_updated: 2024-08-12T08:39:12Z
file_id: '17419'
file_name: 2024_CAV_Meggendorfer.pdf
file_size: 368487
relation: main_file
success: 1
file_date_updated: 2024-08-12T08:39:12Z
has_accepted_license: '1'
intvolume: ' 14683'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 359-372
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 36th International Conference on Computer Aided Verification
publication_identifier:
eisbn:
- '9783031656330'
eissn:
- 1611-3349
isbn:
- '9783031656323'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Playing games with your PET: Extending the Partial Exploration Tool to stochastic
games'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14683
year: '2024'
...
---
OA_place: publisher
OA_type: hybrid
_id: '17474'
abstract:
- lang: eng
text: Entropic risk (ERisk) is an established risk measure in finance, quantifying
risk by an exponential re-weighting of rewards. We study ERisk for the first time
in the context of turn-based stochastic games with the total reward objective.
This gives rise to an objective function that demands the control of systems in
a risk-averse manner. We show that the resulting games are determined and, in
particular, admit optimal memoryless deterministic strategies. This contrasts
risk measures that previously have been considered in the special case of Markov
decision processes and that require randomization and/or memory. We provide several
results on the decidability and the computational complexity of the threshold
problem, i.e. whether the optimal value of ERisk exceeds a given threshold. Furthermore,
an approximation algorithm for the optimal value of ERisk is provided.
acknowledgement: Krishnendu Chatterjee reports financial support was provided by European
Research Council.
article_number: '105214'
article_processing_charge: Yes (in subscription journal)
article_type: original
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. Entropic risk for turn-based
stochastic games. Information and Computation. 2024;301. doi:10.1016/j.ic.2024.105214
apa: Baier, C., Chatterjee, K., Meggendorfer, T., & Piribauer, J. (2024). Entropic
risk for turn-based stochastic games. Information and Computation. Elsevier.
https://doi.org/10.1016/j.ic.2024.105214
chicago: Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob
Piribauer. “Entropic Risk for Turn-Based Stochastic Games.” Information and
Computation. Elsevier, 2024. https://doi.org/10.1016/j.ic.2024.105214.
ieee: C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Entropic risk
for turn-based stochastic games,” Information and Computation, vol. 301.
Elsevier, 2024.
ista: Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2024. Entropic risk for
turn-based stochastic games. Information and Computation. 301, 105214.
mla: Baier, Christel, et al. “Entropic Risk for Turn-Based Stochastic Games.” Information
and Computation, vol. 301, 105214, Elsevier, 2024, doi:10.1016/j.ic.2024.105214.
short: C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, Information and Computation
301 (2024).
corr_author: '1'
date_created: 2024-09-01T22:01:07Z
date_published: 2024-12-01T00:00:00Z
date_updated: 2025-09-08T09:10:06Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1016/j.ic.2024.105214
external_id:
arxiv:
- '2307.06611'
isi:
- '001301143400001'
file:
- access_level: open_access
checksum: f68e0c2f46f9b9c86815406bcf2ee2d4
content_type: application/pdf
creator: dernst
date_created: 2025-01-09T13:49:03Z
date_updated: 2025-01-09T13:49:03Z
file_id: '18817'
file_name: 2024_InformationComputation_Baier.pdf
file_size: 724703
relation: main_file
success: 1
file_date_updated: 2025-01-09T13:49:03Z
has_accepted_license: '1'
intvolume: ' 301'
isi: 1
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
publication: Information and Computation
publication_identifier:
eissn:
- 1090-2651
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '14417'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Entropic risk for turn-based stochastic games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 301
year: '2024'
...
---
_id: '18155'
abstract:
- lang: eng
text: We study the classical problem of verifying programs with respect to formal
specifications given in the linear temporal logic (LTL). We first present novel
sound and complete witnesses for LTL verification over imperative programs. Our
witnesses are applicable to both verification (proving) and refutation (finding
bugs) settings. We then consider LTL formulas in which atomic propositions can
be polynomial constraints and turn our focus to polynomial arithmetic programs,
i.e. programs in which every assignment and guard consists only of polynomial
expressions. For this setting, we provide an efficient algorithm to automatically
synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete.
Finally, we present experimental results demonstrating the effectiveness of our
approach and that it can handle programs which were beyond the reach of previous
state-of-the-art tools.
acknowledgement: This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt)
and the Hong Kong Research Grants Council ECS Project Number 26208122.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
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: Goharshady, Ehsan
last_name: Goharshady
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
- 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, Karrabi M, Zikelic D. Sound and complete
witnesses for template-based verification of LTL properties on polynomial programs.
In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in
Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 14933. Springer
Nature; 2024:600-619. doi:10.1007/978-3-031-71162-6_31'
apa: 'Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., & Zikelic,
D. (2024). Sound and complete witnesses for template-based verification of LTL
properties on polynomial programs. In Lecture Notes in Computer Science (including
subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
(Vol. 14933, pp. 600–619). Milan, Italy: Springer Nature. https://doi.org/10.1007/978-3-031-71162-6_31'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad
Karrabi, and Dorde Zikelic. “Sound and Complete Witnesses for Template-Based Verification
of LTL Properties on Polynomial Programs.” In Lecture Notes in Computer Science
(Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), 14933:600–619. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-71162-6_31.
ieee: K. Chatterjee, A. K. Goharshady, E. Goharshady, M. Karrabi, and D. Zikelic,
“Sound and complete witnesses for template-based verification of LTL properties
on polynomial programs,” in Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
Milan, Italy, 2024, vol. 14933, pp. 600–619.
ista: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound
and complete witnesses for template-based verification of LTL properties on polynomial
programs. Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods,
LNCS, vol. 14933, 600–619.'
mla: Chatterjee, Krishnendu, et al. “Sound and Complete Witnesses for Template-Based
Verification of LTL Properties on Polynomial Programs.” Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), vol. 14933, Springer Nature, 2024, pp. 600–19, doi:10.1007/978-3-031-71162-6_31.
short: K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, D. Zikelic, in:,
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp.
600–619.
conference:
end_date: 2024-09-13
location: Milan, Italy
name: 'FM: Formal Methods'
start_date: 2024-09-09
corr_author: '1'
date_created: 2024-09-29T22:01:37Z
date_published: 2024-09-11T00:00:00Z
date_updated: 2025-09-08T09:51:34Z
day: '11'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-71162-6_31
ec_funded: 1
external_id:
arxiv:
- '2403.05386'
isi:
- '001336893300031'
file:
- access_level: open_access
checksum: 223845be9e754681ee218866827c95e7
content_type: application/pdf
creator: dernst
date_created: 2024-10-01T09:56:54Z
date_updated: 2024-10-01T09:56:54Z
file_id: '18165'
file_name: 2024_LNCS_Chatterjee.pdf
file_size: 650495
relation: main_file
success: 1
file_date_updated: 2024-10-01T09:56:54Z
has_accepted_license: '1'
intvolume: ' 14933'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 600-619
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031711619'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Sound and complete witnesses for template-based verification of LTL properties
on polynomial 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: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14933
year: '2024'
...
---
_id: '18159'
abstract:
- lang: eng
text: "Markov Decision Processes (MDPs) are a classical model for decision making
in the presence of uncertainty. Often they are viewed as state transformers with
planning objectives defned with respect to paths over MDP states. An increasingly\r\npopular
alternative is to view them as distribution transformers, giving rise to a sequence
of probability distributions over MDP states. For instance, reachability and safety
properties in modeling robot swarms or chemical reaction networks are naturally
defned in terms of probability distributions over states. Verifying such distributional
properties is known to be hard and often beyond the reach of classical state-based
verifcation techniques. In this work, we consider the problems of certifed policy
(i.e. controller) verifcation and synthesis in MDPs under distributional reach-avoidance
specifcations. By certifed we mean that, along with a policy, we also aim to synthesize
a (checkable) certifcate ensuring that the MDP indeed satisfes the property. Thus,
given the target set of distributions and an unsafe set of distributions over
MDP states, our goal is to either synthesize a certifcate for a given policy or
synthesize a policy along with a certifcate, proving that the target distribution
can be reached while avoiding unsafe distributions. To solve this problem, we
introduce the novel notion of distributional reach-avoid certifcates and present
automated procedures for (1) synthesizing a certifcate for a given policy, and
(2) synthesizing a policy together with the certifcate, both providing formal
guarantees on certifcate correctness. Our experimental evaluation demonstrates
the ability of our method to solve several non-trivial examples, including a multi-agent
robot-swarm model, to synthesize certifed policies and to certify existing policies. "
acknowledgement: This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt),
the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant,
Google Research Award 2023 and the SBI Foundation Hub for Data and Analytics.
article_processing_charge: No
arxiv: 1
author:
- first_name: S
full_name: Akshay, S
last_name: Akshay
- 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: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. Certified policy verification
and synthesis for MDPs under distributional reach-avoidance properties. In: Proceedings
of the Thirty-Third International Joint Conference on Artificial Intelligence.
International Joint Conferences on Artificial Intelligence; 2024:3-12. doi:10.24963/ijcai.2024/1'
apa: 'Akshay, S., Chatterjee, K., Meggendorfer, T., & Zikelic, D. (2024). Certified
policy verification and synthesis for MDPs under distributional reach-avoidance
properties. In Proceedings of the Thirty-Third International Joint Conference
on Artificial Intelligence (pp. 3–12). Jeju, Korea: International Joint Conferences
on Artificial Intelligence. https://doi.org/10.24963/ijcai.2024/1'
chicago: Akshay, S, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic.
“Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance
Properties.” In Proceedings of the Thirty-Third International Joint Conference
on Artificial Intelligence, 3–12. International Joint Conferences on Artificial
Intelligence, 2024. https://doi.org/10.24963/ijcai.2024/1.
ieee: S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “Certified policy
verification and synthesis for MDPs under distributional reach-avoidance properties,”
in Proceedings of the Thirty-Third International Joint Conference on Artificial
Intelligence, Jeju, Korea, 2024, pp. 3–12.
ista: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2024. Certified policy
verification and synthesis for MDPs under distributional reach-avoidance properties.
Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence.
IJCAI: International Joint Conference on Artificial Intelligence, 3–12.'
mla: Akshay, S., et al. “Certified Policy Verification and Synthesis for MDPs under
Distributional Reach-Avoidance Properties.” Proceedings of the Thirty-Third
International Joint Conference on Artificial Intelligence, International Joint
Conferences on Artificial Intelligence, 2024, pp. 3–12, doi:10.24963/ijcai.2024/1.
short: S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, Proceedings of
the Thirty-Third International Joint Conference on Artificial Intelligence, International
Joint Conferences on Artificial Intelligence, 2024, pp. 3–12.
conference:
end_date: 2024-08-09
location: Jeju, Korea
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2024-08-03
corr_author: '1'
date_created: 2024-09-29T22:01:38Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2025-04-14T07:52:46Z
day: '01'
department:
- _id: KrCh
doi: 10.24963/ijcai.2024/1
ec_funded: 1
external_id:
arxiv:
- '2405.04015'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2405.04015
month: '09'
oa: 1
oa_version: Preprint
page: 3-12
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 Thirty-Third 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'
scopus_import: '1'
status: public
title: Certified policy verification and synthesis for MDPs under distributional reach-avoidance
properties
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2024'
...
---
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
- 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'
date_created: 2024-09-29T22:01:39Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2025-04-14T07:52:46Z
day: '01'
department:
- _id: KrCh
doi: 10.24963/ijcai.2024/741
ec_funded: 1
external_id:
arxiv:
- '2312.13912'
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'
scopus_import: '1'
status: public
title: Solving long-run average reward robust MDPs via stochastic games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2024'
...
---
_id: '17328'
abstract:
- lang: eng
text: "We study selfish mining attacks in longest-chain blockchains like Bitcoin,
but where the proof of work is replaced with efficient proof systems - like proofs
of stake or proofs of space - and consider the problem of computing an optimal
selfish mining attack which maximizes expected relative revenue of the adversary,
thus minimizing the chain quality. To this end, we propose a novel selfish mining
attack that aims to maximize this objective and formally model the attack as a
Markov decision process (MDP). We then present a formal analysis procedure which
computes an ϵ-tight lower bound on the optimal expected relative revenue in the
MDP and a strategy that achieves this ϵ-tight lower bound, where ϵ > 0 may be
any specified precision. Our analysis is fully automated and provides formal guarantees
on the correctness. We evaluate our selfish mining attack and observe that it
achieves superior expected relative revenue compared to two considered baselines.\r\nIn
concurrent work [Sarenche FC'24] does an automated analysis on selfish mining
in predictable longest-chain blockchains based on efficient proof systems. Predictable
means the randomness for the challenges is fixed for many blocks (as used e.g.,
in Ouroboros), while we consider unpredictable (Bitcoin-like) chains where the
challenge is derived from the previous block."
acknowledgement: "This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt)
grant and the MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms) grant.\r\n"
article_processing_charge: Yes (via OA deal)
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: Amirali
full_name: Ebrahimzadeh, Amirali
last_name: Ebrahimzadeh
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
orcid: 0009-0007-5253-9170
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
- first_name: Michelle X
full_name: Yeo, Michelle X
id: 2D82B818-F248-11E8-B48F-1D18A9856A87
last_name: Yeo
orcid: 0009-0001-3676-4809
- 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, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D. Fully
automated selfish mining analysis in efficient proof systems blockchains. In:
Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing.
Association for Computing Machinery; 2024:268-278. doi:10.1145/3662158.3662769'
apa: 'Chatterjee, K., Ebrahimzadeh, A., Karrabi, M., Pietrzak, K. Z., Yeo, M. X.,
& Zikelic, D. (2024). Fully automated selfish mining analysis in efficient
proof systems blockchains. In Proceedings of the 43rd Annual ACM Symposium
on Principles of Distributed Computing (pp. 268–278). Nantes, France: Association
for Computing Machinery. https://doi.org/10.1145/3662158.3662769'
chicago: Chatterjee, Krishnendu, Amirali Ebrahimzadeh, Mehrdad Karrabi, Krzysztof
Z Pietrzak, Michelle X Yeo, and Dorde Zikelic. “Fully Automated Selfish Mining
Analysis in Efficient Proof Systems Blockchains.” In Proceedings of the 43rd
Annual ACM Symposium on Principles of Distributed Computing, 268–78. Association
for Computing Machinery, 2024. https://doi.org/10.1145/3662158.3662769.
ieee: K. Chatterjee, A. Ebrahimzadeh, M. Karrabi, K. Z. Pietrzak, M. X. Yeo, and
D. Zikelic, “Fully automated selfish mining analysis in efficient proof systems
blockchains,” in Proceedings of the 43rd Annual ACM Symposium on Principles
of Distributed Computing, Nantes, France, 2024, pp. 268–278.
ista: 'Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D.
2024. Fully automated selfish mining analysis in efficient proof systems blockchains.
Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing.
PODC: Symposium on Principles of Distributed Computing, 268–278.'
mla: Chatterjee, Krishnendu, et al. “Fully Automated Selfish Mining Analysis in
Efficient Proof Systems Blockchains.” Proceedings of the 43rd Annual ACM Symposium
on Principles of Distributed Computing, Association for Computing Machinery,
2024, pp. 268–78, doi:10.1145/3662158.3662769.
short: K. Chatterjee, A. Ebrahimzadeh, M. Karrabi, K.Z. Pietrzak, M.X. Yeo, D. Zikelic,
in:, Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed
Computing, Association for Computing Machinery, 2024, pp. 268–278.
conference:
end_date: 2024-06-21
location: Nantes, France
name: 'PODC: Symposium on Principles of Distributed Computing'
start_date: 2024-06-17
corr_author: '1'
das_tickbox: '1'
date_created: 2024-07-28T22:01:10Z
date_published: 2024-06-17T00:00:00Z
date_updated: 2026-07-07T13:30:07Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
- _id: KrPi
doi: 10.1145/3662158.3662769
ec_funded: 1
external_id:
arxiv:
- '2405.04420'
file:
- access_level: open_access
checksum: 6122bd97b42751ff81c452a19970f67d
content_type: application/pdf
creator: dernst
date_created: 2024-07-29T07:18:12Z
date_updated: 2024-07-29T07:18:12Z
file_id: '17334'
file_name: 2024_ACM_Chatterjee.pdf
file_size: 832034
relation: main_file
success: 1
file_date_updated: 2024-07-29T07:18:12Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 268-278
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 43rd Annual ACM Symposium on Principles of Distributed
Computing
publication_identifier:
isbn:
- '9798400706684'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Fully automated selfish mining analysis in efficient proof systems blockchains
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2024'
...
---
APC_amount: 3149,96 EUR
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '15297'
abstract:
- lang: eng
text: Populations evolve by accumulating advantageous mutations. Every population
has some spatial structure that can be modeled by an underlying network. The network
then influences the probability that new advantageous mutations fixate. Amplifiers
of selection are networks that increase the fixation probability of advantageous
mutants, as compared to the unstructured fully-connected network. Whether or not
a network is an amplifier depends on the choice of the random process that governs
the evolutionary dynamics. Two popular choices are Moran process with Birth-death
updating and Moran process with death-Birth updating. Interestingly, while some
networks are amplifiers under Birth-death updating and other networks are amplifiers
under death-Birth updating, so far no spatial structures have been found that
function as an amplifier under both types of updating simultaneously. In this
work, we identify networks that act as amplifiers of selection under both versions
of the Moran process. The amplifiers are robust, modular, and increase fixation
probability for any mutant fitness advantage in a range r ∈ (1, 1.2). To complement
this positive result, we also prove that for certain quantities closely related
to fixation probability, it is impossible to improve them simultaneously for both
versions of the Moran process. Together, our results highlight how the two versions
of the Moran process differ and what they have in common.
acknowledgement: "We thank Gavin Rees for helpful discussions. J.S., S.J., and K.C
were supported by\r\nEuropean Research Council (ERC) CoG 863818 (ForM-SMArt). J.T
was supported by Center for Foundations of Modern Computer Science (Charles University
project UNCE/SCI/004) and by the project PRIMUS/24/SCI/012 from Charles University. "
article_number: e1012008
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Soham Shrikant
full_name: Joshi, Soham Shrikant
id: f97aac0e-f57c-11ee-93d0-a5a82d8df168
last_name: Joshi
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- 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, Joshi SS, Tkadlec J, Chatterjee K. Amplifiers of selection for the
Moran process with both Birth-death and death-Birth updating. PLoS Computational
Biology. 2024;20(3). doi:10.1371/journal.pcbi.1012008
apa: Svoboda, J., Joshi, S. S., Tkadlec, J., & Chatterjee, K. (2024). Amplifiers
of selection for the Moran process with both Birth-death and death-Birth updating.
PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1012008
chicago: Svoboda, Jakub, Soham Shrikant Joshi, Josef Tkadlec, and Krishnendu Chatterjee.
“Amplifiers of Selection for the Moran Process with Both Birth-Death and Death-Birth
Updating.” PLoS Computational Biology. Public Library of Science, 2024.
https://doi.org/10.1371/journal.pcbi.1012008.
ieee: J. Svoboda, S. S. Joshi, J. Tkadlec, and K. Chatterjee, “Amplifiers of selection
for the Moran process with both Birth-death and death-Birth updating,” PLoS
Computational Biology, vol. 20, no. 3. Public Library of Science, 2024.
ista: Svoboda J, Joshi SS, Tkadlec J, Chatterjee K. 2024. Amplifiers of selection
for the Moran process with both Birth-death and death-Birth updating. PLoS Computational
Biology. 20(3), e1012008.
mla: Svoboda, Jakub, et al. “Amplifiers of Selection for the Moran Process with
Both Birth-Death and Death-Birth Updating.” PLoS Computational Biology,
vol. 20, no. 3, e1012008, Public Library of Science, 2024, doi:10.1371/journal.pcbi.1012008.
short: J. Svoboda, S.S. Joshi, J. Tkadlec, K. Chatterjee, PLoS Computational Biology
20 (2024).
corr_author: '1'
date_created: 2024-04-07T22:00:55Z
date_published: 2024-03-29T00:00:00Z
date_updated: 2026-07-27T12:52:03Z
day: '29'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1371/journal.pcbi.1012008
ec_funded: 1
external_id:
arxiv:
- '2401.14914'
isi:
- '001194482400002'
file:
- access_level: open_access
checksum: a511cf369d9172beb123fe73f291b5cc
content_type: application/pdf
creator: dernst
date_created: 2024-08-20T10:52:28Z
date_updated: 2024-08-20T10:52:28Z
file_id: '17450'
file_name: 2024_PloSComBio_Svoboda.pdf
file_size: 1425292
relation: main_file
success: 1
file_date_updated: 2024-08-20T10:52:28Z
has_accepted_license: '1'
intvolume: ' 20'
isi: 1
issue: '3'
language:
- iso: eng
month: '03'
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: PLoS Computational Biology
publication_identifier:
eissn:
- 1553-7358
issn:
- 1553-734X
publication_status: published
publisher: Public Library of Science
quality_controlled: '1'
related_material:
record:
- id: '20138'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Amplifiers of selection for the Moran process with both Birth-death and death-Birth
updating
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: 20
year: '2024'
...
---
APC_amount: 3143,76 EUR
OA_place: publisher
OA_type: hybrid
_id: '18703'
abstract:
- lang: eng
text: 'Spatial games provide a simple and elegant mathematical model to study the
evolution of cooperation in networks. In spatial games, individuals reside in
vertices, adopt simple strategies, and interact with neighbors to receive a payoff.
Depending on their own and neighbors’ payoffs, individuals can change their strategy.
The payoff is determined by the Prisoners’ Dilemma, a classical matrix game, where
players cooperate or defect. While cooperation is the desired behavior, defection
provides a higher payoff for a selfish individual. There are many theoretical
and empirical studies related to the role of the network in the evolution of cooperation.
However, the fundamental question of whether there exist networks that for low
initial cooperation rate ensure a high chance of fixation, i.e., cooperation spreads
across the whole population, has remained elusive for spatial games with strong
selection. In this work, we answer this fundamental question in the affirmative
by presenting network structures that ensure high fixation probability for cooperators
in the strong selection regime. Besides, our structures have many desirable properties:
(a) they ensure the spread of cooperation even for a low initial density of cooperation
and high temptation of defection, (b) they have constant degrees, and (c) the
number of steps, until cooperation spreads, is at most quadratic in the size of
the network.'
acknowledgement: J.S. and K.C. were supported by the European Research Council CoG
863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.
article_number: e2405605121
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: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Svoboda J, Chatterjee K. Density amplifiers of cooperation for spatial games.
Proceedings of the National Academy of Sciences of the United States of America.
2024;121(50). doi:10.1073/pnas.2405605121
apa: Svoboda, J., & Chatterjee, K. (2024). Density amplifiers of cooperation
for spatial games. Proceedings of the National Academy of Sciences of the United
States of America. National Academy of Sciences. https://doi.org/10.1073/pnas.2405605121
chicago: Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation
for Spatial Games.” Proceedings of the National Academy of Sciences of the
United States of America. National Academy of Sciences, 2024. https://doi.org/10.1073/pnas.2405605121.
ieee: J. Svoboda and K. Chatterjee, “Density amplifiers of cooperation for spatial
games,” Proceedings of the National Academy of Sciences of the United States
of America, vol. 121, no. 50. National Academy of Sciences, 2024.
ista: Svoboda J, Chatterjee K. 2024. Density amplifiers of cooperation for spatial
games. Proceedings of the National Academy of Sciences of the United States of
America. 121(50), e2405605121.
mla: Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation
for Spatial Games.” Proceedings of the National Academy of Sciences of the
United States of America, vol. 121, no. 50, e2405605121, National Academy
of Sciences, 2024, doi:10.1073/pnas.2405605121.
short: J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences
of the United States of America 121 (2024).
corr_author: '1'
date_created: 2024-12-22T23:01:47Z
date_published: 2024-12-10T00:00:00Z
date_updated: 2026-07-27T12:52:03Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1073/pnas.2405605121
ec_funded: 1
external_id:
isi:
- '001379596100014'
pmid:
- '39642209'
file:
- access_level: open_access
checksum: 0115e9090b478e0644308c6dab58605b
content_type: application/pdf
creator: dernst
date_created: 2025-01-02T12:14:15Z
date_updated: 2025-01-02T12:14:15Z
file_id: '18721'
file_name: 2024_PNAS_Svoboda.pdf
file_size: 2491151
relation: main_file
success: 1
file_date_updated: 2025-01-02T12:14:15Z
has_accepted_license: '1'
intvolume: ' 121'
isi: 1
issue: '50'
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'
publication: Proceedings of the National Academy of Sciences of the United States
of America
publication_identifier:
eissn:
- 1091-6490
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
related_material:
record:
- id: '20138'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Density amplifiers of cooperation for spatial games
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 121
year: '2024'
...
---
OA_type: closed access
_id: '18266'
abstract:
- lang: eng
text: Matrix games are the most basic model in game theory, and yet robustness with
respect to small perturbations of the matrix entries is not fully understood.
In this paper, we introduce value positivity and uniform value positivity, two
properties that refine the notion of optimality in the context of polynomially
perturbed matrix games. The first concept captures how the value depends on the
perturbation parameter, and the second consists of the existence of a fixed strategy
that guarantees the value of the unperturbed matrix game for every sufficiently
small positive parameter. We provide polynomial-time algorithms to check whether
a polynomially perturbed matrix game satisfies these properties. We further provide
the functional form for a parameterized optimal strategy and the value function.
Finally, we translate our results to linear programming and stochastic games,
where value positivity is related to the existence of robust solutions.
acknowledgement: This research was supported by Fondation CFM pour la Recherche, the
H2020 European Research Council [Grant ERC-CoG-863818 (ForM-SMArt)], the Austrian
Science Fund [Grant 10.55776/COE12], ANID Chile [Grant ACT210005], and Agence Nationale
de la Recherche [Grant ANR-21-CE40-0020].
article_processing_charge: No
article_type: original
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Miquel
full_name: Oliu-Barton, Miquel
last_name: Oliu-Barton
- 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: Chatterjee K, Oliu-Barton M, Saona Urmeneta RJ. Value-positivity for matrix
games. Mathematics of Operations Research. 2024;50(4):2433-3282. doi:10.1287/moor.2022.0332
apa: Chatterjee, K., Oliu-Barton, M., & Saona Urmeneta, R. J. (2024). Value-positivity
for matrix games. Mathematics of Operations Research. Institute for Operations
Research and the Management Sciences. https://doi.org/10.1287/moor.2022.0332
chicago: Chatterjee, Krishnendu, Miquel Oliu-Barton, and Raimundo J Saona Urmeneta.
“Value-Positivity for Matrix Games.” Mathematics of Operations Research.
Institute for Operations Research and the Management Sciences, 2024. https://doi.org/10.1287/moor.2022.0332.
ieee: K. Chatterjee, M. Oliu-Barton, and R. J. Saona Urmeneta, “Value-positivity
for matrix games,” Mathematics of Operations Research, vol. 50, no. 4.
Institute for Operations Research and the Management Sciences, pp. 2433–3282,
2024.
ista: Chatterjee K, Oliu-Barton M, Saona Urmeneta RJ. 2024. Value-positivity for
matrix games. Mathematics of Operations Research. 50(4), 2433–3282.
mla: Chatterjee, Krishnendu, et al. “Value-Positivity for Matrix Games.” Mathematics
of Operations Research, vol. 50, no. 4, Institute for Operations Research
and the Management Sciences, 2024, pp. 2433–3282, doi:10.1287/moor.2022.0332.
short: K. Chatterjee, M. Oliu-Barton, R.J. Saona Urmeneta, Mathematics of Operations
Research 50 (2024) 2433–3282.
corr_author: '1'
date_created: 2024-10-09T07:02:20Z
date_published: 2024-10-01T00:00:00Z
date_updated: 2026-07-29T13:14:36Z
day: '01'
department:
- _id: GradSch
- _id: KrCh
doi: 10.1287/moor.2022.0332
ec_funded: 1
external_id:
isi:
- '001328875900001'
intvolume: ' 50'
isi: 1
issue: '4'
language:
- iso: eng
month: '10'
oa_version: None
page: 2433-3282
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Mathematics of Operations Research
publication_identifier:
eissn:
- 1526-5471
issn:
- 0364-765X
publication_status: published
publisher: Institute for Operations Research and the Management Sciences
quality_controlled: '1'
related_material:
record:
- id: '20234'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Value-positivity for matrix games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 50
year: '2024'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '18630'
abstract:
- lang: eng
text: 'Markov chains are the de facto finite-state model for stochastic dynamical
systems, and Markov decision processes (MDPs) extend Markov chains by incorporating
non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization
criterion is the maximal expected total reward where the MDP stops after T steps,
which can be computed by a simple dynamic programming algorithm. We consider a
natural generalization of the problem where the stopping times can be chosen according
to a probability distribution, such that the expected stopping time is T, to optimize
the expected total reward. Quite surprisingly we establish inter-reducibility
of the expected stopping-time problem for Markov chains with the Positivity problem
(which is related to the well-known Skolem problem), for which establishing either
decidability or undecidability would be a major breakthrough. Given the hardness
of the exact problem, we consider the approximate version of the problem: we show
that it can be solved in exponential time for Markov chains and in exponential
space for MDPs.'
acknowledgement: The authors are grateful to the anonymous reviewers of LICS 2021
and of a previous version of this paper for insightful comments that helped improving
the presentation. The research presented in this paper was partially supported by
the grant ERC CoG 863818 (ForM-SMArt).
alternative_title:
- LMCS
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: Laurent
full_name: Doyen, Laurent
last_name: Doyen
citation:
ama: Chatterjee K, Doyen L. Stochastic processes with expected stopping time. Logical
Methods in Computer Science. 2024;20(4):11:1-11:34. doi:10.46298/lmcs-20(4:11)2024
apa: Chatterjee, K., & Doyen, L. (2024). Stochastic processes with expected
stopping time. Logical Methods in Computer Science. EPI Sciences. https://doi.org/10.46298/lmcs-20(4:11)2024
chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected
Stopping Time.” Logical Methods in Computer Science. EPI Sciences, 2024.
https://doi.org/10.46298/lmcs-20(4:11)2024.
ieee: K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,”
Logical Methods in Computer Science, vol. 20, no. 4. EPI Sciences, p. 11:1-11:34,
2024.
ista: Chatterjee K, Doyen L. 2024. Stochastic processes with expected stopping time.
Logical Methods in Computer Science. 20(4), 11:1-11:34.
mla: Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected
Stopping Time.” Logical Methods in Computer Science, vol. 20, no. 4, EPI
Sciences, 2024, p. 11:1-11:34, doi:10.46298/lmcs-20(4:11)2024.
short: K. Chatterjee, L. Doyen, Logical Methods in Computer Science 20 (2024) 11:1-11:34.
corr_author: '1'
date_created: 2024-12-08T23:01:56Z
date_published: 2024-11-12T00:00:00Z
date_updated: 2026-08-12T06:39:26Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.46298/lmcs-20(4:11)2024
ec_funded: 1
external_id:
arxiv:
- '2104.07278'
isi:
- '001367316400002'
file:
- access_level: open_access
checksum: b3315c74ce18ce0a30ed33d8c9972992
content_type: application/pdf
creator: dernst
date_created: 2024-12-09T08:38:48Z
date_updated: 2024-12-09T08:38:48Z
file_id: '18633'
file_name: 2024_LMCS_Chatterjee.pdf
file_size: 416814
relation: main_file
success: 1
file_date_updated: 2024-12-09T08:38:48Z
has_accepted_license: '1'
intvolume: ' 20'
isi: 1
issue: '4'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: 11:1-11:34
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Logical Methods in Computer Science
publication_identifier:
eissn:
- 1860-5974
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
record:
- id: '10004'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Stochastic processes with expected stopping time
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: 20
year: '2024'
...
---
_id: '12676'
abstract:
- lang: eng
text: Turn-based stochastic games (aka simple stochastic games) are two-player zero-sum
games played on directed graphs with probabilistic transitions. The goal of player-max
is to maximize the probability to reach a target state against the adversarial
player-min. These games lie in NP ∩ coNP and are among the rare combinatorial
problems that belong to this complexity class for which the existence of polynomial-time
algorithm is a major open question. While randomized sub-exponential time algorithm
exists, all known deterministic algorithms require exponential time in the worst-case.
An important open question has been whether faster algorithms can be obtained
parametrized by the treewidth of the game graph. Even deterministic sub-exponential
time algorithm for constant treewidth turn-based stochastic games has remain elusive.
In this work our main result is a deterministic algorithm to solve turn-based
stochastic games that, given a game with n states, treewidth at most t, and the
bit-complexity of the probabilistic transition function log D, has running time
O ((tn2 log D)t log n). In particular, our algorithm is quasi-polynomial time
for games with constant or poly-logarithmic treewidth.
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant.
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: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- 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, Meggendorfer T, Saona Urmeneta RJ, Svoboda J. Faster algorithm
for turn-based stochastic games with bounded treewidth. In: Proceedings of
the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms. Society for Industrial
and Applied Mathematics; 2023:4590-4605. doi:10.1137/1.9781611977554.ch173'
apa: 'Chatterjee, K., Meggendorfer, T., Saona Urmeneta, R. J., & Svoboda, J.
(2023). Faster algorithm for turn-based stochastic games with bounded treewidth.
In Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms
(pp. 4590–4605). Florence, Italy: Society for Industrial and Applied Mathematics.
https://doi.org/10.1137/1.9781611977554.ch173'
chicago: Chatterjee, Krishnendu, Tobias Meggendorfer, Raimundo J Saona Urmeneta,
and Jakub Svoboda. “Faster Algorithm for Turn-Based Stochastic Games with Bounded
Treewidth.” In Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete
Algorithms, 4590–4605. Society for Industrial and Applied Mathematics, 2023.
https://doi.org/10.1137/1.9781611977554.ch173.
ieee: K. Chatterjee, T. Meggendorfer, R. J. Saona Urmeneta, and J. Svoboda, “Faster
algorithm for turn-based stochastic games with bounded treewidth,” in Proceedings
of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms, Florence, Italy,
2023, pp. 4590–4605.
ista: 'Chatterjee K, Meggendorfer T, Saona Urmeneta RJ, Svoboda J. 2023. Faster
algorithm for turn-based stochastic games with bounded treewidth. Proceedings
of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium
on Discrete Algorithms, 4590–4605.'
mla: Chatterjee, Krishnendu, et al. “Faster Algorithm for Turn-Based Stochastic
Games with Bounded Treewidth.” Proceedings of the 2023 Annual ACM-SIAM Symposium
on Discrete Algorithms, Society for Industrial and Applied Mathematics, 2023,
pp. 4590–605, doi:10.1137/1.9781611977554.ch173.
short: K. Chatterjee, T. Meggendorfer, R.J. Saona Urmeneta, J. Svoboda, in:, Proceedings
of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial
and Applied Mathematics, 2023, pp. 4590–4605.
conference:
end_date: 2023-01-25
location: Florence, Italy
name: 'SODA: Symposium on Discrete Algorithms'
start_date: 2023-01-22
corr_author: '1'
date_created: 2023-02-24T12:20:47Z
date_published: 2023-02-01T00:00:00Z
date_updated: 2026-06-18T17:28:38Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
doi: 10.1137/1.9781611977554.ch173
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1137/1.9781611977554.ch173
month: '02'
oa: 1
oa_version: Published Version
page: 4590-4605
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 2023 Annual ACM-SIAM Symposium on Discrete Algorithms
publication_identifier:
isbn:
- '9781611977554'
publication_status: published
publisher: Society for Industrial and Applied Mathematics
quality_controlled: '1'
status: public
title: Faster algorithm for turn-based stochastic games with bounded treewidth
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '12706'
abstract:
- lang: eng
text: Allometric settings of population dynamics models are appealing due to their
parsimonious nature and broad utility when studying system level effects. Here,
we parameterise the size-scaled Rosenzweig-MacArthur differential equations to
eliminate prey-mass dependency, facilitating an in depth analytic study of the
equations which incorporates scaling parameters’ contributions to coexistence.
We define the functional response term to match empirical findings, and examine
situations where metabolic theory derivations and observation diverge. The dynamical
properties of the Rosenzweig-MacArthur system, encompassing the distribution of
size-abundance equilibria, the scaling of period and amplitude of population cycling,
and relationships between predator and prey abundances, are consistent with empirical
observation. Our parameterisation is an accurate minimal model across 15+ orders
of mass magnitude.
acknowledgement: "This research was supported by an Australian Government Research
Training Program\r\n(RTP) Scholarship to JCM (https://www.dese.gov.au), and LB is
supported by the Centre de\r\nrecherche sur le vieillissement Fellowship Program.
The funders had no role in study design, data collection and analysis, decision
to publish, or preparation of the manuscript."
article_processing_charge: No
article_type: original
author:
- first_name: Jody C.
full_name: Mckerral, Jody C.
last_name: Mckerral
- first_name: Maria
full_name: Kleshnina, Maria
id: 4E21749C-F248-11E8-B48F-1D18A9856A87
last_name: Kleshnina
- first_name: Vladimir
full_name: Ejov, Vladimir
last_name: Ejov
- first_name: Louise
full_name: Bartle, Louise
last_name: Bartle
- first_name: James G.
full_name: Mitchell, James G.
last_name: Mitchell
- first_name: Jerzy A.
full_name: Filar, Jerzy A.
last_name: Filar
citation:
ama: Mckerral JC, Kleshnina M, Ejov V, Bartle L, Mitchell JG, Filar JA. Empirical
parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur
equations. PLoS One. 2023;18(2):e0279838. doi:10.1371/journal.pone.0279838
apa: Mckerral, J. C., Kleshnina, M., Ejov, V., Bartle, L., Mitchell, J. G., &
Filar, J. A. (2023). Empirical parameterisation and dynamical analysis of the
allometric Rosenzweig-MacArthur equations. PLoS One. Public Library of
Science. https://doi.org/10.1371/journal.pone.0279838
chicago: Mckerral, Jody C., Maria Kleshnina, Vladimir Ejov, Louise Bartle, James
G. Mitchell, and Jerzy A. Filar. “Empirical Parameterisation and Dynamical Analysis
of the Allometric Rosenzweig-MacArthur Equations.” PLoS One. Public Library
of Science, 2023. https://doi.org/10.1371/journal.pone.0279838.
ieee: J. C. Mckerral, M. Kleshnina, V. Ejov, L. Bartle, J. G. Mitchell, and J. A.
Filar, “Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur
equations,” PLoS One, vol. 18, no. 2. Public Library of Science, p. e0279838,
2023.
ista: Mckerral JC, Kleshnina M, Ejov V, Bartle L, Mitchell JG, Filar JA. 2023. Empirical
parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur
equations. PLoS One. 18(2), e0279838.
mla: Mckerral, Jody C., et al. “Empirical Parameterisation and Dynamical Analysis
of the Allometric Rosenzweig-MacArthur Equations.” PLoS One, vol. 18, no.
2, Public Library of Science, 2023, p. e0279838, doi:10.1371/journal.pone.0279838.
short: J.C. Mckerral, M. Kleshnina, V. Ejov, L. Bartle, J.G. Mitchell, J.A. Filar,
PLoS One 18 (2023) e0279838.
date_created: 2023-03-05T23:01:05Z
date_published: 2023-02-27T00:00:00Z
date_updated: 2023-10-17T12:53:30Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1371/journal.pone.0279838
external_id:
isi:
- '000996122900022'
pmid:
- '36848357'
file:
- access_level: open_access
checksum: 798ed5739a4117b03173e5d56e0534c9
content_type: application/pdf
creator: cchlebak
date_created: 2023-03-07T10:26:45Z
date_updated: 2023-03-07T10:26:45Z
file_id: '12712'
file_name: 2023_PLOSOne_Mckerral.pdf
file_size: 1257003
relation: main_file
success: 1
file_date_updated: 2023-03-07T10:26:45Z
has_accepted_license: '1'
intvolume: ' 18'
isi: 1
issue: '2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: e0279838
pmid: 1
publication: PLoS One
publication_identifier:
eissn:
- 1932-6203
publication_status: published
publisher: Public Library of Science
quality_controlled: '1'
scopus_import: '1'
status: public
title: Empirical parameterisation and dynamical analysis of the allometric Rosenzweig-MacArthur
equations
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: 18
year: '2023'
...
---
_id: '12833'
abstract:
- lang: eng
text: 'The input to the token swapping problem is a graph with vertices v1, v2,
. . . , vn, and n tokens with labels 1,2, . . . , n, one on each vertex. The goal
is to get token i to vertex vi for all i= 1, . . . , n using a minimum number
of swaps, where a swap exchanges the tokens on the endpoints of an edge.Token
swapping on a tree, also known as “sorting with a transposition tree,” is not
known to be in P nor NP-complete. We present some partial results: 1. An optimum
swap sequence may need to perform a swap on a leaf vertex that has the correct
token (a “happy leaf”), disproving a conjecture of Vaughan. 2. Any algorithm that
fixes happy leaves—as all known approximation algorithms for the problem do—has
approximation factor at least 4/3. Furthermore, the two best-known 2-approximation
algorithms have approximation factor exactly 2. 3. A generalized problem—weighted
coloured token swapping—is NP-complete on trees, but solvable in polynomial time
on paths and stars. In this version, tokens and vertices have colours, and colours
have weights. The goal is to get every token to a vertex of the same colour, and
the cost of a swap is the sum of the weights of the two tokens involved.'
acknowledgement: "This work was begun at the University of Waterloo and was partially
supported by the Natural Sciences and Engineering Council of Canada (NSERC).\r\n"
article_number: '9'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Ahmad
full_name: Biniaz, Ahmad
last_name: Biniaz
- first_name: Kshitij
full_name: Jain, Kshitij
last_name: Jain
- first_name: Anna
full_name: Lubiw, Anna
last_name: Lubiw
- first_name: Zuzana
full_name: Masárová, Zuzana
id: 45CFE238-F248-11E8-B48F-1D18A9856A87
last_name: Masárová
orcid: 0000-0002-6660-1322
- first_name: Tillmann
full_name: Miltzow, Tillmann
last_name: Miltzow
- first_name: Debajyoti
full_name: Mondal, Debajyoti
last_name: Mondal
- first_name: Anurag Murty
full_name: Naredla, Anurag Murty
last_name: Naredla
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Alexi
full_name: Turcotte, Alexi
last_name: Turcotte
citation:
ama: Biniaz A, Jain K, Lubiw A, et al. Token swapping on trees. Discrete Mathematics
and Theoretical Computer Science. 2023;24(2). doi:10.46298/DMTCS.8383
apa: Biniaz, A., Jain, K., Lubiw, A., Masárová, Z., Miltzow, T., Mondal, D., … Turcotte,
A. (2023). Token swapping on trees. Discrete Mathematics and Theoretical Computer
Science. EPI Sciences. https://doi.org/10.46298/DMTCS.8383
chicago: Biniaz, Ahmad, Kshitij Jain, Anna Lubiw, Zuzana Masárová, Tillmann Miltzow,
Debajyoti Mondal, Anurag Murty Naredla, Josef Tkadlec, and Alexi Turcotte. “Token
Swapping on Trees.” Discrete Mathematics and Theoretical Computer Science.
EPI Sciences, 2023. https://doi.org/10.46298/DMTCS.8383.
ieee: A. Biniaz et al., “Token swapping on trees,” Discrete Mathematics
and Theoretical Computer Science, vol. 24, no. 2. EPI Sciences, 2023.
ista: Biniaz A, Jain K, Lubiw A, Masárová Z, Miltzow T, Mondal D, Naredla AM, Tkadlec
J, Turcotte A. 2023. Token swapping on trees. Discrete Mathematics and Theoretical
Computer Science. 24(2), 9.
mla: Biniaz, Ahmad, et al. “Token Swapping on Trees.” Discrete Mathematics and
Theoretical Computer Science, vol. 24, no. 2, 9, EPI Sciences, 2023, doi:10.46298/DMTCS.8383.
short: A. Biniaz, K. Jain, A. Lubiw, Z. Masárová, T. Miltzow, D. Mondal, A.M. Naredla,
J. Tkadlec, A. Turcotte, Discrete Mathematics and Theoretical Computer Science
24 (2023).
date_created: 2023-04-16T22:01:08Z
date_published: 2023-01-18T00:00:00Z
date_updated: 2025-01-20T14:05:09Z
day: '18'
ddc:
- '000'
department:
- _id: KrCh
- _id: HeEd
- _id: UlWa
doi: 10.46298/DMTCS.8383
external_id:
arxiv:
- '1903.06981'
file:
- access_level: open_access
checksum: 439102ea4f6e2aeefd7107dfb9ccf532
content_type: application/pdf
creator: dernst
date_created: 2023-04-17T08:10:28Z
date_updated: 2023-04-17T08:10:28Z
file_id: '12844'
file_name: 2022_DMTCS_Biniaz.pdf
file_size: 2072197
relation: main_file
success: 1
file_date_updated: 2023-04-17T08:10:28Z
has_accepted_license: '1'
intvolume: ' 24'
issue: '2'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
publication: Discrete Mathematics and Theoretical Computer Science
publication_identifier:
eissn:
- 1365-8050
issn:
- 1462-7264
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
record:
- id: '7950'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Token swapping on trees
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 24
year: '2023'
...
---
_id: '12861'
abstract:
- lang: eng
text: The field of indirect reciprocity investigates how social norms can foster
cooperation when individuals continuously monitor and assess each other’s social
interactions. By adhering to certain social norms, cooperating individuals can
improve their reputation and, in turn, receive benefits from others. Eight social
norms, known as the “leading eight," have been shown to effectively promote the
evolution of cooperation as long as information is public and reliable. These
norms categorize group members as either ’good’ or ’bad’. In this study, we examine
a scenario where individuals instead assign nuanced reputation scores to each
other, and only cooperate with those whose reputation exceeds a certain threshold.
We find both analytically and through simulations that such quantitative assessments
are error-correcting, thus facilitating cooperation in situations where information
is private and unreliable. Moreover, our results identify four specific norms
that are robust to such conditions, and may be relevant for helping to sustain
cooperation in natural populations.
acknowledgement: 'This work was supported by the European Research Council CoG 863818
(ForM-SMArt) (to K.C.) and the European Research Council Starting Grant 850529:
E-DIRECT (to C.H.). L.S. received additional partial support by the Austrian Science
Fund (FWF) under grant Z211-N23 (Wittgenstein Award), and also thanks the support
by the Stochastic Analysis and Application Research Center (SAARC) under National
Research Foundation of Korea grant NRF-2019R1A5A1028324. The authors additionally
thank Stefan Schmid for providing access to his lab infrastructure at the University
of Vienna for the purpose of collecting simulation data.'
article_number: '2086'
article_processing_charge: No
article_type: original
author:
- first_name: Laura
full_name: Schmid, Laura
id: 38B437DE-F248-11E8-B48F-1D18A9856A87
last_name: Schmid
orcid: 0000-0002-6978-7329
- first_name: Farbod
full_name: Ekbatani, Farbod
last_name: Ekbatani
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Schmid L, Ekbatani F, Hilbe C, Chatterjee K. Quantitative assessment can stabilize
indirect reciprocity under imperfect information. Nature Communications.
2023;14. doi:10.1038/s41467-023-37817-x
apa: Schmid, L., Ekbatani, F., Hilbe, C., & Chatterjee, K. (2023). Quantitative
assessment can stabilize indirect reciprocity under imperfect information. Nature
Communications. Springer Nature. https://doi.org/10.1038/s41467-023-37817-x
chicago: Schmid, Laura, Farbod Ekbatani, Christian Hilbe, and Krishnendu Chatterjee.
“Quantitative Assessment Can Stabilize Indirect Reciprocity under Imperfect Information.”
Nature Communications. Springer Nature, 2023. https://doi.org/10.1038/s41467-023-37817-x.
ieee: L. Schmid, F. Ekbatani, C. Hilbe, and K. Chatterjee, “Quantitative assessment
can stabilize indirect reciprocity under imperfect information,” Nature Communications,
vol. 14. Springer Nature, 2023.
ista: Schmid L, Ekbatani F, Hilbe C, Chatterjee K. 2023. Quantitative assessment
can stabilize indirect reciprocity under imperfect information. Nature Communications.
14, 2086.
mla: Schmid, Laura, et al. “Quantitative Assessment Can Stabilize Indirect Reciprocity
under Imperfect Information.” Nature Communications, vol. 14, 2086, Springer
Nature, 2023, doi:10.1038/s41467-023-37817-x.
short: L. Schmid, F. Ekbatani, C. Hilbe, K. Chatterjee, Nature Communications 14
(2023).
date_created: 2023-04-23T22:01:03Z
date_published: 2023-04-12T00:00:00Z
date_updated: 2025-04-15T06:26:15Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/s41467-023-37817-x
ec_funded: 1
external_id:
isi:
- '001003644100020'
pmid:
- '37045828'
file:
- access_level: open_access
checksum: a4b3b7b36fbef068cabf4fb99501fef6
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T09:13:53Z
date_updated: 2023-04-25T09:13:53Z
file_id: '12868'
file_name: 2023_NatureComm_Schmid.pdf
file_size: 1786475
relation: main_file
success: 1
file_date_updated: 2023-04-25T09:13:53Z
has_accepted_license: '1'
intvolume: ' 14'
isi: 1
language:
- iso: eng
month: '04'
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: Nature Communications
publication_identifier:
eissn:
- 2041-1723
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative assessment can stabilize indirect reciprocity under imperfect
information
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 14
year: '2023'
...
---
_id: '13139'
abstract:
- lang: eng
text: A classical problem for Markov chains is determining their stationary (or
steady-state) distribution. This problem has an equally classical solution based
on eigenvectors and linear equation systems. However, this approach does not scale
to large instances, and iterative solutions are desirable. It turns out that a
naive approach, as used by current model checkers, may yield completely wrong
results. We present a new approach, which utilizes recent advances in partial
exploration and mean payoff computation to obtain a correct, converging approximation.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
citation:
ama: 'Meggendorfer T. Correct approximation of stationary distributions. In: TACAS
2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol
13993. Springer Nature; 2023:489-507. doi:10.1007/978-3-031-30823-9_25'
apa: 'Meggendorfer, T. (2023). Correct approximation of stationary distributions.
In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 13993, pp. 489–507). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_25'
chicago: 'Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.”
In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
13993:489–507. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_25.'
ieee: 'T. Meggendorfer, “Correct approximation of stationary distributions,” in
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
Paris, France, 2023, vol. 13993, pp. 489–507.'
ista: 'Meggendorfer T. 2023. Correct approximation of stationary distributions.
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 13993, 489–507.'
mla: 'Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.”
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13993, Springer Nature, 2023, pp. 489–507, doi:10.1007/978-3-031-30823-9_25.'
short: 'T. Meggendorfer, in:, TACAS 2023: Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 489–507.'
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-06-18T22:00:46Z
date_published: 2023-04-22T00:00:00Z
date_updated: 2025-09-09T12:28:12Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-30823-9_25
external_id:
arxiv:
- '2301.08137'
isi:
- '001288688000025'
file:
- access_level: open_access
checksum: 59f707a3949c03793251b0d04c62542a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T07:18:40Z
date_updated: 2023-06-19T07:18:40Z
file_id: '13148'
file_name: 2023_LNCS_Meggendorfer.pdf
file_size: 521951
relation: main_file
success: 1
file_date_updated: 2023-06-19T07:18:40Z
has_accepted_license: '1'
intvolume: ' 13993'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 489-507
publication: 'TACAS 2023: Tools and Algorithms for the Construction and Analysis of
Systems'
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308222'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14990'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Correct approximation of stationary distributions
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13993
year: '2023'
...
---
_id: '13142'
abstract:
- lang: eng
text: Reinforcement learning has received much attention for learning controllers
of deterministic systems. We consider a learner-verifier framework for stochastic
control systems and survey recent methods that formally guarantee a conjunction
of reachability and safety properties. Given a property and a lower bound on the
probability of the property being satisfied, our framework jointly learns a control
policy and a formal certificate to ensure the satisfaction of the property with
a desired probability threshold. Both the control policy and the formal certificate
are continuous functions from states to reals, which are learned as parameterized
neural networks. While in the deterministic case, the certificates are invariant
and barrier functions for safety, or Lyapunov and ranking functions for liveness,
in the stochastic case the certificates are supermartingales. For certificate
verification, we use interval arithmetic abstract interpretation to bound the
expected values of neural network functions.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) 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
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: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- 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, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework
for neural network controllers and certificates of stochastic systems. In: Tools
and Algorithms for the Construction and Analysis of Systems . Vol 13993. Springer
Nature; 2023:3-25. doi:10.1007/978-3-031-30823-9_1'
apa: 'Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic, D. (2023). A
learner-verifier framework for neural network controllers and certificates of
stochastic systems. In Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_1'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde
Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates
of Stochastic Systems.” In Tools and Algorithms for the Construction and Analysis
of Systems , 13993:3–25. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_1.
ieee: K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier
framework for neural network controllers and certificates of stochastic systems,”
in Tools and Algorithms for the Construction and Analysis of Systems ,
Paris, France, 2023, vol. 13993, pp. 3–25.
ista: 'Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier
framework for neural network controllers and certificates of stochastic systems.
Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993,
3–25.'
mla: Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network
Controllers and Certificates of Stochastic Systems.” Tools and Algorithms for
the Construction and Analysis of Systems , vol. 13993, Springer Nature, 2023,
pp. 3–25, doi:10.1007/978-3-031-30823-9_1.
short: K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms
for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-06-18T22:00:47Z
date_published: 2023-04-22T00:00:00Z
date_updated: 2025-09-09T12:29:26Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-031-30823-9_1
ec_funded: 1
external_id:
isi:
- '001288688000001'
file:
- access_level: open_access
checksum: 3d8a8bb24d211bc83360dfc2fd744307
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T08:29:30Z
date_updated: 2023-06-19T08:29:30Z
file_id: '13150'
file_name: 2023_LNCS_Chatterjee.pdf
file_size: 528455
relation: main_file
success: 1
file_date_updated: 2023-06-19T08:29:30Z
has_accepted_license: '1'
intvolume: ' 13993'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 3-25
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: 'Tools and Algorithms for the Construction and Analysis of Systems '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308222'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: A learner-verifier framework for neural network controllers and certificates
of stochastic systems
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13993
year: '2023'
...
---
_id: '13258'
abstract:
- lang: eng
text: Many human interactions feature the characteristics of social dilemmas where
individual actions have consequences for the group and the environment. The feedback
between behavior and environment can be studied with the framework of stochastic
games. In stochastic games, the state of the environment can change, depending
on the choices made by group members. Past work suggests that such feedback can
reinforce cooperative behaviors. In particular, cooperation can evolve in stochastic
games even if it is infeasible in each separate repeated game. In stochastic games,
participants have an interest in conditioning their strategies on the state of
the environment. Yet in many applications, precise information about the state
could be scarce. Here, we study how the availability of information (or lack thereof)
shapes evolution of cooperation. Already for simple examples of two state games
we find surprising effects. In some cases, cooperation is only possible if there
is precise information about the state of the environment. In other cases, cooperation
is most abundant when there is no information about the state of the environment.
We systematically analyze all stochastic games of a given complexity class, to
determine when receiving information about the environment is better, neutral,
or worse for evolution of cooperation.
acknowledgement: 'This work was supported by the European Research Council CoG 863818
(ForM-SMArt) (to K.C.), the European Research Council Starting Grant 850529: E-DIRECT
(to C.H.), the European Union’s Horizon 2020 research and innovation program under
the Marie Sklodowska-Curie Grant Agreement #754411 and the French Agence Nationale
de la Recherche (under the Investissement d’Avenir programme, ANR-17-EURE-0010)
(to M.K.).'
article_number: '4153'
article_processing_charge: Yes
article_type: original
author:
- first_name: Maria
full_name: Kleshnina, Maria
id: 4E21749C-F248-11E8-B48F-1D18A9856A87
last_name: Kleshnina
- first_name: Christian
full_name: Hilbe, Christian
id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
last_name: Hilbe
orcid: 0000-0001-5116-955X
- first_name: Stepan
full_name: Simsa, Stepan
id: 409d615c-2f95-11ee-b934-90a352102c1e
last_name: Simsa
orcid: 0000-0001-6687-1210
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Martin A.
full_name: Nowak, Martin A.
last_name: Nowak
citation:
ama: Kleshnina M, Hilbe C, Simsa S, Chatterjee K, Nowak MA. The effect of environmental
information on evolution of cooperation in stochastic games. Nature Communications.
2023;14. doi:10.1038/s41467-023-39625-9
apa: Kleshnina, M., Hilbe, C., Simsa, S., Chatterjee, K., & Nowak, M. A. (2023).
The effect of environmental information on evolution of cooperation in stochastic
games. Nature Communications. Springer Nature. https://doi.org/10.1038/s41467-023-39625-9
chicago: Kleshnina, Maria, Christian Hilbe, Stepan Simsa, Krishnendu Chatterjee,
and Martin A. Nowak. “The Effect of Environmental Information on Evolution of
Cooperation in Stochastic Games.” Nature Communications. Springer Nature,
2023. https://doi.org/10.1038/s41467-023-39625-9.
ieee: M. Kleshnina, C. Hilbe, S. Simsa, K. Chatterjee, and M. A. Nowak, “The effect
of environmental information on evolution of cooperation in stochastic games,”
Nature Communications, vol. 14. Springer Nature, 2023.
ista: Kleshnina M, Hilbe C, Simsa S, Chatterjee K, Nowak MA. 2023. The effect of
environmental information on evolution of cooperation in stochastic games. Nature
Communications. 14, 4153.
mla: Kleshnina, Maria, et al. “The Effect of Environmental Information on Evolution
of Cooperation in Stochastic Games.” Nature Communications, vol. 14, 4153,
Springer Nature, 2023, doi:10.1038/s41467-023-39625-9.
short: M. Kleshnina, C. Hilbe, S. Simsa, K. Chatterjee, M.A. Nowak, Nature Communications
14 (2023).
corr_author: '1'
date_created: 2023-07-23T22:01:11Z
date_published: 2023-07-12T00:00:00Z
date_updated: 2025-04-14T07:43:55Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/s41467-023-39625-9
ec_funded: 1
external_id:
isi:
- '001029450400031'
pmid:
- '37438341'
file:
- access_level: open_access
checksum: 5aceefdfe76686267b93ae4fe81899f1
content_type: application/pdf
creator: dernst
date_created: 2023-07-31T11:32:36Z
date_updated: 2023-07-31T11:32:36Z
file_id: '13337'
file_name: 2023_NatureComm_Kleshnina.pdf
file_size: 1601682
relation: main_file
success: 1
file_date_updated: 2023-07-31T11:32:36Z
has_accepted_license: '1'
intvolume: ' 14'
isi: 1
language:
- iso: eng
month: '07'
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: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: Nature Communications
publication_identifier:
eissn:
- 2041-1723
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '13336'
relation: research_data
status: public
scopus_import: '1'
status: public
title: The effect of environmental information on evolution of cooperation in stochastic
games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14
year: '2023'
...
---
_id: '13336'
article_processing_charge: No
author:
- first_name: Maria
full_name: Kleshnina, Maria
id: 4E21749C-F248-11E8-B48F-1D18A9856A87
last_name: Kleshnina
citation:
ama: 'Kleshnina M. kleshnina/stochgames_info: The effect of environmental information
on evolution of cooperation in stochastic games. 2023. doi:10.5281/ZENODO.8059564'
apa: 'Kleshnina, M. (2023). kleshnina/stochgames_info: The effect of environmental
information on evolution of cooperation in stochastic games. Zenodo. https://doi.org/10.5281/ZENODO.8059564'
chicago: 'Kleshnina, Maria. “Kleshnina/Stochgames_info: The Effect of Environmental
Information on Evolution of Cooperation in Stochastic Games.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.8059564.'
ieee: 'M. Kleshnina, “kleshnina/stochgames_info: The effect of environmental information
on evolution of cooperation in stochastic games.” Zenodo, 2023.'
ista: 'Kleshnina M. 2023. kleshnina/stochgames_info: The effect of environmental
information on evolution of cooperation in stochastic games, Zenodo, 10.5281/ZENODO.8059564.'
mla: 'Kleshnina, Maria. Kleshnina/Stochgames_info: The Effect of Environmental
Information on Evolution of Cooperation in Stochastic Games. Zenodo, 2023,
doi:10.5281/ZENODO.8059564.'
short: M. Kleshnina, (2023).
corr_author: '1'
date_created: 2023-07-31T11:30:46Z
date_published: 2023-06-20T00:00:00Z
date_updated: 2025-04-15T06:54:58Z
day: '20'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.5281/ZENODO.8059564
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/zenodo.8059564
month: '06'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '13258'
relation: used_in_publication
status: public
status: public
title: 'kleshnina/stochgames_info: The effect of environmental information on evolution
of cooperation in stochastic games'
type: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '14242'
abstract:
- lang: eng
text: We study the problem of training and certifying adversarially robust quantized
neural networks (QNNs). Quantization is a technique for making neural networks
more efficient by running them using low-bit integer arithmetic and is therefore
commonly adopted in industry. Recent work has shown that floating-point neural
networks that have been verified to be robust can become vulnerable to adversarial
attacks after quantization, and certification of the quantized representation
is necessary to guarantee robustness. In this work, we present quantization-aware
interval bound propagation (QA-IBP), a novel method for training robust QNNs.
Inspired by advances in robust learning of non-quantized networks, our training
algorithm computes the gradient of an abstract representation of the actual network.
Unlike existing approaches, our method can handle the discrete semantics of QNNs.
Based on QA-IBP, we also develop a complete verification procedure for verifying
the adversarial robustness of QNNs, which is guaranteed to terminate and produce
a correct answer. Compared to existing approaches, the key advantage of our verification
procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate
experimentally that our approach significantly outperforms existing methods and
establish the new state-of-the-art for training and certifying the robustness
of QNNs.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. Research
was sponsored by the United\r\nStates Air Force Research Laboratory and the United
States Air Force Artificial Intelligence Accelerator and was accomplished under
Cooperative Agreement Number FA8750-19-2-\r\n1000. The views and conclusions contained
in this document are those of the authors and should not be interpreted as representing
the official policies, either expressed or implied,\r\nof the United States Air
Force or the U.S. Government. The U.S. Government is authorized to reproduce and
distribute reprints for Government purposes notwithstanding any copyright\r\nnotation
herein. The research was also funded in part by the AI2050 program at Schmidt Futures
(Grant G-22-63172) and Capgemini SE."
article_processing_charge: No
arxiv: 1
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- 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: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks.
In: Proceedings of the 37th AAAI Conference on Artificial Intelligence.
Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973.
doi:10.1609/aaai.v37i12.26747'
apa: 'Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., & Rus, D.
(2023). Quantization-aware interval bound propagation for training certifiably
robust quantized neural networks. In Proceedings of the 37th AAAI Conference
on Artificial Intelligence (Vol. 37, pp. 14964–14973). Washington, DC, United
States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i12.26747'
chicago: Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, Thomas A Henzinger,
and Daniela Rus. “Quantization-Aware Interval Bound Propagation for Training Certifiably
Robust Quantized Neural Networks.” In Proceedings of the 37th AAAI Conference
on Artificial Intelligence, 37:14964–73. Association for the Advancement of
Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i12.26747.
ieee: M. Lechner, D. Zikelic, K. Chatterjee, T. A. Henzinger, and D. Rus, “Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks,”
in Proceedings of the 37th AAAI Conference on Artificial Intelligence,
Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973.
ista: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks.
Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference
on Artificial Intelligence vol. 37, 14964–14973.'
mla: Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for
Training Certifiably Robust Quantized Neural Networks.” Proceedings of the
37th AAAI Conference on Artificial Intelligence, vol. 37, no. 12, Association
for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:10.1609/aaai.v37i12.26747.
short: M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, D. Rus, in:, Proceedings
of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2023, pp. 14964–14973.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2023-08-27T22:01:17Z
date_published: 2023-06-26T00:00:00Z
date_updated: 2025-03-31T16:01:08Z
day: '26'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i12.26747
ec_funded: 1
external_id:
arxiv:
- '2211.16187'
intvolume: ' 37'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2211.16187
month: '06'
oa: 1
oa_version: Preprint
page: 14964-14973
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _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: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781577358800'
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantization-aware interval bound propagation for training certifiably robust
quantized neural networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '14317'
abstract:
- lang: eng
text: "Markov decision processes can be viewed as transformers of probability distributions.
While this view is useful from a practical standpoint to reason about trajectories
of distributions, basic reachability and safety problems are known to be computationally
intractable (i.e., Skolem-hard) to solve in such models. Further, we show that
even for simple examples of MDPs, strategies for safety objectives over distributions
can require infinite memory and randomization.\r\nIn light of this, we present
a novel overapproximation approach to synthesize strategies in an MDP, such that
a safety objective over the distributions is met. More precisely, we develop a
new framework for template-based synthesis of certificates as affine distributional
and inductive invariants for safety objectives in MDPs. We provide two algorithms
within this framework. One can only synthesize memoryless strategies, but has
relative completeness guarantees, while the other can synthesize general strategies.
The runtime complexity of both algorithms is in PSPACE. We implement these algorithms
and show that they can solve several non-trivial examples."
acknowledgement: This work was supported in part by the ERC CoG 863818 (FoRM-SMArt)
and the European Union’s Horizon 2020 research and innovation programme under the
Marie Skłodowska-Curie Grant Agreement No. 665385 as well as DST/CEFIPRA/INRIA project
EQuaVE and SERB Matrices grant MTR/2018/00074.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: S.
full_name: Akshay, S.
last_name: Akshay
- 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: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. MDPs as distribution transformers:
Affine invariant synthesis for safety objectives. In: International Conference
on Computer Aided Verification. Vol 13966. Springer Nature; 2023:86-112. doi:10.1007/978-3-031-37709-9_5'
apa: 'Akshay, S., Chatterjee, K., Meggendorfer, T., & Zikelic, D. (2023). MDPs
as distribution transformers: Affine invariant synthesis for safety objectives.
In International Conference on Computer Aided Verification (Vol. 13966,
pp. 86–112). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37709-9_5'
chicago: 'Akshay, S., Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic.
“MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.”
In International Conference on Computer Aided Verification, 13966:86–112.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37709-9_5.'
ieee: 'S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “MDPs as distribution
transformers: Affine invariant synthesis for safety objectives,” in International
Conference on Computer Aided Verification, Paris, France, 2023, vol. 13966,
pp. 86–112.'
ista: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution
transformers: Affine invariant synthesis for safety objectives. International
Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 13966, 86–112.'
mla: 'Akshay, S., et al. “MDPs as Distribution Transformers: Affine Invariant Synthesis
for Safety Objectives.” International Conference on Computer Aided Verification,
vol. 13966, Springer Nature, 2023, pp. 86–112, doi:10.1007/978-3-031-37709-9_5.'
short: S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International
Conference on Computer Aided Verification, Springer Nature, 2023, pp. 86–112.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-09-10T22:01:12Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2025-09-09T12:56:00Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37709-9_5
ec_funded: 1
external_id:
isi:
- '001310805600005'
file:
- access_level: open_access
checksum: f143c8eedf609f20f2aad2eeb496d53f
content_type: application/pdf
creator: dernst
date_created: 2023-09-20T08:46:43Z
date_updated: 2023-09-20T08:46:43Z
file_id: '14349'
file_name: 2023_LNCS_Akshay.pdf
file_size: 531745
relation: main_file
success: 1
file_date_updated: 2023-09-20T08:46:43Z
has_accepted_license: '1'
intvolume: ' 13966'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 86-112
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031377082'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'MDPs as distribution transformers: Affine invariant synthesis for safety objectives'
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13966
year: '2023'
...