---
OA_type: closed access
_id: '20024'
abstract:
- lang: eng
text: 'Cooperative software verification divides the task of software verification
among several verification tools in order to increase efficiency and effectiveness.
The basic approach is to let verifiers work on different parts of a program and
at the end join verification results. While this idea is intuitively appealing,
cooperative verification is usually hindered by the fact that program decomposition
(1) is often static, disregarding strengths and weaknesses of employed verifiers,
and (2) often represents the decomposed program parts in a specific proprietary
format, thereby making the use of off-the-shelf verifiers in cooperative verification
difficult. In this paper, we propose a novel cooperative verification scheme that
we call dynamic program splitting (DPS). Splitting decomposes programs into (smaller)
programs, and thus directly enables the use of off-the-shelf tools. In DPS, splitting
is dynamically applied on demand: Verification starts by giving a verification
task (a program plus a correctness specification) to a verifier V1. Whenever V1
finds the current task to be hard to verify, it splits the task (i.e., the program)
and restarts verification on subtasks. DPS continues until (1) a violation is
found, (2) all subtasks are completed or (3) some user-defined stopping criterion
is met. In the latter case, the remaining uncompleted subtasks are merged into
a single one and are given to a next verifier V2, repeating the same procedure
on the still unverified program parts. This way, the decomposition is steered
by what is hard to verify for particular verifiers, leveraging their complementary
strengths. We have implemented dynamic program splitting and evaluated it on benchmarks
of the annual software verification competition SV-COMP. The evaluation shows
that cooperative verification with DPS is able to solve verification tasks that
none of the constituent verifiers can solve, without any significant overhead.'
acknowledgement: This work is partially supported by the German Research Foundation
(DFG) – WE2290/13-2 (Coop2), and in part by the ERC-2020-AdG 101020093.
article_processing_charge: No
author:
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Heike
full_name: Wehrheim, Heike
last_name: Wehrheim
citation:
ama: 'Richter C, Chalupa M, Jakobs M-C, Wehrheim H. Cooperative software verification
via dynamic program splitting. In: 47th International Conference on Software
Engineering. IEEE; 2025:2087-2099. doi:10.1109/ICSE55347.2025.00092'
apa: 'Richter, C., Chalupa, M., Jakobs, M.-C., & Wehrheim, H. (2025). Cooperative
software verification via dynamic program splitting. In 47th International
Conference on Software Engineering (pp. 2087–2099). Ottawa, ON, Canada: IEEE.
https://doi.org/10.1109/ICSE55347.2025.00092'
chicago: Richter, Cedric, Marek Chalupa, Marie-Christine Jakobs, and Heike Wehrheim.
“Cooperative Software Verification via Dynamic Program Splitting.” In 47th
International Conference on Software Engineering, 2087–99. IEEE, 2025. https://doi.org/10.1109/ICSE55347.2025.00092.
ieee: C. Richter, M. Chalupa, M.-C. Jakobs, and H. Wehrheim, “Cooperative software
verification via dynamic program splitting,” in 47th International Conference
on Software Engineering, Ottawa, ON, Canada, 2025, pp. 2087–2099.
ista: 'Richter C, Chalupa M, Jakobs M-C, Wehrheim H. 2025. Cooperative software
verification via dynamic program splitting. 47th International Conference on Software
Engineering. ICSE: International Conference on Software Engineering, 2087–2099.'
mla: Richter, Cedric, et al. “Cooperative Software Verification via Dynamic Program
Splitting.” 47th International Conference on Software Engineering, IEEE,
2025, pp. 2087–99, doi:10.1109/ICSE55347.2025.00092.
short: C. Richter, M. Chalupa, M.-C. Jakobs, H. Wehrheim, in:, 47th International
Conference on Software Engineering, IEEE, 2025, pp. 2087–2099.
conference:
end_date: 2025-05-06
location: Ottawa, ON, Canada
name: 'ICSE: International Conference on Software Engineering'
start_date: 2025-04-26
corr_author: '1'
date_created: 2025-07-16T11:32:29Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-09-30T14:01:55Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/ICSE55347.2025.00092
ec_funded: 1
external_id:
isi:
- '001538318100163'
isi: 1
language:
- iso: eng
month: '05'
oa_version: None
page: 2087-2099
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 47th International Conference on Software Engineering
publication_identifier:
eissn:
- 1558-1225
isbn:
- '9798331505691'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Cooperative software verification via dynamic program splitting
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2025'
...
---
OA_place: publisher
_id: '20147'
abstract:
- lang: eng
text: "Quantitative properties offer a framework for specifying and verifying system
behaviors beyond the traditional boolean perspective. For example, while a boolean
property may specify whether a server eventually grants every request it receives,
a quantitative one may map each server execution to its average response time.
This quantitative view is relatively well-studied in the context of static verification.
However, although such properties often appear in practice as performance or robustness
measures in a dynamic verification context, a general theoretical framework for
their analysis and classification from a monitoring perspective is still missing.\r\n\r\nIn
this thesis, we aim to develop such a framework that takes resource-precision
tradeoffs of monitors as a central consideration. We present the first theory
of monitorability for quantitative properties where monitors can be naturally
approximate and compared regarding their precision and resource use. In particular,
we show that additional monitor resources such as registers or states lead to
strictly better approximations for some properties. To enable such analyses in
a machine-model independent way, we describe an abstract notion of monitors that
can be instantiated with concrete models of monitors. Within this framework, we
study how abstract monitors behave and identify classes of properties amenable
to approximate monitoring with resource-precision considerations. We then extend
the boolean safety-liveness dichotomy and safety-progress hierarchy to the quantitative
setting with a monitoring perspective. In particular, we prove that every property
is the pointwise minimum of a safety property and a liveness property, and properties
that are both safe and co-safe can be approximately monitored arbitrarily precisely
using only finitely many states. We also study the classes of quantitative properties
definable by finite-state quantitative automata and provide algorithms for deciding
their safety or liveness as well as their safety-liveness decompositions. Finally,
we present the first general-purpose tool for automating the analysis, verification,
and monitoring of quantitative automata.\r\n\r\n--------------------------------------------------------------------------------------------------------------------------------------------------------------
In reference to IEEE copyrighted material which is used with permission in this
thesis, the IEEE does not\r\nendorse any of ISTA's products or services. Internal
or personal use of this\r\nmaterial is permitted. If interested in reprinting/republishing
IEEE copyrighted material for advertising or promotional\r\npurposes or for creating
new collective works for resale or redistribution, please go to\r\nhttp://www.ieee.org/publications_standards/publications/rights/rights_link.html
to learn how to obtain a License from\r\nRightsLink.\r\n"
acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF)\r\nunder
grant Z211-N23 (Wittgenstein Award) and the ERC-2020-AdG 101020093.\r\n"
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: Sarac NE. A monitoring-oriented theory and classification of quantitative specifications.
2025. doi:10.15479/AT-ISTA-20147
apa: Sarac, N. E. (2025). A monitoring-oriented theory and classification of
quantitative specifications. Institute of Science and Technology Austria.
https://doi.org/10.15479/AT-ISTA-20147
chicago: Sarac, Naci E. “A Monitoring-Oriented Theory and Classification of Quantitative
Specifications.” Institute of Science and Technology Austria, 2025. https://doi.org/10.15479/AT-ISTA-20147.
ieee: N. E. Sarac, “A monitoring-oriented theory and classification of quantitative
specifications,” Institute of Science and Technology Austria, 2025.
ista: Sarac NE. 2025. A monitoring-oriented theory and classification of quantitative
specifications. Institute of Science and Technology Austria.
mla: Sarac, Naci E. A Monitoring-Oriented Theory and Classification of Quantitative
Specifications. Institute of Science and Technology Austria, 2025, doi:10.15479/AT-ISTA-20147.
short: N.E. Sarac, A Monitoring-Oriented Theory and Classification of Quantitative
Specifications, Institute of Science and Technology Austria, 2025.
corr_author: '1'
date_created: 2025-08-07T15:57:57Z
date_published: 2025-08-07T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '07'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/AT-ISTA-20147
ec_funded: 1
file:
- access_level: closed
checksum: 0f3015f1db36576a23d8d669afb60b41
content_type: application/x-zip-compressed
creator: esarac
date_created: 2025-08-21T09:40:28Z
date_updated: 2025-09-10T08:19:51Z
file_id: '20200'
file_name: 2025_Sarac_NaciEge_Thesis.zip
file_size: 8884801
relation: source_file
- access_level: open_access
checksum: 332ed2fe61f580641664ec3f05d30f14
content_type: application/pdf
creator: esarac
date_created: 2025-08-21T09:40:34Z
date_updated: 2025-08-21T09:40:34Z
file_id: '20201'
file_name: 2025_Sarac_NaciEge_Thesis.pdf
file_size: 2955584
relation: main_file
success: 1
file_date_updated: 2025-09-10T08:19:51Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: '149'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '11775'
relation: part_of_dissertation
status: public
- id: '13140'
relation: part_of_dissertation
status: deleted
- id: '19741'
relation: part_of_dissertation
status: public
- id: '9356'
relation: part_of_dissertation
status: public
- id: '19643'
relation: part_of_dissertation
status: deleted
- id: '17634'
relation: part_of_dissertation
status: public
- id: '20342'
relation: part_of_dissertation
status: public
- id: '13221'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: A monitoring-oriented theory and classification of quantitative specifications
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: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '20186'
abstract:
- lang: eng
text: Enforcement of information-flow policies has been extensively studied by language-based
approaches over the past few decades. In this paper, we propose an alternative,
novel, general, and effective approach using enforcement of hyperproperties– a
powerful formalism for expressing and reasoning about a wide range of information-flow
security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties
expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer
has null, some, or complete information about the implementation of the system
under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce
the problem to controller synthesis for hyperproperties and subsequently to the
satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers
are transferable with low-overhead. We conduct a rich set of case studies, including
information-flow control for JavaScript code, as well as synthesizing obfuscators
for control plants.
acknowledgement: This project was funded in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018]
(ProbInG) and WWTF project ICT22-023 (TAIGER), National Science Foundation (NSF)
CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access
funding provided by Institute of Science and Technology (IST Austria).
article_number: '30'
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Tzu Han
full_name: Hsu, Tzu Han
last_name: Hsu
- first_name: Ana A
full_name: Oliveira Da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira Da Costa
- first_name: Andrew
full_name: Wintenberg, Andrew
last_name: Wintenberg
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Borzoo
full_name: Bonakdarpour, Borzoo
last_name: Bonakdarpour
citation:
ama: Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box
runtime enforcement of hyperproperties. Acta Informatica. 2025;62(3). doi:10.1007/s00236-025-00502-1
apa: Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., & Bonakdarpour,
B. (2025). Gray-box runtime enforcement of hyperproperties. Acta Informatica.
Springer Nature. https://doi.org/10.1007/s00236-025-00502-1
chicago: Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci,
and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” Acta
Informatica. Springer Nature, 2025. https://doi.org/10.1007/s00236-025-00502-1.
ieee: T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour,
“Gray-box runtime enforcement of hyperproperties,” Acta Informatica, vol.
62, no. 3. Springer Nature, 2025.
ista: Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025.
Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30.
mla: Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” Acta
Informatica, vol. 62, no. 3, 30, Springer Nature, 2025, doi:10.1007/s00236-025-00502-1.
short: T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour,
Acta Informatica 62 (2025).
corr_author: '1'
date_created: 2025-08-17T22:01:36Z
date_published: 2025-09-01T00:00:00Z
date_updated: 2025-09-30T14:20:11Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00236-025-00502-1
external_id:
isi:
- '001546115300001'
file:
- access_level: open_access
checksum: 90a43350fd4a8c5cb5b1b0e1aea7970d
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T05:53:47Z
date_updated: 2025-09-02T05:53:47Z
file_id: '20267'
file_name: 2025_ActaInformatica_Hsu.pdf
file_size: 6505049
relation: main_file
success: 1
file_date_updated: 2025-09-02T05:53:47Z
has_accepted_license: '1'
intvolume: ' 62'
isi: 1
issue: '3'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Gray-box runtime enforcement of hyperproperties
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 62
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20189'
abstract:
- lang: eng
text: Certification was made mandatory for the first time in the latest hardware
model checking competition. In this case study, we investigate the trade-offs
of requiring certificates for both passing and failing properties in the competition.
Our evaluation shows that participating model checkers were able to produce compact,
correct certificates that could be verified with minimal overhead. Furthermore,
the certifying winner of the competition outperforms the previous non-certifying
state-of-the-art model checker, demonstrating that certification can be adopted
without compromising model checking efficiency.
acknowledgement: "This work is supported in part by the ERC-2020-AdG 101020093, the
LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland
under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of
course also owe a big thank-you to the submitters of model checkers and benchmarks
to the competition over all these years. Without their enthusiasm and support neither
the competition nor this study would exist."
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
- first_name: Mathias
full_name: Preiner, Mathias
last_name: Preiner
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
- first_name: Keijo
full_name: Heljanko, Keijo
last_name: Heljanko
citation:
ama: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates
to the hardware model checking competition. In: 37th International Conference
on Computer Aided Verification. Vol 15931. Springer Nature; 2025:281-295.
doi:10.1007/978-3-031-98668-0_14'
apa: 'Froleyks, N., Yu, E., Preiner, M., Biere, A., & Heljanko, K. (2025). Introducing
certificates to the hardware model checking competition. In 37th International
Conference on Computer Aided Verification (Vol. 15931, pp. 281–295). Zagreb,
Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98668-0_14'
chicago: Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko.
“Introducing Certificates to the Hardware Model Checking Competition.” In 37th
International Conference on Computer Aided Verification, 15931:281–95. Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-98668-0_14.
ieee: N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates
to the hardware model checking competition,” in 37th International Conference
on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.
ista: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates
to the hardware model checking competition. 37th International Conference on Computer
Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.'
mla: Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking
Competition.” 37th International Conference on Computer Aided Verification,
vol. 15931, Springer Nature, 2025, pp. 281–95, doi:10.1007/978-3-031-98668-0_14.
short: N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International
Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.
conference:
end_date: 2025-07-25
location: Zagreb, Croatia
name: 'CAV: Computer Aided Verification'
start_date: 2025-07-23
date_created: 2025-08-17T22:01:36Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2025-12-01T12:34:05Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98668-0_14
ec_funded: 1
external_id:
isi:
- '001562507100014'
file:
- access_level: open_access
checksum: 15ec1bc9b9409d3b2736f4c9d5f42fd1
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T05:46:10Z
date_updated: 2025-09-02T05:46:10Z
file_id: '20266'
file_name: 2025_CAV_Froleyks.pdf
file_size: 1078274
relation: main_file
success: 1
file_date_updated: 2025-09-02T05:46:10Z
has_accepted_license: '1'
intvolume: ' 15931'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 281-295
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031986673'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Introducing certificates to the hardware model checking competition
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15931
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20225'
abstract:
- lang: eng
text: "We present the first supermartingale certificate for quantitative \r\n-regular
properties of discrete-time infinite-state stochastic systems. Our certificate
is defined on the product of the stochastic system and a limit-deterministic Büchi
automaton that specifies the property of interest; hence we call it a limit-deterministic
Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied
only to quantitative reachability, safety, or reach-avoid properties, and to qualitative
(i.e., probability 1) \r\n-regular properties.We also present fully automated
algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic
system dynamics and the controller can be represented in terms of polynomial inequalities.
Our experiments demonstrate the ability of our method to solve verification and
control tasks for stochastic systems that were beyond the reach of previous supermartingale-based
approaches."
acknowledgement: This work was supported in part by the Singapore Ministry of Education
(MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SIS-SMU-100) and
the ERC project ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Pouya
full_name: Sadeghi, Pouya
last_name: Sadeghi
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Henzinger TA, Mallik K, Sadeghi P, Zikelic D. Supermartingale certificates
for quantitative omega-regular verification and control. In: 37th International
Conference on Computer Aided Verification. Vol 15932. Springer Nature; 2025:29-55.
doi:10.1007/978-3-031-98679-6_2'
apa: 'Henzinger, T. A., Mallik, K., Sadeghi, P., & Zikelic, D. (2025). Supermartingale
certificates for quantitative omega-regular verification and control. In 37th
International Conference on Computer Aided Verification (Vol. 15932, pp. 29–55).
Zagreb, Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98679-6_2'
chicago: Henzinger, Thomas A, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic.
“Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.”
In 37th International Conference on Computer Aided Verification, 15932:29–55.
Springer Nature, 2025. https://doi.org/10.1007/978-3-031-98679-6_2.
ieee: T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates
for quantitative omega-regular verification and control,” in 37th International
Conference on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15932,
pp. 29–55.
ista: 'Henzinger TA, Mallik K, Sadeghi P, Zikelic D. 2025. Supermartingale certificates
for quantitative omega-regular verification and control. 37th International Conference
on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15932,
29–55.'
mla: Henzinger, Thomas A., et al. “Supermartingale Certificates for Quantitative
Omega-Regular Verification and Control.” 37th International Conference on Computer
Aided Verification, vol. 15932, Springer Nature, 2025, pp. 29–55, doi:10.1007/978-3-031-98679-6_2.
short: T.A. Henzinger, K. Mallik, P. Sadeghi, D. Zikelic, in:, 37th International
Conference on Computer Aided Verification, Springer Nature, 2025, pp. 29–55.
conference:
end_date: 2025-07-25
location: Zagreb, Croatia
name: 'CAV: Computer Aided Verification'
start_date: 2025-07-23
date_created: 2025-08-24T22:01:31Z
date_published: 2025-07-22T00:00:00Z
date_updated: 2025-12-01T12:34:41Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98679-6_2
ec_funded: 1
external_id:
arxiv:
- '2505.18833'
isi:
- '001562506600002'
file:
- access_level: open_access
checksum: beb1e2637de5b2268cc2262119439113
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T07:34:33Z
date_updated: 2025-09-02T07:34:33Z
file_id: '20272'
file_name: 2025_CAV_HenzingerT.pdf
file_size: 884831
relation: main_file
success: 1
file_date_updated: 2025-09-02T07:34:33Z
has_accepted_license: '1'
intvolume: ' 15932'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 29-55
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031986789'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Supermartingale certificates for quantitative omega-regular verification and control
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15932
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '20253'
abstract:
- lang: eng
text: "A quantitative word automaton (QWA) defines a function from infinite words
to values. For example, every infinite run of a limit-average QWA \U0001D49C obtains
a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained
by nondeterministic runs of \U0001D49C over w. We introduce quantitative language
automata (QLAs) that define functions from language generators (i.e., implementations)
to values, where a language generator can be nonprobabilistic, defining a set
of infinite words, or probabilistic, defining a probability measure over infinite
words. A QLA consists of a QWA and an aggregator function. For example, given
a QWA \U0001D49C, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest
lower bound assigned by \U0001D49C to any word in L. For boolean value sets, QWAs
define boolean properties of traces, and QLAs define boolean properties of sets
of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a
specification language for a generalization of hyperproperties, called quantitative
hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty
assigns a value to each set (resp. distribution) G of traces, e.g., the minimal
(resp. expected) average response time exhibited by the traces in G. We give several
examples of quantitative hyperproperties and investigate three paradigmatic problems
for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem,
given a QLA \U0001D538 and an implementation G, we ask for the value that \U0001D538
assigns to G. In the nonemptiness (resp. universality) problem, given a QLA \U0001D538
and a value k, we ask whether \U0001D538 assigns at least k to some (resp. every)
language. We provide a comprehensive picture of decidability for these problems
for QLAs with common aggregators as well as their restrictions to ω-regular languages
and trace distributions generated by finite-state Markov chains."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LIPIcs
article_number: '21'
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: Pavol
full_name: Kebis, Pavol
id: 2e0132b3-4e98-11ef-b275-cf7281c2802a
last_name: Kebis
- 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, Kebis P, Mazzocchi NA, Sarac NE. Quantitative language automata.
In: 36th International Conference on Concurrency Theory. Vol 348. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.CONCUR.2025.21'
apa: 'Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2025).
Quantitative language automata. In 36th International Conference on Concurrency
Theory (Vol. 348). Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2025.21'
chicago: Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E
Sarac. “Quantitative Language Automata.” In 36th International Conference on
Concurrency Theory, Vol. 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025. https://doi.org/10.4230/LIPIcs.CONCUR.2025.21.
ieee: T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Quantitative
language automata,” in 36th International Conference on Concurrency Theory,
Aarhus, Denmark, 2025, vol. 348.
ista: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2025. Quantitative language
automata. 36th International Conference on Concurrency Theory. CONCUR: Conference
on Concurrency Theory, LIPIcs, vol. 348, 21.'
mla: Henzinger, Thomas A., et al. “Quantitative Language Automata.” 36th International
Conference on Concurrency Theory, vol. 348, 21, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025, doi:10.4230/LIPIcs.CONCUR.2025.21.
short: T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 36th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025.
conference:
end_date: 2025-08-29
location: Aarhus, Denmark
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2025-08-26
corr_author: '1'
date_created: 2025-08-31T22:01:32Z
date_published: 2025-08-18T00:00:00Z
date_updated: 2025-12-01T12:36:52Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2025.21
ec_funded: 1
external_id:
arxiv:
- '2506.0515'
isi:
- '001570540800021'
file:
- access_level: open_access
checksum: 9d4054058757a73477e6015b10ed6996
content_type: application/pdf
creator: dernst
date_created: 2025-09-03T10:01:53Z
date_updated: 2025-09-03T10:01:53Z
file_id: '20282'
file_name: 2025_CONCUR_HenzingerT.pdf
file_size: 1257397
relation: main_file
success: 1
file_date_updated: 2025-09-03T10:01:53Z
has_accepted_license: '1'
intvolume: ' 348'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 36th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959773898'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative language automata
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: 348
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '20256'
abstract:
- lang: eng
text: We study the problem of predictive runtime monitoring of black-box dynamical
systems with quantitative safety properties. The black-box setting stipulates
that the exact semantics of the dynamical system and the controller are unknown,
and that we are only able to observe the state of the controlled (aka, closed-loop)
system at finitely many time points. We present a novel framework for predicting
future states of the system based on the states observed in the past. The numbers
of past states and of predicted future states are parameters provided by the user.
Our method is based on a combination of Taylor’s expansion and the backward difference
operator for numerical differentiation. We also derive an upper bound on the prediction
error under the assumption that the system dynamics and the controller are smooth.
The predicted states are then used to predict safety violations ahead in time.
Our experiments demonstrate practical applicability of our method for complex
black-box systems, showing that it is computationally lightweight and yet significantly
more accurate than the state-of-the-art predictive safety monitoring techniques.
acknowledgement: "This work was supported in part by the ERC project ERC-2020-AdG
101020093.\r\n"
alternative_title:
- PMLR
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: Fabian
full_name: Kresse, Fabian
id: faff3c84-23f6-11ef-9085-e5187b51c604
last_name: Kresse
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. Predictive monitoring of
black-box dynamical systems. In: 7th Annual Learning for Dynamics & Control
Conference. Vol 283. ML Research Press; 2025:804-816.'
apa: 'Henzinger, T. A., Kresse, F., Mallik, K., Yu, E., & Zikelic, D. (2025).
Predictive monitoring of black-box dynamical systems. In 7th Annual Learning
for Dynamics & Control Conference (Vol. 283, pp. 804–816). Ann Arbor,
MI, United States: ML Research Press.'
chicago: Henzinger, Thomas A, Fabian Kresse, Kaushik Mallik, Emily Yu, and Dorde
Zikelic. “Predictive Monitoring of Black-Box Dynamical Systems.” In 7th Annual
Learning for Dynamics & Control Conference, 283:804–16. ML Research Press,
2025.
ieee: T. A. Henzinger, F. Kresse, K. Mallik, E. Yu, and D. Zikelic, “Predictive
monitoring of black-box dynamical systems,” in 7th Annual Learning for Dynamics
& Control Conference, Ann Arbor, MI, United States, 2025, vol. 283, pp.
804–816.
ista: 'Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. 2025. Predictive monitoring
of black-box dynamical systems. 7th Annual Learning for Dynamics & Control
Conference. L4DC: Learning for Dynamics & Control, PMLR, vol. 283, 804–816.'
mla: Henzinger, Thomas A., et al. “Predictive Monitoring of Black-Box Dynamical
Systems.” 7th Annual Learning for Dynamics & Control Conference, vol.
283, ML Research Press, 2025, pp. 804–16.
short: T.A. Henzinger, F. Kresse, K. Mallik, E. Yu, D. Zikelic, in:, 7th Annual
Learning for Dynamics & Control Conference, ML Research Press, 2025, pp. 804–816.
conference:
end_date: 2025-06-06
location: Ann Arbor, MI, United States
name: 'L4DC: Learning for Dynamics & Control'
start_date: 2025-06-04
corr_author: '1'
date_created: 2025-08-31T22:01:32Z
date_published: 2025-06-01T00:00:00Z
date_updated: 2025-09-03T10:37:59Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: ChLa
ec_funded: 1
external_id:
arxiv:
- '2412.16564'
file:
- access_level: open_access
checksum: d5236e561560635f5ae1d17de4903033
content_type: application/pdf
creator: dernst
date_created: 2025-09-03T10:32:12Z
date_updated: 2025-09-03T10:32:12Z
file_id: '20283'
file_name: 2025_L4DC_HenzingerT.pdf
file_size: 489639
relation: main_file
success: 1
file_date_updated: 2025-09-03T10:32:12Z
has_accepted_license: '1'
intvolume: ' 283'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 804-816
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 7th Annual Learning for Dynamics & Control Conference
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Predictive monitoring of black-box dynamical systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 283
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '20290'
abstract:
- lang: eng
text: 'We consider equilibria in multiplayer stochastic graph games with terminal-node
rewards. In such games, Nash equilibria are defined assuming that each player
seeks to maximise their expected payoff, ignoring their aversion or tolerance
to risk. We therefore study risk-sensitive equilibria (RSEs), where the expected
payoff is replaced by a risk measure. A classical risk measure in the literature
is the entropic risk measure, where each player has a real valued parameter capturing
their risk-averseness. We introduce the extreme risk measure, which corresponds
to extreme cases of entropic risk measure, where players are either extreme optimists
or extreme pessimists. Under extreme risk measure, every player is an extremist:
an extreme optimist perceives their reward as the maximum payoff that can be achieved
with positive probability, while an extreme pessimist expects the minimum payoff
achievable with positive probability. We argue that the extreme risk measure,
especially in multi-player graph based settings, is particularly relevant as they
can model several real life instances such as interactions between secure systems
and potential security threats, or distributed controls for safety critical systems.
We prove that RSEs defined with the extreme risk measure are guaranteed to exist
when all rewards are non-negative. Furthermore, we prove that the problem of deciding
whether a given game contains an RSE that generates risk measures within specified
intervals is decidable and NP-complete for our extreme risk measure, and even
PTIME-complete when all players are extreme optimists, while that same problem
is undecidable using the entropic risk measure or even the classical expected
payoff. This establishes, to our knowledge, the first decidable fragment for equilibria
in simple stochastic games without restrictions on strategy types or number of
players.'
acknowledgement: "This work is a part of project VAMOS that has received funding from
the European\r\nResearch Council (ERC), grant agreement No 101020093. We thank anonymous
reviewers for pointing us to the Hurwicz criterion and to the work of Gallego-Hernández
and Mansutti [13]. We thank Marie van den Bogaard for her valuable feedback on the
first author’s PhD dissertation, which helped improve the quality of this work. "
alternative_title:
- LIPIcs
article_number: '30'
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Léonard
full_name: Brice, Léonard
last_name: Brice
- 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: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Brice L, Henzinger TA, Thejaswini KS. Finding equilibria: Simpler for pessimists,
simplest for optimists. In: 50th International Symposium on Mathematical Foundations
of Computer Science. Vol 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2025. doi:10.4230/LIPIcs.MFCS.2025.30'
apa: 'Brice, L., Henzinger, T. A., & Thejaswini, K. S. (2025). Finding equilibria:
Simpler for pessimists, simplest for optimists. In 50th International Symposium
on Mathematical Foundations of Computer Science (Vol. 345). Warsaw, Poland:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2025.30'
chicago: 'Brice, Léonard, Thomas A Henzinger, and K. S. Thejaswini. “Finding Equilibria:
Simpler for Pessimists, Simplest for Optimists.” In 50th International Symposium
on Mathematical Foundations of Computer Science, Vol. 345. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPIcs.MFCS.2025.30.'
ieee: 'L. Brice, T. A. Henzinger, and K. S. Thejaswini, “Finding equilibria: Simpler
for pessimists, simplest for optimists,” in 50th International Symposium on
Mathematical Foundations of Computer Science, Warsaw, Poland, 2025, vol. 345.'
ista: 'Brice L, Henzinger TA, Thejaswini KS. 2025. Finding equilibria: Simpler for
pessimists, simplest for optimists. 50th International Symposium on Mathematical
Foundations of Computer Science. MFCS: Mathematical Foundations of Computer Science,
LIPIcs, vol. 345, 30.'
mla: 'Brice, Léonard, et al. “Finding Equilibria: Simpler for Pessimists, Simplest
for Optimists.” 50th International Symposium on Mathematical Foundations of
Computer Science, vol. 345, 30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025, doi:10.4230/LIPIcs.MFCS.2025.30.'
short: L. Brice, T.A. Henzinger, K.S. Thejaswini, in:, 50th International Symposium
on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025.
conference:
end_date: 2025-08-29
location: Warsaw, Poland
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2025-08-25
corr_author: '1'
date_created: 2025-09-07T22:01:32Z
date_published: 2025-08-20T00:00:00Z
date_updated: 2025-09-08T07:15:40Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2025.30
ec_funded: 1
external_id:
arxiv:
- '2502.0531'
file:
- access_level: open_access
checksum: 9bc6b8e537662d371d2a27444cbc0b75
content_type: application/pdf
creator: dernst
date_created: 2025-09-08T07:11:12Z
date_updated: 2025-09-08T07:11:12Z
file_id: '20306'
file_name: 2025_MFCS_Brice.pdf
file_size: 1149694
relation: main_file
success: 1
file_date_updated: 2025-09-08T07:11:12Z
has_accepted_license: '1'
intvolume: ' 345'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 50th International Symposium on Mathematical Foundations of Computer
Science
publication_identifier:
isbn:
- '9783959773881'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Finding equilibria: Simpler for pessimists, simplest for optimists'
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: 345
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '20291'
abstract:
- lang: eng
text: "We define and study classes of ω-regular automata for which the nondeterminism
can be resolved by a policy that uses a combination of memory and randomness on
any input word, based solely on the prefix read so far. We examine two settings
for providing the input word to an automaton. In the first setting, called adversarial
resolvability, the input word is constructed letter-by-letter by an adversary,
dependent on the resolver’s previous decisions. In the second setting, called
stochastic resolvability, the adversary pre-commits to an infinite word and reveals
it letter-by-letter. In each setting, we require the existence of an almost-sure
resolver, i.e., a policy that ensures that as long as the adversary provides a
word in the language of the underlying nondeterministic automaton, the run constructed
by the policy is accepting with probability 1.\r\nThe class of automata that are
adversarially resolvable is the well-studied class of history-deterministic automata.
The case of stochastically resolvable automata, on the other hand, defines a novel
class. Restricting the class of resolvers in both settings to stochastic policies
without memory introduces two additional new classes of automata. We show that
the new automata classes offer interesting trade-offs between succinctness, expressivity,
and computational complexity, providing a fine gradation between deterministic
automata and nondeterministic automata."
acknowledgement: This work is a part of project VAMOS that has received funding from
the European Research Council (ERC), grant agreement No 101020093.
alternative_title:
- LIPIcs
article_number: '57'
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: Aditya
full_name: Prakash, Aditya
last_name: Prakash
- first_name: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Henzinger TA, Prakash A, Thejaswini KS. Resolving nondeterminism with randomness.
In: 50th International Symposium on Mathematical Foundations of Computer Science.
Vol 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.MFCS.2025.57'
apa: 'Henzinger, T. A., Prakash, A., & Thejaswini, K. S. (2025). Resolving nondeterminism
with randomness. In 50th International Symposium on Mathematical Foundations
of Computer Science (Vol. 345). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2025.57'
chicago: Henzinger, Thomas A, Aditya Prakash, and K. S. Thejaswini. “Resolving Nondeterminism
with Randomness.” In 50th International Symposium on Mathematical Foundations
of Computer Science, Vol. 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025. https://doi.org/10.4230/LIPIcs.MFCS.2025.57.
ieee: T. A. Henzinger, A. Prakash, and K. S. Thejaswini, “Resolving nondeterminism
with randomness,” in 50th International Symposium on Mathematical Foundations
of Computer Science, Warsaw, Poland, 2025, vol. 345.
ista: 'Henzinger TA, Prakash A, Thejaswini KS. 2025. Resolving nondeterminism with
randomness. 50th International Symposium on Mathematical Foundations of Computer
Science. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 345,
57.'
mla: Henzinger, Thomas A., et al. “Resolving Nondeterminism with Randomness.” 50th
International Symposium on Mathematical Foundations of Computer Science, vol.
345, 57, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:10.4230/LIPIcs.MFCS.2025.57.
short: T.A. Henzinger, A. Prakash, K.S. Thejaswini, in:, 50th International Symposium
on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025.
conference:
end_date: 2025-08-29
location: Warsaw, Poland
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2025-08-25
corr_author: '1'
date_created: 2025-09-07T22:01:32Z
date_published: 2025-08-20T00:00:00Z
date_updated: 2025-09-08T07:06:11Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2025.57
ec_funded: 1
external_id:
arxiv:
- '2502.12872'
file:
- access_level: open_access
checksum: 6068b772aba6cb0d01f3e5a90abed973
content_type: application/pdf
creator: dernst
date_created: 2025-09-08T06:56:56Z
date_updated: 2025-09-08T06:56:56Z
file_id: '20305'
file_name: 2025_MFCS_HenzingerT.pdf
file_size: 1009644
relation: main_file
success: 1
file_date_updated: 2025-09-08T06:56:56Z
has_accepted_license: '1'
intvolume: ' 345'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 50th International Symposium on Mathematical Foundations of Computer
Science
publication_identifier:
isbn:
- '9783959773881'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Resolving nondeterminism with randomness
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: 345
year: '2025'
...
---
OA_place: publisher
_id: '20292'
abstract:
- lang: eng
text: In automated decision-making, it is desirable that outputs of decision-makers
be robust to slight perturbations in their inputs, a property that may be called
input-output robustness. Input-output robustness appears in various different
forms in the literature, such as robustness of AI models to adversarial or semantic
perturbations and individual fairness of AI models that make decisions about humans.
We propose runtime monitoring of input-output robustness of deployed, black-box
AI models, where the goal is to design monitors that would observe one long execution
sequence of the model, and would raise an alarm whenever it is detected that two
similar inputs from the past led to dissimilar outputs. This way, monitoring will
complement existing offline ''robustification'' approaches to increase the trustworthiness
of AI decision-makers. We show that the monitoring problem can be cast as the
fixed-radius nearest neighbor (FRNN) search problem, which, despite being well-studied,
lacks suitable online solutions. We present our tool Clemont, which offers a number
of lightweight monitors, some of which use upgraded online variants of existing
FRNN algorithms, and one uses a novel algorithm based on binary decision diagrams--a
data-structure commonly used in software and hardware verification. We have also
developed an efficient parallelization technique that can substantially cut down
the computation time of monitors for which the distance between input-output pairs
is measured using the L∞norm. Using standard benchmarks from the literature of
adversarial and semantic robustness and individual fairness, we perform a comparative
study of different monitors in Clemont, and demonstrate their effectiveness in
correctly detecting robustness violations at runtime.
acknowledgement: This work was supported in part by the ERC project ERC-2020-AdG 101020093
and the SBI Foundation Hub for Data Science &Analytics, IIT Bombay.
article_processing_charge: No
arxiv: 1
author:
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- 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
- first_name: David
full_name: Pape, David
last_name: Pape
citation:
ama: 'Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. Monitoring robustness
and individual fairness. In: Proceedings of the 31st ACM SIGKDD Conference
on Knowledge Discovery and Data Mining. Vol 2. Association for Computing Machinery;
2025:790-801. doi:10.1145/3711896.3737054'
apa: 'Gupta, A., Henzinger, T. A., Kueffner, K., Mallik, K., & Pape, D. (2025).
Monitoring robustness and individual fairness. In Proceedings of the 31st ACM
SIGKDD Conference on Knowledge Discovery and Data Mining (Vol. 2, pp. 790–801).
Toronto, Canada: Association for Computing Machinery. https://doi.org/10.1145/3711896.3737054'
chicago: Gupta, Ashutosh, Thomas A Henzinger, Konstantin Kueffner, Kaushik Mallik,
and David Pape. “Monitoring Robustness and Individual Fairness.” In Proceedings
of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining,
2:790–801. Association for Computing Machinery, 2025. https://doi.org/10.1145/3711896.3737054.
ieee: A. Gupta, T. A. Henzinger, K. Kueffner, K. Mallik, and D. Pape, “Monitoring
robustness and individual fairness,” in Proceedings of the 31st ACM SIGKDD
Conference on Knowledge Discovery and Data Mining, Toronto, Canada, 2025,
vol. 2, pp. 790–801.
ista: 'Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. 2025. Monitoring robustness
and individual fairness. Proceedings of the 31st ACM SIGKDD Conference on Knowledge
Discovery and Data Mining. KDD: Conference on Knowledge Discovery and Data Mining
vol. 2, 790–801.'
mla: Gupta, Ashutosh, et al. “Monitoring Robustness and Individual Fairness.” Proceedings
of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining,
vol. 2, Association for Computing Machinery, 2025, pp. 790–801, doi:10.1145/3711896.3737054.
short: A. Gupta, T.A. Henzinger, K. Kueffner, K. Mallik, D. Pape, in:, Proceedings
of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining, Association
for Computing Machinery, 2025, pp. 790–801.
conference:
end_date: 2025-08-07
location: Toronto, Canada
name: 'KDD: Conference on Knowledge Discovery and Data Mining'
start_date: 2025-08-03
corr_author: '1'
date_created: 2025-09-07T22:01:33Z
date_published: 2025-08-03T00:00:00Z
date_updated: 2025-09-08T08:54:24Z
day: '03'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3711896.3737054
ec_funded: 1
external_id:
arxiv:
- '2506.00496'
file:
- access_level: open_access
checksum: 81e18cdf9ca5f6dfa79425b326ea9725
content_type: application/pdf
creator: dernst
date_created: 2025-09-08T08:46:31Z
date_updated: 2025-09-08T08:46:31Z
file_id: '20310'
file_name: 2025_KDD_Gupta.pdf
file_size: 7745940
relation: main_file
success: 1
file_date_updated: 2025-09-08T08:46:31Z
has_accepted_license: '1'
intvolume: ' 2'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 790-801
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery
and Data Mining
publication_identifier:
isbn:
- '9798400714542'
issn:
- 2154-817X
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/ariez-xyz/clemont
scopus_import: '1'
status: public
title: Monitoring robustness and individual 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2025'
...
---
OA_place: publisher
OA_type: diamond
_id: '20296'
abstract:
- lang: eng
text: Learning-based systems are increasingly deployed across various domains, yet
the complexity of traditional neural networks poses significant challenges for
formal verification. Unlike conventional neural networks, learned Logic Gate Networks
(LGNs) replace multiplications with Boolean logic gates, yielding a sparse, netlist-like
architecture that is inherently more amenable to symbolic verification, while
still delivering promising performance. In this paper, we introduce a SAT encoding
for verifying global robustness and fairness in LGNs. We evaluate our method on
five benchmark datasets, including a newly constructed 5-class variant, and find
that LGNs are both verification-friendly and maintain strong predictive performance.
acknowledged_ssus:
- _id: ScienComp
acknowledgement: "This work is supported in part by the ERC grant under Grant No.
ERC-2020-AdG 101020093 and\r\nthe Austrian Science Fund (FWF) [10.55776/COE12].
This research was supported by the Scientific\r\nService Units (SSU) of ISTA through
resources provided by Scientific Computing (SciComp)."
alternative_title:
- PMLR
article_number: '26'
article_processing_charge: No
arxiv: 1
author:
- first_name: Fabian
full_name: Kresse, Fabian
id: faff3c84-23f6-11ef-9085-e5187b51c604
last_name: Kresse
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
- first_name: Christoph
full_name: Lampert, Christoph
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
- 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: 'Kresse F, Yu E, Lampert C, Henzinger TA. Logic gate neural networks are good
for verification. In: 2nd International Conferenceon Neuro-Symbolic Systems.
Vol 288. ML Research Press; 2025.'
apa: 'Kresse, F., Yu, E., Lampert, C., & Henzinger, T. A. (2025). Logic gate
neural networks are good for verification. In 2nd International Conferenceon
Neuro-Symbolic Systems (Vol. 288). Philadephia, PA, United States: ML Research
Press.'
chicago: Kresse, Fabian, Emily Yu, Christoph Lampert, and Thomas A Henzinger. “Logic
Gate Neural Networks Are Good for Verification.” In 2nd International Conferenceon
Neuro-Symbolic Systems, Vol. 288. ML Research Press, 2025.
ieee: F. Kresse, E. Yu, C. Lampert, and T. A. Henzinger, “Logic gate neural networks
are good for verification,” in 2nd International Conferenceon Neuro-Symbolic
Systems, Philadephia, PA, United States, 2025, vol. 288.
ista: 'Kresse F, Yu E, Lampert C, Henzinger TA. 2025. Logic gate neural networks
are good for verification. 2nd International Conferenceon Neuro-Symbolic Systems.
NeuS: International Conferenceon Neuro-Symbolic Systems, PMLR, vol. 288, 26.'
mla: Kresse, Fabian, et al. “Logic Gate Neural Networks Are Good for Verification.”
2nd International Conferenceon Neuro-Symbolic Systems, vol. 288, 26, ML
Research Press, 2025.
short: F. Kresse, E. Yu, C. Lampert, T.A. Henzinger, in:, 2nd International Conferenceon
Neuro-Symbolic Systems, ML Research Press, 2025.
conference:
end_date: 2025-05-30
location: Philadephia, PA, United States
name: 'NeuS: International Conferenceon Neuro-Symbolic Systems'
start_date: 2025-05-28
corr_author: '1'
date_created: 2025-09-07T22:01:34Z
date_published: 2025-06-01T00:00:00Z
date_updated: 2025-09-09T08:12:44Z
day: '01'
ddc:
- '000'
department:
- _id: ChLa
- _id: ToHe
ec_funded: 1
external_id:
arxiv:
- '2505.19932'
file:
- access_level: open_access
checksum: 90a32defed34787e771a5c1623b6b0d2
content_type: application/pdf
creator: dernst
date_created: 2025-09-09T08:10:13Z
date_updated: 2025-09-09T08:10:13Z
file_id: '20314'
file_name: 2025_NeuS_Kresse.pdf
file_size: 295466
relation: main_file
success: 1
file_date_updated: 2025-09-09T08:10:13Z
has_accepted_license: '1'
intvolume: ' 288'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 2nd International Conferenceon Neuro-Symbolic Systems
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Logic gate neural networks are good for verification
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 288
year: '2025'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
PlanS_conform: '1'
_id: '20342'
abstract:
- lang: eng
text: Safety and liveness stand as fundamental concepts in formal languages, playing
a key role in verification. 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 the quantitative setting, properties are arbitrary functions from infinite
words to partially-ordered domains. Extending this paradigm to the quantitative
domain, where properties are arbitrary functions mapping infinite words to partially-ordered
domains, we introduce and study the notions of quantitative safety and liveness.
First, we formally define quantitative safety and liveness, and prove that our
definitions induce conservative quantitative generalizations of both the safety-progress
hierarchy and the safety-liveness decomposition of boolean properties. Consequently,
like their boolean counterparts, quantitative properties can be min-decomposed
into safety and liveness parts, or alternatively, max-decomposed into co-safety
and co-liveness parts. We further establish a connection between quantitative
safety and topological continuity and provide alternative characterizations of
quantitative safety and liveness in terms of their boolean analogs. Second, we
instantiate our framework with the specific classes of quantitative properties
expressed by automata. These quantitative automata contain finitely many states
and rational-valued transition weights, and their common value functions Inf,
Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the
totally-ordered domain of real numbers. For all common value functions, we provide
a procedure for deciding whether a given automaton is safe or live, we show how
to construct its safety closure, and we present a min-decomposition into safe
and live automata.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093 and
the Israel Science Foundation grant 2410/22. N. Mazzocchi was affiliated with ISTA
when this work was submitted for publication.
article_number: '13149'
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- 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: Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative
properties and automata. Logical Methods in Computer Science. 2025;21(2).
doi:10.46298/lmcs-21(2:2)2025
apa: Boker, U., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2025). Safety
and liveness of quantitative properties and automata. Logical Methods in Computer
Science. EPI Sciences. https://doi.org/10.46298/lmcs-21(2:2)2025
chicago: Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac.
“ Safety and Liveness of Quantitative Properties and Automata.” Logical Methods
in Computer Science. EPI Sciences, 2025. https://doi.org/10.46298/lmcs-21(2:2)2025.
ieee: U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “ Safety and
liveness of quantitative properties and automata,” Logical Methods in Computer
Science, vol. 21, no. 2. EPI Sciences, 2025.
ista: Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Safety and liveness
of quantitative properties and automata. Logical Methods in Computer Science.
21(2), 13149.
mla: Boker, Udi, et al. “ Safety and Liveness of Quantitative Properties and Automata.”
Logical Methods in Computer Science, vol. 21, no. 2, 13149, EPI Sciences,
2025, doi:10.46298/lmcs-21(2:2)2025.
short: U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, Logical Methods in
Computer Science 21 (2025).
corr_author: '1'
date_created: 2025-09-11T12:17:52Z
date_published: 2025-04-08T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '08'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.46298/lmcs-21(2:2)2025
ec_funded: 1
external_id:
arxiv:
- '2307.06016'
isi:
- '001468887900001'
file:
- access_level: open_access
checksum: 0b4d477bd981379724c35a4de2c176e5
content_type: application/pdf
creator: esarac
date_created: 2025-09-11T12:17:12Z
date_updated: 2025-09-11T12:17:12Z
file_id: '20343'
file_name: 2307.06016.pdf
file_size: 709584
relation: main_file
success: 1
file_date_updated: 2025-09-11T12:17:12Z
has_accepted_license: '1'
intvolume: ' 21'
isi: 1
issue: '2'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Logical Methods in Computer Science
publication_identifier:
eissn:
- 1860-5974
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
related_material:
record:
- id: '13221'
relation: earlier_version
status: public
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: ' Safety and liveness of quantitative properties and automata'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 21
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20723'
abstract:
- lang: eng
text: Information-flow interfaces is a formalism recently proposed for specifying,
composing, and refining system-wide security requirements. In this work, we show
how the widely used concept of security lattices provides a natural semantic interpretation
for information-flow interfaces.
acknowledgement: This project was funded in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe F8502 and by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-Flow
Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber
Physical Systems. Vol 15471. Cham: Springer Nature; 2025:251-263. doi:10.1007/978-3-031-97537-0_15'
apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A.
(2025). Information-Flow Interfaces and Security Lattices. In Engineering Safe
and Trustworthy Cyber Physical Systems (Vol. 15471, pp. 251–263). Cham: Springer
Nature. https://doi.org/10.1007/978-3-031-97537-0_15'
chicago: 'Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
Costa. “Information-Flow Interfaces and Security Lattices.” In Engineering
Safe and Trustworthy Cyber Physical Systems, 15471:251–63. Cham: Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-97537-0_15.'
ieee: 'E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-Flow
Interfaces and Security Lattices,” in Engineering Safe and Trustworthy Cyber
Physical Systems, vol. 15471, Cham: Springer Nature, 2025, pp. 251–263.'
ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.Information-Flow
Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber Physical
Systems. LNCS, vol. 15471, 251–263.'
mla: Bartocci, Ezio, et al. “Information-Flow Interfaces and Security Lattices.”
Engineering Safe and Trustworthy Cyber Physical Systems, vol. 15471, Springer
Nature, 2025, pp. 251–63, doi:10.1007/978-3-031-97537-0_15.
short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, Engineering
Safe and Trustworthy Cyber Physical Systems, Springer Nature, Cham, 2025, pp.
251–263.
corr_author: '1'
date_created: 2025-12-01T15:44:58Z
date_published: 2025-10-02T00:00:00Z
date_updated: 2025-12-09T07:57:55Z
day: '02'
department:
- _id: ToHe
doi: 10.1007/978-3-031-97537-0_15
ec_funded: 1
external_id:
arxiv:
- '2406.14374'
intvolume: ' 15471'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2406.14374
month: '10'
oa: 1
oa_version: Preprint
page: 251-263
place: Cham
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Engineering Safe and Trustworthy Cyber Physical Systems
publication_identifier:
eisbn:
- '9783031975370'
eissn:
- 1611-3349
isbn:
- '9783031975363'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Information-Flow Interfaces and Security Lattices
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15471
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '18169'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of runtime monitoring. Third-party and best-effort monitoring are
especially valuable, yet under-explored areas of runtime monitoring. In this context,
third-party monitoring means monitoring with a limited knowledge of the monitored
software (as it has been developed by a third party). Best-effort monitoring keeps
pace with the monitored software at the cost of possibly imprecise verdicts when
keeping up with the monitored software would not be feasible. Most existing monitoring
frameworks do not support the combination of third-party and best-effort monitoring
because they either require the full access to the monitored code or the ability
to process all observable events, or both.\r\nWe present a middleware framework,
Vamos, for the runtime monitoring of software. Vamos is explicitly designed to
support third-party and best-effort scenarios. The design goals of Vamos are (i)
efficiency (tracing events with low overhead), (ii) flexibility (the ability to
monitor a variety of different event channels, and to connect to a wide range
of monitors), 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 a set
of experiments demonstrating the usability of the scheme. The results indicate
that Vamos enables writing useful yet efficient monitors, 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 STTT reviewers for their valuable feedback and suggestions.
article_number: '103212'
article_processing_charge: Yes (via OA deal)
article_type: original
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. Science of Computer Programming. 2025;240(2). doi:10.1016/j.scico.2024.103212'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2025).
VAMOS: Middleware for best-effort third-party monitoring. Science of Computer
Programming. Elsevier. https://doi.org/10.1016/j.scico.2024.103212'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
“VAMOS: Middleware for Best-Effort Third-Party Monitoring.” Science of Computer
Programming. Elsevier, 2025. https://doi.org/10.1016/j.scico.2024.103212.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “VAMOS: Middleware
for best-effort third-party monitoring,” Science of Computer Programming,
vol. 240, no. 2. Elsevier, 2025.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2025. VAMOS: Middleware
for best-effort third-party monitoring. Science of Computer Programming. 240(2),
103212.'
mla: 'Chalupa, Marek, et al. “VAMOS: Middleware for Best-Effort Third-Party Monitoring.”
Science of Computer Programming, vol. 240, no. 2, 103212, Elsevier, 2025,
doi:10.1016/j.scico.2024.103212.'
short: M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, Science of Computer
Programming 240 (2025).
corr_author: '1'
date_created: 2024-10-06T22:01:10Z
date_published: 2025-02-01T00:00:00Z
date_updated: 2025-09-09T12:25:29Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.scico.2024.103212
ec_funded: 1
external_id:
isi:
- '001327852600001'
file:
- access_level: open_access
checksum: cd93c0c356e479ffccfbe8499b6ba8e2
content_type: application/pdf
creator: dernst
date_created: 2025-01-13T09:02:47Z
date_updated: 2025-01-13T09:02:47Z
file_id: '18831'
file_name: 2024_ScienceCompProg_Chalupa.pdf
file_size: 1173677
relation: main_file
success: 1
file_date_updated: 2025-01-13T09:02:47Z
has_accepted_license: '1'
intvolume: ' 240'
isi: 1
issue: '2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Science of Computer Programming
publication_identifier:
issn:
- 0167-6423
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '12856'
relation: earlier_version
status: public
scopus_import: '1'
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 240
year: '2025'
...
---
_id: '14400'
abstract:
- lang: eng
text: "We consider the problem of computing the maximal probability of satisfying
an \r\n-regular specification for stochastic, continuous-state, nonlinear systems
evolving in discrete time. The problem reduces, after automata-theoretic constructions,
to finding the maximal probability of satisfying a parity condition on a (possibly
hybrid) state space. While characterizing the exact satisfaction probability is
open, we show that a lower bound on this probability can be obtained by (I) computing
an under-approximation of the qualitative winning region, i.e., states from which
the parity condition can be enforced almost surely, and (II) computing the maximal
probability of reaching this qualitative winning region.\r\nThe heart of our approach
is a technique to symbolically compute the under-approximation of the qualitative
winning region in step (I) via a finite-state abstraction of the original system
as a \r\n-player parity game. Our abstraction procedure uses only the support
of the probabilistic evolution; it does not use precise numerical transition probabilities.
We prove that the winning set in the abstract -player game induces an under-approximation
of the qualitative winning region in the original synthesis problem, along with
a policy to solve it. By combining these contributions with (a) a symbolic fixpoint
algorithm to solve \r\n-player games and (b) existing techniques for reachability
policy synthesis in stochastic nonlinear systems, we get an abstraction-based
algorithm for finding a lower bound on the maximal satisfaction probability.\r\nWe
have implemented the abstraction-based algorithm in Mascot-SDS, where we combined
the outlined abstraction step with our tool Genie (Majumdar et al., 2023) that
solves \r\n-player parity games (through a reduction to Rabin games) more efficiently
than existing algorithms. We evaluated our implementation on the nonlinear model
of a perturbed bistable switch from the literature. We show empirically that the
lower bound on the winning region computed by our approach is precise, by comparing
against an over-approximation of the qualitative winning region. Moreover, our
implementation outperforms a recently proposed tool for solving this problem by
a large margin."
acknowledgement: "We thank Daniel Hausmann and Nir Piterman for their valuable comments
on an earlier version of the manuscript of our other paper [22] where we present,
among other things, the parity fixpoint for 2 1/2-player games (for a slightly more
general class of games) with a different and indirect proof of correctness. Based
on their comments we observed that, unlike the other fixpoints that we present in
[22], the parity fixpoint does not follow the exact same structure as its counterpart
for 2-player games, which we also use int his paper.\r\nWe also thank Thejaswini
Raghavan for observing that our symbolic parity fixpoint algorithm can be solved
in quasi-polynomial time using recent improved algorithms for solving \r\n-calculus
expressions. This significantly improved the complexity bounds of our algorithm
in this paper.\r\nThe work of R. Majumdar and A.-K. Schmuck are partially supported
by DFG, Germany project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded
through DFG, Germany project (SCHM 3541/1-1). K. Mallik is supported by the ERC
project ERC-2020-AdG 101020093. S. Soudjani is supported by the following projects:
EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047."
article_number: '101430'
article_processing_charge: Yes (in subscription journal)
article_type: original
arxiv: 1
author:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Anne Kathrin
full_name: Schmuck, Anne Kathrin
last_name: Schmuck
- first_name: Sadegh
full_name: Soudjani, Sadegh
last_name: Soudjani
citation:
ama: 'Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic
systems via finite parity games. Nonlinear Analysis: Hybrid Systems. 2024;51(2).
doi:10.1016/j.nahs.2023.101430'
apa: 'Majumdar, R., Mallik, K., Schmuck, A. K., & Soudjani, S. (2024). Symbolic
control for stochastic systems via finite parity games. Nonlinear Analysis:
Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2023.101430'
chicago: 'Majumdar, Rupak, Kaushik Mallik, Anne Kathrin Schmuck, and Sadegh Soudjani.
“Symbolic Control for Stochastic Systems via Finite Parity Games.” Nonlinear
Analysis: Hybrid Systems. Elsevier, 2024. https://doi.org/10.1016/j.nahs.2023.101430.'
ieee: 'R. Majumdar, K. Mallik, A. K. Schmuck, and S. Soudjani, “Symbolic control
for stochastic systems via finite parity games,” Nonlinear Analysis: Hybrid
Systems, vol. 51, no. 2. Elsevier, 2024.'
ista: 'Majumdar R, Mallik K, Schmuck AK, Soudjani S. 2024. Symbolic control for
stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems.
51(2), 101430.'
mla: 'Majumdar, Rupak, et al. “Symbolic Control for Stochastic Systems via Finite
Parity Games.” Nonlinear Analysis: Hybrid Systems, vol. 51, no. 2, 101430,
Elsevier, 2024, doi:10.1016/j.nahs.2023.101430.'
short: 'R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid
Systems 51 (2024).'
corr_author: '1'
date_created: 2023-10-08T22:01:15Z
date_published: 2024-02-01T00:00:00Z
date_updated: 2025-04-14T07:55:55Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2023.101430
ec_funded: 1
external_id:
arxiv:
- '2101.00834'
isi:
- '001093188100001'
file:
- access_level: open_access
checksum: 4eab70274d1004ea411f7f0e74c033ac
content_type: application/pdf
creator: dernst
date_created: 2024-07-16T10:26:41Z
date_updated: 2024-07-16T10:26:41Z
file_id: '17258'
file_name: 2024_NonlinearAnalysis_Majumdar.pdf
file_size: 1787569
relation: main_file
success: 1
file_date_updated: 2024-07-16T10:26:41Z
has_accepted_license: '1'
intvolume: ' 51'
isi: 1
issue: '2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_identifier:
issn:
- 1751-570X
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic control for stochastic systems via finite parity games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 51
year: '2024'
...
---
_id: '15321'
abstract:
- lang: eng
text: Boolean Networks (BNs) are widely used as a modeling formalism in several
domains, notably systems biology and computer science. A fundamental problem in
BN analysis is the enumeration of trap spaces, which are hypercubes in the state
space that cannot be escaped once entered. Several methods have been proposed
for enumerating trap spaces, however they often suffer from scalability and efficiency
issues, particularly for large and complex models. To our knowledge, the most
efficient and recent methods for the trap space enumeration all rely on Answer
Set Programming (ASP), which has been widely applied to the analysis of BNs. Motivated
by these considerations, our work proposes a new method for enumerating trap spaces
in BNs using ASP. We evaluate the method on a mix of 250+ real-world and 400+
randomly generated BNs, showing that it enables analysis of models beyond the
capabilities of existing tools (namely pyboolnet, mpbn, trappist, and trapmvn).
acknowledgement: This work was supported by Institut Carnot STAR, Marseille, France
and by the European Union’s Horizon 2020 research and innovation programme under
the Marie Skłodowska-Curie Grant Agreement No. 101034413.
article_processing_charge: No
author:
- first_name: Giang
full_name: Trinh, Giang
last_name: Trinh
- first_name: Belaid
full_name: Benhamou, Belaid
last_name: Benhamou
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: Sylvain
full_name: Soliman, Sylvain
last_name: Soliman
citation:
ama: 'Trinh G, Benhamou B, Pastva S, Soliman S. Scalable enumeration of trap spaces
in boolean networks via answer set programming. In: Proceedings of the 38th
AAAI Conference on Artificial Intelligence. Vol 38. Association for the Advancement
of Artificial Intelligence; 2024:10714-10722. doi:10.1609/aaai.v38i9.28943'
apa: Trinh, G., Benhamou, B., Pastva, S., & Soliman, S. (2024). Scalable enumeration
of trap spaces in boolean networks via answer set programming. In Proceedings
of the 38th AAAI Conference on Artificial Intelligence (Vol. 38, pp. 10714–10722).
Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v38i9.28943
chicago: Trinh, Giang, Belaid Benhamou, Samuel Pastva, and Sylvain Soliman. “Scalable
Enumeration of Trap Spaces in Boolean Networks via Answer Set Programming.” In
Proceedings of the 38th AAAI Conference on Artificial Intelligence, 38:10714–22.
Association for the Advancement of Artificial Intelligence, 2024. https://doi.org/10.1609/aaai.v38i9.28943.
ieee: G. Trinh, B. Benhamou, S. Pastva, and S. Soliman, “Scalable enumeration of
trap spaces in boolean networks via answer set programming,” in Proceedings
of the 38th AAAI Conference on Artificial Intelligence, 2024, vol. 38, no.
9, pp. 10714–10722.
ista: Trinh G, Benhamou B, Pastva S, Soliman S. 2024. Scalable enumeration of trap
spaces in boolean networks via answer set programming. Proceedings of the 38th
AAAI Conference on Artificial Intelligence. vol. 38, 10714–10722.
mla: Trinh, Giang, et al. “Scalable Enumeration of Trap Spaces in Boolean Networks
via Answer Set Programming.” Proceedings of the 38th AAAI Conference on Artificial
Intelligence, vol. 38, no. 9, Association for the Advancement of Artificial
Intelligence, 2024, pp. 10714–22, doi:10.1609/aaai.v38i9.28943.
short: G. Trinh, B. Benhamou, S. Pastva, S. Soliman, in:, Proceedings of the 38th
AAAI Conference on Artificial Intelligence, Association for the Advancement of
Artificial Intelligence, 2024, pp. 10714–10722.
date_created: 2024-04-14T22:01:02Z
date_published: 2024-03-25T00:00:00Z
date_updated: 2026-06-18T17:48:08Z
day: '25'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1609/aaai.v38i9.28943
ec_funded: 1
intvolume: ' 38'
issue: '9'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://amu.hal.science/hal-04523118/
month: '03'
oa: 1
oa_version: Published Version
page: 10714-10722
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Proceedings of the 38th AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- '1577358872'
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: Scalable enumeration of trap spaces in boolean networks via answer set programming
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 38
year: '2024'
...
---
_id: '15333'
abstract:
- lang: eng
text: BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts
that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed
for running combinations of verifiers in parallel. In contrast to BUBAAK, that
directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting
the input program into multiple modified versions called program splits. During
the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic
execution with a short timelimit) to analyze each generated program split. If
the weak verifier fails on a program split, we split this program split again
and start the verification process again on the generated program splits. We run
the splitting process until a predefined number of hard-to-verify program splits
is generated or a splitting limit is reached. During the main verification phase,
we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining
unsolved parts of the verification task.
acknowledgement: This work was partially supported by the ERC-2020-AdG 10102009 grant.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
citation:
ama: 'Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition
contribution). In: 30th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems. Vol 14572. Springer Nature; 2024:353–358.
doi:10.1007/978-3-031-57256-2_20'
apa: 'Chalupa, M., & Richter, C. (2024). Bubaak-SpLit: Split what you cannot
verify (Competition contribution). In 30th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (Vol. 14572, pp.
353–358). Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-57256-2_20'
chicago: 'Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot
Verify (Competition Contribution).” In 30th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, 14572:353–358.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-57256-2_20.'
ieee: 'M. Chalupa and C. Richter, “Bubaak-SpLit: Split what you cannot verify (Competition
contribution),” in 30th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems, Luxembourg City, Luxembourg, 2024,
vol. 14572, pp. 353–358.'
ista: 'Chalupa M, Richter C. 2024. Bubaak-SpLit: Split what you cannot verify (Competition
contribution). 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of Systems, LNCS, vol. 14572, 353–358.'
mla: 'Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify
(Competition Contribution).” 30th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, vol. 14572, Springer Nature,
2024, pp. 353–358, doi:10.1007/978-3-031-57256-2_20.'
short: M. Chalupa, C. Richter, in:, 30th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 353–358.
conference:
end_date: 2024-04-11
location: Luxembourg City, Luxembourg
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2024-04-06
corr_author: '1'
date_created: 2024-04-20T18:14:06Z
date_published: 2024-04-05T00:00:00Z
date_updated: 2025-09-04T13:48:25Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_20
ec_funded: 1
external_id:
isi:
- '001284187100020'
file:
- access_level: open_access
checksum: 208c855c60824bec936b8d01d0396474
content_type: application/pdf
creator: cchlebak
date_created: 2024-04-26T11:27:26Z
date_updated: 2024-04-26T11:27:26Z
file_id: '15347'
file_name: 2024_LNCS_Chalupa.pdf
file_size: 577128
relation: main_file
success: 1
file_date_updated: 2024-04-26T11:27:26Z
has_accepted_license: '1'
intvolume: ' 14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 353–358
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eisbn:
- '9783031572562'
eissn:
- 1611-3349
isbn:
- '9783031572555'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Bubaak-SpLit: Split what you cannot verify (Competition contribution)'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
_id: '15376'
abstract:
- lang: eng
text: Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory
objectives. Existing approaches are monolithic, where a single policy fulfills
all objectives. We present auction-based scheduling, a decentralized framework
for multi-objective sequential decision making. Each objective is fulfilled using
a separate and independent policy. Composition of policies is performed at runtime,
where at each step, the policies simultaneously bid from pre-allocated budgets
for the privilege of choosing the next action. The framework allows policies to
be independently created, modified, and replaced. We study path planning problems
on finite graphs with two temporal objectives and present algorithms to synthesize
policies together with bidding policies in a decentralized manner. We consider
three categories of decentralized synthesis problems, parameterized by the assumptions
that the policies make on each other. We identify a class of assumptions called
assume-admissible for which synthesis is always possible for graphs whose every
vertex has at most two outgoing edges.
acknowledgement: This work was supported in part by the ERC project ERC-2020-AdG 101020093
and by ISF grant no. 1679/21.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Suman
full_name: Sadhukhan, Suman
last_name: Sadhukhan
citation:
ama: 'Avni G, Mallik K, Sadhukhan S. Auction-based scheduling. In: 30th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 14572. Springer Nature; 2024:153-172. doi:10.1007/978-3-031-57256-2_8'
apa: 'Avni, G., Mallik, K., & Sadhukhan, S. (2024). Auction-based scheduling.
In 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 14572, pp. 153–172). Luxembourg City, Luxembourg:
Springer Nature. https://doi.org/10.1007/978-3-031-57256-2_8'
chicago: Avni, Guy, Kaushik Mallik, and Suman Sadhukhan. “Auction-Based Scheduling.”
In 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 14572:153–72. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-57256-2_8.
ieee: G. Avni, K. Mallik, and S. Sadhukhan, “Auction-based scheduling,” in 30th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 153–172.
ista: 'Avni G, Mallik K, Sadhukhan S. 2024. Auction-based scheduling. 30th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 14572, 153–172.'
mla: Avni, Guy, et al. “Auction-Based Scheduling.” 30th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, vol.
14572, Springer Nature, 2024, pp. 153–72, doi:10.1007/978-3-031-57256-2_8.
short: G. Avni, K. Mallik, S. Sadhukhan, in:, 30th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, Springer Nature,
2024, pp. 153–172.
conference:
end_date: 2024-04-11
location: Luxembourg City, Luxembourg
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2024-04-06
corr_author: '1'
date_created: 2024-05-12T22:01:02Z
date_published: 2024-04-05T00:00:00Z
date_updated: 2025-09-08T07:33:43Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_8
ec_funded: 1
external_id:
arxiv:
- '2310.11798'
isi:
- '001284187100008'
file:
- access_level: open_access
checksum: dbeb123510997886d11925aedbf9c400
content_type: application/pdf
creator: dernst
date_created: 2024-05-22T07:09:24Z
date_updated: 2024-05-22T07:09:24Z
file_id: '15414'
file_name: 2024_LNCS_Avni.pdf
file_size: 508191
relation: main_file
success: 1
file_date_updated: 2024-05-22T07:09:24Z
has_accepted_license: '1'
intvolume: ' 14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 153-172
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031572555'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Auction-based scheduling
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
_id: '15377'
abstract:
- lang: eng
text: "We provide an algorithmto solve Rabin and Streett games over graphs\r\nwith
n vertices,m edges, and k colours that runs in ˜O³mn(k!)1+o(1)´time and\r\nO(nk
logk logn) space, where ˜O hides poly-logarithmic factors. Our algorithm\r\nis
an improvement by a super quadratic dependence on k! from the currently\r\nbest
known run time of O³mn2(k!)2+o(1)´, obtained by converting a Rabin\r\ngameinto
a parity game,while simultaneously improving its exponential space\r\nrequirement.\r\nOur
main technical ingredient is a characterisation of progress measures for\r\nRabin
games using colourful trees and a combinatorial construction of succinctlyrepresented,\r\nuniversal
colourful trees. Colourful universal trees are generalisations\r\nof universal
trees used by Jurdzi´nski and Lazi´c (2017) to solve parity\r\ngames, as well
as of Rabin progress measures of Klarlund and Kozen (1991).\r\nOur algorithm for
Rabin games is a progress measure lifting algorithm where\r\nthe lifting is performed
on succinct, colourful, universal trees."
acknowledgement: This work is a part of the project VAMOS that has received funding
from the European Research Council (ERC) under the European Union’s Horizon 2020
research and innovation programme, grant agreements No 101020093. Rupak Majumdar
was partially supported by the DFG project 389792660 TRR 248-CPEC.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Irmak
full_name: Sağlam, Irmak
last_name: Sağlam
- first_name: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Majumdar R, Sağlam I, Thejaswini KS. Rabin games and colourful universal trees.
In: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. Vol 14572. Springer Nature; 2024:213-231. doi:10.1007/978-3-031-57256-2_11'
apa: Majumdar, R., Sağlam, I., & Thejaswini, K. S. (2024). Rabin games and colourful
universal trees. In 30th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (Vol. 14572, pp. 213–231). Springer
Nature. https://doi.org/10.1007/978-3-031-57256-2_11
chicago: Majumdar, Rupak, Irmak Sağlam, and K. S. Thejaswini. “Rabin Games and Colourful
Universal Trees.” In 30th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, 14572:213–31. Springer Nature,
2024. https://doi.org/10.1007/978-3-031-57256-2_11.
ieee: R. Majumdar, I. Sağlam, and K. S. Thejaswini, “Rabin games and colourful universal
trees,” in 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 2024, vol. 14572, pp. 213–231.
ista: Majumdar R, Sağlam I, Thejaswini KS. 2024. Rabin games and colourful universal
trees. 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. , LNCS, vol. 14572, 213–231.
mla: Majumdar, Rupak, et al. “Rabin Games and Colourful Universal Trees.” 30th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, vol. 14572, Springer Nature, 2024, pp. 213–31, doi:10.1007/978-3-031-57256-2_11.
short: R. Majumdar, I. Sağlam, K.S. Thejaswini, in:, 30th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, Springer
Nature, 2024, pp. 213–231.
corr_author: '1'
date_created: 2024-05-12T22:01:02Z
date_published: 2024-04-06T00:00:00Z
date_updated: 2025-09-08T07:34:49Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_11
ec_funded: 1
external_id:
arxiv:
- '2401.07548'
isi:
- '001284187100011'
file:
- access_level: open_access
checksum: 492be74f69cd6ea42d38681082d0b521
content_type: application/pdf
creator: dernst
date_created: 2024-05-22T07:24:45Z
date_updated: 2024-05-22T07:24:45Z
file_id: '15415'
file_name: 2024_LNCS_Majumdar.pdf
file_size: 462173
relation: main_file
success: 1
file_date_updated: 2024-05-22T07:24:45Z
has_accepted_license: '1'
intvolume: ' 14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 213-231
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031572555'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Rabin games and colourful universal trees
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '17053'
abstract:
- lang: eng
text: We introduce a formalization of ternary simulation as abstract interpretation
along with a widening operator to speed up convergence. With the same goal, we
present a subsumption algorithm that can determine termination earlier than the
usual approach using hash sets. Additionally, we introduce a narrowing operator
that utilizes recent advances in backbone extraction, allowing to increase the
overapproximation precision in simulation at any time. The experiments evaluate
the presented techniques in the context of hardware model checking.
acknowledgement: This work is supported by the Austrian Science Fund (FWF) under the
project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG
101020093 and by a gift from Intel Corporation.
article_processing_charge: No
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
citation:
ama: 'Froleyks N, Yu E, Biere A. Ternary simulation as abstract interpretation (Work
in Progress). In: 27th Workshop on Methods and Description Languages for Modeling
and Verification of Circuits and Systems. ; 2024:148-151.'
apa: Froleyks, N., Yu, E., & Biere, A. (2024). Ternary simulation as abstract
interpretation (Work in Progress). In 27th Workshop on Methods and Description
Languages for Modeling and Verification of Circuits and Systems (pp. 148–151).
Kaiserslautern, Germany.
chicago: Froleyks, Nils, Emily Yu, and Armin Biere. “Ternary Simulation as Abstract
Interpretation (Work in Progress).” In 27th Workshop on Methods and Description
Languages for Modeling and Verification of Circuits and Systems, 148–51, 2024.
ieee: N. Froleyks, E. Yu, and A. Biere, “Ternary simulation as abstract interpretation
(Work in Progress),” in 27th Workshop on Methods and Description Languages
for Modeling and Verification of Circuits and Systems, Kaiserslautern, Germany,
2024, pp. 148–151.
ista: 'Froleyks N, Yu E, Biere A. 2024. Ternary simulation as abstract interpretation
(Work in Progress). 27th Workshop on Methods and Description Languages for Modeling
and Verification of Circuits and Systems. MBMV: Methods and Description Languages
for Modeling and Verification of Circuits and Systems, 148–151.'
mla: Froleyks, Nils, et al. “Ternary Simulation as Abstract Interpretation (Work
in Progress).” 27th Workshop on Methods and Description Languages for Modeling
and Verification of Circuits and Systems, 2024, pp. 148–51.
short: N. Froleyks, E. Yu, A. Biere, in:, 27th Workshop on Methods and Description
Languages for Modeling and Verification of Circuits and Systems, 2024, pp. 148–151.
conference:
end_date: 2024-02-15
location: Kaiserslautern, Germany
name: 'MBMV: Methods and Description Languages for Modeling and Verification of
Circuits and Systems'
start_date: 2024-02-14
date_created: 2024-05-26T22:00:58Z
date_published: 2024-02-01T00:00:00Z
date_updated: 2026-01-05T14:05:35Z
day: '01'
department:
- _id: ToHe
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://cca.informatik.uni-freiburg.de/papers/FroleyksYuBiere-MBMV24.pdf
month: '02'
oa: 1
oa_version: Submitted Version
page: 148-151
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 27th Workshop on Methods and Description Languages for Modeling and Verification
of Circuits and Systems
publication_identifier:
isbn:
- '9783800762682'
publication_status: published
quality_controlled: '1'
scopus_import: '1'
status: public
title: Ternary simulation as abstract interpretation (Work in Progress)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2024'
...