---
OA_place: repository
OA_type: green
_id: '21042'
abstract:
- lang: eng
text: "Many blockchains such as Ethereum execute all incoming transactions sequentially
significantly limiting the potential throughput. A common approach to scale execution
is parallel execution engines that fully utilize modern multi-core architectures.
Parallel execution is then either done optimistically, by executing transactions
in parallel and detecting conflicts on the fly, or guided, by requiring exhaustive
client transaction hints and scheduling transactions accordingly.\r\n\r\nHowever,
recent studies have shown that the performance of parallel execution engines depends
on the nature of the underlying workload. In fact, in some cases, only a 60% speed-up
compared to sequential execution could be obtained. This is the case, as transactions
that access the same resources must be executed sequentially. For example, if
10% of the transactions in a block access the same resource, the execution cannot
meaningfully scale beyond 10 cores. Therefore, a single popular application can
bottleneck the execution and limit the potential throughput.\r\n\r\nIn this paper,
we introduce Anthemius, a block construction algorithm that optimizes parallel
transaction execution throughput. We evaluate Anthemius exhaustively under a range
of workloads, and show that Anthemius enables the underlying parallel execution
engine to process over twice as many transactions."
acknowledgement: This work was supported by the Austrian Science Fund (FWF) SFB project
SpyCoDe F8502 and the Vienna Science and Technology Fund (WWTF) project SCALE2 CT22-045.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ray
full_name: Neiheiser, Ray
id: f09651b9-fec0-11ec-b5d8-934aff0e52a4
last_name: Neiheiser
orcid: 0000-0001-7227-8309
- first_name: Eleftherios
full_name: Kokoris Kogias, Eleftherios
id: f5983044-d7ef-11ea-ac6d-fd1430a26d30
last_name: Kokoris Kogias
orcid: 0000-0002-8827-3382
citation:
ama: 'Neiheiser R, Kokoris Kogias E. Anthemius: Efficient and modular block assembly
for concurrent execution. In: 29th International Conference on Financial Cryptography
and Data Security. Vol 15751. Springer Nature; 2026:307-323. doi:10.1007/978-3-032-07024-1_18'
apa: 'Neiheiser, R., & Kokoris Kogias, E. (2026). Anthemius: Efficient and modular
block assembly for concurrent execution. In 29th International Conference on
Financial Cryptography and Data Security (Vol. 15751, pp. 307–323). Miyakojima,
Japan: Springer Nature. https://doi.org/10.1007/978-3-032-07024-1_18'
chicago: 'Neiheiser, Ray, and Eleftherios Kokoris Kogias. “Anthemius: Efficient
and Modular Block Assembly for Concurrent Execution.” In 29th International
Conference on Financial Cryptography and Data Security, 15751:307–23. Springer
Nature, 2026. https://doi.org/10.1007/978-3-032-07024-1_18.'
ieee: 'R. Neiheiser and E. Kokoris Kogias, “Anthemius: Efficient and modular block
assembly for concurrent execution,” in 29th International Conference on Financial
Cryptography and Data Security, Miyakojima, Japan, 2026, vol. 15751, pp. 307–323.'
ista: 'Neiheiser R, Kokoris Kogias E. 2026. Anthemius: Efficient and modular block
assembly for concurrent execution. 29th International Conference on Financial
Cryptography and Data Security. FC: Financial Cryptography and Data Security,
LNCS, vol. 15751, 307–323.'
mla: 'Neiheiser, Ray, and Eleftherios Kokoris Kogias. “Anthemius: Efficient and Modular
Block Assembly for Concurrent Execution.” 29th International Conference on
Financial Cryptography and Data Security, vol. 15751, Springer Nature, 2026,
pp. 307–23, doi:10.1007/978-3-032-07024-1_18.'
short: R. Neiheiser, E. Kokoris Kogias, in:, 29th International Conference on Financial
Cryptography and Data Security, Springer Nature, 2026, pp. 307–323.
conference:
end_date: 2025-04-18
location: Miyakojima, Japan
name: 'FC: Financial Cryptography and Data Security'
start_date: 2025-04-14
corr_author: '1'
date_created: 2026-01-25T23:01:40Z
date_published: 2026-01-01T00:00:00Z
date_updated: 2026-02-12T13:39:07Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-032-07024-1_18
external_id:
arxiv:
- '2502.10074'
intvolume: ' 15751'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2502.10074
month: '01'
oa: 1
oa_version: Preprint
page: 307-323
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 7bdd2f70-9f16-11ee-852c-b7950bc6d277
grant_number: ICT22-045
name: SeCure, privAte, and interoperabLe layEr 2
publication: 29th International Conference on Financial Cryptography and Data Security
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032070234'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Anthemius: Efficient and modular block assembly for concurrent execution'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15751
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '21044'
abstract:
- lang: eng
text: 'Scalability is a crucial requirement for modern large-scale systems, enabling
elasticity and ensuring responsiveness under varying load. While cloud systems
have achieved scalable architectures, blockchain systems remain constrained by
the need to over-provision validator machines to handle peak load. This leads
to resource inefficiency, poor cost scaling, and limits on performance. To address
these challenges, we introduce Pilotfish, the first scale-out transaction execution
engine for blockchains. Pilotfish enables validators to scale horizontally by
distributing transaction execution across multiple worker machines, allowing elasticity
without compromising consistency or determinism. It integrates seamlessly with
the lazy blockchain architecture, completing the missing piece of execution elasticity.
To achieve this, Pilotfish tackles several key challenges: ensuring scalable and
strongly consistent distributed transactions, handling partial crash recovery
with lightweight replication, and maintaining concurrency with a novel versioned-queue
scheduling algorithm. Our evaluation shows that Pilotfish scales linearly up to
at least eight workers per validator for compute-bound workloads, while maintaining
low latency. By solving scalable execution, Pilotfish brings blockchains closer
to achieving end-to-end elasticity, unlocking new possibilities for efficient
and adaptable blockchain systems.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Quentin
full_name: Kniep, Quentin
last_name: Kniep
- first_name: Eleftherios
full_name: Kokoris Kogias, Eleftherios
id: f5983044-d7ef-11ea-ac6d-fd1430a26d30
last_name: Kokoris Kogias
orcid: 0000-0002-8827-3382
- first_name: Alberto
full_name: Sonnino, Alberto
last_name: Sonnino
- first_name: Igor
full_name: Zablotchi, Igor
last_name: Zablotchi
- first_name: Nuda
full_name: Zhang, Nuda
last_name: Zhang
citation:
ama: 'Kniep Q, Kokoris Kogias E, Sonnino A, Zablotchi I, Zhang N. Pilotfish: Distributed
execution for scalable blockchains. In: 29th International Conference on Financial
Cryptography and Data Security. Vol 15751. Springer Nature; 2026:287-306.
doi:10.1007/978-3-032-07024-1_17'
apa: 'Kniep, Q., Kokoris Kogias, E., Sonnino, A., Zablotchi, I., & Zhang, N.
(2026). Pilotfish: Distributed execution for scalable blockchains. In 29th
International Conference on Financial Cryptography and Data Security (Vol.
15751, pp. 287–306). Miyakojima, Japan: Springer Nature. https://doi.org/10.1007/978-3-032-07024-1_17'
chicago: 'Kniep, Quentin, Eleftherios Kokoris Kogias, Alberto Sonnino, Igor Zablotchi,
and Nuda Zhang. “Pilotfish: Distributed Execution for Scalable Blockchains.” In
29th International Conference on Financial Cryptography and Data Security,
15751:287–306. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-07024-1_17.'
ieee: 'Q. Kniep, E. Kokoris Kogias, A. Sonnino, I. Zablotchi, and N. Zhang, “Pilotfish:
Distributed execution for scalable blockchains,” in 29th International Conference
on Financial Cryptography and Data Security, Miyakojima, Japan, 2026, vol.
15751, pp. 287–306.'
ista: 'Kniep Q, Kokoris Kogias E, Sonnino A, Zablotchi I, Zhang N. 2026. Pilotfish:
Distributed execution for scalable blockchains. 29th International Conference
on Financial Cryptography and Data Security. FC: Financial Cryptography and Data
Security, LNCS, vol. 15751, 287–306.'
mla: 'Kniep, Quentin, et al. “Pilotfish: Distributed Execution for Scalable Blockchains.”
29th International Conference on Financial Cryptography and Data Security,
vol. 15751, Springer Nature, 2026, pp. 287–306, doi:10.1007/978-3-032-07024-1_17.'
short: Q. Kniep, E. Kokoris Kogias, A. Sonnino, I. Zablotchi, N. Zhang, in:, 29th
International Conference on Financial Cryptography and Data Security, Springer
Nature, 2026, pp. 287–306.
conference:
end_date: 2025-04-18
location: Miyakojima, Japan
name: 'FC: Financial Cryptography and Data Security'
start_date: 2025-04-14
date_created: 2026-01-25T23:01:41Z
date_published: 2026-01-01T00:00:00Z
date_updated: 2026-02-16T07:56:09Z
day: '01'
doi: 10.1007/978-3-032-07024-1_17
external_id:
arxiv:
- '2401.16292'
intvolume: ' 15751'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2401.16292
month: '01'
oa: 1
oa_version: Preprint
page: 287-306
publication: 29th International Conference on Financial Cryptography and Data Security
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032070234'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Pilotfish: Distributed execution for scalable blockchains'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15751
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '21135'
abstract:
- lang: eng
text: Three-dimensional (3D) microscopy data is often anisotropic with significantly
lower resolution (up to 8x) along the z axis than along the xy axes. Computationally
generating plausible isotropic resolution from anisotropic imaging data would
benefit the visual analysis of large-scale volumes. This paper proposes niiv,
a self-supervised method for isotropic reconstruction of 3D microscopy data that
can quickly produce images at arbitrary output resolutions. The representation
embeds a learned latent code within a neural field that describes the implicit
higher-resolution isotropic image region. We use an attention-guided latent interpolation
approach, which allows flexible information exchange over a local latent neighborhood.
Under isotropic volume assumptions, we self-supervise this representation on low-/high-resolution
lateral image pairs to reconstruct an isotropic volume from low-resolution axial
images. We evaluate our method on simulated and real anisotropic electron (EM)
and light microscopy (LM) data. Compared to diffusion-based baselines, niiv shows
improved reconstruction quality (+1 dB PSNR) and is over three orders of magnitude
faster (1,000x) to infer. Specifically, niiv reconstructs a 128^3 voxel volume
in 2/10th of a second, renderable at varying (continuous) high resolutions for
display. Our code is available at https://github.com/jakobtroidl/niiv-miccai.
acknowledgement: This work was supported by NIH grants 1U01NS132158 and R01HD104969.
We thank the reviewers for their constructive feedback.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jakob
full_name: Troidl, Jakob
last_name: Troidl
- first_name: Yiqing
full_name: Liang, Yiqing
last_name: Liang
- first_name: Johanna
full_name: Beyer, Johanna
last_name: Beyer
- first_name: Mojtaba
full_name: Tavakoli, Mojtaba
id: 3A0A06F4-F248-11E8-B48F-1D18A9856A87
last_name: Tavakoli
orcid: 0000-0002-7667-6854
- first_name: Johann G
full_name: Danzl, Johann G
id: 42EFD3B6-F248-11E8-B48F-1D18A9856A87
last_name: Danzl
orcid: 0000-0001-8559-3973
- first_name: Markus
full_name: Hadwiger, Markus
last_name: Hadwiger
- first_name: Hanspeter
full_name: Pfister, Hanspeter
last_name: Pfister
- first_name: James
full_name: Tompkin, James
last_name: Tompkin
citation:
ama: 'Troidl J, Liang Y, Beyer J, et al. niiv: Interactive Self-supervised Neural
Implicit Isotropic Volume Reconstruction. In: 1st International Workshop on
Efficient Medical Artificial Intelligence. Vol 16318. Springer Nature; 2026:257-267.
doi:10.1007/978-3-032-13961-0_26'
apa: 'Troidl, J., Liang, Y., Beyer, J., Tavakoli, M., Danzl, J. G., Hadwiger, M.,
… Tompkin, J. (2026). niiv: Interactive Self-supervised Neural Implicit Isotropic
Volume Reconstruction. In 1st International Workshop on Efficient Medical Artificial
Intelligence (Vol. 16318, pp. 257–267). Daejeon, South Korea: Springer Nature.
https://doi.org/10.1007/978-3-032-13961-0_26'
chicago: 'Troidl, Jakob, Yiqing Liang, Johanna Beyer, Mojtaba Tavakoli, Johann G
Danzl, Markus Hadwiger, Hanspeter Pfister, and James Tompkin. “Niiv: Interactive
Self-Supervised Neural Implicit Isotropic Volume Reconstruction.” In 1st International
Workshop on Efficient Medical Artificial Intelligence, 16318:257–67. Springer
Nature, 2026. https://doi.org/10.1007/978-3-032-13961-0_26.'
ieee: 'J. Troidl et al., “niiv: Interactive Self-supervised Neural Implicit
Isotropic Volume Reconstruction,” in 1st International Workshop on Efficient
Medical Artificial Intelligence, Daejeon, South Korea, 2026, vol. 16318, pp.
257–267.'
ista: 'Troidl J, Liang Y, Beyer J, Tavakoli M, Danzl JG, Hadwiger M, Pfister H,
Tompkin J. 2026. niiv: Interactive Self-supervised Neural Implicit Isotropic Volume
Reconstruction. 1st International Workshop on Efficient Medical Artificial Intelligence.
EMA4MICCAI: Efficient Medical Artificial Intelligence, LNCS, vol. 16318, 257–267.'
mla: 'Troidl, Jakob, et al. “Niiv: Interactive Self-Supervised Neural Implicit Isotropic
Volume Reconstruction.” 1st International Workshop on Efficient Medical Artificial
Intelligence, vol. 16318, Springer Nature, 2026, pp. 257–67, doi:10.1007/978-3-032-13961-0_26.'
short: J. Troidl, Y. Liang, J. Beyer, M. Tavakoli, J.G. Danzl, M. Hadwiger, H. Pfister,
J. Tompkin, in:, 1st International Workshop on Efficient Medical Artificial Intelligence,
Springer Nature, 2026, pp. 257–267.
conference:
end_date: 2025-09-23
location: Daejeon, South Korea
name: 'EMA4MICCAI: Efficient Medical Artificial Intelligence'
start_date: 2025-09-23
date_created: 2026-02-01T23:01:44Z
date_published: 2026-01-03T00:00:00Z
date_updated: 2026-02-16T08:50:50Z
day: '03'
department:
- _id: JoDa
doi: 10.1007/978-3-032-13961-0_26
intvolume: ' 16318'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1101/2024.09.07.611785
month: '01'
oa: 1
oa_version: Preprint
page: 257-267
publication: 1st International Workshop on Efficient Medical Artificial Intelligence
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032139603'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/jakobtroidl/niiv-miccai
scopus_import: '1'
status: public
title: 'niiv: Interactive Self-supervised Neural Implicit Isotropic Volume Reconstruction'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16318
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '21374'
abstract:
- lang: eng
text: "Let . S be a set of distinct points in general position in the\r\nEuclidean
plane. A plane Hamiltonian path on . S is a crossing-free geometric path such
that every point of .S is a vertex of the path. It is\r\nknown that, if. S is
sufficiently large, there exist three edge-disjoint plane\r\nHamiltonian paths
on . S. In this paper we study an edge-constrained\r\nversion of the problem of
finding Hamiltonian paths on a point set. We\r\nfirst consider the problem of
finding a single plane Hamiltonian path . π\r\nwith endpoints .s, t ∈ S and constraints
given by a segment . ab, where\r\n.a, b ∈ S. We consider the following scenarios:
(i) .ab ∈ π; (ii) .ab π. We\r\ncharacterize those quintuples . S, a, b, s, t for
which . π exists. Secondly,\r\nwe consider the problem of finding two plane Hamiltonian
paths . π1, π2\r\non a set . S with constraints given by a segment . ab, where
.a, b ∈ S. We\r\nconsider the following scenarios: (i) .π1 and .π2 share no edges
and .ab is\r\nan edge of . π1; (ii) .π1 and .π2 share no edges and none of them
includes\r\n.ab as an edge; (iii) both .π1 and .π2 include .ab as an edge and
share no\r\nother edges. In all cases, we characterize those triples . S, a, b
for which\r\n.π1 and .π2 exist."
acknowledgement: "We thank the organizers of the HOMONOLO 2024 workshop in Nová Louka,
Czech Republic, for the fruitful atmosphere where the research on this project was
initiated.\r\n\r\nT. Antić, A. Džuklevski, J. Kratochvíl and M. Saumell received
funding from GAČR grant 23–04949X, T.A and A.Dž were additionally supported by GAUK
grant SVV–2025–260822. G. Liotta was supported in part by MUR of Italy, PRIN Project
no. 2022TS4Y3N – EXPAND and PON Project ARS01_00540. J. Fiala was in part supported
by GAČR grant 25-16847S."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Todor
full_name: Antić, Todor
last_name: Antić
- first_name: Aleksa
full_name: Džuklevski, Aleksa
last_name: Džuklevski
- first_name: Jiří
full_name: Fiala, Jiří
last_name: Fiala
- first_name: Jan
full_name: Kratochvíl, Jan
last_name: Kratochvíl
- first_name: Giuseppe
full_name: Liotta, Giuseppe
last_name: Liotta
- first_name: Morteza
full_name: Saghafian, Morteza
id: f86f7148-b140-11ec-9577-95435b8df824
last_name: Saghafian
- first_name: Maria
full_name: Saumell, Maria
last_name: Saumell
- first_name: Johannes
full_name: Zink, Johannes
last_name: Zink
citation:
ama: 'Antić T, Džuklevski A, Fiala J, et al. Edge-constrained Hamiltonian paths
on a point set. In: 51st International Conference on Current Trends in Theory
and Practice of Computer Science. Vol 16448. Springer Nature; 2026:532-546.
doi:10.1007/978-3-032-17801-5_39'
apa: 'Antić, T., Džuklevski, A., Fiala, J., Kratochvíl, J., Liotta, G., Saghafian,
M., … Zink, J. (2026). Edge-constrained Hamiltonian paths on a point set. In 51st
International Conference on Current Trends in Theory and Practice of Computer
Science (Vol. 16448, pp. 532–546). Krakow, Poland: Springer Nature. https://doi.org/10.1007/978-3-032-17801-5_39'
chicago: Antić, Todor, Aleksa Džuklevski, Jiří Fiala, Jan Kratochvíl, Giuseppe Liotta,
Morteza Saghafian, Maria Saumell, and Johannes Zink. “Edge-Constrained Hamiltonian
Paths on a Point Set.” In 51st International Conference on Current Trends in
Theory and Practice of Computer Science, 16448:532–46. Springer Nature, 2026.
https://doi.org/10.1007/978-3-032-17801-5_39.
ieee: T. Antić et al., “Edge-constrained Hamiltonian paths on a point set,”
in 51st International Conference on Current Trends in Theory and Practice of
Computer Science, Krakow, Poland, 2026, vol. 16448, pp. 532–546.
ista: 'Antić T, Džuklevski A, Fiala J, Kratochvíl J, Liotta G, Saghafian M, Saumell
M, Zink J. 2026. Edge-constrained Hamiltonian paths on a point set. 51st International
Conference on Current Trends in Theory and Practice of Computer Science. SOFSEM:
Conference on Current Trends in Theory and Practice of Computer Science, LNCS,
vol. 16448, 532–546.'
mla: Antić, Todor, et al. “Edge-Constrained Hamiltonian Paths on a Point Set.” 51st
International Conference on Current Trends in Theory and Practice of Computer
Science, vol. 16448, Springer Nature, 2026, pp. 532–46, doi:10.1007/978-3-032-17801-5_39.
short: T. Antić, A. Džuklevski, J. Fiala, J. Kratochvíl, G. Liotta, M. Saghafian,
M. Saumell, J. Zink, in:, 51st International Conference on Current Trends in Theory
and Practice of Computer Science, Springer Nature, 2026, pp. 532–546.
conference:
end_date: 2026-02-13
location: Krakow, Poland
name: 'SOFSEM: Conference on Current Trends in Theory and Practice of Computer Science'
start_date: 2026-02-09
date_created: 2026-03-01T23:01:40Z
date_published: 2026-02-13T00:00:00Z
date_updated: 2026-03-02T08:49:20Z
day: '13'
department:
- _id: HeEd
doi: 10.1007/978-3-032-17801-5_39
external_id:
arxiv:
- '2511.22526'
intvolume: ' 16448'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2511.22526
month: '02'
oa: 1
oa_version: Preprint
page: 532-546
publication: 51st International Conference on Current Trends in Theory and Practice
of Computer Science
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032178008'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Edge-constrained Hamiltonian paths on a point set
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16448
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '21410'
abstract:
- lang: eng
text: Given a finite set of red and blue points in R^d, the MST-ratio is defined
as the total length of the Euclidean minimum spanning trees of the red points
and the blue points, divided by the length of the Euclidean minimum spanning tree
of their union. The MST-ratio has recently gained attention due to its direct
interpretation in topological models for studying point sets with applications
in spatial biology. The maximum MST-ratio of a point set is the maximum MST-ratio
over all proper colorings of its points by red and blue. We prove that finding
the maximum MST-ratio of a given point set is NP-hard when the dimension is part
of the input. Moreover, we present a quadratic-time 3-approximation algorithm
for this problem. As part of the proof, we show that in any metric space, the
maximum MST-ratio is smaller than 3. Furthermore, we study the average MST-ratio
over all colorings of a set of n points. We show that this average is always at
least n-2/n-1, and for n random points uniformly distributed in a d-dimensional
unit cube, the average tends to (math formular) in expectation as n approaches
infinity.
acknowledgement: "A. J. Ameli—Supported by the project COALESCE (ERC grant no. 853234).\r\nM.
Saghafian—Partially supported by the European Research Council (ERC), grant no.
788183, and by the Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z
342-N31."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Afrouz
full_name: Jabal Ameli, Afrouz
last_name: Jabal Ameli
- first_name: Faezeh
full_name: Motiei, Faezeh
last_name: Motiei
- first_name: Morteza
full_name: Saghafian, Morteza
id: f86f7148-b140-11ec-9577-95435b8df824
last_name: Saghafian
citation:
ama: 'Jabal Ameli A, Motiei F, Saghafian M. On the MST-ratio: Theoretical bounds
and complexity of finding the maximum. In: 20th International Conference and
Workshops on Algorithms and Computation. Vol 16444. Springer Nature; 2026:386-401.
doi:10.1007/978-981-95-7127-7_26'
apa: 'Jabal Ameli, A., Motiei, F., & Saghafian, M. (2026). On the MST-ratio:
Theoretical bounds and complexity of finding the maximum. In 20th International
Conference and Workshops on Algorithms and Computation (Vol. 16444, pp. 386–401).
Perugia, Italy: Springer Nature. https://doi.org/10.1007/978-981-95-7127-7_26'
chicago: 'Jabal Ameli, Afrouz, Faezeh Motiei, and Morteza Saghafian. “On the MST-Ratio:
Theoretical Bounds and Complexity of Finding the Maximum.” In 20th International
Conference and Workshops on Algorithms and Computation, 16444:386–401. Springer
Nature, 2026. https://doi.org/10.1007/978-981-95-7127-7_26.'
ieee: 'A. Jabal Ameli, F. Motiei, and M. Saghafian, “On the MST-ratio: Theoretical
bounds and complexity of finding the maximum,” in 20th International Conference
and Workshops on Algorithms and Computation, Perugia, Italy, 2026, vol. 16444,
pp. 386–401.'
ista: 'Jabal Ameli A, Motiei F, Saghafian M. 2026. On the MST-ratio: Theoretical
bounds and complexity of finding the maximum. 20th International Conference and
Workshops on Algorithms and Computation. WALCOM: International Conference and
Workshops on Algorithms and Computation, LNCS, vol. 16444, 386–401.'
mla: 'Jabal Ameli, Afrouz, et al. “On the MST-Ratio: Theoretical Bounds and Complexity
of Finding the Maximum.” 20th International Conference and Workshops on Algorithms
and Computation, vol. 16444, Springer Nature, 2026, pp. 386–401, doi:10.1007/978-981-95-7127-7_26.'
short: A. Jabal Ameli, F. Motiei, M. Saghafian, in:, 20th International Conference
and Workshops on Algorithms and Computation, Springer Nature, 2026, pp. 386–401.
conference:
end_date: 2026-03-06
location: Perugia, Italy
name: 'WALCOM: International Conference and Workshops on Algorithms and Computation'
start_date: 2026-03-04
date_created: 2026-03-08T23:01:45Z
date_published: 2026-02-14T00:00:00Z
date_updated: 2026-03-09T10:25:41Z
day: '14'
department:
- _id: HeEd
doi: 10.1007/978-981-95-7127-7_26
ec_funded: 1
external_id:
arxiv:
- '2409.11079'
intvolume: ' 16444'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2409.11079
month: '02'
oa: 1
oa_version: Preprint
page: 386-401
project:
- _id: 266A2E9E-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '788183'
name: Alpha Shape Theory Extended
- _id: 268116B8-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z00342
name: Mathematics, Computer Science
publication: 20th International Conference and Workshops on Algorithms and Computation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9789819571260'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'On the MST-ratio: Theoretical bounds and complexity of finding the maximum'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16444
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '21134'
abstract:
- lang: eng
text: "The Nakamoto consensus protocol underlying the Bitcoin blockchain uses proof
of work as a voting mechanism. Honest miners who contribute hashing power towards
securing the chain try to extend the longest chain they are aware of. Despite
its simplicity, Nakamoto consensus achieves meaningful security guarantees assuming
that at any point in time, a majority of the hashing power is controlled by honest
parties. This also holds under “resource variability”, i.e., if the total hashing
power varies greatly over time.\r\nProofs of space (PoSpace) have been suggested
as a more sustainable replacement for proofs of work. Unfortunately, no construction
of a “longest-chain” blockchain based on PoSpace, that is secure under dynamic
availability, is known. In this work, we prove that without additional assumptions
no such protocol exists. We exactly quantify this impossibility result by proving
a bound on the length of the fork required for double spending as a function of
the adversarial capabilities. This bound holds for any chain selection rule, and
we also show a chain selection rule (albeit a very strange one) that almost matches
this bound.\r\nThe Nakamoto consensus protocol underlying the Bitcoin blockchain
uses proof of work as a voting mechanism. Honest miners who contribute hashing
power towards securing the chain try to extend the longest chain they are aware
of. Despite its simplicity, Nakamoto consensus achieves meaningful security guarantees
assuming that at any point in time, a majority of the hashing power is controlled
by honest parties. This also holds under “resource variability”, i.e., if the
total hashing power varies greatly over time.\r\n\r\nProofs of space (PoSpace)
have been suggested as a more sustainable replacement for proofs of work. Unfortunately,
no construction of a “longest-chain” blockchain based on PoSpace, that is secure
under dynamic availability, is known. In this work, we prove that without additional
assumptions no such protocol exists. We exactly quantify this impossibility result
by proving a bound on the length of the fork required for double spending as a
function of the adversarial capabilities. This bound holds for any chain selection
rule, and we also show a chain selection rule (albeit a very strange one) that
almost matches this bound.\r\n\r\nConcretely, we consider a security game in which
the honest parties at any point control 0 > 1\r\n times more space than the adversary.
The adversary can change the honest space by a factor 1+- E with every block (dynamic
availability), and “replotting” the space (which allows answering two challenges
using the same space) takes as much time as p blocks.\r\nWe prove that no matter
what chain selection rule is used, in this game the adversary can create a fork
of length o^2 . p/E that will be picked as the winner by the chain selection rule.\r\nWe
also provide an upper bound that matches the lower bound up to a factor o. There
exists a chain selection rule (albeit a very strange one) which in the above game
requires forks of length at least o . p/E\r\nOur results show the necessity of
additional assumptions to create a secure PoSpace based longest-chain blockchain.
The Chia network in addition to PoSpace uses a verifiable delay function. Our
bounds show that an additional primitive like that is necessary."
acknowledgement: 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
arxiv: 1
author:
- first_name: Mirza Ahad
full_name: Baig, Mirza Ahad
id: 3EDE6DE4-AA5A-11E9-986D-341CE6697425
last_name: Baig
- 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: 'Baig MA, Pietrzak KZ. On the (in)security of Proofs-of-space based longest-chain
blockchains. In: 29th International Conference on Financial Cryptography and
Data Security. Vol 15752. Springer Nature; 2026:127-142. doi:10.1007/978-3-032-07035-7_8'
apa: 'Baig, M. A., & Pietrzak, K. Z. (2026). On the (in)security of Proofs-of-space
based longest-chain blockchains. In 29th International Conference on Financial
Cryptography and Data Security (Vol. 15752, pp. 127–142). Miyakojima, Japan:
Springer Nature. https://doi.org/10.1007/978-3-032-07035-7_8'
chicago: Baig, Mirza Ahad, and Krzysztof Z Pietrzak. “On the (in)Security of Proofs-of-Space
Based Longest-Chain Blockchains.” In 29th International Conference on Financial
Cryptography and Data Security, 15752:127–42. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-07035-7_8.
ieee: M. A. Baig and K. Z. Pietrzak, “On the (in)security of Proofs-of-space based
longest-chain blockchains,” in 29th International Conference on Financial Cryptography
and Data Security, Miyakojima, Japan, 2026, vol. 15752, pp. 127–142.
ista: 'Baig MA, Pietrzak KZ. 2026. On the (in)security of Proofs-of-space based
longest-chain blockchains. 29th International Conference on Financial Cryptography
and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 15752,
127–142.'
mla: Baig, Mirza Ahad, and Krzysztof Z. Pietrzak. “On the (in)Security of Proofs-of-Space
Based Longest-Chain Blockchains.” 29th International Conference on Financial
Cryptography and Data Security, vol. 15752, Springer Nature, 2026, pp. 127–42,
doi:10.1007/978-3-032-07035-7_8.
short: M.A. Baig, K.Z. Pietrzak, in:, 29th International Conference on Financial
Cryptography and Data Security, Springer Nature, 2026, pp. 127–142.
conference:
end_date: 2025-04-18
location: Miyakojima, Japan
name: 'FC: Financial Cryptography and Data Security'
start_date: 2025-04-14
corr_author: '1'
date_created: 2026-02-01T23:01:43Z
date_published: 2026-01-01T00:00:00Z
date_updated: 2026-04-15T08:45:18Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-032-07035-7_8
external_id:
arxiv:
- '2505.14891'
intvolume: ' 15752'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2505.14891
month: '01'
oa: 1
oa_version: Preprint
page: 127-142
project:
- _id: 34a34d57-11ca-11ed-8bc3-a2688a8724e1
grant_number: F8509
name: Security and Privacy by Design for Complex Systems
publication: 29th International Conference on Financial Cryptography and Data Security
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032070340'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '21651'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: On the (in)security of Proofs-of-space based longest-chain blockchains
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15752
year: '2026'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20189'
abstract:
- lang: eng
text: Certification was made mandatory for the first time in the latest hardware
model checking competition. In this case study, we investigate the trade-offs
of requiring certificates for both passing and failing properties in the competition.
Our evaluation shows that participating model checkers were able to produce compact,
correct certificates that could be verified with minimal overhead. Furthermore,
the certifying winner of the competition outperforms the previous non-certifying
state-of-the-art model checker, demonstrating that certification can be adopted
without compromising model checking efficiency.
acknowledgement: "This work is supported in part by the ERC-2020-AdG 101020093, the
LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland
under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of
course also owe a big thank-you to the submitters of model checkers and benchmarks
to the competition over all these years. Without their enthusiasm and support neither
the competition nor this study would exist."
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
- first_name: Mathias
full_name: Preiner, Mathias
last_name: Preiner
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
- first_name: Keijo
full_name: Heljanko, Keijo
last_name: Heljanko
citation:
ama: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates
to the hardware model checking competition. In: 37th International Conference
on Computer Aided Verification. Vol 15931. Springer Nature; 2025:281-295.
doi:10.1007/978-3-031-98668-0_14'
apa: 'Froleyks, N., Yu, E., Preiner, M., Biere, A., & Heljanko, K. (2025). Introducing
certificates to the hardware model checking competition. In 37th International
Conference on Computer Aided Verification (Vol. 15931, pp. 281–295). Zagreb,
Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98668-0_14'
chicago: Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko.
“Introducing Certificates to the Hardware Model Checking Competition.” In 37th
International Conference on Computer Aided Verification, 15931:281–95. Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-98668-0_14.
ieee: N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates
to the hardware model checking competition,” in 37th International Conference
on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.
ista: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates
to the hardware model checking competition. 37th International Conference on Computer
Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.'
mla: Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking
Competition.” 37th International Conference on Computer Aided Verification,
vol. 15931, Springer Nature, 2025, pp. 281–95, doi:10.1007/978-3-031-98668-0_14.
short: N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International
Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.
conference:
end_date: 2025-07-25
location: Zagreb, Croatia
name: 'CAV: Computer Aided Verification'
start_date: 2025-07-23
date_created: 2025-08-17T22:01:36Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2025-12-01T12:34:05Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98668-0_14
ec_funded: 1
external_id:
isi:
- '001562507100014'
file:
- access_level: open_access
checksum: 15ec1bc9b9409d3b2736f4c9d5f42fd1
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T05:46:10Z
date_updated: 2025-09-02T05:46:10Z
file_id: '20266'
file_name: 2025_CAV_Froleyks.pdf
file_size: 1078274
relation: main_file
success: 1
file_date_updated: 2025-09-02T05:46:10Z
has_accepted_license: '1'
intvolume: ' 15931'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 281-295
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031986673'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Introducing certificates to the hardware model checking competition
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15931
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20225'
abstract:
- lang: eng
text: "We present the first supermartingale certificate for quantitative \r\n-regular
properties of discrete-time infinite-state stochastic systems. Our certificate
is defined on the product of the stochastic system and a limit-deterministic Büchi
automaton that specifies the property of interest; hence we call it a limit-deterministic
Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied
only to quantitative reachability, safety, or reach-avoid properties, and to qualitative
(i.e., probability 1) \r\n-regular properties.We also present fully automated
algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic
system dynamics and the controller can be represented in terms of polynomial inequalities.
Our experiments demonstrate the ability of our method to solve verification and
control tasks for stochastic systems that were beyond the reach of previous supermartingale-based
approaches."
acknowledgement: This work was supported in part by the Singapore Ministry of Education
(MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SIS-SMU-100) and
the ERC project ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Pouya
full_name: Sadeghi, Pouya
last_name: Sadeghi
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Henzinger TA, Mallik K, Sadeghi P, Zikelic D. Supermartingale certificates
for quantitative omega-regular verification and control. In: 37th International
Conference on Computer Aided Verification. Vol 15932. Springer Nature; 2025:29-55.
doi:10.1007/978-3-031-98679-6_2'
apa: 'Henzinger, T. A., Mallik, K., Sadeghi, P., & Zikelic, D. (2025). Supermartingale
certificates for quantitative omega-regular verification and control. In 37th
International Conference on Computer Aided Verification (Vol. 15932, pp. 29–55).
Zagreb, Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98679-6_2'
chicago: Henzinger, Thomas A, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic.
“Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.”
In 37th International Conference on Computer Aided Verification, 15932:29–55.
Springer Nature, 2025. https://doi.org/10.1007/978-3-031-98679-6_2.
ieee: T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates
for quantitative omega-regular verification and control,” in 37th International
Conference on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15932,
pp. 29–55.
ista: 'Henzinger TA, Mallik K, Sadeghi P, Zikelic D. 2025. Supermartingale certificates
for quantitative omega-regular verification and control. 37th International Conference
on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15932,
29–55.'
mla: Henzinger, Thomas A., et al. “Supermartingale Certificates for Quantitative
Omega-Regular Verification and Control.” 37th International Conference on Computer
Aided Verification, vol. 15932, Springer Nature, 2025, pp. 29–55, doi:10.1007/978-3-031-98679-6_2.
short: T.A. Henzinger, K. Mallik, P. Sadeghi, D. Zikelic, in:, 37th International
Conference on Computer Aided Verification, Springer Nature, 2025, pp. 29–55.
conference:
end_date: 2025-07-25
location: Zagreb, Croatia
name: 'CAV: Computer Aided Verification'
start_date: 2025-07-23
date_created: 2025-08-24T22:01:31Z
date_published: 2025-07-22T00:00:00Z
date_updated: 2025-12-01T12:34:41Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98679-6_2
ec_funded: 1
external_id:
arxiv:
- '2505.18833'
isi:
- '001562506600002'
file:
- access_level: open_access
checksum: beb1e2637de5b2268cc2262119439113
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T07:34:33Z
date_updated: 2025-09-02T07:34:33Z
file_id: '20272'
file_name: 2025_CAV_HenzingerT.pdf
file_size: 884831
relation: main_file
success: 1
file_date_updated: 2025-09-02T07:34:33Z
has_accepted_license: '1'
intvolume: ' 15932'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 29-55
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031986789'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Supermartingale certificates for quantitative omega-regular verification and control
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15932
year: '2025'
...
---
_id: '20610'
abstract:
- lang: eng
text: "Markov decision processes (MDPs) are a fundamental model of decision making
which exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally,
verification assumes exact knowledge of the probabilities that govern the behaviour
of an MDP. However, this assumption often is unrealistic, e.g. when modelling
cyber-physical systems or biological processes. There, we can employ statistical
model checking (SMC) to obtain an estimate of the MDP’s value (e.g. the maximal
probability of reaching a goal state) that is close to the true value with high
confidence (probably approximately correct). Model-based SMC algorithms sample
the MDP and build a model of it by estimating all transition probabilities, essentially
for every transition answering the question: “What are the odds?” However, so
far the statistical methods employed by state-of-the-art SMC verification algorithms
are quite naive or even compromise the correctness guarantees.\r\n\r\nOur first
contribution is to survey, categorize, and analyse statistical methods, identifying
those few that are most efficient and that provide suitable guarantees for the
verification setting. Secondly, we propose improvements that exploit structural
knowledge of the MDP. Both contributions generalize to many types of problem statements
as they are largely independent of the setting. Moreover, our experimental evaluation
shows that they lead to significant gains, reducing the number of samples that
an SMC algorithm has to collect by up to two orders of magnitude."
acknowledgement: This work was supported by the European Union’s Horizon 2020 research
and innovation programme under the Marie Sklodowska-Curie grant agreement No 10103441,
the ERC Starting Grant DEUCE (101077178) and the DFG through the Cluster of Excellence
EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy)
and the DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
- first_name: Patrick
full_name: Wienhöft, Patrick
last_name: Wienhöft
citation:
ama: 'Meggendorfer T, Weininger M, Wienhöft P. What are the odds? Improving statistical
model checking of Markov decision processes. In: Second International Joint
Conference on QEST+FORMATS. Vol 16143. Springer Nature; 2025:195-218. doi:10.1007/978-3-032-05792-1_11'
apa: 'Meggendorfer, T., Weininger, M., & Wienhöft, P. (2025). What are the odds?
Improving statistical model checking of Markov decision processes. In Second
International Joint Conference on QEST+FORMATS (Vol. 16143, pp. 195–218).
Aarhus, Denmark: Springer Nature. https://doi.org/10.1007/978-3-032-05792-1_11'
chicago: Meggendorfer, Tobias, Maximilian Weininger, and Patrick Wienhöft. “What
Are the Odds? Improving Statistical Model Checking of Markov Decision Processes.”
In Second International Joint Conference on QEST+FORMATS, 16143:195–218.
Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05792-1_11.
ieee: T. Meggendorfer, M. Weininger, and P. Wienhöft, “What are the odds? Improving
statistical model checking of Markov decision processes,” in Second International
Joint Conference on QEST+FORMATS, Aarhus, Denmark, 2025, vol. 16143, pp. 195–218.
ista: 'Meggendorfer T, Weininger M, Wienhöft P. 2025. What are the odds? Improving
statistical model checking of Markov decision processes. Second International
Joint Conference on QEST+FORMATS. QEST-FORMATS: International Conference on Quantitative
Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, LNCS,
vol. 16143, 195–218.'
mla: Meggendorfer, Tobias, et al. “What Are the Odds? Improving Statistical Model
Checking of Markov Decision Processes.” Second International Joint Conference
on QEST+FORMATS, vol. 16143, Springer Nature, 2025, pp. 195–218, doi:10.1007/978-3-032-05792-1_11.
short: T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Second International Joint
Conference on QEST+FORMATS, Springer Nature, 2025, pp. 195–218.
conference:
end_date: 2025-08-28
location: Aarhus, Denmark
name: 'QEST-FORMATS: International Conference on Quantitative Evaluation of Systems
and Formal Modeling and Analysis of Timed Systems'
start_date: 2025-08-26
date_created: 2025-11-09T23:01:34Z
date_published: 2025-10-02T00:00:00Z
date_updated: 2025-11-10T08:06:27Z
day: '02'
department:
- _id: KrCh
doi: 10.1007/978-3-032-05792-1_11
ec_funded: 1
intvolume: ' 16143'
language:
- iso: eng
month: '10'
oa_version: None
page: 195-218
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Second International Joint Conference on QEST+FORMATS
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032057914'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: What are the odds? Improving statistical model checking of Markov decision
processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16143
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20648'
abstract:
- lang: eng
text: Polynomial quantified entailments with existentially and universally quantified
variables arise in many problems of verification and program analysis. We present
PolyQEnt which is a tool for solving polynomial quantified entailments in which
variables on both sides of the implication are real valued or unbounded integers.
Our tool provides a unified framework for polynomial quantified entailment problems
that arise in several papers in the literature. Our experimental evaluation over
a wide range of benchmarks shows the applicability of the tool as well as its
benefits as opposed to simply using existing SMT solvers to solve such constraints.
acknowledgement: 'This work was supported by the following grants: ERC CoG 863818
(ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, ERC StG 101222524 (SPES),
the Ethereum Foundation Research Grant FY24-1793, and the Singapore Ministry of
Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SISSMU-100).'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
orcid: 0009-0007-5253-9170
- first_name: Milad
full_name: Saadat, Milad
last_name: Saadat
- first_name: Maximilian
full_name: Seeliger, Maximilian
last_name: Seeliger
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady AK, Goharshady E, et al. PolyQEnt: A polynomial quantified
entailment solver. In: 23rd International Symposium on Automated Technology
for Verification and Analysis. Vol 16145. Springer Nature; 2025:411-424. doi:10.1007/978-3-032-08707-2_19'
apa: 'Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., Saadat, M.,
Seeliger, M., & Zikelic, D. (2025). PolyQEnt: A polynomial quantified entailment
solver. In 23rd International Symposium on Automated Technology for Verification
and Analysis (Vol. 16145, pp. 411–424). Bengaluru, India: Springer Nature.
https://doi.org/10.1007/978-3-032-08707-2_19'
chicago: 'Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad
Karrabi, Milad Saadat, Maximilian Seeliger, and Dorde Zikelic. “PolyQEnt: A Polynomial
Quantified Entailment Solver.” In 23rd International Symposium on Automated
Technology for Verification and Analysis, 16145:411–24. Springer Nature, 2025.
https://doi.org/10.1007/978-3-032-08707-2_19.'
ieee: 'K. Chatterjee et al., “PolyQEnt: A polynomial quantified entailment
solver,” in 23rd International Symposium on Automated Technology for Verification
and Analysis, Bengaluru, India, 2025, vol. 16145, pp. 411–424.'
ista: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger
M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd
International Symposium on Automated Technology for Verification and Analysis.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424.'
mla: 'Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment
Solver.” 23rd International Symposium on Automated Technology for Verification
and Analysis, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:10.1007/978-3-032-08707-2_19.'
short: K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, M. Saadat, M.
Seeliger, D. Zikelic, in:, 23rd International Symposium on Automated Technology
for Verification and Analysis, Springer Nature, 2025, pp. 411–424.
conference:
end_date: 2025-10-31
location: Bengaluru, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2025-10-27
corr_author: '1'
date_created: 2025-11-16T23:01:24Z
date_published: 2025-10-26T00:00:00Z
date_updated: 2025-11-24T13:11:10Z
day: '26'
department:
- _id: KrCh
doi: 10.1007/978-3-032-08707-2_19
ec_funded: 1
external_id:
arxiv:
- '2408.03796'
intvolume: ' 16145'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2408.03796
month: '10'
oa: 1
oa_version: Preprint
page: 411-424
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 23rd International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032087065'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'PolyQEnt: A polynomial quantified entailment solver'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16145
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20658'
abstract:
- lang: eng
text: The medial axis of a smoothly embedded surface in R^3 consists of all points
for which the Euclidean distance function on the surface has at least two global
minima. We generalize this notion to the mid-sphere axis, which consists of all
points for which the Euclidean distance function has two interchanging saddles
that swap their partners in the pairing by persistent homology. It offers a discrete-algebraic
multi-scale approach to computing ridge-like structures on the surface. As a proof
of concept, an algorithm that computes stair-case approximations of the mid-sphere
axis is provided.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Elizabeth R
full_name: Stephenson, Elizabeth R
id: 2D04F932-F248-11E8-B48F-1D18A9856A87
last_name: Stephenson
orcid: 0000-0002-6862-208X
- first_name: Martin H
full_name: Thoresen, Martin H
id: 47CB1472-F248-11E8-B48F-1D18A9856A87
last_name: Thoresen
citation:
ama: 'Edelsbrunner H, Stephenson ER, Thoresen MH. The mid-sphere cousin of the medial
axis transform. In: 4th International Joint Conference on Discrete Geometry
and Mathematical Morphology. Vol 16296. Springer Nature; 2025:133-147. doi:10.1007/978-3-032-09544-2_10'
apa: 'Edelsbrunner, H., Stephenson, E. R., & Thoresen, M. H. (2025). The mid-sphere
cousin of the medial axis transform. In 4th International Joint Conference
on Discrete Geometry and Mathematical Morphology (Vol. 16296, pp. 133–147).
Groningen, The Netherlands: Springer Nature. https://doi.org/10.1007/978-3-032-09544-2_10'
chicago: Edelsbrunner, Herbert, Elizabeth R Stephenson, and Martin H Thoresen. “The
Mid-Sphere Cousin of the Medial Axis Transform.” In 4th International Joint
Conference on Discrete Geometry and Mathematical Morphology, 16296:133–47.
Springer Nature, 2025. https://doi.org/10.1007/978-3-032-09544-2_10.
ieee: H. Edelsbrunner, E. R. Stephenson, and M. H. Thoresen, “The mid-sphere cousin
of the medial axis transform,” in 4th International Joint Conference on Discrete
Geometry and Mathematical Morphology, Groningen, The Netherlands, 2025, vol.
16296, pp. 133–147.
ista: 'Edelsbrunner H, Stephenson ER, Thoresen MH. 2025. The mid-sphere cousin of the medial
axis transform. 4th International Joint Conference on Discrete Geometry and Mathematical
Morphology. DGMM: Discrete Geometry and Mathematical Morphology, LNCS, vol. 16296,
133–147.'
mla: Edelsbrunner, Herbert, et al. “The Mid-Sphere Cousin of the Medial Axis Transform.”
4th International Joint Conference on Discrete Geometry and Mathematical Morphology,
vol. 16296, Springer Nature, 2025, pp. 133–47, doi:10.1007/978-3-032-09544-2_10.
short: H. Edelsbrunner, E.R. Stephenson, M.H. Thoresen, in:, 4th International Joint
Conference on Discrete Geometry and Mathematical Morphology, Springer Nature,
2025, pp. 133–147.
conference:
end_date: 2025-11-06
location: Groningen, The Netherlands
name: 'DGMM: Discrete Geometry and Mathematical Morphology'
start_date: 2025-11-03
date_created: 2025-11-23T23:01:37Z
date_published: 2025-11-01T00:00:00Z
date_updated: 2025-11-24T10:05:11Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-032-09544-2_10
external_id:
arxiv:
- '2504.14743'
intvolume: ' 16296'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2504.14743
month: '11'
oa: 1
oa_version: Preprint
page: 133-147
publication: 4th International Joint Conference on Discrete Geometry and Mathematical
Morphology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032095435'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: The mid-sphere cousin of the medial axis transform
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16296
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20723'
abstract:
- lang: eng
text: Information-flow interfaces is a formalism recently proposed for specifying,
composing, and refining system-wide security requirements. In this work, we show
how the widely used concept of security lattices provides a natural semantic interpretation
for information-flow interfaces.
acknowledgement: This project was funded in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe F8502 and by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-Flow
Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber
Physical Systems. Vol 15471. Cham: Springer Nature; 2025:251-263. doi:10.1007/978-3-031-97537-0_15'
apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A.
(2025). Information-Flow Interfaces and Security Lattices. In Engineering Safe
and Trustworthy Cyber Physical Systems (Vol. 15471, pp. 251–263). Cham: Springer
Nature. https://doi.org/10.1007/978-3-031-97537-0_15'
chicago: 'Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
Costa. “Information-Flow Interfaces and Security Lattices.” In Engineering
Safe and Trustworthy Cyber Physical Systems, 15471:251–63. Cham: Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-97537-0_15.'
ieee: 'E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-Flow
Interfaces and Security Lattices,” in Engineering Safe and Trustworthy Cyber
Physical Systems, vol. 15471, Cham: Springer Nature, 2025, pp. 251–263.'
ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.Information-Flow
Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber Physical
Systems. LNCS, vol. 15471, 251–263.'
mla: Bartocci, Ezio, et al. “Information-Flow Interfaces and Security Lattices.”
Engineering Safe and Trustworthy Cyber Physical Systems, vol. 15471, Springer
Nature, 2025, pp. 251–63, doi:10.1007/978-3-031-97537-0_15.
short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, Engineering
Safe and Trustworthy Cyber Physical Systems, Springer Nature, Cham, 2025, pp.
251–263.
corr_author: '1'
date_created: 2025-12-01T15:44:58Z
date_published: 2025-10-02T00:00:00Z
date_updated: 2025-12-09T07:57:55Z
day: '02'
department:
- _id: ToHe
doi: 10.1007/978-3-031-97537-0_15
ec_funded: 1
external_id:
arxiv:
- '2406.14374'
intvolume: ' 15471'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2406.14374
month: '10'
oa: 1
oa_version: Preprint
page: 251-263
place: Cham
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Engineering Safe and Trustworthy Cyber Physical Systems
publication_identifier:
eisbn:
- '9783031975370'
eissn:
- 1611-3349
isbn:
- '9783031975363'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Information-Flow Interfaces and Security Lattices
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15471
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19375'
abstract:
- lang: eng
text: "Despite the advances in probabilistic model checking, the scalability of
the verification methods remains limited. In particular, the state space often
becomes extremely large when instantiating parameterized Markov decision processes
(MDPs) even with moderate values. Synthesizing policies for such huge MDPs is
beyond the reach of available tools. We propose a learning-based approach to obtain
a reasonable policy for such huge MDPs.\r\n\r\nThe idea is to generalize optimal
policies obtained by model-checking small instances to larger ones using decision-tree
learning. Consequently, our method bypasses the need for explicit state-space
exploration of large models, providing a practical solution to the state-space
explosion problem. We demonstrate the efficacy of our approach by performing extensive
experimentation on the relevant models from the quantitative verification benchmark
set. The experimental results indicate that our policies perform well, even when
the size of the model is orders of magnitude beyond the reach of state-of-the-art
analysis tools."
acknowledgement: This research was funded in part by the DFG project 427755713 GOPro,
the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021)
of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement
101034413 (IST-BRIDGE).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Muqsit
full_name: Azeem, Muqsit
last_name: Azeem
- first_name: Debraj
full_name: Chakraborty, Debraj
last_name: Chakraborty
- first_name: Sudeep
full_name: Kanav, Sudeep
last_name: Kanav
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Mohammadsadegh
full_name: Mohagheghi, Mohammadsadegh
last_name: Mohagheghi
- first_name: Stefanie
full_name: Mohr, Stefanie
last_name: Mohr
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
citation:
ama: 'Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized
Markov decision processes via decision-tree learning and generalization. In: 26th
International Conference on Verification, Model Checking, and Abstract Interpretation.
Vol 15530. Springer Nature; 2025:97-120. doi:10.1007/978-3-031-82703-7_5'
apa: 'Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr,
S., & Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov
decision processes via decision-tree learning and generalization. In 26th International
Conference on Verification, Model Checking, and Abstract Interpretation (Vol.
15530, pp. 97–120). Denver, CO, United States: Springer Nature. https://doi.org/10.1007/978-3-031-82703-7_5'
chicago: Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh
Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis
for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.”
In 26th International Conference on Verification, Model Checking, and Abstract
Interpretation, 15530:97–120. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-82703-7_5.
ieee: M. Azeem et al., “1–2–3–Go! Policy synthesis for parameterized Markov
decision processes via decision-tree learning and generalization,” in 26th
International Conference on Verification, Model Checking, and Abstract Interpretation,
Denver, CO, United States, 2025, vol. 15530, pp. 97–120.
ista: 'Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger
M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes
via decision-tree learning and generalization. 26th International Conference on
Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification,
Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.'
mla: Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov
Decision Processes via Decision-Tree Learning and Generalization.” 26th International
Conference on Verification, Model Checking, and Abstract Interpretation, vol.
15530, Springer Nature, 2025, pp. 97–120, doi:10.1007/978-3-031-82703-7_5.
short: M. Azeem, D. Chakraborty, S. Kanav, J. Kretinsky, M. Mohagheghi, S. Mohr,
M. Weininger, in:, 26th International Conference on Verification, Model Checking,
and Abstract Interpretation, Springer Nature, 2025, pp. 97–120.
conference:
end_date: 2025-01-21
location: Denver, CO, United States
name: 'VMCAI: Verification, Model Checking, and Abstract Interpretation'
start_date: 2025-01-20
date_created: 2025-03-09T23:01:29Z
date_published: 2025-01-23T00:00:00Z
date_updated: 2025-09-30T10:46:54Z
day: '23'
department:
- _id: KrCh
doi: 10.1007/978-3-031-82703-7_5
ec_funded: 1
external_id:
arxiv:
- '2410.18293'
isi:
- '001446577100005'
intvolume: ' 15530'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2410.18293
month: '01'
oa: 1
oa_version: Preprint
page: 97-120
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 26th International Conference on Verification, Model Checking, and Abstract
Interpretation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031827020'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree
learning and generalization
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15530
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19445'
abstract:
- lang: eng
text: "In reconfiguration, we are given two solutions to a graph problem, such as
Vertex Cover or Dominating Set, with each solution represented by a placement
of tokens on vertices of the graph. Our task is to reconfigure one into the other
using small steps while ensuring the intermediate configurations of tokens are
also valid solutions. The two commonly studied settings are Token Jumping and
Token Sliding, which allows moving a single token to an arbitrary or an adjacent
vertex, respectively.\r\n\r\nWe introduce new rules that generalize Token Jumping,
parameterized by the number of tokens allowed to move at once and by the maximum
distance of each move. Our main contribution is identifying minimal rules that
allow reconfiguring any possible given solution into any other for Independent
Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide
an efficient algorithm that finds a corresponding reconfiguration sequence.\r\n\r\nWe
further focus on the rule that allows each token to move to an adjacent vertex
in a single step. This natural variant turns out to be the minimal rule that guarantees
reconfigurability for Vertex Cover. We determine the computational complexity
of deciding whether a (shortest) reconfiguration sequence exists under this rule
for the three studied problems. While reachability for Vertex Cover is shown to
be in P, finding a shortest sequence is shown to be NP-complete. For Independent
Set and Dominating Set, even reachability is shown to be PSPACE-complete."
acknowledgement: J. M. Křišťan acknowledges the support of the Czech Science Foundation
Grant No. 24-12046S. This work was supported by the Grant Agency of the Czech Technical
University in Prague, grant No. SGS23/205/OHK3/3T/18. J. Svoboda acknowledges the
support of the ERC CoG 863818 (ForM-SMArt) grant.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Jan Matyáš
full_name: Křišťan, Jan Matyáš
last_name: Křišťan
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Křišťan JM, Svoboda J. Reconfiguration using generalized token jumping. In:
19th International Conference and Workshops on Algorithms and Computation.
Vol 15411. Springer Nature; 2025:244-265. doi:10.1007/978-981-96-2845-2_16'
apa: 'Křišťan, J. M., & Svoboda, J. (2025). Reconfiguration using generalized
token jumping. In 19th International Conference and Workshops on Algorithms
and Computation (Vol. 15411, pp. 244–265). Chengdu, China: Springer Nature.
https://doi.org/10.1007/978-981-96-2845-2_16'
chicago: Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized
Token Jumping.” In 19th International Conference and Workshops on Algorithms
and Computation, 15411:244–65. Springer Nature, 2025. https://doi.org/10.1007/978-981-96-2845-2_16.
ieee: J. M. Křišťan and J. Svoboda, “Reconfiguration using generalized token jumping,”
in 19th International Conference and Workshops on Algorithms and Computation,
Chengdu, China, 2025, vol. 15411, pp. 244–265.
ista: 'Křišťan JM, Svoboda J. 2025. Reconfiguration using generalized token jumping.
19th International Conference and Workshops on Algorithms and Computation. WALCOM:
International Conference and Workshops on Algorithms and Computation, LNCS, vol.
15411, 244–265.'
mla: Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized
Token Jumping.” 19th International Conference and Workshops on Algorithms and
Computation, vol. 15411, Springer Nature, 2025, pp. 244–65, doi:10.1007/978-981-96-2845-2_16.
short: J.M. Křišťan, J. Svoboda, in:, 19th International Conference and Workshops
on Algorithms and Computation, Springer Nature, 2025, pp. 244–265.
conference:
end_date: 2025-03-02
location: Chengdu, China
name: 'WALCOM: International Conference and Workshops on Algorithms and Computation'
start_date: 2025-02-28
date_created: 2025-03-23T23:01:27Z
date_published: 2025-02-20T00:00:00Z
date_updated: 2025-09-30T11:14:33Z
day: '20'
department:
- _id: KrCh
doi: 10.1007/978-981-96-2845-2_16
ec_funded: 1
external_id:
arxiv:
- '2411.12582'
isi:
- '001537885900016'
intvolume: ' 15411'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2411.12582
month: '02'
oa: 1
oa_version: Preprint
page: 244-265
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 19th International Conference and Workshops on Algorithms and Computation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9789819628445'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reconfiguration using generalized token jumping
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15411
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19600'
abstract:
- lang: eng
text: In this work, we explore route discovery in private payment channel networks.
We first determine what “ideal" privacy for a routing protocol means in this setting.
We observe that protocols achieving this strong privacy definition exist by leveraging
Multi-Party Computation but they are inherently inefficient as they must involve
the entire network. We then present protocols with weaker privacy guarantees but
much better efficiency (involving only a small fraction of the nodes). The core
idea is that both sender and receiver gossip a message which propagates through
the network, and the moment any node in the network receives both messages, a
path is found. In our first protocol the message is always sent to all neighbouring
nodes with a delay proportional to the fees of that edge. In our second protocol
the message is only sent to one neighbour chosen randomly with a probability proportional
to its degree. We additionally propose a more realistic notion of privacy in order
to measure the privacy leakage of our protocols in practice. Our realistic notion
of privacy challenges an adversary that join the network with a fixed budget to
create channels to guess the sender and receiver of a transaction upon receiving
messages from our protocols. Simulations of our protocols on the Lightning network
topology (for random transactions and uniform fees) show that 1) forming edges
with high degree nodes is a more effective attack strategy for the adversary,
2) there is a tradeoff between the number of nodes involved in our protocols (privacy)
and the optimality of the discovered path, and 3) our protocols involve a very
small fraction of the network on average.
acknowledgement: This work was supported in part by the ERC CoG 863818 (ForM-SMArt),
Austrian Science Fund (FWF) 10.55776/COE12, and MOE-T2EP20122-0014 (Data-Driven
Distributed Algorithms) grants.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Zeta
full_name: Avarikioti, Zeta
last_name: Avarikioti
- first_name: Mahsa
full_name: Bastankhah, Mahsa
last_name: Bastankhah
- first_name: Mohammad Ali
full_name: Maddah-Ali, Mohammad Ali
last_name: Maddah-Ali
- 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: 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: 'Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX.
Route discovery in private payment channel networks. In: Computer Security.
ESORICS 2024 International Workshops. Vol 15263. Springer Nature; 2025:207-223.
doi:10.1007/978-3-031-82349-7_15'
apa: 'Avarikioti, Z., Bastankhah, M., Maddah-Ali, M. A., Pietrzak, K. Z., Svoboda,
J., & Yeo, M. X. (2025). Route discovery in private payment channel networks.
In Computer Security. ESORICS 2024 International Workshops (Vol. 15263,
pp. 207–223). Bydgoszcz, Poland: Springer Nature. https://doi.org/10.1007/978-3-031-82349-7_15'
chicago: Avarikioti, Zeta, Mahsa Bastankhah, Mohammad Ali Maddah-Ali, Krzysztof
Z Pietrzak, Jakub Svoboda, and Michelle X Yeo. “Route Discovery in Private Payment
Channel Networks.” In Computer Security. ESORICS 2024 International Workshops,
15263:207–23. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-82349-7_15.
ieee: Z. Avarikioti, M. Bastankhah, M. A. Maddah-Ali, K. Z. Pietrzak, J. Svoboda,
and M. X. Yeo, “Route discovery in private payment channel networks,” in Computer
Security. ESORICS 2024 International Workshops, Bydgoszcz, Poland, 2025, vol.
15263, pp. 207–223.
ista: 'Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX.
2025. Route discovery in private payment channel networks. Computer Security.
ESORICS 2024 International Workshops. ESORICS: European Symposium on Research
in Computer Security, LNCS, vol. 15263, 207–223.'
mla: Avarikioti, Zeta, et al. “Route Discovery in Private Payment Channel Networks.”
Computer Security. ESORICS 2024 International Workshops, vol. 15263, Springer
Nature, 2025, pp. 207–23, doi:10.1007/978-3-031-82349-7_15.
short: Z. Avarikioti, M. Bastankhah, M.A. Maddah-Ali, K.Z. Pietrzak, J. Svoboda,
M.X. Yeo, in:, Computer Security. ESORICS 2024 International Workshops, Springer
Nature, 2025, pp. 207–223.
conference:
end_date: 2024-09-20
location: Bydgoszcz, Poland
name: 'ESORICS: European Symposium on Research in Computer Security'
start_date: 2024-09-16
date_created: 2025-04-20T22:01:28Z
date_published: 2025-04-01T00:00:00Z
date_updated: 2025-11-05T07:52:35Z
day: '01'
department:
- _id: KrPi
- _id: KrCh
doi: 10.1007/978-3-031-82349-7_15
ec_funded: 1
intvolume: ' 15263'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2021/1539
month: '04'
oa: 1
oa_version: Submitted Version
page: 207-223
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Computer Security. ESORICS 2024 International Workshops
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031823480'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Route discovery in private payment channel networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15263
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19712'
abstract:
- lang: eng
text: "We study recent algebraic attacks (Briaud-Øygarden EC’23) on the Regular
Syndrome Decoding (RSD) problem and the assumptions underlying the correctness
of their attacks’ complexity estimates. By relating these assumptions to interesting
algebraic-combinatorial problems, we prove that they do not hold in full generality.
However, we show that they are (asymptotically) true for most parameter sets,
supporting the soundness of algebraic attacks on RSD. Further, we prove—without
any heuristics or assumptions—that RSD can be broken in polynomial time whenever
the number of error blocks times the square of the size of error blocks is larger
than 2 times the square of the dimension of the code.\r\nAdditionally, we use
our methodology to attack a variant of the Learning With Errors problem where
each error term lies in a fixed set of constant size. We prove that this problem
can be broken in polynomial time, given a sufficient number of samples. This result
improves on the seminal work by Arora and Ge (ICALP’11), as the attack’s time
complexity is independent of the LWE modulus."
acknowledgement: We thank Pierre Briaud and Morten Øygarden for helpful discussions
on algebraic attacks on RSD, and the EC reviewers for helpful comments.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Simon-Philipp
full_name: Merz, Simon-Philipp
last_name: Merz
- first_name: Patrick
full_name: Stählin, Patrick
last_name: Stählin
- first_name: Akin
full_name: Ünal, Akin
id: f6b56fb6-dc63-11ee-9dbf-f6780863a85a
last_name: Ünal
orcid: 0000-0002-8929-0221
citation:
ama: 'Cueto Noval M, Merz S-P, Stählin P, Ünal A. On the soundness of algebraic
attacks against code-based assumptions. In: 44th Annual International Conference
on the Theory and Applications of Cryptographic Techniques. Vol 15606. Springer
Nature; 2025:385-415. doi:10.1007/978-3-031-91095-1_14'
apa: 'Cueto Noval, M., Merz, S.-P., Stählin, P., & Ünal, A. (2025). On the soundness
of algebraic attacks against code-based assumptions. In 44th Annual International
Conference on the Theory and Applications of Cryptographic Techniques (Vol.
15606, pp. 385–415). Madrid, Spain: Springer Nature. https://doi.org/10.1007/978-3-031-91095-1_14'
chicago: Cueto Noval, Miguel, Simon-Philipp Merz, Patrick Stählin, and Akin Ünal.
“On the Soundness of Algebraic Attacks against Code-Based Assumptions.” In 44th
Annual International Conference on the Theory and Applications of Cryptographic
Techniques, 15606:385–415. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-91095-1_14.
ieee: M. Cueto Noval, S.-P. Merz, P. Stählin, and A. Ünal, “On the soundness of algebraic
attacks against code-based assumptions,” in 44th Annual International Conference
on the Theory and Applications of Cryptographic Techniques, Madrid, Spain,
2025, vol. 15606, pp. 385–415.
ista: 'Cueto Noval M, Merz S-P, Stählin P, Ünal A. 2025. On the soundness of algebraic
attacks against code-based assumptions. 44th Annual International Conference on
the Theory and Applications of Cryptographic Techniques. EUROCRYPT: International
Conference on the Theory and Applications of Cryptographic Techniques, LNCS, vol.
15606, 385–415.'
mla: Cueto Noval, Miguel, et al. “On the Soundness of Algebraic Attacks against
Code-Based Assumptions.” 44th Annual International Conference on the Theory
and Applications of Cryptographic Techniques, vol. 15606, Springer Nature,
2025, pp. 385–415, doi:10.1007/978-3-031-91095-1_14.
short: M. Cueto Noval, S.-P. Merz, P. Stählin, A. Ünal, in:, 44th Annual International
Conference on the Theory and Applications of Cryptographic Techniques, Springer
Nature, 2025, pp. 385–415.
conference:
end_date: 2025-05-08
location: Madrid, Spain
name: 'EUROCRYPT: International Conference on the Theory and Applications of Cryptographic
Techniques'
start_date: 2025-05-04
corr_author: '1'
date_created: 2025-05-19T14:15:01Z
date_published: 2025-04-28T00:00:00Z
date_updated: 2025-05-28T06:12:39Z
day: '28'
department:
- _id: KrPi
doi: 10.1007/978-3-031-91095-1_14
intvolume: ' 15606'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.research-collection.ethz.ch/handle/20.500.11850/732894
month: '04'
oa: 1
oa_version: Submitted Version
page: 385-415
publication: 44th Annual International Conference on the Theory and Applications of
Cryptographic Techniques
publication_identifier:
eisbn:
- '9783031910951'
eissn:
- 1611-3349
isbn:
- '9783031910944'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: On the soundness of algebraic attacks against code-based assumptions
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15606
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19738'
abstract:
- lang: eng
text: "Garbling is a fundamental cryptographic primitive, with numerous theoretical
and practical applications. Since the first construction by Yao (FOCS’82, ’86),
a line of work has concerned itself with reducing the communication and computational
complexity of that construction. One of the most efficient garbling schemes presently
is the ‘Half Gates’ scheme by Zahur, Rosulek, and Evans (Eurocrypt’15). Despite
its widespread adoption, the provable security of this scheme has been based on
assumptions whose only instantiations are in idealized models. For example, in
their original paper, Zahur, Rosulek, and Evans showed that hash functions satisfying
a notion called circular correlation robustness (CCR) suffice for this task, and
then proved that CCR secure hash functions can be instantiated in the random permutation
model.\r\nIn this work, we show how to securely instantiate the Half Gates scheme
in the standard model. To this end, we first show how this scheme can be securely
instantiated given a (family of) weak CCR hash function, a notion that we introduce.
Furthermore, we show how a weak CCR hash function can be used to securely instantiate
other efficient garbling schemes, namely the ones by Rosulek and Roy (Crypto’21)
and Heath (Eurocrypt’24). Thus we believe this notion to be of independent interest.\r\nFinally,
we construct such weak CCR hash functions using indistinguishability obfuscation
and one-way functions. The security proof of this construction constitutes our
main technical contribution. While our construction is not practical, it serves
as a proof of concept supporting the soundness of these garbling schemes, which
we regard to be particularly important given the recent initiative by NIST to
standardize garbling, and the optimizations in Half Gates being potentially adopted."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Anasuya
full_name: Acharya, Anasuya
last_name: Acharya
- first_name: Karen
full_name: Azari, Karen
last_name: Azari
- first_name: Mirza Ahad
full_name: Baig, Mirza Ahad
id: 3EDE6DE4-AA5A-11E9-986D-341CE6697425
last_name: Baig
- first_name: Dennis
full_name: Hofheinz, Dennis
last_name: Hofheinz
- first_name: Chethan
full_name: Kamath, Chethan
last_name: Kamath
citation:
ama: 'Acharya A, Azari K, Baig MA, Hofheinz D, Kamath C. Securely instantiating
‘Half Gates’ garbling in the standard model. In: 28th IACR International Conference
on Practice and Theory of Public-Key Cryptography. Vol 15677. Springer Nature;
2025:37-75. doi:10.1007/978-3-031-91829-2_2'
apa: 'Acharya, A., Azari, K., Baig, M. A., Hofheinz, D., & Kamath, C. (2025).
Securely instantiating ‘Half Gates’ garbling in the standard model. In 28th
IACR International Conference on Practice and Theory of Public-Key Cryptography
(Vol. 15677, pp. 37–75). Roros, Norway: Springer Nature. https://doi.org/10.1007/978-3-031-91829-2_2'
chicago: Acharya, Anasuya, Karen Azari, Mirza Ahad Baig, Dennis Hofheinz, and Chethan
Kamath. “Securely Instantiating ‘Half Gates’ Garbling in the Standard Model.”
In 28th IACR International Conference on Practice and Theory of Public-Key
Cryptography, 15677:37–75. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-91829-2_2.
ieee: A. Acharya, K. Azari, M. A. Baig, D. Hofheinz, and C. Kamath, “Securely instantiating
‘Half Gates’ garbling in the standard model,” in 28th IACR International Conference
on Practice and Theory of Public-Key Cryptography, Roros, Norway, 2025, vol.
15677, pp. 37–75.
ista: 'Acharya A, Azari K, Baig MA, Hofheinz D, Kamath C. 2025. Securely instantiating
‘Half Gates’ garbling in the standard model. 28th IACR International Conference
on Practice and Theory of Public-Key Cryptography. PKC: Public-Key Cryptography,
LNCS, vol. 15677, 37–75.'
mla: Acharya, Anasuya, et al. “Securely Instantiating ‘Half Gates’ Garbling in the Standard
Model.” 28th IACR International Conference on Practice and Theory of Public-Key
Cryptography, vol. 15677, Springer Nature, 2025, pp. 37–75, doi:10.1007/978-3-031-91829-2_2.
short: A. Acharya, K. Azari, M.A. Baig, D. Hofheinz, C. Kamath, in:, 28th IACR International
Conference on Practice and Theory of Public-Key Cryptography, Springer Nature,
2025, pp. 37–75.
conference:
end_date: 2025-05-15
location: Roros, Norway
name: 'PKC: Public-Key Cryptography'
start_date: 2025-05-12
date_created: 2025-05-25T22:17:02Z
date_published: 2025-05-05T00:00:00Z
date_updated: 2025-06-02T07:01:45Z
day: '05'
department:
- _id: KrPi
- _id: GradSch
doi: 10.1007/978-3-031-91829-2_2
intvolume: ' 15677'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/281
month: '05'
oa: 1
oa_version: Preprint
page: 37-75
publication: 28th IACR International Conference on Practice and Theory of Public-Key
Cryptography
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031918285'
issn:
- 0302-9743
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Securely instantiating ‘Half Gates’ garbling in the standard model
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15677
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19739'
abstract:
- lang: eng
text: "Cooperative verification is gaining momentum in recent years. The usual setup
in cooperative verification is that a verifier A is run with some pre-defined
resources, and if it is not able to verify the program, the verification task
is passed to a verifier B together with information learned about the program
by verifier A, then the chain can continue to a verifier C, and so on. This scheme
is static: tools run one after another in a fixed pre-defined order and fixed
parameters and resource limits (the scheme may differ for properties to be analyzed,
though).\r\n\r\nBubaak is a program analysis tool that allows to run multiple
program verifiers in a dynamically changing combination of parallel and sequential
portfolios. Bubaak starts the verification process by invoking an initial set
of tasks; every task, when it is done (e.g., because of hitting a time limit or
finishing its job), rewrites itself into one or more successor tasks. New tasks
can be also spawned upon events generated by other tasks. This all happens dynamically
based on the information gathered by finished and running tasks. During their
execution, tasks that run in parallel can exchange (partial) verification artifacts,
either directly or with Bubaak as an intermediary."
acknowledgement: This work was in part supported by the ERC-2020-AdG 10102009 grant,
and in part by the German Research Foundation (DFG) - WE2290/13-2 (Coop2).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
citation:
ama: 'Chalupa M, Richter C. BUBAAK: Dynamic cooperative verification. In: 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. Vol 15698. Springer Nature; 2025:212-216. doi:10.1007/978-3-031-90660-2_14'
apa: 'Chalupa, M., & Richter, C. (2025). BUBAAK: Dynamic cooperative verification.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15698, pp. 212–216). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90660-2_14'
chicago: 'Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.”
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 15698:212–16. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90660-2_14.'
ieee: 'M. Chalupa and C. Richter, “BUBAAK: Dynamic cooperative verification,” in
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15698, pp. 212–216.'
ista: 'Chalupa M, Richter C. 2025. BUBAAK: Dynamic cooperative verification. 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
LNCS, vol. 15698, 212–216.'
mla: 'Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.”
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 15698, Springer Nature, 2025, pp. 212–16, doi:10.1007/978-3-031-90660-2_14.'
short: M. Chalupa, C. Richter, in:, 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 212–216.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:04Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T07:21:41Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-90660-2_14
ec_funded: 1
file:
- access_level: open_access
checksum: 3f604f25dbe37383acb7f8308aad3ca6
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T07:10:35Z
date_updated: 2025-06-02T07:10:35Z
file_id: '19766'
file_name: 2025_TACAS_Chalupa.pdf
file_size: 259050
relation: main_file
success: 1
file_date_updated: 2025-06-02T07:10:35Z
has_accepted_license: '1'
intvolume: ' 15698'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 212-216
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906596'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'BUBAAK: Dynamic cooperative verification'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15698
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19740'
abstract:
- lang: eng
text: Two standard models for probabilistic systems are Markov chains (MCs) and
Markov decision processes (MDPs). Classic objectives for such probabilistic models
for control and planning problems are reachability and stochastic shortest path.
The widely studied algorithmic approach for these problems is the Value Iteration
(VI) algorithm which iteratively applies local updates called Bellman updates.
There are many practical approaches for VI in the literature but they all require
exponentially many Bellman updates for MCs in the worst case. A preprocessing
step is an algorithm that is discrete, graph-theoretical, and requires linear
space. An important open question is whether, after a polynomial-time preprocessing,
VI can be achieved with sub-exponentially many Bellman updates. In this work,
we present a new approach for VI based on guessing values. Our theoretical contributions
are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm
after which, along with guessing values, VI requires only subexponentially many
Bellman updates. Second, we present an improved analysis of the speed of convergence
of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our
new approach. Experimental results show that our approach provides a considerable
improvement over existing VI-based approaches on several benchmark examples from
the literature.
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant and Austrian Science Fund (FWF) 10.55776/COE12 grant.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Mahdi
full_name: Jafariraviz, Mahdi
last_name: Jafariraviz
- first_name: Raimundo J
full_name: Saona Urmeneta, Raimundo J
id: BD1DF4C4-D767-11E9-B658-BC13E6697425
last_name: Saona Urmeneta
orcid: 0000-0001-5103-038X
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. Value iteration
with guessing for Markov chains and Markov decision processes. In: 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 15697. Springer Nature; 2025:217-236. doi:10.1007/978-3-031-90653-4_11'
apa: 'Chatterjee, K., Jafariraviz, M., Saona Urmeneta, R. J., & Svoboda, J.
(2025). Value iteration with guessing for Markov chains and Markov decision processes.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15697, pp. 217–236). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90653-4_11'
chicago: Chatterjee, Krishnendu, Mahdi Jafariraviz, Raimundo J Saona Urmeneta, and
Jakub Svoboda. “Value Iteration with Guessing for Markov Chains and Markov Decision
Processes.” In 31st International Conference on Tools and Algorithms for the
Construction and Analysis of Systems, 15697:217–36. Springer Nature, 2025.
https://doi.org/10.1007/978-3-031-90653-4_11.
ieee: K. Chatterjee, M. Jafariraviz, R. J. Saona Urmeneta, and J. Svoboda, “Value
iteration with guessing for Markov chains and Markov decision processes,” in 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Hamilton, ON, Canada, 2025, vol. 15697, pp. 217–236.
ista: 'Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. 2025. Value iteration
with guessing for Markov chains and Markov decision processes. 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 15697, 217–236.'
mla: Chatterjee, Krishnendu, et al. “Value Iteration with Guessing for Markov Chains
and Markov Decision Processes.” 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, vol. 15697, Springer
Nature, 2025, pp. 217–36, doi:10.1007/978-3-031-90653-4_11.
short: K. Chatterjee, M. Jafariraviz, R.J. Saona Urmeneta, J. Svoboda, in:, 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Springer Nature, 2025, pp. 217–236.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:06Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T07:35:06Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90653-4_11
ec_funded: 1
external_id:
arxiv:
- '2505.06769'
file:
- access_level: open_access
checksum: 45da6efbcbed20aada16c48c8e55e2d6
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T07:31:12Z
date_updated: 2025-06-02T07:31:12Z
file_id: '19767'
file_name: 2025_TACAS_Chatterjee.pdf
file_size: 557481
relation: main_file
success: 1
file_date_updated: 2025-06-02T07:31:12Z
has_accepted_license: '1'
intvolume: ' 15697'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 217-236
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906527'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Value iteration with guessing for Markov chains and Markov decision processes
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15697
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19742'
abstract:
- lang: eng
text: Statistical model checking estimates probabilities and expectations of interest
in probabilistic system models by using random simulations. Its results come with
statistical guarantees. However, many tools use unsound statistical methods that
produce incorrect results more often than they claim. In this paper, we provide
a comprehensive overview of tools and their correctness, as well as of sound methods
available for estimating probabilities from the literature. For expected rewards,
we investigate how to bound the path reward distribution to apply sound statistical
methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz
inequality that has not been used in SMC so far. We prove that even reachability
rewards can be bounded in theory, and formalise the concept of limit-PAC procedures
for a practical solution. The modes SMC tool implements our methods and recommendations,
which we use to experimentally confirm our results.
acknowledgement: This work was supported by the DFG through the Cluster of Excellence
EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy)
and the TRR 248 (see perspicuous-computing.science, project ID 389792660), by the
European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie
grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED),
by the EU under NextGenerationEU projects D53D23008400006 (Smartitude) under MUR
PRIN 2022 and PE00000014 (SERICS) under MUR PNRR, by the Interreg North Sea project
STORM_SAFE, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Carlos E.
full_name: Budde, Carlos E.
last_name: Budde
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
- first_name: Patrick
full_name: Wienhöft, Patrick
last_name: Wienhöft
citation:
ama: 'Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical
model checking for probabilities and expected rewards. In: 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 15696. Springer Nature; 2025:167-190. doi:10.1007/978-3-031-90643-5_9'
apa: 'Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., & Wienhöft,
P. (2025). Sound statistical model checking for probabilities and expected rewards.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90643-5_9'
chicago: Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger,
and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and
Expected Rewards.” In 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, 15696:167–90. Springer Nature,
2025. https://doi.org/10.1007/978-3-031-90643-5_9.
ieee: C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft,
“Sound statistical model checking for probabilities and expected rewards,” in
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190.
ista: 'Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound
statistical model checking for probabilities and expected rewards. 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 15696, 167–190.'
mla: Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities
and Expected Rewards.” 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, vol. 15696, Springer Nature,
2025, pp. 167–90, doi:10.1007/978-3-031-90643-5_9.
short: C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:,
31st International Conference on Tools and Algorithms for the Construction and
Analysis of Systems, Springer Nature, 2025, pp. 167–190.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
date_created: 2025-05-25T22:17:08Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T09:45:41Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90643-5_9
ec_funded: 1
external_id:
arxiv:
- '2411.00559'
file:
- access_level: open_access
checksum: d45856b503b1dd4f8f14c3566327225b
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T09:35:42Z
date_updated: 2025-06-02T09:35:42Z
file_id: '19770'
file_name: 2025_TACAS_Budde.pdf
file_size: 711271
relation: main_file
success: 1
file_date_updated: 2025-06-02T09:35:42Z
has_accepted_license: '1'
intvolume: ' 15696'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 167-190
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906428'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '19769'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Sound statistical model checking for probabilities and expected rewards
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15696
year: '2025'
...