---
APC_amount: 3143,76 EUR
OA_place: publisher
OA_type: hybrid
_id: '18703'
abstract:
- lang: eng
text: 'Spatial games provide a simple and elegant mathematical model to study the
evolution of cooperation in networks. In spatial games, individuals reside in
vertices, adopt simple strategies, and interact with neighbors to receive a payoff.
Depending on their own and neighbors’ payoffs, individuals can change their strategy.
The payoff is determined by the Prisoners’ Dilemma, a classical matrix game, where
players cooperate or defect. While cooperation is the desired behavior, defection
provides a higher payoff for a selfish individual. There are many theoretical
and empirical studies related to the role of the network in the evolution of cooperation.
However, the fundamental question of whether there exist networks that for low
initial cooperation rate ensure a high chance of fixation, i.e., cooperation spreads
across the whole population, has remained elusive for spatial games with strong
selection. In this work, we answer this fundamental question in the affirmative
by presenting network structures that ensure high fixation probability for cooperators
in the strong selection regime. Besides, our structures have many desirable properties:
(a) they ensure the spread of cooperation even for a low initial density of cooperation
and high temptation of defection, (b) they have constant degrees, and (c) the
number of steps, until cooperation spreads, is at most quadratic in the size of
the network.'
acknowledgement: J.S. and K.C. were supported by the European Research Council CoG
863818 (ForM-SMArt) and Austrian Science Fund 10.55776/COE12.
article_number: e2405605121
article_processing_charge: Yes
article_type: original
author:
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Svoboda J, Chatterjee K. Density amplifiers of cooperation for spatial games.
Proceedings of the National Academy of Sciences of the United States of America.
2024;121(50). doi:10.1073/pnas.2405605121
apa: Svoboda, J., & Chatterjee, K. (2024). Density amplifiers of cooperation
for spatial games. Proceedings of the National Academy of Sciences of the United
States of America. National Academy of Sciences. https://doi.org/10.1073/pnas.2405605121
chicago: Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation
for Spatial Games.” Proceedings of the National Academy of Sciences of the
United States of America. National Academy of Sciences, 2024. https://doi.org/10.1073/pnas.2405605121.
ieee: J. Svoboda and K. Chatterjee, “Density amplifiers of cooperation for spatial
games,” Proceedings of the National Academy of Sciences of the United States
of America, vol. 121, no. 50. National Academy of Sciences, 2024.
ista: Svoboda J, Chatterjee K. 2024. Density amplifiers of cooperation for spatial
games. Proceedings of the National Academy of Sciences of the United States of
America. 121(50), e2405605121.
mla: Svoboda, Jakub, and Krishnendu Chatterjee. “Density Amplifiers of Cooperation
for Spatial Games.” Proceedings of the National Academy of Sciences of the
United States of America, vol. 121, no. 50, e2405605121, National Academy
of Sciences, 2024, doi:10.1073/pnas.2405605121.
short: J. Svoboda, K. Chatterjee, Proceedings of the National Academy of Sciences
of the United States of America 121 (2024).
corr_author: '1'
das_tickbox: '1'
dataavailabilitystatement: 'Code data have been deposited in Code: Amplifiers of Cooperation
(DOI: https://doi.org/10.5281/zenodo.10832535)'
date_created: 2024-12-22T23:01:47Z
date_published: 2024-12-10T00:00:00Z
date_updated: 2026-10-16T08:00:05Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1073/pnas.2405605121
ec_funded: 1
external_id:
isi:
- '001379596100014'
pmid:
- '39642209'
file:
- access_level: open_access
checksum: 0115e9090b478e0644308c6dab58605b
content_type: application/pdf
creator: dernst
date_created: 2025-01-02T12:14:15Z
date_updated: 2025-01-02T12:14:15Z
file_id: '18721'
file_name: 2024_PNAS_Svoboda.pdf
file_size: 2491151
relation: main_file
success: 1
file_date_updated: 2025-01-02T12:14:15Z
fulldoi: https://doi.org/10.1073/pnas.2405605121
has_accepted_license: '1'
intvolume: ' 121'
isi: 1
issue: '50'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the National Academy of Sciences of the United States
of America
publication_identifier:
eissn:
- 1091-6490
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
related_material:
record:
- id: '20138'
relation: dissertation_contains
status: public
researchdata_availability: yes
scopus_import: '1'
status: public
supplementarymaterial: yes
title: Density amplifiers of cooperation for spatial games
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 121
year: '2024'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '18630'
abstract:
- lang: eng
text: 'Markov chains are the de facto finite-state model for stochastic dynamical
systems, and Markov decision processes (MDPs) extend Markov chains by incorporating
non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization
criterion is the maximal expected total reward where the MDP stops after T steps,
which can be computed by a simple dynamic programming algorithm. We consider a
natural generalization of the problem where the stopping times can be chosen according
to a probability distribution, such that the expected stopping time is T, to optimize
the expected total reward. Quite surprisingly we establish inter-reducibility
of the expected stopping-time problem for Markov chains with the Positivity problem
(which is related to the well-known Skolem problem), for which establishing either
decidability or undecidability would be a major breakthrough. Given the hardness
of the exact problem, we consider the approximate version of the problem: we show
that it can be solved in exponential time for Markov chains and in exponential
space for MDPs.'
acknowledgement: The authors are grateful to the anonymous reviewers of LICS 2021
and of a previous version of this paper for insightful comments that helped improving
the presentation. The research presented in this paper was partially supported by
the grant ERC CoG 863818 (ForM-SMArt).
alternative_title:
- LMCS
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
citation:
ama: Chatterjee K, Doyen L. Stochastic processes with expected stopping time. Logical
Methods in Computer Science. 2024;20(4):11:1-11:34. doi:10.46298/lmcs-20(4:11)2024
apa: Chatterjee, K., & Doyen, L. (2024). Stochastic processes with expected
stopping time. Logical Methods in Computer Science. EPI Sciences. https://doi.org/10.46298/lmcs-20(4:11)2024
chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected
Stopping Time.” Logical Methods in Computer Science. EPI Sciences, 2024.
https://doi.org/10.46298/lmcs-20(4:11)2024.
ieee: K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,”
Logical Methods in Computer Science, vol. 20, no. 4. EPI Sciences, p. 11:1-11:34,
2024.
ista: Chatterjee K, Doyen L. 2024. Stochastic processes with expected stopping time.
Logical Methods in Computer Science. 20(4), 11:1-11:34.
mla: Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected
Stopping Time.” Logical Methods in Computer Science, vol. 20, no. 4, EPI
Sciences, 2024, p. 11:1-11:34, doi:10.46298/lmcs-20(4:11)2024.
short: K. Chatterjee, L. Doyen, Logical Methods in Computer Science 20 (2024) 11:1-11:34.
corr_author: '1'
das_tickbox: '0'
date_created: 2024-12-08T23:01:56Z
date_published: 2024-11-12T00:00:00Z
date_updated: 2026-10-16T07:57:38Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.46298/lmcs-20(4:11)2024
ec_funded: 1
external_id:
arxiv:
- '2104.07278'
isi:
- '001367316400002'
file:
- access_level: open_access
checksum: b3315c74ce18ce0a30ed33d8c9972992
content_type: application/pdf
creator: dernst
date_created: 2024-12-09T08:38:48Z
date_updated: 2024-12-09T08:38:48Z
file_id: '18633'
file_name: 2024_LMCS_Chatterjee.pdf
file_size: 416814
relation: main_file
success: 1
file_date_updated: 2024-12-09T08:38:48Z
fulldoi: https://doi.org/10.46298/lmcs-20(4:11)2024
has_accepted_license: '1'
intvolume: ' 20'
isi: 1
issue: '4'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: 11:1-11:34
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Logical Methods in Computer Science
publication_identifier:
eissn:
- 1860-5974
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
record:
- id: '10004'
relation: earlier_version
status: public
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Stochastic processes with expected stopping time
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 20
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18600'
abstract:
- lang: eng
text: 'The analysis of formal models that include quantitative aspects such as timing
or probabilistic choices is performed by quantitative verification tools. Broad
and mature tool support is available for computing basic properties such as expected
rewards on basic models such as Markov chains. Previous editions of QComp, the
comparison of tools for the analysis of quantitative formal models, focused on
this setting. Many application scenarios, however, require more advanced property
types such as LTL and parameter synthesis queries as well as advanced models like
stochastic games and partially observable MDPs. For these, tool support is in
its infancy today. This paper presents the outcomes of QComp 2023: a survey of
the state of the art in quantitative verification tool support for advanced property
types and models. With tools ranging from first research prototypes to well-supported
integrations into established toolsets, this report highlights today’s active
areas and tomorrow’s challenges in tool-focused research for quantitative verification.'
acknowledgement: The authors are ordered alphabetically. This work was supported by
DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU
under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199
(ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075
(CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA),
by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006
(SMARTITUDE), and by NWO VENI grant 639.021.754.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Roman
full_name: Andriushchenko, Roman
last_name: Andriushchenko
- first_name: Alexander
full_name: Bork, Alexander
last_name: Bork
- first_name: Carlos E.
full_name: Budde, Carlos E.
last_name: Budde
- first_name: Milan
full_name: Češka, Milan
last_name: Češka
- first_name: Kush
full_name: Grover, Kush
last_name: Grover
- first_name: Ernst Moritz
full_name: Hahn, Ernst Moritz
last_name: Hahn
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- first_name: Bryant
full_name: Israelsen, Bryant
last_name: Israelsen
- first_name: Nils
full_name: Jansen, Nils
last_name: Jansen
- first_name: Joshua
full_name: Jeppson, Joshua
last_name: Jeppson
- first_name: Sebastian
full_name: Junges, Sebastian
last_name: Junges
- first_name: Maximilian A.
full_name: Köhl, Maximilian A.
last_name: Köhl
- first_name: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- 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: David
full_name: Parker, David
last_name: Parker
- first_name: Stefan
full_name: Pranger, Stefan
last_name: Pranger
- first_name: Tim
full_name: Quatmann, Tim
last_name: Quatmann
- first_name: Enno
full_name: Ruijters, Enno
last_name: Ruijters
- first_name: Landon
full_name: Taylor, Landon
last_name: Taylor
- first_name: Matthias
full_name: Volk, Matthias
last_name: Volk
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
- first_name: Zhen
full_name: Zhang, Zhen
last_name: Zhang
citation:
ama: 'Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report. In: TOOLympics Challenge 2023.
Vol 14550. Springer Nature; 2024:90-146. doi:10.1007/978-3-031-67695-6_4'
apa: 'Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E.
M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp
2023 Competition Report. In TOOLympics Challenge 2023 (Vol. 14550, pp.
90–146). Springer Nature. https://doi.org/10.1007/978-3-031-67695-6_4'
chicago: 'Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush
Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report.” In TOOLympics Challenge 2023,
14550:90–146. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-67695-6_4.'
ieee: 'R. Andriushchenko et al., “Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report,” in TOOLympics Challenge 2023,
2024, vol. 14550, pp. 90–146.'
ista: 'Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns
A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky
J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk
M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification:
QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550,
90–146.'
mla: 'Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification:
QComp 2023 Competition Report.” TOOLympics Challenge 2023, vol. 14550,
Springer Nature, 2024, pp. 90–146, doi:10.1007/978-3-031-67695-6_4.'
short: R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A.
Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer,
J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters,
L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer
Nature, 2024, pp. 90–146.
das_tickbox: '1'
dataavailabilitystatement: All model files used for the comparison, as well as the
resulting log files, are available at DOI 10.5281/zenodo.8219191
date_created: 2024-12-01T23:01:53Z
date_published: 2024-11-01T00:00:00Z
date_updated: 2026-10-16T07:53:26Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-031-67695-6_4
external_id:
arxiv:
- '2405.13583'
isi:
- '001434957500004'
fulldoi: https://doi.org/10.1007/978-3-031-67695-6_4
intvolume: ' 14550'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2405.13583'
month: '11'
oa: 1
oa_version: Preprint
page: 90-146
publication: TOOLympics Challenge 2023
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031676949'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '23142'
relation: research_data
status: public
researchdata_availability: yes
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition
Report'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14550
year: '2024'
...
---
OA_place: publisher
OA_type: gold
_id: '17099'
abstract:
- lang: eng
text: "We study two-player zero-sum concurrent stochastic games with finite state
and action space played for an infinite number of steps. In every step, the two
players simultaneously and independently choose an action. Given the current state
and the chosen actions, the next state is obtained according to a stochastic transition
function. An objective is a measurable function on plays (or infinite trajectories)
of the game, and the value for an objective is the maximal expectation that the
player can guarantee against the adversarial player. We consider: (a) stateful-discounted
objectives, which are similar to the classical discounted-sum objectives, but
states are associated with different discount factors rather than a single discount
factor; and (b) parity objectives, which are a canonical representation for ω-regular
objectives. For stateful-discounted objectives, given an ordering of the discount
factors, the limit value is the limit of the value of the stateful-discounted
objectives, as the discount factors approach zero according to the given order.\r\nThe
computational problem we consider is the approximation of the value within an
arbitrary\r\nadditive error. The above problem is known to be in EXPSPACE for
the limit value of statefuldiscounted objectives and in PSPACE for parity objectives.
The best-known algorithms for both the above problems are at least exponential
time, with an exponential dependence on the number of states and actions. Our
main results for the value approximation problem for the limit value of stateful-discounted
objectives and parity objectives are as follows: (a) we establish TFNP[NP] complexity;
and (b) we present algorithms that improve the dependency on the number of actions
in the exponent from linear to logarithmic. In particular, if the number of states
is constant, our algorithms run in polynomial time."
acknowledgement: "This research was partially supported by ERC CoG 863818 (ForM-SMArt),
Austrian\r\nScience Fund (FWF) 10.55776/COE12, and French Agence Nationale de la
Recherche (ANR)\r\nANR-21-CE40-0020 (CONVERGENCE project)"
alternative_title:
- LIPIcs
article_number: '5'
article_processing_charge: No
arxiv: 1
author:
- first_name: Ali
full_name: Asadi, Ali
id: 02d96aae-000e-11ec-b801-cadd0a5eefbb
last_name: Asadi
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Raimundo J
full_name: Saona Urmeneta, Raimundo J
id: BD1DF4C4-D767-11E9-B658-BC13E6697425
last_name: Saona Urmeneta
orcid: 0000-0001-5103-038X
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Asadi A, Chatterjee K, Saona Urmeneta RJ, Svoboda J. Concurrent stochastic
games with stateful-discounted and parity objectives: Complexity and algorithms.
In: 44th IARCS Annual Conference on Foundations of Software Technology and
Theoretical Computer Science. Vol 323. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2024. doi:10.4230/LIPIcs.FSTTCS.2024.5'
apa: 'Asadi, A., Chatterjee, K., Saona Urmeneta, R. J., & Svoboda, J. (2024).
Concurrent stochastic games with stateful-discounted and parity objectives: Complexity
and algorithms. In 44th IARCS Annual Conference on Foundations of Software
Technology and Theoretical Computer Science (Vol. 323). Gujarat, India: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5'
chicago: 'Asadi, Ali, Krishnendu Chatterjee, Raimundo J Saona Urmeneta, and Jakub
Svoboda. “Concurrent Stochastic Games with Stateful-Discounted and Parity Objectives:
Complexity and Algorithms.” In 44th IARCS Annual Conference on Foundations
of Software Technology and Theoretical Computer Science, Vol. 323. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2024. https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5.'
ieee: 'A. Asadi, K. Chatterjee, R. J. Saona Urmeneta, and J. Svoboda, “Concurrent
stochastic games with stateful-discounted and parity objectives: Complexity and
algorithms,” in 44th IARCS Annual Conference on Foundations of Software Technology
and Theoretical Computer Science, Gujarat, India, 2024, vol. 323.'
ista: 'Asadi A, Chatterjee K, Saona Urmeneta RJ, Svoboda J. 2024. Concurrent stochastic
games with stateful-discounted and parity objectives: Complexity and algorithms.
44th IARCS Annual Conference on Foundations of Software Technology and Theoretical
Computer Science. FSTTCS: Foundations of Software Technology and Theoretical Computer
Science, LIPIcs, vol. 323, 5.'
mla: 'Asadi, Ali, et al. “Concurrent Stochastic Games with Stateful-Discounted and
Parity Objectives: Complexity and Algorithms.” 44th IARCS Annual Conference
on Foundations of Software Technology and Theoretical Computer Science, vol.
323, 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:10.4230/LIPIcs.FSTTCS.2024.5.'
short: A. Asadi, K. Chatterjee, R.J. Saona Urmeneta, J. Svoboda, in:, 44th IARCS
Annual Conference on Foundations of Software Technology and Theoretical Computer
Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
conference:
end_date: 2024-12-18
location: Gujarat, India
name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
start_date: 2024-12-16
corr_author: '1'
das_tickbox: '0'
date_created: 2024-06-03T07:44:27Z
date_published: 2024-12-05T00:00:00Z
date_updated: 2026-10-16T08:00:46Z
day: '05'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.FSTTCS.2024.5
ec_funded: 1
external_id:
arxiv:
- '2405.02486'
isi:
- '001537516500005'
file:
- access_level: open_access
checksum: 5b544ab4692b93300b404435c036ddd4
content_type: application/pdf
creator: dernst
date_created: 2025-01-08T09:49:31Z
date_updated: 2025-01-08T09:49:31Z
file_id: '18777'
file_name: 2024_LIPIcs_Asadi.pdf
file_size: 847960
relation: main_file
success: 1
file_date_updated: 2025-01-08T09:49:31Z
fulldoi: https://doi.org/10.4230/LIPIcs.FSTTCS.2024.5
has_accepted_license: '1'
intvolume: ' 323'
isi: 1
language:
- iso: eng
month: '12'
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: 44th IARCS Annual Conference on Foundations of Software Technology and
Theoretical Computer Science
publication_identifier:
isbn:
- '9783959773553'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
record:
- id: '23079'
relation: dissertation_contains
status: public
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Concurrent stochastic games with stateful-discounted and parity objectives:
Complexity and algorithms'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 323
year: '2024'
...
---
_id: '18159'
abstract:
- lang: eng
text: "Markov Decision Processes (MDPs) are a classical model for decision making
in the presence of uncertainty. Often they are viewed as state transformers with
planning objectives defned with respect to paths over MDP states. An increasingly\r\npopular
alternative is to view them as distribution transformers, giving rise to a sequence
of probability distributions over MDP states. For instance, reachability and safety
properties in modeling robot swarms or chemical reaction networks are naturally
defned in terms of probability distributions over states. Verifying such distributional
properties is known to be hard and often beyond the reach of classical state-based
verifcation techniques. In this work, we consider the problems of certifed policy
(i.e. controller) verifcation and synthesis in MDPs under distributional reach-avoidance
specifcations. By certifed we mean that, along with a policy, we also aim to synthesize
a (checkable) certifcate ensuring that the MDP indeed satisfes the property. Thus,
given the target set of distributions and an unsafe set of distributions over
MDP states, our goal is to either synthesize a certifcate for a given policy or
synthesize a policy along with a certifcate, proving that the target distribution
can be reached while avoiding unsafe distributions. To solve this problem, we
introduce the novel notion of distributional reach-avoid certifcates and present
automated procedures for (1) synthesizing a certifcate for a given policy, and
(2) synthesizing a policy together with the certifcate, both providing formal
guarantees on certifcate correctness. Our experimental evaluation demonstrates
the ability of our method to solve several non-trivial examples, including a multi-agent
robot-swarm model, to synthesize certifed policies and to certify existing policies. "
acknowledgement: This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt),
the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant,
Google Research Award 2023 and the SBI Foundation Hub for Data and Analytics.
article_processing_charge: No
arxiv: 1
author:
- first_name: S
full_name: Akshay, S
last_name: Akshay
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. Certified policy verification
and synthesis for MDPs under distributional reach-avoidance properties. In: Proceedings
of the Thirty-Third International Joint Conference on Artificial Intelligence.
International Joint Conferences on Artificial Intelligence; 2024:3-12. doi:10.24963/ijcai.2024/1'
apa: 'Akshay, S., Chatterjee, K., Meggendorfer, T., & Zikelic, D. (2024). Certified
policy verification and synthesis for MDPs under distributional reach-avoidance
properties. In Proceedings of the Thirty-Third International Joint Conference
on Artificial Intelligence (pp. 3–12). Jeju, Korea: International Joint Conferences
on Artificial Intelligence. https://doi.org/10.24963/ijcai.2024/1'
chicago: Akshay, S, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic.
“Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance
Properties.” In Proceedings of the Thirty-Third International Joint Conference
on Artificial Intelligence, 3–12. International Joint Conferences on Artificial
Intelligence, 2024. https://doi.org/10.24963/ijcai.2024/1.
ieee: S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “Certified policy
verification and synthesis for MDPs under distributional reach-avoidance properties,”
in Proceedings of the Thirty-Third International Joint Conference on Artificial
Intelligence, Jeju, Korea, 2024, pp. 3–12.
ista: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2024. Certified policy
verification and synthesis for MDPs under distributional reach-avoidance properties.
Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence.
IJCAI: International Joint Conference on Artificial Intelligence, 3–12.'
mla: Akshay, S., et al. “Certified Policy Verification and Synthesis for MDPs under
Distributional Reach-Avoidance Properties.” Proceedings of the Thirty-Third
International Joint Conference on Artificial Intelligence, International Joint
Conferences on Artificial Intelligence, 2024, pp. 3–12, doi:10.24963/ijcai.2024/1.
short: S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, Proceedings of
the Thirty-Third International Joint Conference on Artificial Intelligence, International
Joint Conferences on Artificial Intelligence, 2024, pp. 3–12.
conference:
end_date: 2024-08-09
location: Jeju, Korea
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2024-08-03
corr_author: '1'
das_tickbox: '0'
date_created: 2024-09-29T22:01:38Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2026-10-16T08:08:15Z
day: '01'
department:
- _id: KrCh
doi: 10.24963/ijcai.2024/1
ec_funded: 1
external_id:
arxiv:
- '2405.04015'
fulldoi: https://doi.org/10.24963/ijcai.2024/1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2405.04015
month: '09'
oa: 1
oa_version: Preprint
page: 3-12
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the Thirty-Third International Joint Conference on Artificial
Intelligence
publication_identifier:
isbn:
- '9781956792041'
issn:
- 1045-0823
publication_status: published
publisher: International Joint Conferences on Artificial Intelligence
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Certified policy verification and synthesis for MDPs under distributional reach-avoidance
properties
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
---
OA_place: publisher
OA_type: hybrid
_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: Yes (via OA deal)
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
orcid: 0000-0002-6143-1926
- 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. 2024;63:40-80.
doi:10.1007/s10703-023-00411-4
apa: Chatterjee, K., Katoen, J. P., Mohr, S., Weininger, M., & Winkler, T. (2024).
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, 2024. 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,
vol. 63. Springer Nature, pp. 40–80, 2024.
ista: Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2024. Stochastic
games with lexicographic objectives. Formal Methods in System Design. 63, 40–80.
mla: Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Objectives.”
Formal Methods in System Design, vol. 63, Springer Nature, 2024, pp. 40–80,
doi:10.1007/s10703-023-00411-4.
short: K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods
in System Design 63 (2024) 40–80.
das_tickbox: '1'
dataavailabilitystatement: The software and data used to generate the experimental
results of this paper are available online(See https://doi.org/10.5281/zenodo.5798108
and https://doi.org/10.5281/zenodo.7233605 for the experiments described in Sect.
5.1 and Sect. 5.2, respectively.).
date_created: 2023-03-19T23:00:59Z
date_published: 2024-10-01T00:00:00Z
date_updated: 2026-10-16T08:04:16Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s10703-023-00411-4
ec_funded: 1
external_id:
isi:
- '000946174300001'
file:
- access_level: open_access
checksum: 111e76b76163640a2c89237642af586f
content_type: application/pdf
creator: dernst
date_created: 2025-01-09T07:31:31Z
date_updated: 2025-01-09T07:31:31Z
file_id: '18781'
file_name: 2024_FromMethodsSys_Chatterjee.pdf
file_size: 2614190
relation: main_file
success: 1
file_date_updated: 2025-01-09T07:31:31Z
fulldoi: https://doi.org/10.1007/s10703-023-00411-4
has_accepted_license: '1'
intvolume: ' 63'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 40-80
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: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '8272'
relation: earlier_version
status: public
researchdata_availability: yes
scopus_import: '1'
status: public
supplementarymaterial: no
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 63
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18160'
abstract:
- lang: eng
text: 'Markov decision processes (MDPs) provide a standard framework for sequential
decision making under uncertainty. However, MDPs do not take uncertainty in transition
probabilities into account. Robust Markov decision processes (RMDPs) address this
shortcoming of MDPs by assigning to each transition an uncertainty set rather
than a single probability value. In this work, we consider polytopic RMDPs in
which all uncertainty sets are polytopes and study the problem of solving long-run
average reward polytopic RMDPs. We present a novel perspective on this problem
and show that it can be reduced to solving long-run average reward turn-based
stochastic games with finite state and action spaces. This reduction allows us
to derive several important consequences that were hitherto not known to hold
for polytopic RMDPs. First, we derive new computational complexity bounds for
solving long-run average reward polytopic RMDPs, showing for the first time that
the threshold decision problem for them is in NP∩CONP and that they admit a randomized
algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic
Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run
average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is
much more efficient in solving long-run average reward polytopic RMDPs compared
to state-of-the-art methods based on value iteration. '
acknowledgement: "This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt)
and the Czech Science Foundation\r\ngrant no. GA23-06963S."
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
orcid: 0009-0007-5253-9170
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. Solving long-run
average reward robust MDPs via stochastic games. In: 33rd International Joint
Conference on Artificial Intelligence. International Joint Conferences on
Artificial Intelligence; 2024:6707-6715. doi:10.24963/ijcai.2024/741'
apa: 'Chatterjee, K., Goharshady, E., Karrabi, M., Novotný, P., & Zikelic, D.
(2024). Solving long-run average reward robust MDPs via stochastic games. In 33rd
International Joint Conference on Artificial Intelligence (pp. 6707–6715).
Jeju, South Korea: International Joint Conferences on Artificial Intelligence.
https://doi.org/10.24963/ijcai.2024/741'
chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Petr Novotný,
and Dorde Zikelic. “Solving Long-Run Average Reward Robust MDPs via Stochastic
Games.” In 33rd International Joint Conference on Artificial Intelligence,
6707–15. International Joint Conferences on Artificial Intelligence, 2024. https://doi.org/10.24963/ijcai.2024/741.
ieee: K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, and D. Zikelic, “Solving
long-run average reward robust MDPs via stochastic games,” in 33rd International
Joint Conference on Artificial Intelligence, Jeju, South Korea, 2024, pp.
6707–6715.
ista: 'Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving
long-run average reward robust MDPs via stochastic games. 33rd International Joint
Conference on Artificial Intelligence. IJCAI: International Joint Conference on
Artificial Intelligence, 6707–6715.'
mla: Chatterjee, Krishnendu, et al. “Solving Long-Run Average Reward Robust MDPs
via Stochastic Games.” 33rd International Joint Conference on Artificial Intelligence,
International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–15,
doi:10.24963/ijcai.2024/741.
short: K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, D. Zikelic, in:, 33rd
International Joint Conference on Artificial Intelligence, International Joint
Conferences on Artificial Intelligence, 2024, pp. 6707–6715.
conference:
end_date: 2024-08-09
location: Jeju, South Korea
name: 'IJCAI: International Joint Conference on Artificial Intelligence'
start_date: 2024-08-03
corr_author: '1'
das_tickbox: '0'
date_created: 2024-09-29T22:01:39Z
date_published: 2024-09-01T00:00:00Z
date_updated: 2026-10-16T08:07:05Z
day: '01'
department:
- _id: KrCh
doi: 10.24963/ijcai.2024/741
ec_funded: 1
external_id:
arxiv:
- '2312.13912'
fulldoi: https://doi.org/10.24963/ijcai.2024/741
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2312.13912
month: '09'
oa: 1
oa_version: Preprint
page: 6707-6715
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 33rd International Joint Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781956792041'
issn:
- 1045-0823
publication_status: published
publisher: International Joint Conferences on Artificial Intelligence
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Solving long-run average reward robust MDPs via stochastic games
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
---
OA_place: publisher
OA_type: hybrid
_id: '17474'
abstract:
- lang: eng
text: Entropic risk (ERisk) is an established risk measure in finance, quantifying
risk by an exponential re-weighting of rewards. We study ERisk for the first time
in the context of turn-based stochastic games with the total reward objective.
This gives rise to an objective function that demands the control of systems in
a risk-averse manner. We show that the resulting games are determined and, in
particular, admit optimal memoryless deterministic strategies. This contrasts
risk measures that previously have been considered in the special case of Markov
decision processes and that require randomization and/or memory. We provide several
results on the decidability and the computational complexity of the threshold
problem, i.e. whether the optimal value of ERisk exceeds a given threshold. Furthermore,
an approximation algorithm for the optimal value of ERisk is provided.
acknowledgement: Krishnendu Chatterjee reports financial support was provided by European
Research Council.
article_number: '105214'
article_processing_charge: Yes (in subscription journal)
article_type: original
arxiv: 1
author:
- first_name: Christel
full_name: Baier, Christel
last_name: Baier
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Jakob
full_name: Piribauer, Jakob
last_name: Piribauer
citation:
ama: Baier C, Chatterjee K, Meggendorfer T, Piribauer J. Entropic risk for turn-based
stochastic games. Information and Computation. 2024;301. doi:10.1016/j.ic.2024.105214
apa: Baier, C., Chatterjee, K., Meggendorfer, T., & Piribauer, J. (2024). Entropic
risk for turn-based stochastic games. Information and Computation. Elsevier.
https://doi.org/10.1016/j.ic.2024.105214
chicago: Baier, Christel, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob
Piribauer. “Entropic Risk for Turn-Based Stochastic Games.” Information and
Computation. Elsevier, 2024. https://doi.org/10.1016/j.ic.2024.105214.
ieee: C. Baier, K. Chatterjee, T. Meggendorfer, and J. Piribauer, “Entropic risk
for turn-based stochastic games,” Information and Computation, vol. 301.
Elsevier, 2024.
ista: Baier C, Chatterjee K, Meggendorfer T, Piribauer J. 2024. Entropic risk for
turn-based stochastic games. Information and Computation. 301, 105214.
mla: Baier, Christel, et al. “Entropic Risk for Turn-Based Stochastic Games.” Information
and Computation, vol. 301, 105214, Elsevier, 2024, doi:10.1016/j.ic.2024.105214.
short: C. Baier, K. Chatterjee, T. Meggendorfer, J. Piribauer, Information and Computation
301 (2024).
corr_author: '1'
das_tickbox: '0'
date_created: 2024-09-01T22:01:07Z
date_published: 2024-12-01T00:00:00Z
date_updated: 2026-10-16T08:04:31Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1016/j.ic.2024.105214
external_id:
arxiv:
- '2307.06611'
isi:
- '001301143400001'
file:
- access_level: open_access
checksum: f68e0c2f46f9b9c86815406bcf2ee2d4
content_type: application/pdf
creator: dernst
date_created: 2025-01-09T13:49:03Z
date_updated: 2025-01-09T13:49:03Z
file_id: '18817'
file_name: 2024_InformationComputation_Baier.pdf
file_size: 724703
relation: main_file
success: 1
file_date_updated: 2025-01-09T13:49:03Z
fulldoi: https://doi.org/10.1016/j.ic.2024.105214
has_accepted_license: '1'
intvolume: ' 301'
isi: 1
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
publication: Information and Computation
publication_identifier:
eissn:
- 1090-2651
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '14417'
relation: earlier_version
status: public
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Entropic risk for turn-based stochastic games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 301
year: '2024'
...
---
OA_place: other
OA_type: green
_id: '18925'
abstract:
- lang: eng
text: Given the increasingly stringent requirements on the performance and efficiency
of communication networks, over the last years, great efforts have been made to
render networks more flexible and programmable. In particular, modern networks
support a flexible rerouting of flows, e.g., depending on the dynamically changing
traffic or network conditions. However, the underlying algorithmic problems are
still not well-understood today.In this paper, we revisit the k-Network Flow Update
problem that asks for a schedule to reroute k unsplittable flows from their current
paths to the given new paths, in a congestion-free manner in a capacitated network.
We show that the problem is already NP-hard for three acyclic flows on simple
directed graphs. Our main contribution is an efficient algorithm for sparse networks;
specifically the algorithm is fixed parameter tractable in the number of flows
and the treewidth of a graph that is the union of all flows. Our results also
settle the open complexity question in the literature.
acknowledgement: Research was supported by the Austrian Science Fund (FWF), project
I 5025-N (DELTA), 2020-2024. Esra Ceylan’s research was supported by FFG, FEMtech
Praktika für Studentinnen. Jakub Svoboda and Krishnendu Chatterjee were supported
by the European Research Council (ERC) CoG 863818 (ForM-SMArt).
article_processing_charge: No
author:
- first_name: Esra
full_name: Ceylan, Esra
id: cb1ca1d8-dcc0-11ef-baa5-9f1b3ef75933
last_name: Ceylan
- 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
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Ceylan E, Chatterjee K, Schmid S, Svoboda J. Congestion-free rerouting of
network flows: Hardness and an FPT algorithm. In: NOMS 2024-2024 IEEE Network
Operations and Management Symposium. IEEE; 2024. doi:10.1109/noms59830.2024.10575579'
apa: 'Ceylan, E., Chatterjee, K., Schmid, S., & Svoboda, J. (2024). Congestion-free
rerouting of network flows: Hardness and an FPT algorithm. In NOMS 2024-2024
IEEE Network Operations and Management Symposium. Seoul, Republic of Korea:
IEEE. https://doi.org/10.1109/noms59830.2024.10575579'
chicago: 'Ceylan, Esra, Krishnendu Chatterjee, Stefan Schmid, and Jakub Svoboda.
“Congestion-Free Rerouting of Network Flows: Hardness and an FPT Algorithm.” In
NOMS 2024-2024 IEEE Network Operations and Management Symposium. IEEE,
2024. https://doi.org/10.1109/noms59830.2024.10575579.'
ieee: 'E. Ceylan, K. Chatterjee, S. Schmid, and J. Svoboda, “Congestion-free rerouting
of network flows: Hardness and an FPT algorithm,” in NOMS 2024-2024 IEEE Network
Operations and Management Symposium, Seoul, Republic of Korea, 2024.'
ista: 'Ceylan E, Chatterjee K, Schmid S, Svoboda J. 2024. Congestion-free rerouting
of network flows: Hardness and an FPT algorithm. NOMS 2024-2024 IEEE Network Operations
and Management Symposium. NOMS: Network Operations and Management Symposiu .'
mla: 'Ceylan, Esra, et al. “Congestion-Free Rerouting of Network Flows: Hardness
and an FPT Algorithm.” NOMS 2024-2024 IEEE Network Operations and Management
Symposium, IEEE, 2024, doi:10.1109/noms59830.2024.10575579.'
short: E. Ceylan, K. Chatterjee, S. Schmid, J. Svoboda, in:, NOMS 2024-2024 IEEE
Network Operations and Management Symposium, IEEE, 2024.
conference:
end_date: 2024-05-10
location: Seoul, Republic of Korea
name: 'NOMS: Network Operations and Management Symposiu '
start_date: 2024-05-06
corr_author: '1'
das_tickbox: '0'
date_created: 2025-01-27T15:06:45Z
date_published: 2024-05-01T00:00:00Z
date_updated: 2026-10-16T08:07:55Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/noms59830.2024.10575579
ec_funded: 1
external_id:
isi:
- '001270140300143'
fulldoi: https://doi.org/10.1109/noms59830.2024.10575579
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://schmiste.github.io/noms24.pdf
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: bd622a5c-d553-11ed-ba76-bae280ba8aff
grant_number: '894907'
name: Graphical Games
publication: NOMS 2024-2024 IEEE Network Operations and Management Symposium
publication_identifier:
eissn:
- 2374-9709
isbn:
- '9798350327946'
publication_status: published
publisher: IEEE
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Congestion-free rerouting of network flows: Hardness and an FPT algorithm'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
---
_id: '17328'
abstract:
- lang: eng
text: "We study selfish mining attacks in longest-chain blockchains like Bitcoin,
but where the proof of work is replaced with efficient proof systems - like proofs
of stake or proofs of space - and consider the problem of computing an optimal
selfish mining attack which maximizes expected relative revenue of the adversary,
thus minimizing the chain quality. To this end, we propose a novel selfish mining
attack that aims to maximize this objective and formally model the attack as a
Markov decision process (MDP). We then present a formal analysis procedure which
computes an ϵ-tight lower bound on the optimal expected relative revenue in the
MDP and a strategy that achieves this ϵ-tight lower bound, where ϵ > 0 may be
any specified precision. Our analysis is fully automated and provides formal guarantees
on the correctness. We evaluate our selfish mining attack and observe that it
achieves superior expected relative revenue compared to two considered baselines.\r\nIn
concurrent work [Sarenche FC'24] does an automated analysis on selfish mining
in predictable longest-chain blockchains based on efficient proof systems. Predictable
means the randomness for the challenges is fixed for many blocks (as used e.g.,
in Ouroboros), while we consider unpredictable (Bitcoin-like) chains where the
challenge is derived from the previous block."
acknowledgement: "This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt)
grant and the MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms) grant.\r\n"
article_processing_charge: Yes (via OA deal)
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amirali
full_name: Ebrahimzadeh, Amirali
last_name: Ebrahimzadeh
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
orcid: 0009-0007-5253-9170
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
- first_name: Michelle X
full_name: Yeo, Michelle X
id: 2D82B818-F248-11E8-B48F-1D18A9856A87
last_name: Yeo
orcid: 0009-0001-3676-4809
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D. Fully
automated selfish mining analysis in efficient proof systems blockchains. In:
Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing.
Association for Computing Machinery; 2024:268-278. doi:10.1145/3662158.3662769'
apa: 'Chatterjee, K., Ebrahimzadeh, A., Karrabi, M., Pietrzak, K. Z., Yeo, M. X.,
& Zikelic, D. (2024). Fully automated selfish mining analysis in efficient
proof systems blockchains. In Proceedings of the 43rd Annual ACM Symposium
on Principles of Distributed Computing (pp. 268–278). Nantes, France: Association
for Computing Machinery. https://doi.org/10.1145/3662158.3662769'
chicago: Chatterjee, Krishnendu, Amirali Ebrahimzadeh, Mehrdad Karrabi, Krzysztof
Z Pietrzak, Michelle X Yeo, and Dorde Zikelic. “Fully Automated Selfish Mining
Analysis in Efficient Proof Systems Blockchains.” In Proceedings of the 43rd
Annual ACM Symposium on Principles of Distributed Computing, 268–78. Association
for Computing Machinery, 2024. https://doi.org/10.1145/3662158.3662769.
ieee: K. Chatterjee, A. Ebrahimzadeh, M. Karrabi, K. Z. Pietrzak, M. X. Yeo, and
D. Zikelic, “Fully automated selfish mining analysis in efficient proof systems
blockchains,” in Proceedings of the 43rd Annual ACM Symposium on Principles
of Distributed Computing, Nantes, France, 2024, pp. 268–278.
ista: 'Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D.
2024. Fully automated selfish mining analysis in efficient proof systems blockchains.
Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing.
PODC: Symposium on Principles of Distributed Computing, 268–278.'
mla: Chatterjee, Krishnendu, et al. “Fully Automated Selfish Mining Analysis in
Efficient Proof Systems Blockchains.” Proceedings of the 43rd Annual ACM Symposium
on Principles of Distributed Computing, Association for Computing Machinery,
2024, pp. 268–78, doi:10.1145/3662158.3662769.
short: K. Chatterjee, A. Ebrahimzadeh, M. Karrabi, K.Z. Pietrzak, M.X. Yeo, D. Zikelic,
in:, Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed
Computing, Association for Computing Machinery, 2024, pp. 268–278.
conference:
end_date: 2024-06-21
location: Nantes, France
name: 'PODC: Symposium on Principles of Distributed Computing'
start_date: 2024-06-17
corr_author: '1'
das_tickbox: '0'
date_created: 2024-07-28T22:01:10Z
date_published: 2024-06-17T00:00:00Z
date_updated: 2026-10-16T08:09:09Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
- _id: KrPi
doi: 10.1145/3662158.3662769
ec_funded: 1
external_id:
arxiv:
- '2405.04420'
file:
- access_level: open_access
checksum: 6122bd97b42751ff81c452a19970f67d
content_type: application/pdf
creator: dernst
date_created: 2024-07-29T07:18:12Z
date_updated: 2024-07-29T07:18:12Z
file_id: '17334'
file_name: 2024_ACM_Chatterjee.pdf
file_size: 832034
relation: main_file
success: 1
file_date_updated: 2024-07-29T07:18:12Z
fulldoi: https://doi.org/10.1145/3662158.3662769
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 268-278
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed
Computing
publication_identifier:
isbn:
- '9798400706684'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Fully automated selfish mining analysis in efficient proof systems blockchains
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
---
_id: '15007'
abstract:
- lang: eng
text: Traditional blockchains grant the miner of a block full control not only over
which transactions but also their order. This constitutes a major flaw discovered
with the introduction of decentralized finance and allows miners to perform MEV
attacks. In this paper, we address the issue of sandwich attacks by providing
a construction that takes as input a blockchain protocol and outputs a new blockchain
protocol with the same security but in which sandwich attacks are not profitable.
Furthermore, our protocol is fully decentralized with no trusted third parties
or heavy cryptography primitives and carries a linear increase in latency and
minimum computation overhead.
acknowledgement: "We would like to thank Krzysztof Pietrzak and Jovana Mićić for useful
discussions. This work has been funded by the Swiss National Science Foundation
(SNSF) under grant agreement Nr. 200021_188443 (Advanced Consensus Protocols).\r\n"
alternative_title:
- LIPIcs
article_number: '12'
article_processing_charge: No
arxiv: 1
author:
- first_name: Orestis
full_name: Alpos, Orestis
last_name: Alpos
- first_name: Ignacio
full_name: Amores-Sesar, Ignacio
last_name: Amores-Sesar
- first_name: Christian
full_name: Cachin, Christian
last_name: Cachin
- 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: 'Alpos O, Amores-Sesar I, Cachin C, Yeo MX. Eating sandwiches: Modular and
lightweight elimination of transaction reordering attacks. 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.12'
apa: 'Alpos, O., Amores-Sesar, I., Cachin, C., & Yeo, M. X. (2024). Eating sandwiches:
Modular and lightweight elimination of transaction reordering attacks. 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.12'
chicago: 'Alpos, Orestis, Ignacio Amores-Sesar, Christian Cachin, and Michelle X
Yeo. “Eating Sandwiches: Modular and Lightweight Elimination of Transaction Reordering
Attacks.” 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.12.'
ieee: 'O. Alpos, I. Amores-Sesar, C. Cachin, and M. X. Yeo, “Eating sandwiches:
Modular and lightweight elimination of transaction reordering attacks,” in 27th
International Conference on Principles of Distributed Systems, Tokyo, Japan,
2024, vol. 286.'
ista: 'Alpos O, Amores-Sesar I, Cachin C, Yeo MX. 2024. Eating sandwiches: Modular
and lightweight elimination of transaction reordering attacks. 27th International
Conference on Principles of Distributed Systems. OPODIS: Conference on Principles
of Distributed Systems, LIPIcs, vol. 286, 12.'
mla: 'Alpos, Orestis, et al. “Eating Sandwiches: Modular and Lightweight Elimination
of Transaction Reordering Attacks.” 27th International Conference on Principles
of Distributed Systems, vol. 286, 12, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2024, doi:10.4230/LIPIcs.OPODIS.2023.12.'
short: O. Alpos, I. Amores-Sesar, C. Cachin, M.X. Yeo, 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
corr_author: '1'
das_tickbox: '0'
date_created: 2024-02-18T23:01:02Z
date_published: 2024-01-18T00:00:00Z
date_updated: 2026-10-16T08:10:21Z
day: '18'
ddc:
- '000'
department:
- _id: KrPi
doi: 10.4230/LIPIcs.OPODIS.2023.12
external_id:
arxiv:
- '2307.02954'
isi:
- '001585185800012'
file:
- access_level: open_access
checksum: 2993e810a45e8c8056106834b07aea92
content_type: application/pdf
creator: dernst
date_created: 2024-02-26T10:16:57Z
date_updated: 2024-02-26T10:16:57Z
file_id: '15031'
file_name: 2024_LIPICs_Alpos.pdf
file_size: 1505994
relation: main_file
success: 1
file_date_updated: 2024-02-26T10:16:57Z
fulldoi: https://doi.org/10.4230/LIPIcs.OPODIS.2023.12
has_accepted_license: '1'
intvolume: ' 286'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
publication: 27th International Conference on Principles of Distributed Systems
publication_identifier:
isbn:
- '9783959773089'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Eating sandwiches: Modular and lightweight elimination of transaction reordering
attacks'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 286
year: '2024'
...
---
_id: '17051'
abstract:
- lang: eng
text: "Memory-hard functions (MHF) are functions whose evaluation provably requires\r\na
lot of memory. While MHFs are an unkeyed primitive, it is natural to consider
the\r\nnotion of trapdoor MHFs (TMHFs). A TMHF is like an MHF, but when sampling\r\nthe
public parameters one also samples a trapdoor which allows evaluating the\r\nfunction
much cheaper.\r\nBiryukov and Perrin (Asiacrypt’17) were the first to consider
TMHFs and put\r\nforth a candidate TMHF construction called Diodon that is based
on the Scrypt\r\nMHF (Percival, BSDCan’09). To allow for a trapdoor, Scrypt’s
initial hash chain\r\nis replaced by a sequence of squares in a group of unknown
order where the order of\r\nthe group is the trapdoor. For a length n sequence
of squares and a group of order\r\nN, Diodon’s cumulative memory complexity (CMC)
is O(n2log N) without the\r\ntrapdoor and O(n log(n) log(N)2) with knowledge of
it.\r\nWhile Scrypt is proven to be optimally memory-hard in the random oracle\r\nmodel
(Alwen et al., Eurocrypt’17), Diodon’s memory-hardness has not been\r\nproven
so far. In this work, we fill this gap by rigorously analyzing a specific\r\ninstantiation
of Diodon. We show that its CMC is lower bounded by Ω( n2log nlog N)\r\nwhich
almost matches the upper bound. Our proof is based Alwen et al.’s lower\r\nbound
on Scrypt’s CMC but requires non-trivial modifications due to the algebraic\r\nstructure
of Diodon. Most importantly, our analysis involves a more elaborate\r\ncompression
argument and a solvability criterion for certain systems of Diophantine\r\nequations."
acknowledgement: We thank the Eurocrypt reviewers for their thorough review and for
pointing out related works. This research was funded in whole or in part by the
Austrian Science Fund (FWF) 10.55776/F85.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Benedikt
full_name: Auerbach, Benedikt
id: D33D2B18-E445-11E9-ABB7-15F4E5697425
last_name: Auerbach
orcid: 0000-0002-7553-6606
- first_name: Christoph Ullrich
full_name: Günther, Christoph Ullrich
id: ec98511c-eb8e-11eb-b029-edd25d7271a1
last_name: Günther
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
citation:
ama: 'Auerbach B, Günther CU, Pietrzak KZ. Trapdoor memory-hard functions. In: 43rd
Annual International Conference on the Theory and Applications of Cryptographic
Techniques. Vol 14653. Springer Nature; 2024:315-344. doi:10.1007/978-3-031-58734-4_11'
apa: 'Auerbach, B., Günther, C. U., & Pietrzak, K. Z. (2024). Trapdoor memory-hard
functions. In 43rd Annual International Conference on the Theory and Applications
of Cryptographic Techniques (Vol. 14653, pp. 315–344). Zurich, Switzerland:
Springer Nature. https://doi.org/10.1007/978-3-031-58734-4_11'
chicago: Auerbach, Benedikt, Christoph Ullrich Günther, and Krzysztof Z Pietrzak.
“Trapdoor Memory-Hard Functions.” In 43rd Annual International Conference on
the Theory and Applications of Cryptographic Techniques, 14653:315–44. Springer
Nature, 2024. https://doi.org/10.1007/978-3-031-58734-4_11.
ieee: B. Auerbach, C. U. Günther, and K. Z. Pietrzak, “Trapdoor memory-hard functions,”
in 43rd Annual International Conference on the Theory and Applications of Cryptographic
Techniques, Zurich, Switzerland, 2024, vol. 14653, pp. 315–344.
ista: 'Auerbach B, Günther CU, Pietrzak KZ. 2024. Trapdoor memory-hard functions.
43rd Annual International Conference on the Theory and Applications of Cryptographic
Techniques. EUROCRYPT: Theory and Applications of Cryptographic Techniques, LNCS,
vol. 14653, 315–344.'
mla: Auerbach, Benedikt, et al. “Trapdoor Memory-Hard Functions.” 43rd Annual
International Conference on the Theory and Applications of Cryptographic Techniques,
vol. 14653, Springer Nature, 2024, pp. 315–44, doi:10.1007/978-3-031-58734-4_11.
short: B. Auerbach, C.U. Günther, K.Z. Pietrzak, in:, 43rd Annual International
Conference on the Theory and Applications of Cryptographic Techniques, Springer
Nature, 2024, pp. 315–344.
conference:
end_date: 2024-05-30
location: Zurich, Switzerland
name: 'EUROCRYPT: Theory and Applications of Cryptographic Techniques'
start_date: 2024-05-26
corr_author: '1'
das_tickbox: '0'
date_created: 2024-05-26T22:00:58Z
date_published: 2024-05-01T00:00:00Z
date_updated: 2026-10-16T08:09:46Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-031-58734-4_11
external_id:
isi:
- '001274940200011'
fulldoi: https://doi.org/10.1007/978-3-031-58734-4_11
intvolume: ' 14653'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2024/312
month: '05'
oa: 1
oa_version: Preprint
page: 315-344
project:
- _id: 34a34d57-11ca-11ed-8bc3-a2688a8724e1
grant_number: F8509
name: Security and Privacy by Design for Complex Systems
publication: 43rd Annual International Conference on the Theory and Applications of
Cryptographic Techniques
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031587337'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Trapdoor memory-hard functions
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14653
year: '2024'
...
---
OA_place: publisher
OA_type: hybrid
_id: '17283'
abstract:
- lang: eng
text: 'We consider the problems of statically refuting equivalence and similarity
of output distributions defined by a pair of probabilistic programs. Equivalence
and similarity are two fundamental relational properties of probabilistic programs
that are essential for their correctness both in implementation and in compilation.
In this work, we present a new method for static equivalence and similarity refutation.
Our method refutes equivalence and similarity by computing a function over program
outputs whose expected value with respect to the output distributions of two programs
is different. The function is computed simultaneously with an upper expectation
supermartingale and a lower expectation submartingale for the two programs, which
we show to together provide a formal certificate for refuting equivalence and
similarity. To the best of our knowledge, our method is the first approach to
relational program analysis to offer the combination of the following desirable
features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic
programs, and (3) it provides formal guarantees on the correctness of its results.
We implement a prototype of our method and our experiments demonstrate the effectiveness
of our method to refute equivalence and similarity for a number of examples collected
from the literature.'
acknowledgement: "This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant. Petr Novotný\r\nis supported by the Czech Science Foundation grant no. GA23-06963S.\r\n"
article_number: '232'
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: Chatterjee K, Goharshady E, Novotný P, Zikelic D. Equivalence and similarity
refutation for probabilistic programs. Proceedings of the ACM on Programming
Languages. 2024;8. doi:10.1145/3656462
apa: Chatterjee, K., Goharshady, E., Novotný, P., & Zikelic, D. (2024). Equivalence
and similarity refutation for probabilistic programs. Proceedings of the ACM
on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3656462
chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic.
“Equivalence and Similarity Refutation for Probabilistic Programs.” Proceedings
of the ACM on Programming Languages. Association for Computing Machinery,
2024. https://doi.org/10.1145/3656462.
ieee: K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Equivalence and
similarity refutation for probabilistic programs,” Proceedings of the ACM on
Programming Languages, vol. 8. Association for Computing Machinery, 2024.
ista: Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2024. Equivalence and similarity
refutation for probabilistic programs. Proceedings of the ACM on Programming Languages.
8, 232.
mla: Chatterjee, Krishnendu, et al. “Equivalence and Similarity Refutation for Probabilistic
Programs.” Proceedings of the ACM on Programming Languages, vol. 8, 232,
Association for Computing Machinery, 2024, doi:10.1145/3656462.
short: K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, Proceedings of the
ACM on Programming Languages 8 (2024).
corr_author: '1'
das_tickbox: '0'
date_created: 2024-07-21T22:01:01Z
date_published: 2024-06-20T00:00:00Z
date_updated: 2026-10-16T08:08:51Z
day: '20'
ddc:
- '000'
department:
- _id: KrCh
- _id: GradSch
doi: 10.1145/3656462
ec_funded: 1
external_id:
arxiv:
- '2404.03430'
file:
- access_level: open_access
checksum: 8cbf220f284a4a87d093db5320c5afdd
content_type: application/pdf
creator: dernst
date_created: 2024-07-22T07:17:14Z
date_updated: 2024-07-22T07:17:14Z
file_id: '17290'
file_name: 2024_ACMProgLang_Chatterjee.pdf
file_size: 355421
relation: main_file
success: 1
file_date_updated: 2024-07-22T07:17:14Z
fulldoi: https://doi.org/10.1145/3656462
has_accepted_license: '1'
intvolume: ' 8'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Equivalence and similarity refutation for probabilistic programs
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 8
year: '2024'
...
---
_id: '14820'
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 many 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 \r\n 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+E) . (1+3) for some arbitrary E>0."
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.
article_number: '114353'
article_processing_charge: Yes (via OA deal)
article_type: original
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. Theoretical Computer
Science. 2024;989. doi:10.1016/j.tcs.2023.114353'
apa: 'Schmid, S., Svoboda, J., & Yeo, M. X. (2024). Weighted packet selection
for rechargeable links in cryptocurrency networks: Complexity and approximation.
Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2023.114353'
chicago: 'Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection
for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.”
Theoretical Computer Science. Elsevier, 2024. https://doi.org/10.1016/j.tcs.2023.114353.'
ieee: 'S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable
links in cryptocurrency networks: Complexity and approximation,” Theoretical
Computer Science, vol. 989. Elsevier, 2024.'
ista: 'Schmid S, Svoboda J, Yeo MX. 2024. Weighted packet selection for rechargeable
links in cryptocurrency networks: Complexity and approximation. Theoretical Computer
Science. 989, 114353.'
mla: 'Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in
Cryptocurrency Networks: Complexity and Approximation.” Theoretical Computer
Science, vol. 989, 114353, Elsevier, 2024, doi:10.1016/j.tcs.2023.114353.'
short: S. Schmid, J. Svoboda, M.X. Yeo, Theoretical Computer Science 989 (2024).
corr_author: '1'
das_tickbox: '0'
date_created: 2024-01-16T13:40:41Z
date_published: 2024-03-21T00:00:00Z
date_updated: 2026-10-16T08:09:27Z
day: '21'
ddc:
- '000'
department:
- _id: KrCh
- _id: KrPi
doi: 10.1016/j.tcs.2023.114353
ec_funded: 1
external_id:
isi:
- '001168211400001'
file:
- access_level: open_access
checksum: efd5b7e738bf845312ba53889a3e13e4
content_type: application/pdf
creator: dernst
date_created: 2024-07-16T12:02:25Z
date_updated: 2024-07-16T12:02:25Z
file_id: '17263'
file_name: 2024_TheorComputerScience_Schmid.pdf
file_size: 603570
relation: main_file
success: 1
file_date_updated: 2024-07-16T12:02:25Z
fulldoi: https://doi.org/10.1016/j.tcs.2023.114353
has_accepted_license: '1'
intvolume: ' 989'
isi: 1
keyword:
- General Computer Science
- Theoretical Computer Science
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: Theoretical Computer Science
publication_identifier:
issn:
- 0304-3975
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '19985'
relation: earlier_version
status: public
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Weighted packet selection for rechargeable links in cryptocurrency networks:
Complexity and approximation'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 989
year: '2024'
...
---
_id: '17126'
abstract:
- lang: eng
text: "Functional encryption (FE) is a primitive where the holder of a master secret
key can control which functions a user can evaluate on encrypted data. It is a
powerful primitive that even implies indistinguishability obfuscation (iO), given
sufficiently compact ciphertexts (Ananth-Jain, CRYPTO’15 and Bitansky-Vaikuntanathan,
FOCS’15). However, despite being extensively studied, there are FE schemes, such
as function-hiding inner-product FE (Bishop-Jain-Kowalczyk, AC’15, Abdalla-Catalano-Fiore-Gay-Ursu,
CRYPTO’18) and compact quadratic FE (Baltico-Catalano-Fiore-Gay, Lin, CRYPTO’17),
that can be only realized using pairings. This raises the question if there are
some mathematical barriers that hinder us from realizing these FE schemes from
other assumptions.\r\n\r\nIn this paper, we study the difficulty of constructing
lattice-based compact FE. We generalize the impossibility results of Ünal (EC’20)
for lattice-based function-hiding FE, and extend it to the case of compact FE.
Concretely, we prove lower bounds for lattice-based compact FE schemes which meet
some (natural) algebraic restrictions at encryption and decryption, and have ciphertexts
of linear size and secret keys of minimal degree. We see our results as important
indications of why it is hard to construct lattice-based FE schemes for new functionalities,
and which mathematical barriers have to be overcome."
acknowledgement: We want to thank the anonymous reviewers of TCC and Eurocrypt for
their very helpful comments and suggestions. This work has received funding from
the Austrian Science Fund (FWF) and netidee SCIENCE via grant P31621-N38 (PROFET).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Erkan
full_name: Tairi, Erkan
last_name: Tairi
- first_name: Akin
full_name: Ünal, Akin
id: f6b56fb6-dc63-11ee-9dbf-f6780863a85a
last_name: Ünal
orcid: 0000-0002-8929-0221
citation:
ama: 'Tairi E, Ünal A. Lower bounds for lattice-based compact functional encryption.
In: Advances in Cryptology – EUROCRYPT 2024. Vol 14652. Springer Nature;
2024:249-279. doi:10.1007/978-3-031-58723-8_9'
apa: 'Tairi, E., & Ünal, A. (2024). Lower bounds for lattice-based compact functional
encryption. In Advances in Cryptology – EUROCRYPT 2024 (Vol. 14652, pp.
249–279). Zurich, Switzerland: Springer Nature. https://doi.org/10.1007/978-3-031-58723-8_9'
chicago: Tairi, Erkan, and Akin Ünal. “Lower Bounds for Lattice-Based Compact Functional
Encryption.” In Advances in Cryptology – EUROCRYPT 2024, 14652:249–79.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-58723-8_9.
ieee: E. Tairi and A. Ünal, “Lower bounds for lattice-based compact functional encryption,”
in Advances in Cryptology – EUROCRYPT 2024, Zurich, Switzerland, 2024,
vol. 14652, pp. 249–279.
ista: 'Tairi E, Ünal A. 2024. Lower bounds for lattice-based compact functional
encryption. Advances in Cryptology – EUROCRYPT 2024. EUROCRYPT: Theory and Applications
of Cryptographic Techniques, LNCS, vol. 14652, 249–279.'
mla: Tairi, Erkan, and Akin Ünal. “Lower Bounds for Lattice-Based Compact Functional
Encryption.” Advances in Cryptology – EUROCRYPT 2024, vol. 14652, Springer
Nature, 2024, pp. 249–79, doi:10.1007/978-3-031-58723-8_9.
short: E. Tairi, A. Ünal, in:, Advances in Cryptology – EUROCRYPT 2024, Springer
Nature, 2024, pp. 249–279.
conference:
end_date: 2024-05-30
location: Zurich, Switzerland
name: 'EUROCRYPT: Theory and Applications of Cryptographic Techniques'
start_date: 2024-05-26
das_tickbox: '0'
date_created: 2024-06-09T22:01:03Z
date_published: 2024-05-08T00:00:00Z
date_updated: 2026-10-16T08:10:05Z
day: '08'
department:
- _id: KrPi
doi: 10.1007/978-3-031-58723-8_9
external_id:
isi:
- '001278247600009'
fulldoi: https://doi.org/10.1007/978-3-031-58723-8_9
intvolume: ' 14652'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2023/719.pdf
month: '05'
oa: 1
oa_version: Submitted Version
page: 249-279
publication: Advances in Cryptology – EUROCRYPT 2024
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031587221'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Lower bounds for lattice-based compact functional encryption
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14652
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18755'
abstract:
- lang: eng
text: "A universalthresholdizer (UT), constructed from a threshold fully homomorphic
encryption by Boneh et. al , Crypto 2018, is a general framework for universally
thresholdizing many cryptographic schemes. However, their framework is insufficient
to construct strongly secure threshold schemes, such as threshold signatures and
threshold public-key encryption, etc.\r\n\r\nIn this paper, we strengthen the
security definition for a universal thresholdizer and propose a scheme which satisfies
our stronger security notion. Our UT scheme is an improvement of Boneh et. al
’s construction at the level of threshold fully homomorphic encryption using a
key homomorphic pseudorandom function. We apply our strongly secure UT scheme
to construct strongly secure threshold signatures and threshold public-key encryption."
acknowledgement: Ehsan Ebrahimi is supported by the Luxembourg National Research Fund
under the Junior CORE project QSP (C22/IS/17272217/QSP/Ebrahimi).
article_processing_charge: No
author:
- first_name: Ehsan
full_name: Ebrahimi, Ehsan
last_name: Ebrahimi
- first_name: Anshu
full_name: Yadav, Anshu
id: dc8f1524-403e-11ee-bf07-9649ad996e21
last_name: Yadav
citation:
ama: 'Ebrahimi E, Yadav A. Strongly secure universal thresholdizer. In: 30th
International Conference on the Theory and Application of Cryptology and Information
Security. Vol 15486. Springer Nature; 2024:207-239. doi:10.1007/978-981-96-0891-1_7'
apa: 'Ebrahimi, E., & Yadav, A. (2024). Strongly secure universal thresholdizer.
In 30th International Conference on the Theory and Application of Cryptology
and Information Security (Vol. 15486, pp. 207–239). Kolkata, India: Springer
Nature. https://doi.org/10.1007/978-981-96-0891-1_7'
chicago: Ebrahimi, Ehsan, and Anshu Yadav. “Strongly Secure Universal Thresholdizer.”
In 30th International Conference on the Theory and Application of Cryptology
and Information Security, 15486:207–39. Springer Nature, 2024. https://doi.org/10.1007/978-981-96-0891-1_7.
ieee: E. Ebrahimi and A. Yadav, “Strongly secure universal thresholdizer,” in 30th
International Conference on the Theory and Application of Cryptology and Information
Security, Kolkata, India, 2024, vol. 15486, pp. 207–239.
ista: 'Ebrahimi E, Yadav A. 2024. Strongly secure universal thresholdizer. 30th
International Conference on the Theory and Application of Cryptology and Information
Security. ASIACRYPT: Conference on the Theory and Application of Cryptology and
Information Security vol. 15486, 207–239.'
mla: Ebrahimi, Ehsan, and Anshu Yadav. “Strongly Secure Universal Thresholdizer.”
30th International Conference on the Theory and Application of Cryptology and
Information Security, vol. 15486, Springer Nature, 2024, pp. 207–39, doi:10.1007/978-981-96-0891-1_7.
short: E. Ebrahimi, A. Yadav, in:, 30th International Conference on the Theory and
Application of Cryptology and Information Security, Springer Nature, 2024, pp.
207–239.
conference:
end_date: 2024-12-13
location: Kolkata, India
name: 'ASIACRYPT: Conference on the Theory and Application of Cryptology and Information
Security'
start_date: 2024-12-09
das_tickbox: '0'
date_created: 2025-01-05T23:01:56Z
date_published: 2024-12-12T00:00:00Z
date_updated: 2026-10-16T08:10:40Z
day: '12'
department:
- _id: KrPi
doi: 10.1007/978-981-96-0891-1_7
external_id:
isi:
- '001443889100007'
fulldoi: https://doi.org/10.1007/978-981-96-0891-1_7
intvolume: ' 15486'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2024/2078
month: '12'
oa: 1
oa_version: Preprint
page: 207-239
publication: 30th International Conference on the Theory and Application of Cryptology
and Information Security
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9789819608904'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Strongly secure universal thresholdizer
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15486
year: '2024'
...
---
OA_place: publisher
OA_type: green
_id: '18974'
abstract:
- lang: eng
text: Reinforcement Learning (RL) from temporal logical specifications is a fundamental
problem in sequential decision making. One of the basic and core such specification
is the reachability specification that requires a target set to be eventually
visited. Despite strong empirical results for RL from such specifications, the
theoretical guarantees are bleak, including the impossibility of Probably Approximately
Correct (PAC) guarantee for reachability specifications. Given the impossibility
result, in this work we consider the problem of RL from reachability specifications
along with the information of expected conditional distance (ECD). We present
(a) lower bound results which establish the necessity of ECD information for PAC
guarantees and (b) an algorithm that establishes PAC-guarantees given the ECD
information. To the best of our knowledge, this is the first RL from reachability
specifications that does not make any assumptions on the underlying environment
to learn policies.
alternative_title:
- PMLR
article_processing_charge: No
author:
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Suguman
full_name: Bansal, Suguman
last_name: Bansal
- 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, Bansal S, Chatterjee K. Reinforcement learning from reachability
specifications: PAC guarantees with expected conditional distance. In: 41st
International Conference on Machine Learning. Vol 235. ML Research Press;
2024:47331-47344.'
apa: 'Svoboda, J., Bansal, S., & Chatterjee, K. (2024). Reinforcement learning
from reachability specifications: PAC guarantees with expected conditional distance.
In 41st International Conference on Machine Learning (Vol. 235, pp. 47331–47344).
Vienna, Austria: ML Research Press.'
chicago: 'Svoboda, Jakub, Suguman Bansal, and Krishnendu Chatterjee. “Reinforcement
Learning from Reachability Specifications: PAC Guarantees with Expected Conditional
Distance.” In 41st International Conference on Machine Learning, 235:47331–44.
ML Research Press, 2024.'
ieee: 'J. Svoboda, S. Bansal, and K. Chatterjee, “Reinforcement learning from reachability
specifications: PAC guarantees with expected conditional distance,” in 41st
International Conference on Machine Learning, Vienna, Austria, 2024, vol.
235, pp. 47331–47344.'
ista: 'Svoboda J, Bansal S, Chatterjee K. 2024. Reinforcement learning from reachability
specifications: PAC guarantees with expected conditional distance. 41st International
Conference on Machine Learning. ICML: International Conference on Machine Learning,
PMLR, vol. 235, 47331–47344.'
mla: 'Svoboda, Jakub, et al. “Reinforcement Learning from Reachability Specifications:
PAC Guarantees with Expected Conditional Distance.” 41st International Conference
on Machine Learning, vol. 235, ML Research Press, 2024, pp. 47331–44.'
short: J. Svoboda, S. Bansal, K. Chatterjee, in:, 41st International Conference
on Machine Learning, ML Research Press, 2024, pp. 47331–47344.
conference:
end_date: 2024-07-27
location: Vienna, Austria
name: 'ICML: International Conference on Machine Learning'
start_date: 2024-07-21
corr_author: '1'
das_tickbox: '0'
date_created: 2025-01-30T07:45:22Z
date_published: 2024-07-29T00:00:00Z
date_updated: 2026-10-16T08:08:33Z
day: '29'
department:
- _id: KrCh
intvolume: ' 235'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://openreview.net/forum?id=mXUDDL4r1Q
month: '07'
oa: 1
oa_version: Preprint
page: 47331-47344
publication: 41st International Conference on Machine Learning
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Reinforcement learning from reachability specifications: PAC guarantees with
expected conditional distance'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 235
year: '2024'
...
---
OA_place: publisher
_id: '18088'
abstract:
- lang: eng
text: "Instant messaging applications like Whatsapp, Signal or Telegram have become
ubiquitous in today's society.\r\nMany of them provide not only end-to-end encryption,
but also security guarantees even when the key material gets compromised.\r\nThese
are achieved through frequent key update performed by users.\r\nIn particular,
the compromise of a group key should preserve confidentiality of previously exchanged
messages (forward secrecy), and a subsequent key update will ensure security for
future ones (post-compromise security).\r\nThough great protocols for one-on-one
communication have been known for some time, the design of ones that scale efficiently
for larger groups while achieving akin security guarantees is a hard problem.\r\nA
great deal of research has been aimed at this topic, much of it under the umbrella
of the Messaging Layer Security (MLS) working group at the IETF. \r\nStarted in
2018, this joint effort by academics and industry culminated in 2023 with the
publication of the first standard for secure group messaging [IETF, RFC9420].\r\n\r\nAt
the core of secure group messaging is a cryptographic primitive termed Continuous
Group Key Agreement, or CGKA [Alwen et al. 2021], that essentially allows a changing
group of users to agree on a common key with the added functionality security
against compromises is achieved by users asynchronously issuing a key update.
In this thesis we contribute to the understanding of CGKA across different angles.\r\nFirst,
we present a new technique to effect dynamic operations in groups, i.e., add or
remove members, that can be more efficient that the one employed by MLS in certain
settings.\r\nConsidering the setting of users belonging to multiple overlapping
groups, we then show lowerbounds on the communication cost of constructions that
leverage said overlap, at the same time showing protocols that are asymptotically
optimal and efficient for practical settings, respectively. Along the way, we
show that the communication cost of key updates in MLS is average-cost optimal.\r\nAn
important feature in CGKA protocols, particularly for big groups, is the possibility
of executing several group operations concurrently. While later versions of MLS
support this, they do at the cost of worsening the communication efficiency of
future group operations.\r\nIn this thesis we introduce two new protocols that
permit concurrency without any negative effect on efficiency. Our protocols circumvent
previously existing lower bounds by satisfying a new notion of post-compromise
security that only asks for security to be re-established after a certain number
of key updates have taken place. While this can be slower than MLS in terms of
rounds of communication, we show that it leads to more efficient overall communication.
\r\nAdditionally, we introduce a new technique that allows group members to decrease
the information they need to store and download, which makes one of our protocols
enjoy much lower download cost than any other existing CGKA constructions. "
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Guillermo
full_name: Pascual Perez, Guillermo
id: 2D7ABD02-F248-11E8-B48F-1D18A9856A87
last_name: Pascual Perez
orcid: 0000-0001-8630-415X
citation:
ama: Pascual Perez G. On the efficiency and security of secure group messaging.
2024. doi:10.15479/at:ista:18088
apa: Pascual Perez, G. (2024). On the efficiency and security of secure group
messaging. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:18088
chicago: Pascual Perez, Guillermo. “On the Efficiency and Security of Secure Group
Messaging.” Institute of Science and Technology Austria, 2024. https://doi.org/10.15479/at:ista:18088.
ieee: G. Pascual Perez, “On the efficiency and security of secure group messaging,”
Institute of Science and Technology Austria, 2024.
ista: Pascual Perez G. 2024. On the efficiency and security of secure group messaging.
Institute of Science and Technology Austria.
mla: Pascual Perez, Guillermo. On the Efficiency and Security of Secure Group
Messaging. Institute of Science and Technology Austria, 2024, doi:10.15479/at:ista:18088.
short: G. Pascual Perez, On the Efficiency and Security of Secure Group Messaging,
Institute of Science and Technology Austria, 2024.
corr_author: '1'
das_tickbox: '1'
date_created: 2024-09-18T12:59:49Z
date_published: 2024-09-18T00:00:00Z
date_updated: 2026-10-16T08:11:08Z
day: '18'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: KrPi
- _id: GradSch
doi: 10.15479/at:ista:18088
doi_confirm: '1'
ec_funded: 1
file:
- access_level: closed
checksum: ce0dca715b3df48e52e2e891b6ac1bc5
content_type: application/x-zip-compressed
creator: gpascual
date_created: 2024-09-19T12:35:38Z
date_updated: 2024-09-19T12:35:38Z
file_id: '18099'
file_name: thesis_bundle.zip
file_size: 11917734
relation: source_file
- access_level: open_access
checksum: 4a2c72e90f1a0ef2a13cff800f8d1265
content_type: application/pdf
creator: gpascual
date_created: 2024-09-19T12:36:08Z
date_updated: 2024-09-19T12:36:08Z
file_id: '18100'
file_name: thesis_gpasper.pdf
file_size: 2729427
relation: main_file
file_date_updated: 2024-09-19T12:36:08Z
fulldoi: https://doi.org/10.15479/at:ista:18088
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '239'
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '10408'
relation: part_of_dissertation
status: public
- id: '11476'
relation: part_of_dissertation
status: public
- id: '10049'
relation: part_of_dissertation
status: public
- id: '18086'
relation: part_of_dissertation
status: public
researchdata_availability: yes
status: public
supervisor:
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
supplementarymaterial: not applicable
title: On the efficiency and security of secure group messaging
tmp:
image: /images/cc_by_nc_sa.png
legal_code_url: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC
BY-NC-SA 4.0)
short: CC BY-NC-SA (4.0)
type: dissertation
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
---
_id: '18086'
abstract:
- lang: eng
text: "Abstract. Continuous group key agreement (CGKA) allows a group of\r\nusers
to maintain a continuously updated shared key in an asynchronous\r\nsetting where
parties only come online sporadically and their messages\r\nare relayed by an
untrusted server. CGKA captures the basic primitive\r\nunderlying group messaging
schemes.\r\nCurrent solutions including TreeKEM (“Messaging Layer Security”\r\n(MLS)
IETF RFC 9420) cannot handle concurrent requests while retaining low communication
complexity. The exception being CoCoA, which\r\nis concurrent while having extremely
low communication complexity (in\r\ngroups of size n and for m concurrent updates
the communication per\r\nuser is log(n), i.e., independent of m). The main downside
of CoCoA\r\nis that in groups of size n, users might have to do up to log(n) update\r\nrequests
to the server to ensure their (potentially corrupted) key material has been refreshed.\r\nIn
this work we present a “fast healing” concurrent CGKA protocol,\r\nnamed DeCAF,
where users will heal after at most log(t) requests, with\r\nt being the number
of corrupted users. While also suitable for the standard central-server setting,
our protocol is particularly interesting for\r\nrealizing decentralized group
messaging, where protocol messages (add,\r\nremove, update) are being posted on
some append-only data structure\r\nrather than sent to a server. In this setting,
concurrency is crucial once\r\nthe rate of requests exceeds, say, the rate at
which new blocks are added\r\nto a blockchain.\r\nIn the central-server setting,
CoCoA (the only alternative with concurrency, sub-linear communication and basic
post-compromise security)\r\nenjoys much lower download communication. However,
in the decentralized setting – where there is no server which can craft specific
messages\r\nfor different users to reduce their download communication – our protocol\r\nsignificantly
outperforms CoCoA. DeCAF heals in fewer epochs (log(t)\r\nvs. log(n)) while incurring
a similar per epoch per user communication\r\ncost."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Joel F
full_name: Alwen, Joel F
id: 2A8DFA8C-F248-11E8-B48F-1D18A9856A87
last_name: Alwen
- first_name: Benedikt
full_name: Auerbach, Benedikt
id: D33D2B18-E445-11E9-ABB7-15F4E5697425
last_name: Auerbach
orcid: 0000-0002-7553-6606
- first_name: Miguel
full_name: Cueto Noval, Miguel
id: ffc563a3-f6e0-11ea-865d-e3cce03d17cc
last_name: Cueto Noval
orcid: 0000-0002-2505-4246
- first_name: Karen
full_name: Klein, Karen
id: 3E83A2F8-F248-11E8-B48F-1D18A9856A87
last_name: Klein
- first_name: Guillermo
full_name: Pascual Perez, Guillermo
id: 2D7ABD02-F248-11E8-B48F-1D18A9856A87
last_name: Pascual Perez
orcid: 0000-0001-8630-415X
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
citation:
ama: 'Alwen JF, Auerbach B, Cueto Noval M, Klein K, Pascual Perez G, Pietrzak KZ.
DeCAF: Decentralizable CGKA with fast healing. In: Galdi C, Phan DH, eds. Security
and Cryptography for Networks: 14th International Conference. Vol 14974. Cham:
Springer Nature; 2024:294–313. doi:10.1007/978-3-031-71073-5_14'
apa: 'Alwen, J. F., Auerbach, B., Cueto Noval, M., Klein, K., Pascual Perez, G.,
& Pietrzak, K. Z. (2024). DeCAF: Decentralizable CGKA with fast healing. In
C. Galdi & D. H. Phan (Eds.), Security and Cryptography for Networks: 14th
International Conference (Vol. 14974, pp. 294–313). Cham: Springer Nature.
https://doi.org/10.1007/978-3-031-71073-5_14'
chicago: 'Alwen, Joel F, Benedikt Auerbach, Miguel Cueto Noval, Karen Klein, Guillermo
Pascual Perez, and Krzysztof Z Pietrzak. “DeCAF: Decentralizable CGKA with Fast
Healing.” In Security and Cryptography for Networks: 14th International Conference,
edited by Clemente Galdi and Duong Hieu Phan, 14974:294–313. Cham: Springer Nature,
2024. https://doi.org/10.1007/978-3-031-71073-5_14.'
ieee: 'J. F. Alwen, B. Auerbach, M. Cueto Noval, K. Klein, G. Pascual Perez, and
K. Z. Pietrzak, “DeCAF: Decentralizable CGKA with fast healing,” in Security
and Cryptography for Networks: 14th International Conference, Amalfi, Italy,
2024, vol. 14974, pp. 294–313.'
ista: 'Alwen JF, Auerbach B, Cueto Noval M, Klein K, Pascual Perez G, Pietrzak KZ.
2024. DeCAF: Decentralizable CGKA with fast healing. Security and Cryptography
for Networks: 14th International Conference. SCN: Security and Cryptography for
Networks, LNCS, vol. 14974, 294–313.'
mla: 'Alwen, Joel F., et al. “DeCAF: Decentralizable CGKA with Fast Healing.” Security
and Cryptography for Networks: 14th International Conference, edited by Clemente
Galdi and Duong Hieu Phan, vol. 14974, Springer Nature, 2024, pp. 294–313, doi:10.1007/978-3-031-71073-5_14.'
short: 'J.F. Alwen, B. Auerbach, M. Cueto Noval, K. Klein, G. Pascual Perez, K.Z.
Pietrzak, in:, C. Galdi, D.H. Phan (Eds.), Security and Cryptography for Networks:
14th International Conference, Springer Nature, Cham, 2024, pp. 294–313.'
conference:
end_date: 2024-09-13
location: Amalfi, Italy
name: 'SCN: Security and Cryptography for Networks'
start_date: 2024-09-11
corr_author: '1'
das_tickbox: '0'
date_created: 2024-09-18T11:35:14Z
date_published: 2024-09-10T00:00:00Z
date_updated: 2026-10-16T08:11:07Z
day: '10'
department:
- _id: GradSch
- _id: KrPi
doi: 10.1007/978-3-031-71073-5_14
editor:
- first_name: Clemente
full_name: Galdi, Clemente
last_name: Galdi
- first_name: Duong Hieu
full_name: Phan, Duong Hieu
last_name: Phan
external_id:
isi:
- '001330408000014'
fulldoi: https://doi.org/10.1007/978-3-031-71073-5_14
intvolume: ' 14974'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 294–313
place: Cham
publication: 'Security and Cryptography for Networks: 14th International Conference'
publication_identifier:
eisbn:
- '9783031710735'
eissn:
- 1611-3349
isbn:
- '9783031710728'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '18088'
relation: dissertation_contains
status: public
researchdata_availability: no
status: public
supplementarymaterial: no
title: 'DeCAF: Decentralizable CGKA with fast healing'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14974
year: '2024'
...
---
OA_place: publisher
OA_type: gold
_id: '18961'
abstract:
- lang: eng
text: "Automated contact tracing (ACT) emerged as a promising measure to curb the
spread of Covid-19. Users enable ACT on their smartphones to automatically record
contacts with other users. If a user tests positive for the disease, they report
their diagnosis to alert their contacts.\r\nDesigning effective ACT protocols
is challenging since they need to be efficient and secure while also ensuring
users' privacy. As ACT protocols necessarily leak some information by design,
defining privacy is difficult. For example, a user cannot deny having met another
user. Ideally, however, the user can plausibly deny everything else, in particular,
when they met. We call this privacy property contact-time deniability.\r\nWhile
some early works discussed contact-time deniability informally, it has received
little attention since then. We investigate deniability from a rigorous, theoretical
point of view and arrive at the following impossibility result:\r\nA decentralized
protocol with unidirectional communication cannot be contact-time deniable and
replay-secure. This holds even if malicious users treat smartphones as black-boxes.\r\n
Unidirectional protocols are usually very efficient and many proposals are unidirectional,
e.g., the widely-deployed Google-Apple Exposure Notifications. So the impossibility
result considerably constrains the design space of efficient, secure, and private
ACT protocols. However, it can also be used as a guide; we discuss several possibilities
to achieve contact-time deniability in practice."
acknowledgement: "We thank Raluca-Georgia Diugan for her initial contributions and
support afterward.\r\nThis research was funded in whole or in part by the Austrian
Science Fund (FWF) 10.55776/F85."
article_processing_charge: No
article_type: original
author:
- first_name: Christoph Ullrich
full_name: Günther, Christoph Ullrich
id: ec98511c-eb8e-11eb-b029-edd25d7271a1
last_name: Günther
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
citation:
ama: 'Günther CU, Pietrzak KZ. Deniability in automated contact tracing: Impossibilities
and possibilities. Proceedings on Privacy Enhancing Technologies. 2024;2024(4):636-648.
doi:10.56553/popets-2024-0134'
apa: 'Günther, C. U., & Pietrzak, K. Z. (2024). Deniability in automated contact
tracing: Impossibilities and possibilities. Proceedings on Privacy Enhancing
Technologies. Bristol, UK/Virtual: Privacy Enhancing Technologies Symposium
Advisory Board. https://doi.org/10.56553/popets-2024-0134'
chicago: 'Günther, Christoph Ullrich, and Krzysztof Z Pietrzak. “Deniability in
Automated Contact Tracing: Impossibilities and Possibilities.” Proceedings
on Privacy Enhancing Technologies. Privacy Enhancing Technologies Symposium
Advisory Board, 2024. https://doi.org/10.56553/popets-2024-0134.'
ieee: 'C. U. Günther and K. Z. Pietrzak, “Deniability in automated contact tracing:
Impossibilities and possibilities,” Proceedings on Privacy Enhancing Technologies,
vol. 2024, no. 4. Privacy Enhancing Technologies Symposium Advisory Board, pp.
636–648, 2024.'
ista: 'Günther CU, Pietrzak KZ. 2024. Deniability in automated contact tracing:
Impossibilities and possibilities. Proceedings on Privacy Enhancing Technologies.
2024(4), 636–648.'
mla: 'Günther, Christoph Ullrich, and Krzysztof Z. Pietrzak. “Deniability in Automated
Contact Tracing: Impossibilities and Possibilities.” Proceedings on Privacy
Enhancing Technologies, vol. 2024, no. 4, Privacy Enhancing Technologies Symposium
Advisory Board, 2024, pp. 636–48, doi:10.56553/popets-2024-0134.'
short: C.U. Günther, K.Z. Pietrzak, Proceedings on Privacy Enhancing Technologies
2024 (2024) 636–648.
conference:
end_date: 2024-07-20
location: Bristol, UK/Virtual
name: 'PETs: Privacy Enhancing Technologies Symposium '
start_date: 2024-07-15
corr_author: '1'
das_tickbox: '0'
date_created: 2025-01-29T13:39:34Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2026-10-16T08:29:47Z
day: '01'
ddc:
- '000'
department:
- _id: KrPi
- _id: GradSch
doi: 10.56553/popets-2024-0134
file:
- access_level: open_access
checksum: 348ed6adcf6ad2f925227bde1758cae6
content_type: application/pdf
creator: dernst
date_created: 2025-01-29T13:44:47Z
date_updated: 2025-01-29T13:44:47Z
file_id: '18962'
file_name: 2024_ProcPrivacyEnhTech_Guenther.pdf
file_size: 611567
relation: main_file
success: 1
file_date_updated: 2025-01-29T13:44:47Z
fulldoi: https://doi.org/10.56553/popets-2024-0134
has_accepted_license: '1'
intvolume: ' 2024'
issue: '4'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 636-648
project:
- _id: 34a34d57-11ca-11ed-8bc3-a2688a8724e1
grant_number: F8509
name: Security and Privacy by Design for Complex Systems
publication: Proceedings on Privacy Enhancing Technologies
publication_identifier:
issn:
- 2299-0984
publication_status: published
publisher: Privacy Enhancing Technologies Symposium Advisory Board
quality_controlled: '1'
researchdata_availability: no
status: public
supplementarymaterial: no
title: 'Deniability in automated contact tracing: Impossibilities and possibilities'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 2024
year: '2024'
...