---
_id: '15006'
abstract:
- lang: eng
text: Graphical games are a useful framework for modeling the interactions of (selfish)
agents who are connected via an underlying topology and whose behaviors influence
each other. They have wide applications ranging from computer science to economics
and biology. Yet, even though an agent’s payoff only depends on the actions of
their direct neighbors in graphical games, computing the Nash equilibria and making
statements about the convergence time of "natural" local dynamics in particular
can be highly challenging. In this work, we present a novel approach for classifying
complexity of Nash equilibria in graphical games by establishing a connection
to local graph algorithms, a subfield of distributed computing. In particular,
we make the observation that the equilibria of graphical games are equivalent
to locally verifiable labelings (LVL) in graphs; vertex labelings which are verifiable
with constant-round local algorithms. This connection allows us to derive novel
lower bounds on the convergence time to equilibrium of best-response dynamics
in graphical games. Since we establish that distributed convergence can sometimes
be provably slow, we also introduce and give bounds on an intuitive notion of
"time-constrained" inefficiency of best responses. We exemplify how our results
can be used in the implementation of mechanisms that ensure convergence of best
responses to a Nash equilibrium. Our results thus also give insight into the convergence
of strategy-proof algorithms for graphical games, which is still not well understood.
acknowledgement: This work was partially funded by the Academy of Finland, grant 314888,
the European Research Council CoG 863818 (ForM-SMArt), and the Austrian Science
Fund (FWF) project I 4800-N (ADVISE). LS was supported by the Stochastic Analysis
and Application Research Center (SAARC) under National Research Foundation of Korea
grant NRF-2019R1A5A1028324.
alternative_title:
- LIPIcs
article_number: '11'
article_processing_charge: No
arxiv: 1
author:
- first_name: Juho
full_name: Hirvonen, Juho
last_name: Hirvonen
- first_name: Laura
full_name: Schmid, Laura
id: 38B437DE-F248-11E8-B48F-1D18A9856A87
last_name: Schmid
orcid: 0000-0002-6978-7329
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Stefan
full_name: Schmid, Stefan
last_name: Schmid
citation:
ama: 'Hirvonen J, Schmid L, Chatterjee K, Schmid S. On the convergence time in graphical
games: A locality-sensitive approach. In: 27th International Conference on
Principles of Distributed Systems. Vol 286. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2024. doi:10.4230/LIPIcs.OPODIS.2023.11'
apa: 'Hirvonen, J., Schmid, L., Chatterjee, K., & Schmid, S. (2024). On the
convergence time in graphical games: A locality-sensitive approach. In 27th
International Conference on Principles of Distributed Systems (Vol. 286).
Tokyo, Japan: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.OPODIS.2023.11'
chicago: 'Hirvonen, Juho, Laura Schmid, Krishnendu Chatterjee, and Stefan Schmid.
“On the Convergence Time in Graphical Games: A Locality-Sensitive Approach.” In
27th International Conference on Principles of Distributed Systems, Vol.
286. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. https://doi.org/10.4230/LIPIcs.OPODIS.2023.11.'
ieee: 'J. Hirvonen, L. Schmid, K. Chatterjee, and S. Schmid, “On the convergence
time in graphical games: A locality-sensitive approach,” in 27th International
Conference on Principles of Distributed Systems, Tokyo, Japan, 2024, vol.
286.'
ista: 'Hirvonen J, Schmid L, Chatterjee K, Schmid S. 2024. On the convergence time
in graphical games: A locality-sensitive approach. 27th International Conference
on Principles of Distributed Systems. OPODIS: Conference on Principles of Distributed
Systems, LIPIcs, vol. 286, 11.'
mla: 'Hirvonen, Juho, et al. “On the Convergence Time in Graphical Games: A Locality-Sensitive
Approach.” 27th International Conference on Principles of Distributed Systems,
vol. 286, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:10.4230/LIPIcs.OPODIS.2023.11.'
short: J. Hirvonen, L. Schmid, K. Chatterjee, S. Schmid, in:, 27th International
Conference on Principles of Distributed Systems, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2024.
conference:
end_date: 2023-12-08
location: Tokyo, Japan
name: 'OPODIS: Conference on Principles of Distributed Systems'
start_date: 2023-12-06
date_created: 2024-02-18T23:01:01Z
date_published: 2024-01-18T00:00:00Z
date_updated: 2025-07-14T09:10:03Z
day: '18'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.OPODIS.2023.11
ec_funded: 1
external_id:
arxiv:
- '2102.13457'
file:
- access_level: open_access
checksum: 4fc7eea6e4ba140b904781fc7df868ec
content_type: application/pdf
creator: dernst
date_created: 2024-02-26T09:04:58Z
date_updated: 2024-02-26T09:04:58Z
file_id: '15028'
file_name: 2024_LIPICs_Hirvonen.pdf
file_size: 867363
relation: main_file
success: 1
file_date_updated: 2024-02-26T09:04:58Z
has_accepted_license: '1'
intvolume: ' 286'
language:
- iso: eng
month: '01'
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: 27th International Conference on Principles of Distributed Systems
publication_identifier:
isbn:
- '9783959773089'
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'On the convergence time in graphical games: A locality-sensitive approach'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 286
year: '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
date_created: 2023-02-24T12:20:47Z
date_published: 2023-02-01T00:00:00Z
date_updated: 2025-07-14T09:09:50Z
day: '01'
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: '12738'
abstract:
- lang: eng
text: We study turn-based stochastic zero-sum games with lexicographic preferences
over objectives. Stochastic games are standard models in control, verification,
and synthesis of stochastic reactive systems that exhibit both randomness as well
as controllable and adversarial non-determinism. Lexicographic order allows one
to consider multiple objectives with a strict preference order. To the best of
our knowledge, stochastic games with lexicographic objectives have not been studied
before. For a mixture of reachability and safety objectives, we show that deterministic
lexicographically optimal strategies exist and memory is only required to remember
the already satisfied and violated objectives. For a constant number of objectives,
we show that the relevant decision problem is in NP∩coNP, matching the current
known bound for single objectives; and in general the decision problem is PSPACE-hard
and can be solved in NEXPTIME∩coNEXPTIME. We present an algorithm that computes
the lexicographically optimal strategies via a reduction to the computation of
optimal strategies in a sequence of single-objectives games. For omega-regular
objectives, we restrict our analysis to one-player games, also known as Markov
decision processes. We show that lexicographically optimal strategies exist and
need either randomization or finite memory. We present an algorithm that solves
the relevant decision problem in polynomial time. We have implemented our algorithms
and report experimental results on various case studies.
acknowledgement: Tobias Winkler and Joost-Pieter Katoen are supported by the DFG RTG
2236 UnRAVeL and the innovation programme under the Marie Skłodowska-Curie grant
agreement No. 101008233 (Mission). Krishnendu Chatterjee is supported by the ERC
CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) Project
ICT15-003. Maximilian Weininger is supported by the DFG projects 383882557 Statistical
Unbounded Verification (SUV) and 427755713 Group-By Objectives in Probabilistic
Verification (GOPro). Stefanie Mohr is supported by the DFG RTG 2428 CONVEY. Open
Access funding enabled and organized by Projekt DEAL.
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: Joost P
full_name: Katoen, Joost P
id: 4524F760-F248-11E8-B48F-1D18A9856A87
last_name: Katoen
- first_name: Stefanie
full_name: Mohr, Stefanie
last_name: Mohr
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
- first_name: Tobias
full_name: Winkler, Tobias
last_name: Winkler
citation:
ama: Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. Stochastic games with
lexicographic objectives. Formal Methods in System Design. 2023. doi:10.1007/s10703-023-00411-4
apa: Chatterjee, K., Katoen, J. P., Mohr, S., Weininger, M., & Winkler, T. (2023).
Stochastic games with lexicographic objectives. Formal Methods in System Design.
Springer Nature. https://doi.org/10.1007/s10703-023-00411-4
chicago: Chatterjee, Krishnendu, Joost P Katoen, Stefanie Mohr, Maximilian Weininger,
and Tobias Winkler. “Stochastic Games with Lexicographic Objectives.” Formal
Methods in System Design. Springer Nature, 2023. https://doi.org/10.1007/s10703-023-00411-4.
ieee: K. Chatterjee, J. P. Katoen, S. Mohr, M. Weininger, and T. Winkler, “Stochastic
games with lexicographic objectives,” Formal Methods in System Design.
Springer Nature, 2023.
ista: Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2023. Stochastic
games with lexicographic objectives. Formal Methods in System Design.
mla: Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Objectives.”
Formal Methods in System Design, Springer Nature, 2023, doi:10.1007/s10703-023-00411-4.
short: K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods
in System Design (2023).
date_created: 2023-03-19T23:00:59Z
date_published: 2023-03-08T00:00:00Z
date_updated: 2025-07-14T09:10:14Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s10703-023-00411-4
ec_funded: 1
external_id:
isi:
- '000946174300001'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1007/s10703-023-00411-4
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'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Formal Methods in System Design
publication_identifier:
eissn:
- 1572-8102
publication_status: epub_ahead
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '8272'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Stochastic games with lexicographic 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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '12787'
abstract:
- lang: eng
text: "Populations evolve in spatially heterogeneous environments. While a certain
trait might bring a fitness advantage in some patch of the environment, a different
trait might be advantageous in another patch. Here, we study the Moran birth–death
process with two types of individuals in a population stretched across two patches
of size N, each patch favouring one of the two types. We show that the long-term
fate of such populations crucially depends on the migration rate μ\r\n between
the patches. To classify the possible fates, we use the distinction between polynomial
(short) and exponential (long) timescales. We show that when μ is high then one
of the two types fixates on the whole population after a number of steps that
is only polynomial in N. By contrast, when μ is low then each type holds majority
in the patch where it is favoured for a number of steps that is at least exponential
in N. Moreover, we precisely identify the threshold migration rate μ⋆ that separates
those two scenarios, thereby exactly delineating the situations that support long-term
coexistence of the two types. We also discuss the case of various cycle graphs
and we present computer simulations that perfectly match our analytical results."
acknowledgement: J.S. and K.C. acknowledge support from the ERC CoG 863818 (ForM-SMArt)
article_number: '20220685'
article_processing_charge: No
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: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Kamran
full_name: Kaveh, Kamran
last_name: Kaveh
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: 'Svoboda J, Tkadlec J, Kaveh K, Chatterjee K. Coexistence times in the Moran
process with environmental heterogeneity. Proceedings of the Royal Society
A: Mathematical, Physical and Engineering Sciences. 2023;479(2271). doi:10.1098/rspa.2022.0685'
apa: 'Svoboda, J., Tkadlec, J., Kaveh, K., & Chatterjee, K. (2023). Coexistence
times in the Moran process with environmental heterogeneity. Proceedings of
the Royal Society A: Mathematical, Physical and Engineering Sciences. The
Royal Society. https://doi.org/10.1098/rspa.2022.0685'
chicago: 'Svoboda, Jakub, Josef Tkadlec, Kamran Kaveh, and Krishnendu Chatterjee.
“Coexistence Times in the Moran Process with Environmental Heterogeneity.” Proceedings
of the Royal Society A: Mathematical, Physical and Engineering Sciences. The
Royal Society, 2023. https://doi.org/10.1098/rspa.2022.0685.'
ieee: 'J. Svoboda, J. Tkadlec, K. Kaveh, and K. Chatterjee, “Coexistence times in
the Moran process with environmental heterogeneity,” Proceedings of the Royal
Society A: Mathematical, Physical and Engineering Sciences, vol. 479, no.
2271. The Royal Society, 2023.'
ista: 'Svoboda J, Tkadlec J, Kaveh K, Chatterjee K. 2023. Coexistence times in the
Moran process with environmental heterogeneity. Proceedings of the Royal Society
A: Mathematical, Physical and Engineering Sciences. 479(2271), 20220685.'
mla: 'Svoboda, Jakub, et al. “Coexistence Times in the Moran Process with Environmental
Heterogeneity.” Proceedings of the Royal Society A: Mathematical, Physical
and Engineering Sciences, vol. 479, no. 2271, 20220685, The Royal Society,
2023, doi:10.1098/rspa.2022.0685.'
short: 'J. Svoboda, J. Tkadlec, K. Kaveh, K. Chatterjee, Proceedings of the Royal
Society A: Mathematical, Physical and Engineering Sciences 479 (2023).'
date_created: 2023-04-02T22:01:09Z
date_published: 2023-03-29T00:00:00Z
date_updated: 2025-07-14T09:09:51Z
day: '29'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rspa.2022.0685
ec_funded: 1
external_id:
isi:
- '000957125500002'
file:
- access_level: open_access
checksum: 13953d349fbefcb5d21ccc6b303297eb
content_type: application/pdf
creator: dernst
date_created: 2023-04-03T06:25:29Z
date_updated: 2023-04-03T06:25:29Z
file_id: '12796'
file_name: 2023_ProceedingsRoyalSocietyA_Svoboda.pdf
file_size: 827784
relation: main_file
success: 1
file_date_updated: 2023-04-03T06:25:29Z
has_accepted_license: '1'
intvolume: ' 479'
isi: 1
issue: '2271'
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: 'Proceedings of the Royal Society A: Mathematical, Physical and Engineering
Sciences'
publication_identifier:
eissn:
- 1471-2946
issn:
- 1364-5021
publication_status: published
publisher: The Royal Society
quality_controlled: '1'
related_material:
link:
- relation: research_data
url: https://doi.org/10.6084/m9.figshare.21261771.v1
scopus_import: '1'
status: public
title: Coexistence times in the Moran process with environmental heterogeneity
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: 479
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: 2024-01-04T12:42: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-07-14T09:09:52Z
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: The Wittgenstein Prize
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
date_created: 2023-06-18T22:00:46Z
date_published: 2023-04-22T00:00:00Z
date_updated: 2024-02-27T07:19:33Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-30823-9_25
external_id:
arxiv:
- '2301.08137'
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'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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
date_created: 2023-06-18T22:00:47Z
date_published: 2023-04-22T00:00:00Z
date_updated: 2025-07-14T09:09:52Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-031-30823-9_1
ec_funded: 1
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'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13993
year: '2023'
...
---
_id: '13238'
abstract:
- lang: eng
text: "We consider a natural problem dealing with weighted packet selection across
a rechargeable link, which e.g., finds applications in cryptocurrency networks.
The capacity of a link (u, v) is determined by how much nodes u and v allocate
for this link. Specifically, the input is a finite ordered sequence of packets
that arrive in both directions along a link. Given (u, v) and a packet of weight
x going from u to v, node u can either accept or reject the packet. If u accepts
the packet, the capacity on link (u, v) decreases by x. Correspondingly, v’s capacity
on (u, v) increases by x. If a node rejects the packet, this will entail a cost
affinely linear in the weight of the packet. A link is “rechargeable” in the sense
that the total capacity of the link has to remain constant, but the allocation
of capacity at the ends of the link can depend arbitrarily on the nodes’ decisions.
The goal is to minimise the sum of the capacity injected into the link and the
cost of rejecting packets. We show that the problem is NP-hard, but can be approximated
efficiently with a ratio of (1+ε)⋅(1+3–√) for some arbitrary ε>0.\r\n."
acknowledgement: We thank Mahsa Bastankhah and Mohammad Ali Maddah-Ali for fruitful
discussions about different variants of the problem. This work is supported by the
European Research Council (ERC) Consolidator Project 864228 (AdjustNet), 2020-2025,
the ERC CoG 863818 (ForM-SMArt), and the German Research Foundation (DFG) grant
470029389 (FlexNets), 2021–2024.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Stefan
full_name: Schmid, Stefan
last_name: Schmid
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Michelle X
full_name: Yeo, Michelle X
id: 2D82B818-F248-11E8-B48F-1D18A9856A87
last_name: Yeo
orcid: 0009-0001-3676-4809
citation:
ama: 'Schmid S, Svoboda J, Yeo MX. Weighted packet selection for rechargeable links
in cryptocurrency networks: Complexity and approximation. In: SIROCCO 2023:
Structural Information and Communication Complexity . Vol 13892. Springer
Nature; 2023:576-594. doi:10.1007/978-3-031-32733-9_26'
apa: 'Schmid, S., Svoboda, J., & Yeo, M. X. (2023). Weighted packet selection
for rechargeable links in cryptocurrency networks: Complexity and approximation.
In SIROCCO 2023: Structural Information and Communication Complexity (Vol.
13892, pp. 576–594). Alcala de Henares, Spain: Springer Nature. https://doi.org/10.1007/978-3-031-32733-9_26'
chicago: 'Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection
for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.”
In SIROCCO 2023: Structural Information and Communication Complexity ,
13892:576–94. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-32733-9_26.'
ieee: 'S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable
links in cryptocurrency networks: Complexity and approximation,” in SIROCCO
2023: Structural Information and Communication Complexity , Alcala de Henares,
Spain, 2023, vol. 13892, pp. 576–594.'
ista: 'Schmid S, Svoboda J, Yeo MX. 2023. Weighted packet selection for rechargeable
links in cryptocurrency networks: Complexity and approximation. SIROCCO 2023:
Structural Information and Communication Complexity . SIROCCO: Structural Information
and Communication Complexity, LNCS, vol. 13892, 576–594.'
mla: 'Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency
Networks: Complexity and Approximation.” SIROCCO 2023: Structural Information
and Communication Complexity , vol. 13892, Springer Nature, 2023, pp. 576–94,
doi:10.1007/978-3-031-32733-9_26.'
short: 'S. Schmid, J. Svoboda, M.X. Yeo, in:, SIROCCO 2023: Structural Information
and Communication Complexity , Springer Nature, 2023, pp. 576–594.'
conference:
end_date: 2023-06-09
location: Alcala de Henares, Spain
name: 'SIROCCO: Structural Information and Communication Complexity'
start_date: 2023-06-06
date_created: 2023-07-16T22:01:12Z
date_published: 2023-05-25T00:00:00Z
date_updated: 2025-07-14T09:09:53Z
day: '25'
department:
- _id: KrPi
- _id: KrCh
doi: 10.1007/978-3-031-32733-9_26
ec_funded: 1
external_id:
arxiv:
- '2204.13459'
intvolume: ' 13892'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2204.13459
month: '05'
oa: 1
oa_version: Preprint
page: 576-594
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 'SIROCCO 2023: Structural Information and Communication Complexity '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031327322'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14506'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'Weighted packet selection for rechargeable links in cryptocurrency networks:
Complexity and approximation'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13892
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).
date_created: 2023-07-23T22:01:11Z
date_published: 2023-07-12T00:00:00Z
date_updated: 2025-07-14T09:09:53Z
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).
date_created: 2023-07-31T11:30:46Z
date_published: 2023-06-20T00:00:00Z
date_updated: 2025-07-14T09:09:53Z
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: '14830'
abstract:
- lang: eng
text: We study the problem of learning controllers for discrete-time non-linear
stochastic dynamical systems with formal reach-avoid guarantees. This work presents
the first method for providing formal reach-avoid guarantees, which combine and
generalize stability and safety guarantees, with a tolerable probability threshold
p in [0,1] over the infinite time horizon. Our method leverages advances in machine
learning literature and it represents formal certificates as neural networks.
In particular, we learn a certificate in the form of a reach-avoid supermartingale
(RASM), a novel notion that we introduce in this work. Our RASMs provide reachability
and avoidance guarantees by imposing constraints on what can be viewed as a stochastic
extension of level sets of Lyapunov functions for deterministic systems. Our approach
solves several important problems -- it can be used to learn a control policy
from scratch, to verify a reach-avoid specification for a fixed control policy,
or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification.
We validate our approach on 3 stochastic non-linear reinforcement learning tasks.
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.
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- 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: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: 'Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. In: Proceedings of the
37th AAAI Conference on Artificial Intelligence. Vol 37. Association for the
Advancement of Artificial Intelligence; 2023:11926-11935. doi:10.1609/aaai.v37i10.26407'
apa: 'Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (2023). Learning
control policies for stochastic systems with reach-avoid guarantees. In Proceedings
of the 37th AAAI Conference on Artificial Intelligence (Vol. 37, pp. 11926–11935).
Washington, DC, United States: Association for the Advancement of Artificial Intelligence.
https://doi.org/10.1609/aaai.v37i10.26407'
chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee.
“Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.”
In Proceedings of the 37th AAAI Conference on Artificial Intelligence,
37:11926–35. Association for the Advancement of Artificial Intelligence, 2023.
https://doi.org/10.1609/aaai.v37i10.26407.
ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control
policies for stochastic systems with reach-avoid guarantees,” in Proceedings
of the 37th AAAI Conference on Artificial Intelligence, Washington, DC, United
States, 2023, vol. 37, no. 10, pp. 11926–11935.
ista: 'Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control
policies for stochastic systems with reach-avoid guarantees. Proceedings of the
37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial
Intelligence vol. 37, 11926–11935.'
mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with
Reach-Avoid Guarantees.” Proceedings of the 37th AAAI Conference on Artificial
Intelligence, vol. 37, no. 10, Association for the Advancement of Artificial
Intelligence, 2023, pp. 11926–35, doi:10.1609/aaai.v37i10.26407.
short: D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of
the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2023, pp. 11926–11935.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2024-01-18T07:44:31Z
date_published: 2023-06-26T00:00:00Z
date_updated: 2025-07-14T09:10:02Z
day: '26'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i10.26407
ec_funded: 1
external_id:
arxiv:
- '2210.05308'
intvolume: ' 37'
issue: '10'
keyword:
- General Medicine
language:
- iso: eng
month: '06'
oa_version: Preprint
page: 11926-11935
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:
eissn:
- 2374-3468
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
related_material:
record:
- id: '14600'
relation: earlier_version
status: public
status: public
title: Learning control policies for stochastic systems with reach-avoid guarantees
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '14990'
abstract:
- lang: eng
text: The software artefact to evaluate the approximation of stationary distributions
implementation.
article_processing_charge: No
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. Artefact for: Correct Approximation of Stationary Distributions.
2023. doi:10.5281/ZENODO.7548214'
apa: 'Meggendorfer, T. (2023). Artefact for: Correct Approximation of Stationary
Distributions. Zenodo. https://doi.org/10.5281/ZENODO.7548214'
chicago: 'Meggendorfer, Tobias. “Artefact for: Correct Approximation of Stationary
Distributions.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.7548214.'
ieee: 'T. Meggendorfer, “Artefact for: Correct Approximation of Stationary Distributions.”
Zenodo, 2023.'
ista: 'Meggendorfer T. 2023. Artefact for: Correct Approximation of Stationary Distributions,
Zenodo, 10.5281/ZENODO.7548214.'
mla: 'Meggendorfer, Tobias. Artefact for: Correct Approximation of Stationary
Distributions. Zenodo, 2023, doi:10.5281/ZENODO.7548214.'
short: T. Meggendorfer, (2023).
date_created: 2024-02-14T14:27:06Z
date_published: 2023-01-18T00:00:00Z
date_updated: 2024-02-27T07:19:32Z
day: '18'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.5281/ZENODO.7548214
has_accepted_license: '1'
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/zenodo.7548214
month: '01'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '13139'
relation: used_in_publication
status: public
status: public
title: 'Artefact for: 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: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '15023'
abstract:
- lang: eng
text: Reinforcement learning has shown promising results in learning neural network
policies for complicated control tasks. However, the lack of formal guarantees
about the behavior of such policies remains an impediment to their deployment.
We propose a novel method for learning a composition of neural network policies
in stochastic environments, along with a formal certificate which guarantees that
a specification over the policy's behavior is satisfied with the desired probability.
Unlike prior work on verifiable RL, our approach leverages the compositional nature
of logical specifications provided in SpectRL, to learn over graphs of probabilistic
reach-avoid specifications. The formal guarantees are provided by learning neural
network policies together with reach-avoid supermartingales (RASM) for the graph’s
sub-tasks and then composing them into a global policy. We also derive a tighter
lower bound compared to previous work on the probability of reach-avoidance implied
by a RASM, which is required to find a compositional policy with an acceptable
probabilistic threshold for complex tasks with multiple edge policies. We implement
a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS)
and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt)."
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Abhinav
full_name: Verma, Abhinav
id: a235593c-d7fa-11eb-a0c5-b22ca3c66ee6
last_name: Verma
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. Compositional policy
learning in stochastic control systems with formal guarantees. In: 37th Conference
on Neural Information Processing Systems. ; 2023.'
apa: Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., & Henzinger, T. A.
(2023). Compositional policy learning in stochastic control systems with formal
guarantees. In 37th Conference on Neural Information Processing Systems.
New Orleans, LO, United States.
chicago: Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee,
and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems
with Formal Guarantees.” In 37th Conference on Neural Information Processing
Systems, 2023.
ieee: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional
policy learning in stochastic control systems with formal guarantees,” in 37th
Conference on Neural Information Processing Systems, New Orleans, LO, United
States, 2023.
ista: 'Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional
policy learning in stochastic control systems with formal guarantees. 37th Conference
on Neural Information Processing Systems. NeurIPS: Neural Information Processing
Systems.'
mla: Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control
Systems with Formal Guarantees.” 37th Conference on Neural Information Processing
Systems, 2023.
short: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th
Conference on Neural Information Processing Systems, 2023.
conference:
end_date: 2023-12-16
location: New Orleans, LO, United States
name: 'NeurIPS: Neural Information Processing Systems'
start_date: 2023-12-10
date_created: 2024-02-25T09:23:24Z
date_published: 2023-12-15T00:00:00Z
date_updated: 2025-07-14T09:10:04Z
day: '15'
department:
- _id: ToHe
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '2312.01456'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2312.01456
month: '12'
oa: 1
oa_version: Preprint
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th Conference on Neural Information Processing Systems
publication_status: epub_ahead
quality_controlled: '1'
status: public
title: Compositional policy learning in stochastic control systems with formal guarantees
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '13967'
abstract:
- lang: eng
text: 'A classic solution technique for Markov decision processes (MDP) and stochastic
games (SG) is value iteration (VI). Due to its good practical performance, this
approximative approach is typically preferred over exact techniques, even though
no practical bounds on the imprecision of the result could be given until recently.
As a consequence, even the most used model checkers could return arbitrarily wrong
results. Over the past decade, different works derived stopping criteria, indicating
when the precision reaches the desired level, for various settings, in particular
MDP with reachability, total reward, and mean payoff, and SG with reachability.In
this paper, we provide the first stopping criteria for VI on SG with total reward
and mean payoff, yielding the first anytime algorithms in these settings. To this
end, we provide the solution in two flavours: First through a reduction to the
MDP case and second directly on SG. The former is simpler and automatically utilizes
any advances on MDP. The latter allows for more local computations, heading towards
better practical efficiency.Our solution unifies the previously mentioned approaches
for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific
subroutines as well as identify objective-independent concepts. These structural
concepts, while surprisingly simple, form the very essence of the unified solution.'
acknowledgement: This research was funded in part by DFG projects 383882557 “SUV”
and 427755713 “GOPro”.
article_processing_charge: No
arxiv: 1
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- 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: 'Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration
on stochastic games with quantitative objectives. In: 38th Annual ACM/IEEE
Symposium on Logic in Computer Science. Vol 2023. Institute of Electrical
and Electronics Engineers; 2023. doi:10.1109/LICS56636.2023.10175771'
apa: 'Kretinsky, J., Meggendorfer, T., & Weininger, M. (2023). Stopping criteria
for value iteration on stochastic games with quantitative objectives. In 38th
Annual ACM/IEEE Symposium on Logic in Computer Science (Vol. 2023). Boston,
MA, United States: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/LICS56636.2023.10175771'
chicago: Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping
Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.”
In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Vol. 2023.
Institute of Electrical and Electronics Engineers, 2023. https://doi.org/10.1109/LICS56636.2023.10175771.
ieee: J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value
iteration on stochastic games with quantitative objectives,” in 38th Annual
ACM/IEEE Symposium on Logic in Computer Science, Boston, MA, United States,
2023, vol. 2023.
ista: 'Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value
iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE
Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science
vol. 2023.'
mla: Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic
Games with Quantitative Objectives.” 38th Annual ACM/IEEE Symposium on Logic
in Computer Science, vol. 2023, Institute of Electrical and Electronics Engineers,
2023, doi:10.1109/LICS56636.2023.10175771.
short: J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium
on Logic in Computer Science, Institute of Electrical and Electronics Engineers,
2023.
conference:
end_date: 2023-06-29
location: Boston, MA, United States
name: 'LICS: Symposium on Logic in Computer Science'
start_date: 2023-06-26
date_created: 2023-08-06T22:01:10Z
date_published: 2023-07-01T00:00:00Z
date_updated: 2023-12-13T12:06:10Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS56636.2023.10175771
external_id:
arxiv:
- '2304.09930'
isi:
- '001036707700042'
intvolume: ' 2023'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2304.09930
month: '07'
oa: 1
oa_version: Preprint
publication: 38th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
isbn:
- '9798350335873'
issn:
- 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stopping criteria for value iteration on stochastic games with quantitative
objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2023
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-07-14T09:09:56Z
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: '14243'
abstract:
- lang: eng
text: 'Two-player zero-sum "graph games" are central in logic, verification, and
multi-agent systems. The game proceeds by placing a token on a vertex of a graph,
and allowing the players to move it to produce an infinite path, which determines
the winner or payoff of the game. Traditionally, the players alternate turns in
moving the token. In "bidding games", however, the players have budgets and in
each turn, an auction (bidding) determines which player moves the token. So far,
bidding games have only been studied as full-information games. In this work we
initiate the study of partial-information bidding games: we study bidding games
in which a player''s initial budget is drawn from a known probability distribution.
We show that while for some bidding mechanisms and objectives, it is straightforward
to adapt the results from the full-information setting to the partial-information
setting, for others, the analysis is significantly more challenging, requires
new techniques, and gives rise to interesting results. Specifically, we study
games with "mean-payoff" objectives in combination with "poorman" bidding. We
construct optimal strategies for a partially-informed player who plays against
a fully-informed adversary. We show that, somewhat surprisingly, the "value" under
pure strategies does not necessarily exist in such games.'
acknowledgement: This research was supported in part by ISF grant no.1679/21, 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.
article_processing_charge: No
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Ismael R
full_name: Jecker, Ismael R
id: 85D7C63E-7D5D-11E9-9C0F-98C4E5697425
last_name: Jecker
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable
budgets. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence.
Vol 37. ; 2023:5464-5471. doi:10.1609/aaai.v37i5.25679'
apa: Avni, G., Jecker, I. R., & Zikelic, D. (2023). Bidding graph games with
partially-observable budgets. In Proceedings of the 37th AAAI Conference on
Artificial Intelligence (Vol. 37, pp. 5464–5471). Washington, DC, United States.
https://doi.org/10.1609/aaai.v37i5.25679
chicago: Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with
Partially-Observable Budgets.” In Proceedings of the 37th AAAI Conference on
Artificial Intelligence, 37:5464–71, 2023. https://doi.org/10.1609/aaai.v37i5.25679.
ieee: G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable
budgets,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence,
Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471.
ista: 'Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable
budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI:
Conference on Artificial Intelligence vol. 37, 5464–5471.'
mla: Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.”
Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol.
37, no. 5, 2023, pp. 5464–71, doi:10.1609/aaai.v37i5.25679.
short: G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference
on Artificial Intelligence, 2023, pp. 5464–5471.
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:18Z
date_published: 2023-06-27T00:00:00Z
date_updated: 2025-07-14T09:09:56Z
day: '27'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i5.25679
ec_funded: 1
external_id:
arxiv:
- '2211.13626'
intvolume: ' 37'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1609/aaai.v37i5.25679
month: '06'
oa: 1
oa_version: Published Version
page: 5464-5471
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: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781577358800'
publication_status: published
quality_controlled: '1'
scopus_import: '1'
status: public
title: Bidding graph games with partially-observable budgets
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '14259'
abstract:
- lang: eng
text: "We provide a learning-based technique for guessing a winning strategy in
a parity game originating from an LTL synthesis problem. A cheaply obtained guess
can be useful in several applications. Not only can the guessed strategy be applied
as best-effort in cases where the game’s huge size prohibits rigorous approaches,
but it can also increase the scalability of rigorous LTL synthesis in several
ways. Firstly, checking whether a guessed strategy is winning is easier than constructing
one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy
iteration faster than constructing one from scratch. Thirdly, the guess can be
used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn
contrast to previous works, we (i) reflect the highly structured logical information
in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata
translations, and (ii) learn to reflect it properly by learning from previously
solved games, bringing the solving process closer to human-like reasoning."
acknowledgement: This research was funded in part by the German Research Foundation
(DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- 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: Prokop, Maximilian
last_name: Prokop
- first_name: Sabine
full_name: Rieder, Sabine
last_name: Rieder
citation:
ama: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies
in LTL synthesis by semantic learning. In: 35th International Conference on
Computer Aided Verification . Vol 13964. Springer Nature; 2023:390-414. doi:10.1007/978-3-031-37706-8_20'
apa: 'Kretinsky, J., Meggendorfer, T., Prokop, M., & Rieder, S. (2023). Guessing
winning policies in LTL synthesis by semantic learning. In 35th International
Conference on Computer Aided Verification (Vol. 13964, pp. 390–414). Paris,
France: Springer Nature. https://doi.org/10.1007/978-3-031-37706-8_20'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder.
“Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In 35th
International Conference on Computer Aided Verification , 13964:390–414. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-37706-8_20.
ieee: J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning
policies in LTL synthesis by semantic learning,” in 35th International Conference
on Computer Aided Verification , Paris, France, 2023, vol. 13964, pp. 390–414.
ista: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies
in LTL synthesis by semantic learning. 35th International Conference on Computer
Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.'
mla: Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic
Learning.” 35th International Conference on Computer Aided Verification ,
vol. 13964, Springer Nature, 2023, pp. 390–414, doi:10.1007/978-3-031-37706-8_20.
short: J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International
Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-09-03T22:01:16Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2023-09-06T08:27:33Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37706-8_20
file:
- access_level: open_access
checksum: ed66278b61bb869e1baba3d9b9081271
content_type: application/pdf
creator: dernst
date_created: 2023-09-06T08:25:50Z
date_updated: 2023-09-06T08:25:50Z
file_id: '14276'
file_name: 2023_LNCS_CAV_Kretinsky.pdf
file_size: 428354
relation: main_file
success: 1
file_date_updated: 2023-09-06T08:25:50Z
has_accepted_license: '1'
intvolume: ' 13964'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 390-414
publication: '35th International Conference on Computer Aided Verification '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031377051'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Guessing winning policies in LTL synthesis by semantic learning
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13964
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-07-14T09:09:56Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37709-9_5
ec_funded: 1
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'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13966
year: '2023'
...