---
_id: '14888'
abstract:
- lang: eng
text: 'A face in a curve arrangement is called popular if it is bounded by the same
curve multiple times. Motivated by the automatic generation of curved nonogram
puzzles, we investigate possibilities to eliminate the popular faces in an arrangement
by inserting a single additional curve. This turns out to be NP-hard; however,
it becomes tractable when the number of popular faces is small: We present a probabilistic
FPT-approach in the number of popular faces.'
acknowledgement: 'This work was initiated at the 16th European Research Week on Geometric
Graphs in Strobl in 2019. A.W. is supported by the Austrian Science Fund (FWF):
W1230. S.T. has been funded by the Vienna Science and Technology Fund (WWTF) [10.47379/ICT19035].
A preliminary version of this work has been presented at the 38th European Workshop
on Computational Geometry (EuroCG 2022) in Perugia [9]. A full version of this paper,
which includes appendices but is otherwise identical, is available as a technical
report [10].'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Phoebe
full_name: De Nooijer, Phoebe
last_name: De Nooijer
- first_name: Soeren
full_name: Terziadis, Soeren
last_name: Terziadis
- first_name: Alexandra
full_name: Weinberger, Alexandra
last_name: Weinberger
- first_name: Zuzana
full_name: Masárová, Zuzana
id: 45CFE238-F248-11E8-B48F-1D18A9856A87
last_name: Masárová
orcid: 0000-0002-6660-1322
- first_name: Tamara
full_name: Mchedlidze, Tamara
last_name: Mchedlidze
- first_name: Maarten
full_name: Löffler, Maarten
last_name: Löffler
- first_name: Günter
full_name: Rote, Günter
last_name: Rote
citation:
ama: 'De Nooijer P, Terziadis S, Weinberger A, et al. Removing popular faces in curve
arrangements. In: 31st International Symposium on Graph Drawing and Network
Visualization. Vol 14466. Springer Nature; 2024:18-33. doi:10.1007/978-3-031-49275-4_2'
apa: 'De Nooijer, P., Terziadis, S., Weinberger, A., Masárová, Z., Mchedlidze, T.,
Löffler, M., & Rote, G. (2024). Removing popular faces in curve arrangements.
In 31st International Symposium on Graph Drawing and Network Visualization
(Vol. 14466, pp. 18–33). Isola delle Femmine, Palermo, Italy: Springer Nature.
https://doi.org/10.1007/978-3-031-49275-4_2'
chicago: De Nooijer, Phoebe, Soeren Terziadis, Alexandra Weinberger, Zuzana Masárová,
Tamara Mchedlidze, Maarten Löffler, and Günter Rote. “Removing Popular Faces in Curve
Arrangements.” In 31st International Symposium on Graph Drawing and Network
Visualization, 14466:18–33. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-49275-4_2.
ieee: P. De Nooijer et al., “Removing popular faces in curve arrangements,”
in 31st International Symposium on Graph Drawing and Network Visualization,
Isola delle Femmine, Palermo, Italy, 2024, vol. 14466, pp. 18–33.
ista: 'De Nooijer P, Terziadis S, Weinberger A, Masárová Z, Mchedlidze T, Löffler
M, Rote G. 2024. Removing popular faces in curve arrangements. 31st International
Symposium on Graph Drawing and Network Visualization. GD: Graph Drawing and Network
Visualization, LNCS, vol. 14466, 18–33.'
mla: De Nooijer, Phoebe, et al. “Removing Popular Faces in Curve Arrangements.”
31st International Symposium on Graph Drawing and Network Visualization,
vol. 14466, Springer Nature, 2024, pp. 18–33, doi:10.1007/978-3-031-49275-4_2.
short: P. De Nooijer, S. Terziadis, A. Weinberger, Z. Masárová, T. Mchedlidze, M.
Löffler, G. Rote, in:, 31st International Symposium on Graph Drawing and Network
Visualization, Springer Nature, 2024, pp. 18–33.
conference:
end_date: 2023-09-22
location: Isola delle Femmine, Palermo, Italy
name: 'GD: Graph Drawing and Network Visualization'
start_date: 2023-09-20
date_created: 2024-01-28T23:01:43Z
date_published: 2024-01-06T00:00:00Z
date_updated: 2025-07-21T07:28:03Z
day: '06'
department:
- _id: UlWa
- _id: HeEd
doi: 10.1007/978-3-031-49275-4_2
external_id:
arxiv:
- '2202.12175'
intvolume: ' 14466'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2202.12175
month: '01'
oa: 1
oa_version: Preprint
page: 18-33
project:
- _id: bdb2a702-d553-11ed-ba76-f12e3e5a3bc6
grant_number: '101087907'
name: 'A quantum hybrid of atoms and milligram-scale pendulums: towards gravitational
quantum mechanics'
publication: 31st International Symposium on Graph Drawing and Network Visualization
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031492747'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Removing popular faces in curve arrangements
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14466
year: '2024'
...
---
_id: '12467'
abstract:
- lang: eng
text: Safety and liveness are elementary concepts of computation, and the foundation
of many verification paradigms. The safety-liveness classification of boolean
properties characterizes whether a given property can be falsified by observing
a finite prefix of an infinite computation trace (always for safety, never for
liveness). In quantitative specification and verification, properties assign not
truth values, but quantitative values to infinite traces (e.g., a cost, or the
distance to a boolean property). We introduce quantitative safety and liveness,
and we prove that our definitions induce conservative quantitative generalizations
of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness
decomposition of boolean properties. In particular, we show that every quantitative
property can be written as the pointwise minimum of a quantitative safety property
and a quantitative liveness property. Consequently, like boolean properties, also
quantitative properties can be min-decomposed into safety and liveness parts,
or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover,
quantitative properties can be approximated naturally. We prove that every quantitative
property that has both safe and co-safe approximations can be monitored arbitrarily
precisely by a monitor that uses only a finite number of states.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
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: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In:
26th International Conference Foundations of Software Science and Computation
Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative
safety and liveness. In 26th International Conference Foundations of Software
Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France:
Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative
Safety and Liveness.” In 26th International Conference Foundations of Software
Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17.
ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and
liveness,” in 26th International Conference Foundations of Software Science
and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness.
26th International Conference Foundations of Software Science and Computation
Structures. FOSSACS: Foundations of Software Science and Computation Structures,
LNCS, vol. 13992, 349–370.'
mla: Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International
Conference Foundations of Software Science and Computation Structures, vol.
13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference
Foundations of Software Science and Computation Structures, Springer Nature, 2023,
pp. 349–370.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FOSSACS: Foundations of Software Science and Computation Structures'
start_date: 2023-04-22
date_created: 2023-01-31T07:23:56Z
date_published: 2023-04-21T00:00:00Z
date_updated: 2023-07-14T11:20:27Z
day: '21'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-30829-1_17
ec_funded: 1
external_id:
arxiv:
- '2301.11175'
file:
- access_level: open_access
checksum: 981025aed580b6b27c426cb8856cf63e
content_type: application/pdf
creator: esarac
date_created: 2023-01-31T07:22:21Z
date_updated: 2023-01-31T07:22:21Z
file_id: '12468'
file_name: qsl.pdf
file_size: 449027
relation: main_file
success: 1
- access_level: open_access
checksum: f16e2af1e0eb243158ab0f0fe74e7d5a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T10:28:09Z
date_updated: 2023-06-19T10:28:09Z
file_id: '13153'
file_name: 2023_LNCS_HenzingerT.pdf
file_size: 1048171
relation: main_file
success: 1
file_date_updated: 2023-06-19T10:28:09Z
has_accepted_license: '1'
intvolume: ' 13992'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '04'
oa: 1
oa_version: Published Version
page: 349-370
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 26th International Conference Foundations of Software Science and Computation
Structures
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308284'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative safety and liveness
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: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 13992
year: '2023'
...
---
_id: '12854'
abstract:
- lang: eng
text: "The main idea behind BUBAAK is to run multiple program analyses in parallel
and use runtime monitoring and enforcement to observe and control their progress
in real time. The analyses send information about (un)explored states of the program
and discovered invariants to a monitor. The monitor processes the received data
and can force an analysis to stop the search of certain program parts (which have
already been analyzed by other analyses), or to make it utilize a program invariant
found by another analysis.\r\nAt SV-COMP 2023, the implementation of data exchange
between the monitor and the analyses was not yet completed, which is why BUBAAK
only ran several analyses in parallel, without any coordination. Still, BUBAAK
won the meta-category FalsificationOverall and placed very well in several other
(sub)-categories of the competition."
acknowledgement: This work was supported by the ERC-2020-AdG 10102009 grant.
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers.
In: Tools and Algorithms for the Construction and Analysis of Systems.
Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32'
apa: 'Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of
program verifiers. In Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32'
chicago: 'Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of
Program Verifiers.” In Tools and Algorithms for the Construction and Analysis
of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.'
ieee: 'M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,”
in Tools and Algorithms for the Construction and Analysis of Systems, Paris,
France, 2023, vol. 13994, pp. 535–540.'
ista: 'Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers.
Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994,
535–540.'
mla: 'Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program
Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.'
short: M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 535–540.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-04-20T08:22:53Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-04-25T07:02:43Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_32
ec_funded: 1
file:
- access_level: open_access
checksum: 120d2c2a38384058ad0630fdf8288312
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T06:58:36Z
date_updated: 2023-04-25T06:58:36Z
file_id: '12864'
file_name: 2023_LNCS_Chalupa.pdf
file_size: 16096413
relation: main_file
success: 1
file_date_updated: 2023-04-25T06:58:36Z
has_accepted_license: '1'
intvolume: ' 13994'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 535-540
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783031308208'
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: 'Bubaak: Runtime monitoring of program verifiers'
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: 13994
year: '2023'
...
---
_id: '12856'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of run-time monitoring. Third-party monitoring, with limited knowledge
of the monitored software, and best-effort monitoring, which keeps pace with the
monitored software, are especially valuable, yet underexplored areas of run-time
monitoring. Most existing monitoring frameworks do not support their combination
because they either require access to the monitored code for instrumentation purposes
or the processing of all observed events, or both.\r\n\r\nWe present a middleware
framework, VAMOS, for the run-time monitoring of software which is explicitly
designed to support third-party and best-effort scenarios. The design goals of
VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the
ability to monitor black-box code through a variety of different event channels,
and the connectability to monitors written in different specification languages),
and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker
and event recognition systems with aspects of stream processing systems.\r\nWe
implemented a prototype toolchain for VAMOS and conducted experiments including
a case study of monitoring for data races. The results indicate that VAMOS enables
writing useful yet efficient monitors, is compatible with a variety of event sources
and monitor specifications, and simplifies key aspects of setting up a monitoring
system from scratch."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
authors would like to thank the anonymous FASE reviewers for their valuable feedback
and suggestions.
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: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort
third-party monitoring. In: Fundamental Approaches to Software Engineering.
Vol 13991. Springer Nature; 2023:260-281. doi:10.1007/978-3-031-30826-0_15'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023).
Vamos: Middleware for best-effort third-party monitoring. In Fundamental Approaches
to Software Engineering (Vol. 13991, pp. 260–281). Paris, France: Springer
Nature. https://doi.org/10.1007/978-3-031-30826-0_15'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
“Vamos: Middleware for Best-Effort Third-Party Monitoring.” In Fundamental
Approaches to Software Engineering, 13991:260–81. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30826-0_15.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware
for best-effort third-party monitoring,” in Fundamental Approaches to Software
Engineering, Paris, France, 2023, vol. 13991, pp. 260–281.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware
for best-effort third-party monitoring. Fundamental Approaches to Software Engineering.
FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.'
mla: 'Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.”
Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature,
2023, pp. 260–81, doi:10.1007/978-3-031-30826-0_15.'
short: M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental
Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FASE: Fundamental Approaches to Software Engineering'
start_date: 2023-04-22
date_created: 2023-04-20T08:29:42Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-04-25T07:19:07Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30826-0_15
ec_funded: 1
file:
- access_level: open_access
checksum: 17a7c8e08be609cf2408d37ea55e322c
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T07:16:36Z
date_updated: 2023-04-25T07:16:36Z
file_id: '12865'
file_name: 2023_LNCS_ChalupaM.pdf
file_size: 580828
relation: main_file
success: 1
file_date_updated: 2023-04-25T07:16:36Z
has_accepted_license: '1'
intvolume: ' 13991'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 260-281
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Fundamental Approaches to Software Engineering
publication_identifier:
eisbn:
- '9783031308260'
eissn:
- 1611-3349
isbn:
- '9783031308253'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '12407'
relation: earlier_version
status: public
status: public
title: 'Vamos: Middleware for best-effort third-party monitoring'
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: 13991
year: '2023'
...
---
_id: '13139'
abstract:
- lang: eng
text: A classical problem for Markov chains is determining their stationary (or
steady-state) distribution. This problem has an equally classical solution based
on eigenvectors and linear equation systems. However, this approach does not scale
to large instances, and iterative solutions are desirable. It turns out that a
naive approach, as used by current model checkers, may yield completely wrong
results. We present a new approach, which utilizes recent advances in partial
exploration and mean payoff computation to obtain a correct, converging approximation.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
citation:
ama: 'Meggendorfer T. Correct approximation of stationary distributions. In: TACAS
2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol
13993. Springer Nature; 2023:489-507. doi:10.1007/978-3-031-30823-9_25'
apa: 'Meggendorfer, T. (2023). Correct approximation of stationary distributions.
In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 13993, pp. 489–507). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_25'
chicago: 'Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.”
In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
13993:489–507. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_25.'
ieee: 'T. Meggendorfer, “Correct approximation of stationary distributions,” in
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
Paris, France, 2023, vol. 13993, pp. 489–507.'
ista: 'Meggendorfer T. 2023. Correct approximation of stationary distributions.
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 13993, 489–507.'
mla: 'Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.”
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13993, Springer Nature, 2023, pp. 489–507, doi:10.1007/978-3-031-30823-9_25.'
short: 'T. Meggendorfer, in:, TACAS 2023: Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 489–507.'
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-06-18T22:00:46Z
date_published: 2023-04-22T00:00:00Z
date_updated: 2024-02-27T07:19:33Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-30823-9_25
external_id:
arxiv:
- '2301.08137'
file:
- access_level: open_access
checksum: 59f707a3949c03793251b0d04c62542a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T07:18:40Z
date_updated: 2023-06-19T07:18:40Z
file_id: '13148'
file_name: 2023_LNCS_Meggendorfer.pdf
file_size: 521951
relation: main_file
success: 1
file_date_updated: 2023-06-19T07:18:40Z
has_accepted_license: '1'
intvolume: ' 13993'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 489-507
publication: 'TACAS 2023: Tools and Algorithms for the Construction and Analysis of
Systems'
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308222'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14990'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Correct approximation of stationary distributions
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13993
year: '2023'
...
---
_id: '13141'
abstract:
- lang: eng
text: "We automatically compute a new class of environment assumptions in two-player
turn-based finite graph games which characterize an “adequate cooperation” needed
from the environment to allow the system player to win. Given an ω-regular winning
condition Φ for the system player, we compute an ω-regular assumption Ψ for the
environment player, such that (i) every environment strategy compliant with Ψ
allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the
environment for every strategy of the system (implementability), and (iii) Ψ does
not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games,
which are canonical representations of ω-regular games, we present a polynomial-time
algorithm for the symbolic computation of adequately permissive assumptions and
show that our algorithm runs faster and produces better assumptions than existing
approaches—both theoretically and empirically. To the best of our knowledge, for
ω\r\n-regular games, we provide the first algorithm to compute sufficient and
implementable environment assumptions that are also permissive."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ashwani
full_name: Anand, Ashwani
last_name: Anand
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Satya Prakash
full_name: Nayak, Satya Prakash
last_name: Nayak
- first_name: Anne Kathrin
full_name: Schmuck, Anne Kathrin
last_name: Schmuck
citation:
ama: 'Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions
for synthesis. In: TACAS 2023: Tools and Algorithms for the Construction and
Analysis of Systems. Vol 13994. Springer Nature; 2023:211-228. doi:10.1007/978-3-031-30820-8_15'
apa: 'Anand, A., Mallik, K., Nayak, S. P., & Schmuck, A. K. (2023). Computing
adequately permissive assumptions for synthesis. In TACAS 2023: Tools and Algorithms
for the Construction and Analysis of Systems (Vol. 13994, pp. 211–228). Paris,
France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_15'
chicago: 'Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin
Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In TACAS
2023: Tools and Algorithms for the Construction and Analysis of Systems, 13994:211–28.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_15.'
ieee: 'A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately
permissive assumptions for synthesis,” in TACAS 2023: Tools and Algorithms
for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994,
pp. 211–228.'
ista: 'Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive
assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of Systems, LNCS, vol. 13994, 211–228.'
mla: 'Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.”
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 211–28, doi:10.1007/978-3-031-30820-8_15.'
short: 'A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and
Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023,
pp. 211–228.'
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-06-18T22:00:47Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-06-19T08:49:46Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_15
file:
- access_level: open_access
checksum: 60dcafc1b4f6f070be43bad3fe877974
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T08:43:21Z
date_updated: 2023-06-19T08:43:21Z
file_id: '13151'
file_name: 2023_LNCS_Anand.pdf
file_size: 521425
relation: main_file
success: 1
file_date_updated: 2023-06-19T08:43:21Z
has_accepted_license: '1'
intvolume: ' 13994'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 211-228
publication: 'TACAS 2023: Tools and Algorithms for the Construction and Analysis of
Systems'
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing adequately permissive assumptions for synthesis
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: 13994
year: '2023'
...
---
_id: '13142'
abstract:
- lang: eng
text: Reinforcement learning has received much attention for learning controllers
of deterministic systems. We consider a learner-verifier framework for stochastic
control systems and survey recent methods that formally guarantee a conjunction
of reachability and safety properties. Given a property and a lower bound on the
probability of the property being satisfied, our framework jointly learns a control
policy and a formal certificate to ensure the satisfaction of the property with
a desired probability threshold. Both the control policy and the formal certificate
are continuous functions from states to reals, which are learned as parameterized
neural networks. While in the deterministic case, the certificates are invariant
and barrier functions for safety, or Lyapunov and ranking functions for liveness,
in the stochastic case the certificates are supermartingales. For certificate
verification, we use interval arithmetic abstract interpretation to bound the
expected values of neural network functions.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework
for neural network controllers and certificates of stochastic systems. In: Tools
and Algorithms for the Construction and Analysis of Systems . Vol 13993. Springer
Nature; 2023:3-25. doi:10.1007/978-3-031-30823-9_1'
apa: 'Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic, D. (2023). A
learner-verifier framework for neural network controllers and certificates of
stochastic systems. In Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_1'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde
Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates
of Stochastic Systems.” In Tools and Algorithms for the Construction and Analysis
of Systems , 13993:3–25. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_1.
ieee: K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier
framework for neural network controllers and certificates of stochastic systems,”
in Tools and Algorithms for the Construction and Analysis of Systems ,
Paris, France, 2023, vol. 13993, pp. 3–25.
ista: 'Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier
framework for neural network controllers and certificates of stochastic systems.
Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993,
3–25.'
mla: Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network
Controllers and Certificates of Stochastic Systems.” Tools and Algorithms for
the Construction and Analysis of Systems , vol. 13993, Springer Nature, 2023,
pp. 3–25, doi:10.1007/978-3-031-30823-9_1.
short: K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms
for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-06-18T22:00:47Z
date_published: 2023-04-22T00:00:00Z
date_updated: 2025-07-14T09:09:52Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-031-30823-9_1
ec_funded: 1
file:
- access_level: open_access
checksum: 3d8a8bb24d211bc83360dfc2fd744307
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T08:29:30Z
date_updated: 2023-06-19T08:29:30Z
file_id: '13150'
file_name: 2023_LNCS_Chatterjee.pdf
file_size: 528455
relation: main_file
success: 1
file_date_updated: 2023-06-19T08:29:30Z
has_accepted_license: '1'
intvolume: ' 13993'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 3-25
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: 'Tools and Algorithms for the Construction and Analysis of Systems '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308222'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: A learner-verifier framework for neural network controllers and certificates
of stochastic systems
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13993
year: '2023'
...
---
_id: '13143'
abstract:
- lang: eng
text: "GIMPS and PrimeGrid are large-scale distributed projects dedicated to searching
giant prime numbers, usually of special forms like Mersenne and Proth primes.
The numbers in the current search-space are millions of digits large and the participating
volunteers need to run resource-consuming primality tests. Once a candidate prime
N has been found, the only way for another party to independently verify the primality
of N used to be by repeating the expensive primality test. To avoid the need for
second recomputation of each primality test, these projects have recently adopted
certifying mechanisms that enable efficient verification of performed tests. However,
the mechanisms presently in place only detect benign errors and there is no guarantee
against adversarial behavior: a malicious volunteer can mislead the project to
reject a giant prime as being non-prime.\r\nIn this paper, we propose a practical,
cryptographically-sound mechanism for certifying the non-primality of Proth numbers.
That is, a volunteer can – parallel to running the primality test for N – generate
an efficiently verifiable proof at a little extra cost certifying that N is not
prime. The interactive protocol has statistical soundness and can be made non-interactive
using the Fiat-Shamir heuristic.\r\nOur approach is based on a cryptographic primitive
called Proof of Exponentiation (PoE) which, for a group G, certifies that a tuple
(x,y,T)∈G2×N satisfies x2T=y (Pietrzak, ITCS 2019 and Wesolowski, J. Cryptol.
2020). In particular, we show how to adapt Pietrzak’s PoE at a moderate additional
cost to make it a cryptographically-sound certificate of non-primality."
acknowledgement: 'We are grateful to Pavel Atnashev for clarifying via e-mail several
aspects of the primality tests implementated in the PrimeGrid project. Pavel Hubáček
is supported by the Czech Academy of Sciences (RVO 67985840), the Grant Agency of
the Czech Republic under the grant agreement no. 19-27871X, and by the Charles University
project UNCE/SCI/004. Chethan Kamath is supported by Azrieli International Postdoctoral
Fellowship, ISF grants 484/18 and 1789/19, and ERC StG project SPP: Secrecy Preserving
Proofs.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Charlotte
full_name: Hoffmann, Charlotte
id: 0f78d746-dc7d-11ea-9b2f-83f92091afe7
last_name: Hoffmann
- first_name: Pavel
full_name: Hubáček, Pavel
last_name: Hubáček
- first_name: Chethan
full_name: Kamath, Chethan
last_name: Kamath
- 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: 'Hoffmann C, Hubáček P, Kamath C, Pietrzak KZ. Certifying giant nonprimes.
In: Public-Key Cryptography - PKC 2023. Vol 13940. Springer Nature; 2023:530-553.
doi:10.1007/978-3-031-31368-4_19'
apa: 'Hoffmann, C., Hubáček, P., Kamath, C., & Pietrzak, K. Z. (2023). Certifying
giant nonprimes. In Public-Key Cryptography - PKC 2023 (Vol. 13940, pp.
530–553). Atlanta, GA, United States: Springer Nature. https://doi.org/10.1007/978-3-031-31368-4_19'
chicago: Hoffmann, Charlotte, Pavel Hubáček, Chethan Kamath, and Krzysztof Z Pietrzak.
“Certifying Giant Nonprimes.” In Public-Key Cryptography - PKC 2023, 13940:530–53.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-31368-4_19.
ieee: C. Hoffmann, P. Hubáček, C. Kamath, and K. Z. Pietrzak, “Certifying giant
nonprimes,” in Public-Key Cryptography - PKC 2023, Atlanta, GA, United
States, 2023, vol. 13940, pp. 530–553.
ista: 'Hoffmann C, Hubáček P, Kamath C, Pietrzak KZ. 2023. Certifying giant nonprimes.
Public-Key Cryptography - PKC 2023. PKC: Public-Key Cryptography, LNCS, vol. 13940,
530–553.'
mla: Hoffmann, Charlotte, et al. “Certifying Giant Nonprimes.” Public-Key Cryptography
- PKC 2023, vol. 13940, Springer Nature, 2023, pp. 530–53, doi:10.1007/978-3-031-31368-4_19.
short: C. Hoffmann, P. Hubáček, C. Kamath, K.Z. Pietrzak, in:, Public-Key Cryptography
- PKC 2023, Springer Nature, 2023, pp. 530–553.
conference:
end_date: 2023-05-10
location: Atlanta, GA, United States
name: 'PKC: Public-Key Cryptography'
start_date: 2023-05-07
date_created: 2023-06-18T22:00:47Z
date_published: 2023-05-02T00:00:00Z
date_updated: 2023-06-19T08:03:37Z
day: '02'
department:
- _id: KrPi
doi: 10.1007/978-3-031-31368-4_19
intvolume: ' 13940'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2023/238
month: '05'
oa: 1
oa_version: Submitted Version
page: 530-553
publication: Public-Key Cryptography - PKC 2023
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031313677'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Certifying giant nonprimes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13940
year: '2023'
...
---
_id: '13236'
abstract:
- lang: eng
text: We present an auction algorithm using multiplicative instead of constant weight
updates to compute a (1−ε)-approximate maximum weight matching (MWM) in a bipartite
graph with n vertices and m edges in time O(mε−1log(ε−1)), matching the running
time of the linear-time approximation algorithm of Duan and Pettie [JACM ’14].
Our algorithm is very simple and it can be extended to give a dynamic data structure
that maintains a (1−ε)-approximate maximum weight matching under (1) one-sided
vertex deletions (with incident edges) and (2) one-sided vertex insertions (with
incident edges sorted by weight) to the other side. The total time time used is
O(mε−1log(ε−1)), where m is the sum of the number of initially existing and inserted
edges.
acknowledgement: The first author thanks to Chandra Chekuri for useful discussions
about this paper. This project has received funding from the European Research Council
(ERC) under the European Union’s Horizon 2020 research and innovation programme
(Grant agreement No. 101019564 “The Design of Modern Fully Dynamic Data Structures
(MoDynStruct)” and from the Austrian Science Fund (FWF) project “Fast Algorithms
for a Reactive Network Layer (ReactNet)”, P 33775-N, with additional funding from
the netidee SCIENCE Stiftung, 2020–2024.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Da Wei
full_name: Zheng, Da Wei
last_name: Zheng
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
citation:
ama: 'Zheng DW, Henzinger MH. Multiplicative auction algorithm for approximate maximum
weight bipartite matching. In: International Conference on Integer Programming
and Combinatorial Optimization. Vol 13904. Springer Nature; 2023:453-465.
doi:10.1007/978-3-031-32726-1_32'
apa: 'Zheng, D. W., & Henzinger, M. H. (2023). Multiplicative auction algorithm
for approximate maximum weight bipartite matching. In International Conference
on Integer Programming and Combinatorial Optimization (Vol. 13904, pp. 453–465).
Madison, WI, United States: Springer Nature. https://doi.org/10.1007/978-3-031-32726-1_32'
chicago: Zheng, Da Wei, and Monika H Henzinger. “Multiplicative Auction Algorithm
for Approximate Maximum Weight Bipartite Matching.” In International Conference
on Integer Programming and Combinatorial Optimization, 13904:453–65. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-32726-1_32.
ieee: D. W. Zheng and M. H. Henzinger, “Multiplicative auction algorithm for approximate
maximum weight bipartite matching,” in International Conference on Integer
Programming and Combinatorial Optimization, Madison, WI, United States, 2023,
vol. 13904, pp. 453–465.
ista: 'Zheng DW, Henzinger MH. 2023. Multiplicative auction algorithm for approximate
maximum weight bipartite matching. International Conference on Integer Programming
and Combinatorial Optimization. IPCO: Integer Programming and Combinatorial Optimization,
LNCS, vol. 13904, 453–465.'
mla: Zheng, Da Wei, and Monika H. Henzinger. “Multiplicative Auction Algorithm for Approximate
Maximum Weight Bipartite Matching.” International Conference on Integer Programming
and Combinatorial Optimization, vol. 13904, Springer Nature, 2023, pp. 453–65,
doi:10.1007/978-3-031-32726-1_32.
short: D.W. Zheng, M.H. Henzinger, in:, International Conference on Integer Programming
and Combinatorial Optimization, Springer Nature, 2023, pp. 453–465.
conference:
end_date: 2023-06-23
location: Madison, WI, United States
name: 'IPCO: Integer Programming and Combinatorial Optimization'
start_date: 2023-06-21
date_created: 2023-07-16T22:01:11Z
date_published: 2023-05-22T00:00:00Z
date_updated: 2023-07-18T07:08:51Z
day: '22'
department:
- _id: MoHe
doi: 10.1007/978-3-031-32726-1_32
ec_funded: 1
external_id:
arxiv:
- '2301.09217'
intvolume: ' 13904'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2301.09217
month: '05'
oa: 1
oa_version: Preprint
page: 453-465
project:
- _id: bd9ca328-d553-11ed-ba76-dc4f890cfe62
call_identifier: H2020
grant_number: '101019564'
name: The design and evaluation of modern fully dynamic data structures
- _id: bd9e3a2e-d553-11ed-ba76-8aa684ce17fe
grant_number: 'P33775 '
name: Fast Algorithms for a Reactive Network Layer
publication: International Conference on Integer Programming and Combinatorial Optimization
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031327254'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Multiplicative auction algorithm for approximate maximum weight bipartite matching
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13904
year: '2023'
...
---
_id: '13238'
abstract:
- lang: eng
text: "We consider a natural problem dealing with weighted packet selection across
a rechargeable link, which e.g., finds applications in cryptocurrency networks.
The capacity of a link (u, v) is determined by how much nodes u and v allocate
for this link. Specifically, the input is a finite ordered sequence of packets
that arrive in both directions along a link. Given (u, v) and a packet of weight
x going from u to v, node u can either accept or reject the packet. If u accepts
the packet, the capacity on link (u, v) decreases by x. Correspondingly, v’s capacity
on (u, v) increases by x. If a node rejects the packet, this will entail a cost
affinely linear in the weight of the packet. A link is “rechargeable” in the sense
that the total capacity of the link has to remain constant, but the allocation
of capacity at the ends of the link can depend arbitrarily on the nodes’ decisions.
The goal is to minimise the sum of the capacity injected into the link and the
cost of rejecting packets. We show that the problem is NP-hard, but can be approximated
efficiently with a ratio of (1+ε)⋅(1+3–√) for some arbitrary ε>0.\r\n."
acknowledgement: We thank Mahsa Bastankhah and Mohammad Ali Maddah-Ali for fruitful
discussions about different variants of the problem. This work is supported by the
European Research Council (ERC) Consolidator Project 864228 (AdjustNet), 2020-2025,
the ERC CoG 863818 (ForM-SMArt), and the German Research Foundation (DFG) grant
470029389 (FlexNets), 2021–2024.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Stefan
full_name: Schmid, Stefan
last_name: Schmid
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
- first_name: Michelle X
full_name: Yeo, Michelle X
id: 2D82B818-F248-11E8-B48F-1D18A9856A87
last_name: Yeo
orcid: 0009-0001-3676-4809
citation:
ama: 'Schmid S, Svoboda J, Yeo MX. Weighted packet selection for rechargeable links
in cryptocurrency networks: Complexity and approximation. In: SIROCCO 2023:
Structural Information and Communication Complexity . Vol 13892. Springer
Nature; 2023:576-594. doi:10.1007/978-3-031-32733-9_26'
apa: 'Schmid, S., Svoboda, J., & Yeo, M. X. (2023). Weighted packet selection
for rechargeable links in cryptocurrency networks: Complexity and approximation.
In SIROCCO 2023: Structural Information and Communication Complexity (Vol.
13892, pp. 576–594). Alcala de Henares, Spain: Springer Nature. https://doi.org/10.1007/978-3-031-32733-9_26'
chicago: 'Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection
for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.”
In SIROCCO 2023: Structural Information and Communication Complexity ,
13892:576–94. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-32733-9_26.'
ieee: 'S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable
links in cryptocurrency networks: Complexity and approximation,” in SIROCCO
2023: Structural Information and Communication Complexity , Alcala de Henares,
Spain, 2023, vol. 13892, pp. 576–594.'
ista: 'Schmid S, Svoboda J, Yeo MX. 2023. Weighted packet selection for rechargeable
links in cryptocurrency networks: Complexity and approximation. SIROCCO 2023:
Structural Information and Communication Complexity . SIROCCO: Structural Information
and Communication Complexity, LNCS, vol. 13892, 576–594.'
mla: 'Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency
Networks: Complexity and Approximation.” SIROCCO 2023: Structural Information
and Communication Complexity , vol. 13892, Springer Nature, 2023, pp. 576–94,
doi:10.1007/978-3-031-32733-9_26.'
short: 'S. Schmid, J. Svoboda, M.X. Yeo, in:, SIROCCO 2023: Structural Information
and Communication Complexity , Springer Nature, 2023, pp. 576–594.'
conference:
end_date: 2023-06-09
location: Alcala de Henares, Spain
name: 'SIROCCO: Structural Information and Communication Complexity'
start_date: 2023-06-06
date_created: 2023-07-16T22:01:12Z
date_published: 2023-05-25T00:00:00Z
date_updated: 2025-07-14T09:09:53Z
day: '25'
department:
- _id: KrPi
- _id: KrCh
doi: 10.1007/978-3-031-32733-9_26
ec_funded: 1
external_id:
arxiv:
- '2204.13459'
intvolume: ' 13892'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2204.13459
month: '05'
oa: 1
oa_version: Preprint
page: 576-594
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 'SIROCCO 2023: Structural Information and Communication Complexity '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031327322'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14506'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'Weighted packet selection for rechargeable links in cryptocurrency networks:
Complexity and approximation'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13892
year: '2023'
...
---
_id: '13310'
abstract:
- lang: eng
text: Machine-learned systems are in widespread use for making decisions about humans,
and it is important that they are fair, i.e., not biased against individuals based
on sensitive attributes. We present runtime verification of algorithmic fairness
for systems whose models are unknown, but are assumed to have a Markov chain structure.
We introduce a specification language that can model many common algorithmic fairness
properties, such as demographic parity, equal opportunity, and social burden.
We build monitors that observe a long sequence of events as generated by a given
system, and output, after each observation, a quantitative estimate of how fair
or biased the system was on that run until that point in time. The estimate is
proven to be correct modulo a variable error bound and a given confidence level,
where the error bound gets tighter as the observed sequence gets longer. Our monitors
are of two types, and use, respectively, frequentist and Bayesian statistical
inference techniques. While the frequentist monitors compute estimates that are
objectively correct with respect to the ground truth, the Bayesian monitors compute
estimates that are correct subject to a given prior belief about the system’s
model. Using a prototype implementation, we show how we can monitor if a bank
is fair in giving loans to applicants from different social backgrounds, and if
a college is fair in admitting students while maintaining a reasonable financial
burden on the society. Although they exhibit different theoretical complexities
in certain cases, in our experiments, both frequentist and Bayesian monitors took
less than a millisecond to update their verdicts after each observation.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG101020093.'
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: Mahyar
full_name: Karimi, Mahyar
id: f1dedef5-2f78-11ee-989a-c4c97bccf506
last_name: Karimi
orcid: 0009-0005-0820-1696
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness.
In: Computer Aided Verification. Vol 13965. Springer Nature; 2023:358–382.
doi:10.1007/978-3-031-37703-7_17'
apa: 'Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Monitoring
algorithmic fairness. In Computer Aided Verification (Vol. 13965, pp. 358–382).
Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37703-7_17'
chicago: Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik.
“Monitoring Algorithmic Fairness.” In Computer Aided Verification, 13965:358–382.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37703-7_17.
ieee: T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic
fairness,” in Computer Aided Verification, Paris, France, 2023, vol. 13965,
pp. 358–382.
ista: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Monitoring algorithmic
fairness. Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 13965, 358–382.'
mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” Computer
Aided Verification, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:10.1007/978-3-031-37703-7_17.
short: T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification,
Springer Nature, 2023, pp. 358–382.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-07-25T18:32:40Z
date_published: 2023-07-18T00:00:00Z
date_updated: 2023-09-05T15:14:00Z
day: '18'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-37703-7_17
ec_funded: 1
external_id:
arxiv:
- '2305.15979'
file:
- access_level: open_access
checksum: ccaf94bf7d658ba012c016e11869b54c
content_type: application/pdf
creator: dernst
date_created: 2023-07-31T08:11:20Z
date_updated: 2023-07-31T08:11:20Z
file_id: '13327'
file_name: 2023_LNCS_CAV_HenzingerT.pdf
file_size: 647760
relation: main_file
success: 1
file_date_updated: 2023-07-31T08:11:20Z
has_accepted_license: '1'
intvolume: ' 13965'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 358–382
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Computer Aided Verification
publication_identifier:
eisbn:
- '9783031377037'
eissn:
- 1611-3349
isbn:
- '9783031377020'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Monitoring algorithmic fairness
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13965
year: '2023'
...
---
_id: '14829'
abstract:
- lang: eng
text: 'This paper explores a modular design architecture aimed at helping blockchains
(and other SMR implementation) to scale to a very large number of processes. This
comes in contrast to existing monolithic architectures that interleave transaction
dissemination, ordering, and execution in a single functionality. To achieve this
we first split the monolith to multiple layers which can use existing distributed
computing primitives. The exact specifications of the data dissemination part
are formally defined by the Proof of Availability & Retrieval (PoA &R) abstraction.
Solutions to the PoA &R problem contain two related sub-protocols: one that “pushes”
information into the network and another that “pulls” this information. Regarding
the latter, there is a dearth of research literature which is rectified in this
paper. We present a family of pulling sub-protocols and rigorously analyze them.
Extensive simulations support the theoretical claims of efficiency and robustness
in case of a very large number of players. Finally, actual implementation and
deployment on a small number of machines (roughly the size of several industrial
systems) demonstrates the viability of the architecture’s paradigm.'
acknowledgement: 'This work is partially supported by Meta. Eleftherios Kokoris-Kogias
is partially supported by Austrian Science Fund (FWF) grant No: F8512-N. Shir Cohen
is supported by the Adams Fellowship Program of the Israel Academy of Sciences and
Humanities.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Shir
full_name: Cohen, Shir
last_name: Cohen
- first_name: Guy
full_name: Goren, Guy
last_name: Goren
- first_name: Eleftherios
full_name: Kokoris Kogias, Eleftherios
id: f5983044-d7ef-11ea-ac6d-fd1430a26d30
last_name: Kokoris Kogias
- first_name: Alberto
full_name: Sonnino, Alberto
last_name: Sonnino
- first_name: Alexander
full_name: Spiegelman, Alexander
last_name: Spiegelman
citation:
ama: 'Cohen S, Goren G, Kokoris Kogias E, Sonnino A, Spiegelman A. Proof of availability
and retrieval in a modular blockchain architecture. In: 27th International
Conference on Financial Cryptography and Data Security. Vol 13951. Springer
Nature; 2023:36-53. doi:10.1007/978-3-031-47751-5_3'
apa: 'Cohen, S., Goren, G., Kokoris Kogias, E., Sonnino, A., & Spiegelman, A.
(2023). Proof of availability and retrieval in a modular blockchain architecture.
In 27th International Conference on Financial Cryptography and Data Security
(Vol. 13951, pp. 36–53). Bol, Brac, Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-47751-5_3'
chicago: Cohen, Shir, Guy Goren, Eleftherios Kokoris Kogias, Alberto Sonnino, and
Alexander Spiegelman. “Proof of Availability and Retrieval in a Modular Blockchain
Architecture.” In 27th International Conference on Financial Cryptography and
Data Security, 13951:36–53. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-47751-5_3.
ieee: S. Cohen, G. Goren, E. Kokoris Kogias, A. Sonnino, and A. Spiegelman, “Proof
of availability and retrieval in a modular blockchain architecture,” in 27th
International Conference on Financial Cryptography and Data Security, Bol,
Brac, Croatia, 2023, vol. 13951, pp. 36–53.
ista: 'Cohen S, Goren G, Kokoris Kogias E, Sonnino A, Spiegelman A. 2023. Proof
of availability and retrieval in a modular blockchain architecture. 27th International
Conference on Financial Cryptography and Data Security. FC: Financial Cryptography
and Data Security, LNCS, vol. 13951, 36–53.'
mla: Cohen, Shir, et al. “Proof of Availability and Retrieval in a Modular Blockchain
Architecture.” 27th International Conference on Financial Cryptography and
Data Security, vol. 13951, Springer Nature, 2023, pp. 36–53, doi:10.1007/978-3-031-47751-5_3.
short: S. Cohen, G. Goren, E. Kokoris Kogias, A. Sonnino, A. Spiegelman, in:, 27th
International Conference on Financial Cryptography and Data Security, Springer
Nature, 2023, pp. 36–53.
conference:
end_date: 2023-05-05
location: Bol, Brac, Croatia
name: 'FC: Financial Cryptography and Data Security'
start_date: 2023-05-01
date_created: 2024-01-18T07:41:12Z
date_published: 2023-12-01T00:00:00Z
date_updated: 2024-01-22T13:58:07Z
day: '01'
department:
- _id: ElKo
doi: 10.1007/978-3-031-47751-5_3
intvolume: ' 13951'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://fc23.ifca.ai/preproceedings/150.pdf
month: '12'
oa: 1
oa_version: Submitted Version
page: 36-53
project:
- _id: 34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f
grant_number: F8512
name: Secure Network and Hardware for Efficient Blockchains
publication: 27th International Conference on Financial Cryptography and Data Security
publication_identifier:
eisbn:
- '9783031477515'
eissn:
- 1611-3349
isbn:
- '9783031477508'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Proof of availability and retrieval in a modular blockchain architecture
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13951
year: '2023'
...
---
_id: '14259'
abstract:
- lang: eng
text: "We provide a learning-based technique for guessing a winning strategy in
a parity game originating from an LTL synthesis problem. A cheaply obtained guess
can be useful in several applications. Not only can the guessed strategy be applied
as best-effort in cases where the game’s huge size prohibits rigorous approaches,
but it can also increase the scalability of rigorous LTL synthesis in several
ways. Firstly, checking whether a guessed strategy is winning is easier than constructing
one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy
iteration faster than constructing one from scratch. Thirdly, the guess can be
used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn
contrast to previous works, we (i) reflect the highly structured logical information
in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata
translations, and (ii) learn to reflect it properly by learning from previously
solved games, bringing the solving process closer to human-like reasoning."
acknowledgement: This research was funded in part by the German Research Foundation
(DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Prokop, Maximilian
last_name: Prokop
- first_name: Sabine
full_name: Rieder, Sabine
last_name: Rieder
citation:
ama: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies
in LTL synthesis by semantic learning. In: 35th International Conference on
Computer Aided Verification . Vol 13964. Springer Nature; 2023:390-414. doi:10.1007/978-3-031-37706-8_20'
apa: 'Kretinsky, J., Meggendorfer, T., Prokop, M., & Rieder, S. (2023). Guessing
winning policies in LTL synthesis by semantic learning. In 35th International
Conference on Computer Aided Verification (Vol. 13964, pp. 390–414). Paris,
France: Springer Nature. https://doi.org/10.1007/978-3-031-37706-8_20'
chicago: Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder.
“Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In 35th
International Conference on Computer Aided Verification , 13964:390–414. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-37706-8_20.
ieee: J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning
policies in LTL synthesis by semantic learning,” in 35th International Conference
on Computer Aided Verification , Paris, France, 2023, vol. 13964, pp. 390–414.
ista: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies
in LTL synthesis by semantic learning. 35th International Conference on Computer
Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.'
mla: Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic
Learning.” 35th International Conference on Computer Aided Verification ,
vol. 13964, Springer Nature, 2023, pp. 390–414, doi:10.1007/978-3-031-37706-8_20.
short: J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International
Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-09-03T22:01:16Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2023-09-06T08:27:33Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37706-8_20
file:
- access_level: open_access
checksum: ed66278b61bb869e1baba3d9b9081271
content_type: application/pdf
creator: dernst
date_created: 2023-09-06T08:25:50Z
date_updated: 2023-09-06T08:25:50Z
file_id: '14276'
file_name: 2023_LNCS_CAV_Kretinsky.pdf
file_size: 428354
relation: main_file
success: 1
file_date_updated: 2023-09-06T08:25:50Z
has_accepted_license: '1'
intvolume: ' 13964'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 390-414
publication: '35th International Conference on Computer Aided Verification '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031377051'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Guessing winning policies in LTL synthesis by semantic learning
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13964
year: '2023'
...
---
_id: '14260'
abstract:
- lang: eng
text: "This paper presents Lincheck, a new practical and user-friendly framework
for testing concurrent algorithms on the Java Virtual Machine (JVM). Lincheck
provides a simple and declarative way to write concurrent tests: instead of describing
how to perform the test, users specify what to test by declaring all the operations
to examine; the framework automatically handles the rest. As a result, tests written
with Lincheck are concise and easy to understand. The framework automatically
generates a set of concurrent scenarios, examines them using stress-testing or
bounded model checking, and verifies that the results of each invocation are correct.
Notably, if an error is detected via model checking, Lincheck provides an easy-to-follow
trace to reproduce it, significantly simplifying the bug investigation.\r\n\r\nTo
the best of our knowledge, Lincheck is the first production-ready tool on the
JVM that offers such a simple way of writing concurrent tests, without requiring
special skills or expertise. We successfully integrated Lincheck in the development
process of several large projects, such as Kotlin Coroutines, and identified new
bugs in popular concurrency libraries, such as a race in Java’s standard ConcurrentLinkedDeque
and a liveliness bug in Java’s AbstractQueuedSynchronizer framework, which is
used in most of the synchronization primitives. We believe that Lincheck can significantly
improve the quality and productivity of concurrent algorithms research and development
and become the state-of-the-art tool for checking their correctness."
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Nikita
full_name: Koval, Nikita
id: 2F4DB10C-F248-11E8-B48F-1D18A9856A87
last_name: Koval
- first_name: Alexander
full_name: Fedorov, Alexander
id: 2e711909-896a-11ed-bdf8-eb0f5a2984c6
last_name: Fedorov
- first_name: Maria
full_name: Sokolova, Maria
last_name: Sokolova
- first_name: Dmitry
full_name: Tsitelov, Dmitry
last_name: Tsitelov
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
citation:
ama: 'Koval N, Fedorov A, Sokolova M, Tsitelov D, Alistarh D-A. Lincheck: A practical
framework for testing concurrent data structures on JVM. In: 35th International
Conference on Computer Aided Verification . Vol 13964. Springer Nature; 2023:156-169.
doi:10.1007/978-3-031-37706-8_8'
apa: 'Koval, N., Fedorov, A., Sokolova, M., Tsitelov, D., & Alistarh, D.-A.
(2023). Lincheck: A practical framework for testing concurrent data structures
on JVM. In 35th International Conference on Computer Aided Verification
(Vol. 13964, pp. 156–169). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37706-8_8'
chicago: 'Koval, Nikita, Alexander Fedorov, Maria Sokolova, Dmitry Tsitelov, and
Dan-Adrian Alistarh. “Lincheck: A Practical Framework for Testing Concurrent Data
Structures on JVM.” In 35th International Conference on Computer Aided Verification
, 13964:156–69. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37706-8_8.'
ieee: 'N. Koval, A. Fedorov, M. Sokolova, D. Tsitelov, and D.-A. Alistarh, “Lincheck:
A practical framework for testing concurrent data structures on JVM,” in 35th
International Conference on Computer Aided Verification , Paris, France, 2023,
vol. 13964, pp. 156–169.'
ista: 'Koval N, Fedorov A, Sokolova M, Tsitelov D, Alistarh D-A. 2023. Lincheck:
A practical framework for testing concurrent data structures on JVM. 35th International
Conference on Computer Aided Verification . CAV: Computer Aided Verification,
LNCS, vol. 13964, 156–169.'
mla: 'Koval, Nikita, et al. “Lincheck: A Practical Framework for Testing Concurrent
Data Structures on JVM.” 35th International Conference on Computer Aided Verification
, vol. 13964, Springer Nature, 2023, pp. 156–69, doi:10.1007/978-3-031-37706-8_8.'
short: N. Koval, A. Fedorov, M. Sokolova, D. Tsitelov, D.-A. Alistarh, in:, 35th
International Conference on Computer Aided Verification , Springer Nature, 2023,
pp. 156–169.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-09-03T22:01:16Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2024-02-27T07:46:52Z
day: '17'
ddc:
- '000'
department:
- _id: DaAl
- _id: GradSch
doi: 10.1007/978-3-031-37706-8_8
file:
- access_level: open_access
checksum: c346016393123a0a2338ad4d976f61bc
content_type: application/pdf
creator: dernst
date_created: 2023-09-06T08:16:25Z
date_updated: 2023-09-06T08:16:25Z
file_id: '14275'
file_name: 2023_LNCS_Koval.pdf
file_size: 421408
relation: main_file
success: 1
file_date_updated: 2023-09-06T08:16:25Z
has_accepted_license: '1'
intvolume: ' 13964'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 156-169
publication: '35th International Conference on Computer Aided Verification '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031377051'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14995'
relation: research_data
status: public
scopus_import: '1'
status: public
title: 'Lincheck: A practical framework for testing concurrent data structures on JVM'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13964
year: '2023'
...
---
_id: '14317'
abstract:
- lang: eng
text: "Markov decision processes can be viewed as transformers of probability distributions.
While this view is useful from a practical standpoint to reason about trajectories
of distributions, basic reachability and safety problems are known to be computationally
intractable (i.e., Skolem-hard) to solve in such models. Further, we show that
even for simple examples of MDPs, strategies for safety objectives over distributions
can require infinite memory and randomization.\r\nIn light of this, we present
a novel overapproximation approach to synthesize strategies in an MDP, such that
a safety objective over the distributions is met. More precisely, we develop a
new framework for template-based synthesis of certificates as affine distributional
and inductive invariants for safety objectives in MDPs. We provide two algorithms
within this framework. One can only synthesize memoryless strategies, but has
relative completeness guarantees, while the other can synthesize general strategies.
The runtime complexity of both algorithms is in PSPACE. We implement these algorithms
and show that they can solve several non-trivial examples."
acknowledgement: This work was supported in part by the ERC CoG 863818 (FoRM-SMArt)
and the European Union’s Horizon 2020 research and innovation programme under the
Marie Skłodowska-Curie Grant Agreement No. 665385 as well as DST/CEFIPRA/INRIA project
EQuaVE and SERB Matrices grant MTR/2018/00074.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: S.
full_name: Akshay, S.
last_name: Akshay
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. MDPs as distribution transformers:
Affine invariant synthesis for safety objectives. In: International Conference
on Computer Aided Verification. Vol 13966. Springer Nature; 2023:86-112. doi:10.1007/978-3-031-37709-9_5'
apa: 'Akshay, S., Chatterjee, K., Meggendorfer, T., & Zikelic, D. (2023). MDPs
as distribution transformers: Affine invariant synthesis for safety objectives.
In International Conference on Computer Aided Verification (Vol. 13966,
pp. 86–112). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37709-9_5'
chicago: 'Akshay, S., Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic.
“MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.”
In International Conference on Computer Aided Verification, 13966:86–112.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37709-9_5.'
ieee: 'S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “MDPs as distribution
transformers: Affine invariant synthesis for safety objectives,” in International
Conference on Computer Aided Verification, Paris, France, 2023, vol. 13966,
pp. 86–112.'
ista: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution
transformers: Affine invariant synthesis for safety objectives. International
Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 13966, 86–112.'
mla: 'Akshay, S., et al. “MDPs as Distribution Transformers: Affine Invariant Synthesis
for Safety Objectives.” International Conference on Computer Aided Verification,
vol. 13966, Springer Nature, 2023, pp. 86–112, doi:10.1007/978-3-031-37709-9_5.'
short: S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International
Conference on Computer Aided Verification, Springer Nature, 2023, pp. 86–112.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-09-10T22:01:12Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2025-07-14T09:09:56Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37709-9_5
ec_funded: 1
file:
- access_level: open_access
checksum: f143c8eedf609f20f2aad2eeb496d53f
content_type: application/pdf
creator: dernst
date_created: 2023-09-20T08:46:43Z
date_updated: 2023-09-20T08:46:43Z
file_id: '14349'
file_name: 2023_LNCS_Akshay.pdf
file_size: 531745
relation: main_file
success: 1
file_date_updated: 2023-09-20T08:46:43Z
has_accepted_license: '1'
intvolume: ' 13966'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 86-112
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031377082'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'MDPs as distribution transformers: Affine invariant synthesis for safety objectives'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13966
year: '2023'
...
---
_id: '14318'
abstract:
- lang: eng
text: "Probabilistic recurrence relations (PRRs) are a standard formalism for describing
the runtime of a randomized algorithm. Given a PRR and a time limit κ, we consider
the tail probability Pr[T≥κ], i.e., the probability that the randomized runtime
T of the PRR exceeds κ. Our focus is the formal analysis of tail bounds that aims
at finding a tight asymptotic upper bound u≥Pr[T≥κ]. To address this problem,
the classical and most well-known approach is the cookbook method by Karp (JACM
1994), while other approaches are mostly limited to deriving tail bounds of specific
PRRs via involved custom analysis.\r\nIn this work, we propose a novel approach
for deriving the common exponentially-decreasing tail bounds for PRRs whose preprocessing
time and random passed sizes observe discrete or (piecewise) uniform distribution
and whose recursive call is either a single procedure call or a divide-and-conquer.
We first establish a theoretical approach via Markov’s inequality, and then instantiate
the theoretical approach with a template-based algorithmic approach via a refined
treatment of exponentiation. Experimental evaluation shows that our algorithmic
approach is capable of deriving tail bounds that are (i) asymptotically tighter
than Karp’s method, (ii) match the best-known manually-derived asymptotic tail
bound for QuickSelect, and (iii) is only slightly worse (with a loglogn factor)
than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover,
our algorithmic approach handles all examples (including realistic PRRs such as
QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1 s, showing
that our approach is efficient in practice."
acknowledgement: We thank Prof. Bican Xia for valuable information on the exponential
theory of reals. The work is partially supported by the National Natural Science
Foundation of China (NSFC) with Grant No. 62172271, ERC CoG 863818 (ForM-SMArt),
the Hong Kong Research Grants Council ECS Project Number 26208122, the HKUST-Kaisa
Joint Research Institute Project Grant HKJRI3A-055 and the HKUST Startup Grant R9272.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Yican
full_name: Sun, Yican
last_name: Sun
- first_name: Hongfei
full_name: Fu, Hongfei
last_name: Fu
- 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
citation:
ama: 'Sun Y, Fu H, Chatterjee K, Goharshady AK. Automated tail bound analysis for probabilistic
recurrence relations. In: Computer Aided Verification. Vol 13966. Springer
Nature; 2023:16-39. doi:10.1007/978-3-031-37709-9_2'
apa: 'Sun, Y., Fu, H., Chatterjee, K., & Goharshady, A. K. (2023). Automated
tail bound analysis for probabilistic recurrence relations. In Computer Aided
Verification (Vol. 13966, pp. 16–39). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37709-9_2'
chicago: Sun, Yican, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady.
“Automated Tail Bound Analysis for Probabilistic Recurrence Relations.” In Computer
Aided Verification, 13966:16–39. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37709-9_2.
ieee: Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Automated tail bound
analysis for probabilistic recurrence relations,” in Computer Aided Verification,
Paris, France, 2023, vol. 13966, pp. 16–39.
ista: 'Sun Y, Fu H, Chatterjee K, Goharshady AK. 2023. Automated tail bound analysis
for probabilistic recurrence relations. Computer Aided Verification. CAV: Computer
Aided Verification, LNCS, vol. 13966, 16–39.'
mla: Sun, Yican, et al. “Automated Tail Bound Analysis for Probabilistic Recurrence
Relations.” Computer Aided Verification, vol. 13966, Springer Nature, 2023,
pp. 16–39, doi:10.1007/978-3-031-37709-9_2.
short: Y. Sun, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Computer Aided Verification,
Springer Nature, 2023, pp. 16–39.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-09-10T22:01:12Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2025-07-14T09:09:57Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37709-9_2
ec_funded: 1
file:
- access_level: open_access
checksum: 42917e086f8c7699f3bccf84f74fe000
content_type: application/pdf
creator: dernst
date_created: 2023-09-20T08:24:47Z
date_updated: 2023-09-20T08:24:47Z
file_id: '14348'
file_name: 2023_LNCS_Sun.pdf
file_size: 624647
relation: main_file
success: 1
file_date_updated: 2023-09-20T08:24:47Z
has_accepted_license: '1'
intvolume: ' 13966'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 16-39
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031377082'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/boyvolcano/PRR
scopus_import: '1'
status: public
title: Automated tail bound analysis for probabilistic recurrence relations
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13966
year: '2023'
...
---
_id: '14410'
abstract:
- lang: eng
text: This paper focuses on the implementation details of the baseline methods and
a recent lightweight conditional model extrapolation algorithm LIMES [5] for streaming
data under class-prior shift. LIMES achieves superior performance over the baseline
methods, especially concerning the minimum-across-day accuracy, which is important
for the users of the system. In this work, the key measures to facilitate reproducibility
and enhance the credibility of the results are described.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Paulina
full_name: Tomaszewska, Paulina
last_name: Tomaszewska
- first_name: Christoph
full_name: Lampert, Christoph
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
citation:
ama: 'Tomaszewska P, Lampert C. On the implementation of baselines and lightweight
conditional model extrapolation (LIMES) under class-prior shift. In: International
Workshop on Reproducible Research in Pattern Recognition. Vol 14068. Springer
Nature; 2023:67-73. doi:10.1007/978-3-031-40773-4_6'
apa: 'Tomaszewska, P., & Lampert, C. (2023). On the implementation of baselines
and lightweight conditional model extrapolation (LIMES) under class-prior shift.
In International Workshop on Reproducible Research in Pattern Recognition
(Vol. 14068, pp. 67–73). Montreal, Canada: Springer Nature. https://doi.org/10.1007/978-3-031-40773-4_6'
chicago: Tomaszewska, Paulina, and Christoph Lampert. “On the Implementation of Baselines
and Lightweight Conditional Model Extrapolation (LIMES) under Class-Prior Shift.”
In International Workshop on Reproducible Research in Pattern Recognition,
14068:67–73. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-40773-4_6.
ieee: P. Tomaszewska and C. Lampert, “On the implementation of baselines and lightweight
conditional model extrapolation (LIMES) under class-prior shift,” in International
Workshop on Reproducible Research in Pattern Recognition, Montreal, Canada,
2023, vol. 14068, pp. 67–73.
ista: 'Tomaszewska P, Lampert C. 2023. On the implementation of baselines and lightweight
conditional model extrapolation (LIMES) under class-prior shift. International
Workshop on Reproducible Research in Pattern Recognition. RRPR: Reproducible Research
in Pattern Recognition, LNCS, vol. 14068, 67–73.'
mla: Tomaszewska, Paulina, and Christoph Lampert. “On the Implementation of Baselines
and Lightweight Conditional Model Extrapolation (LIMES) under Class-Prior Shift.”
International Workshop on Reproducible Research in Pattern Recognition,
vol. 14068, Springer Nature, 2023, pp. 67–73, doi:10.1007/978-3-031-40773-4_6.
short: P. Tomaszewska, C. Lampert, in:, International Workshop on Reproducible Research
in Pattern Recognition, Springer Nature, 2023, pp. 67–73.
conference:
end_date: 2022-08-21
location: Montreal, Canada
name: 'RRPR: Reproducible Research in Pattern Recognition'
start_date: 2022-08-21
date_created: 2023-10-08T22:01:18Z
date_published: 2023-08-20T00:00:00Z
date_updated: 2023-10-09T06:48:02Z
day: '20'
department:
- _id: ChLa
doi: 10.1007/978-3-031-40773-4_6
intvolume: ' 14068'
language:
- iso: eng
month: '08'
oa_version: None
page: 67-73
publication: International Workshop on Reproducible Research in Pattern Recognition
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031407727'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: On the implementation of baselines and lightweight conditional model extrapolation
(LIMES) under class-prior shift
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14068
year: '2023'
...
---
_id: '14411'
abstract:
- lang: eng
text: "Partially specified Boolean networks (PSBNs) represent a promising framework
for the qualitative modelling of biological systems in which the logic of interactions
is not completely known. Phenotype control aims to stabilise the network in states
exhibiting specific traits.\r\nIn this paper, we define the phenotype control
problem in the context of asynchronous PSBNs and propose a novel semi-symbolic
algorithm for solving this problem with permanent variable perturbations."
acknowledgement: This work was supported by the Czech Foundation grant No. GA22-10845S,
Grant Agency of Masaryk University grant No. MUNI/G/1771/2020, and the European
Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie
Grant Agreement No. 101034413.
alternative_title:
- LNBI
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
- first_name: Eva
full_name: Šmijáková, Eva
last_name: Šmijáková
citation:
ama: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. Phenotype control of partially
specified boolean networks. In: 21st International Conference on Computational
Methods in Systems Biology. Vol 14137. Springer Nature; 2023:18-35. doi:10.1007/978-3-031-42697-1_2'
apa: 'Beneš, N., Brim, L., Pastva, S., Šafránek, D., & Šmijáková, E. (2023).
Phenotype control of partially specified boolean networks. In 21st International
Conference on Computational Methods in Systems Biology (Vol. 14137, pp. 18–35).
Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-42697-1_2'
chicago: Beneš, Nikola, Luboš Brim, Samuel Pastva, David Šafránek, and Eva Šmijáková.
“Phenotype Control of Partially Specified Boolean Networks.” In 21st International
Conference on Computational Methods in Systems Biology, 14137:18–35. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-42697-1_2.
ieee: N. Beneš, L. Brim, S. Pastva, D. Šafránek, and E. Šmijáková, “Phenotype control
of partially specified boolean networks,” in 21st International Conference
on Computational Methods in Systems Biology, Luxembourg City, Luxembourg,
2023, vol. 14137, pp. 18–35.
ista: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. 2023. Phenotype control
of partially specified boolean networks. 21st International Conference on Computational
Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNBI,
vol. 14137, 18–35.'
mla: Beneš, Nikola, et al. “Phenotype Control of Partially Specified Boolean Networks.”
21st International Conference on Computational Methods in Systems Biology,
vol. 14137, Springer Nature, 2023, pp. 18–35, doi:10.1007/978-3-031-42697-1_2.
short: N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková, in:, 21st International
Conference on Computational Methods in Systems Biology, Springer Nature, 2023,
pp. 18–35.
conference:
end_date: 2023-09-15
location: Luxembourg City, Luxembourg
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2023-09-13
date_created: 2023-10-08T22:01:18Z
date_published: 2023-09-09T00:00:00Z
date_updated: 2024-02-20T09:02:04Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-42697-1_2
ec_funded: 1
file:
- access_level: open_access
checksum: 6f71bdaedb770b52380222fd9f4d7937
content_type: application/pdf
creator: spastva
date_created: 2024-02-16T08:26:32Z
date_updated: 2024-02-16T08:26:32Z
file_id: '14997'
file_name: cmsb2023.pdf
file_size: 691582
relation: main_file
success: 1
file_date_updated: 2024-02-16T08:26:32Z
has_accepted_license: '1'
intvolume: ' 14137'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 18-35
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 21st International Conference on Computational Methods in Systems Biology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031426964'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Phenotype control of partially specified boolean networks
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: 14137
year: '2023'
...
---
_id: '14428'
abstract:
- lang: eng
text: "Suppose we have two hash functions h1 and h2, but we trust the security of
only one of them. To mitigate this worry, we wish to build a hash combiner Ch1,h2
which is secure so long as one of the underlying hash functions is. This question
has been well-studied in the regime of collision resistance. In this case, concatenating
the two hash function outputs clearly works. Unfortunately, a long series of works
(Boneh and Boyen, CRYPTO’06; Pietrzak, Eurocrypt’07; Pietrzak, CRYPTO’08) showed
no (noticeably) shorter combiner for collision resistance is possible.\r\nIn this
work, we revisit this pessimistic state of affairs, motivated by the observation
that collision-resistance is insufficient for many interesting applications of
cryptographic hash functions anyway. We argue the right formulation of the “hash
combiner” is to build what we call random oracle (RO) combiners, utilizing stronger
assumptions for stronger constructions.\r\nIndeed, we circumvent the previous
lower bounds for collision resistance by constructing a simple length-preserving
RO combiner C˜h1,h2Z1,Z2(M)=h1(M,Z1)⊕h2(M,Z2),where Z1,Z2\r\n are random salts
of appropriate length. We show that this extra randomness is necessary for RO
combiners, and indeed our construction is somewhat tight with this lower bound.\r\nOn
the negative side, we show that one cannot generically apply the composition theorem
to further replace “monolithic” hash functions h1 and h2 by some simpler indifferentiable
construction (such as the Merkle-Damgård transformation) from smaller components,
such as fixed-length compression functions. Finally, despite this issue, we directly
prove collision resistance of the Merkle-Damgård variant of our combiner, where
h1 and h2 are replaced by iterative Merkle-Damgård hashes applied to a fixed-length
compression function. Thus, we can still subvert the concatenation barrier for
collision-resistance combiners while utilizing practically small fixed-length
components underneath."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Yevgeniy
full_name: Dodis, Yevgeniy
last_name: Dodis
- first_name: Niels
full_name: Ferguson, Niels
last_name: Ferguson
- first_name: Eli
full_name: Goldin, Eli
last_name: Goldin
- first_name: Peter
full_name: Hall, Peter
last_name: Hall
- 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: 'Dodis Y, Ferguson N, Goldin E, Hall P, Pietrzak KZ. Random oracle combiners:
Breaking the concatenation barrier for collision-resistance. In: 43rd Annual
International Cryptology Conference. Vol 14082. Springer Nature; 2023:514-546.
doi:10.1007/978-3-031-38545-2_17'
apa: 'Dodis, Y., Ferguson, N., Goldin, E., Hall, P., & Pietrzak, K. Z. (2023).
Random oracle combiners: Breaking the concatenation barrier for collision-resistance.
In 43rd Annual International Cryptology Conference (Vol. 14082, pp. 514–546).
Santa Barbara, CA, United States: Springer Nature. https://doi.org/10.1007/978-3-031-38545-2_17'
chicago: 'Dodis, Yevgeniy, Niels Ferguson, Eli Goldin, Peter Hall, and Krzysztof
Z Pietrzak. “Random Oracle Combiners: Breaking the Concatenation Barrier for Collision-Resistance.”
In 43rd Annual International Cryptology Conference, 14082:514–46. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-38545-2_17.'
ieee: 'Y. Dodis, N. Ferguson, E. Goldin, P. Hall, and K. Z. Pietrzak, “Random oracle
combiners: Breaking the concatenation barrier for collision-resistance,” in 43rd
Annual International Cryptology Conference, Santa Barbara, CA, United States,
2023, vol. 14082, pp. 514–546.'
ista: 'Dodis Y, Ferguson N, Goldin E, Hall P, Pietrzak KZ. 2023. Random oracle combiners:
Breaking the concatenation barrier for collision-resistance. 43rd Annual International
Cryptology Conference. CRYPTO: Advances in Cryptology, LNCS, vol. 14082, 514–546.'
mla: 'Dodis, Yevgeniy, et al. “Random Oracle Combiners: Breaking the Concatenation
Barrier for Collision-Resistance.” 43rd Annual International Cryptology Conference,
vol. 14082, Springer Nature, 2023, pp. 514–46, doi:10.1007/978-3-031-38545-2_17.'
short: Y. Dodis, N. Ferguson, E. Goldin, P. Hall, K.Z. Pietrzak, in:, 43rd Annual
International Cryptology Conference, Springer Nature, 2023, pp. 514–546.
conference:
end_date: 2023-08-24
location: Santa Barbara, CA, United States
name: 'CRYPTO: Advances in Cryptology'
start_date: 2023-08-20
date_created: 2023-10-15T22:01:11Z
date_published: 2023-08-09T00:00:00Z
date_updated: 2023-10-16T08:02:11Z
day: '09'
department:
- _id: KrPi
doi: 10.1007/978-3-031-38545-2_17
intvolume: ' 14082'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2023/1041
month: '08'
oa: 1
oa_version: Preprint
page: 514-546
publication: 43rd Annual International Cryptology Conference
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031385445'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Random oracle combiners: Breaking the concatenation barrier for collision-resistance'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14082
year: '2023'
...
---
_id: '14454'
abstract:
- lang: eng
text: As AI and machine-learned software are used increasingly for making decisions
that affect humans, it is imperative that they remain fair and unbiased in their
decisions. To complement design-time bias mitigation measures, runtime verification
techniques have been introduced recently to monitor the algorithmic fairness of
deployed systems. Previous monitoring techniques assume full observability of
the states of the (unknown) monitored system. Moreover, they can monitor only
fairness properties that are specified as arithmetic expressions over the probabilities
of different events. In this work, we extend fairness monitoring to systems modeled
as partially observed Markov chains (POMC), and to specifications containing arithmetic
expressions over the expected values of numerical functions on event sequences.
The only assumptions we make are that the underlying POMC is aperiodic and starts
in the stationary distribution, with a bound on its mixing time being known. These
assumptions enable us to estimate a given property for the entire distribution
of possible executions of the monitored POMC, by observing only a single execution.
Our monitors observe a long run of the system and, after each new observation,
output updated PAC-estimates of how fair or biased the system is. The monitors
are computationally lightweight and, using a prototype implementation, we demonstrate
their effectiveness on several real-world examples.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG 101020093.'
alternative_title:
- LNCS
article_processing_charge: No
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: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Henzinger TA, Kueffner K, Mallik K. Monitoring algorithmic fairness under
partial observations. In: 23rd International Conference on Runtime Verification.
Vol 14245. Springer Nature; 2023:291-311. doi:10.1007/978-3-031-44267-4_15'
apa: 'Henzinger, T. A., Kueffner, K., & Mallik, K. (2023). Monitoring algorithmic
fairness under partial observations. In 23rd International Conference on Runtime
Verification (Vol. 14245, pp. 291–311). Thessaloniki, Greece: Springer Nature.
https://doi.org/10.1007/978-3-031-44267-4_15'
chicago: Henzinger, Thomas A, Konstantin Kueffner, and Kaushik Mallik. “Monitoring
Algorithmic Fairness under Partial Observations.” In 23rd International Conference
on Runtime Verification, 14245:291–311. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_15.
ieee: T. A. Henzinger, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness
under partial observations,” in 23rd International Conference on Runtime Verification,
Thessaloniki, Greece, 2023, vol. 14245, pp. 291–311.
ista: 'Henzinger TA, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness
under partial observations. 23rd International Conference on Runtime Verification.
RV: Conference on Runtime Verification, LNCS, vol. 14245, 291–311.'
mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness under Partial
Observations.” 23rd International Conference on Runtime Verification, vol.
14245, Springer Nature, 2023, pp. 291–311, doi:10.1007/978-3-031-44267-4_15.
short: T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference
on Runtime Verification, Springer Nature, 2023, pp. 291–311.
conference:
end_date: 2023-10-06
location: Thessaloniki, Greece
name: 'RV: Conference on Runtime Verification'
start_date: 2023-10-03
date_created: 2023-10-29T23:01:15Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2023-10-31T11:48:20Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-031-44267-4_15
ec_funded: 1
external_id:
arxiv:
- '2308.00341'
intvolume: ' 14245'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2308.00341
month: '10'
oa: 1
oa_version: Preprint
page: 291-311
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 23rd International Conference on Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031442667'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring algorithmic fairness under partial observations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14245
year: '2023'
...