---
_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
license: https://creativecommons.org/licenses/by/4.0/
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'
...
---
_id: '17327'
abstract:
- lang: eng
text: Sequential decision-making in probabilistic environments is a fundamental
problem with many applications in AI and economics. In this paper, we present
an algorithm for synthesizing sequential decision-making agents that optimize
statistical properties such as maximum and average response times. In the general
setting of sequential decision-making, the environment is modeled as a random
process that generates inputs. The agent responds to each input, aiming to maximize
rewards and minimize costs within a specified time horizon. The corresponding
synthesis problem is known to be PSPACE-hard. We consider the special case where
the input distribution, reward, and cost depend on input-output statistics specified
by counter automata. For such problems, this paper presents the first PTIME synthesis
algorithms. We introduce the notion of statistical abstraction, which clusters
statistically indistinguishable input-output sequences into equivalence classes.
This abstraction allows for a dynamic programming algorithm whose complexity grows
polynomially with the considered horizon, making the statistical case exponentially
more efficient than the general case. We evaluate our algorithm on three different
application scenarios of a client-server protocol, where multiple clients compete
via bidding to gain access to the service offered by the server. The synthesized
policies optimize profit while guaranteeing that none of the server’s clients
is disproportionately starved of the service.
acknowledgement: "This work is partly supported by the European Research Council under
Grant No.: ERC2020-AdG 101020093. It is also partially supported by the State Government
of Styria, Austria –\r\nDepartment Zukunftsfonds Steiermark."
alternative_title:
- LIPIcs
article_number: '2'
article_processing_charge: Yes
author:
- first_name: Filip
full_name: Cano, Filip
last_name: Cano
- 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: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Cano F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. Abstraction-based
decision making for statistical properties. In: 9th International Conference
on Formal Structures for Computation and Deduction. Vol 299. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.FSCD.2024.2'
apa: 'Cano, F., Henzinger, T. A., Könighofer, B., Kueffner, K., & Mallik, K.
(2024). Abstraction-based decision making for statistical properties. In 9th
International Conference on Formal Structures for Computation and Deduction
(Vol. 299). Tallinn, Estonia: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.FSCD.2024.2'
chicago: Cano, Filip, Thomas A Henzinger, Bettina Könighofer, Konstantin Kueffner,
and Kaushik Mallik. “Abstraction-Based Decision Making for Statistical Properties.”
In 9th International Conference on Formal Structures for Computation and Deduction,
Vol. 299. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. https://doi.org/10.4230/LIPIcs.FSCD.2024.2.
ieee: F. Cano, T. A. Henzinger, B. Könighofer, K. Kueffner, and K. Mallik, “Abstraction-based
decision making for statistical properties,” in 9th International Conference
on Formal Structures for Computation and Deduction, Tallinn, Estonia, 2024,
vol. 299.
ista: 'Cano F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. 2024. Abstraction-based
decision making for statistical properties. 9th International Conference on Formal
Structures for Computation and Deduction. FSCD: Conference on Formal Structures
for Computation and Deduction, LIPIcs, vol. 299, 2.'
mla: Cano, Filip, et al. “Abstraction-Based Decision Making for Statistical Properties.”
9th International Conference on Formal Structures for Computation and Deduction,
vol. 299, 2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:10.4230/LIPIcs.FSCD.2024.2.
short: F. Cano, T.A. Henzinger, B. Könighofer, K. Kueffner, K. Mallik, in:, 9th
International Conference on Formal Structures for Computation and Deduction, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
conference:
end_date: 2024-07-13
location: Tallinn, Estonia
name: 'FSCD: Conference on Formal Structures for Computation and Deduction'
start_date: 2024-07-10
corr_author: '1'
date_created: 2024-07-28T22:01:09Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2025-12-02T13:43:50Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.FSCD.2024.2
ec_funded: 1
external_id:
isi:
- '001587746100002'
file:
- access_level: open_access
checksum: cc6bb89be0eaa404a6ce019392cd293e
content_type: application/pdf
creator: dernst
date_created: 2024-07-29T11:15:59Z
date_updated: 2024-07-29T11:15:59Z
file_id: '17341'
file_name: 2024_LIPICs_Cano.pdf
file_size: 1391381
relation: main_file
success: 1
file_date_updated: 2024-07-29T11:15:59Z
has_accepted_license: '1'
intvolume: ' 299'
isi: 1
language:
- iso: eng
month: '07'
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: 9th International Conference on Formal Structures for Computation and
Deduction
publication_identifier:
isbn:
- '9783959773232'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstraction-based decision making for statistical properties
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: 299
year: '2024'
...
---
_id: '17413'
abstract:
- lang: eng
text: Certification helps to increase trust in formal verification of safety-critical
systems which require assurance on their correctness. In hardware model checking,
a widely used formal verification technique, phase abstraction is considered one
of the most commonly used preprocessing techniques. We present an approach to
certify an extended form of phase abstraction using a generic certificate format.
As in earlier works our approach involves constructing a witness circuit with
an inductive invariant property that certifies the correctness of the entire model
checking process, which is then validated by an independent certificate checker.
We have implemented and evaluated the proposed approach including certification
for various preprocessing configurations on hardware model checking competition
benchmarks. As an improvement on previous work in this area, the proposed method
is able to efficiently complete certification with an overhead of a fraction of
model checking time.
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, the Academy of Finland under the project 336092 and by a gift from Intel
Corporation.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
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
- 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, Biere A, Heljanko K. Certifying phase abstraction. In: Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics). Vol 14739. Springer Nature; 2024:284-303.
doi:10.1007/978-3-031-63498-7_17'
apa: 'Froleyks, N., Yu, E., Biere, A., & Heljanko, K. (2024). Certifying phase
abstraction. In Lecture Notes in Computer Science (including subseries Lecture
Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol.
14739, pp. 284–303). Nancy, France: Springer Nature. https://doi.org/10.1007/978-3-031-63498-7_17'
chicago: Froleyks, Nils, Emily Yu, Armin Biere, and Keijo Heljanko. “Certifying
Phase Abstraction.” In Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
14739:284–303. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-63498-7_17.
ieee: N. Froleyks, E. Yu, A. Biere, and K. Heljanko, “Certifying phase abstraction,”
in Lecture Notes in Computer Science (including subseries Lecture Notes in
Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France,
2024, vol. 14739, pp. 284–303.
ista: 'Froleyks N, Yu E, Biere A, Heljanko K. 2024. Certifying phase abstraction.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics). IJCAR: International Joint
Conference on Automated Reasoning, LNCS, vol. 14739, 284–303.'
mla: Froleyks, Nils, et al. “Certifying Phase Abstraction.” Lecture Notes in
Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 14739, Springer Nature, 2024, pp.
284–303, doi:10.1007/978-3-031-63498-7_17.
short: N. Froleyks, E. Yu, A. Biere, K. Heljanko, in:, Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), Springer Nature, 2024, pp. 284–303.
conference:
end_date: 2024-07-06
location: Nancy, France
name: 'IJCAR: International Joint Conference on Automated Reasoning'
start_date: 2024-07-03
date_created: 2024-08-11T22:01:13Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2025-09-08T08:49:53Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-63498-7_17
ec_funded: 1
external_id:
arxiv:
- '2405.04297'
isi:
- '001273489700017'
file:
- access_level: open_access
checksum: 7d7839fc8c5c680ea3ac09f40a66e55d
content_type: application/pdf
creator: dernst
date_created: 2024-08-12T06:53:39Z
date_updated: 2024-08-12T06:53:39Z
file_id: '17414'
file_name: 2024_LNCS_Froleyks.pdf
file_size: 556902
relation: main_file
success: 1
file_date_updated: 2024-08-12T06:53:39Z
has_accepted_license: '1'
intvolume: ' 14739'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 284-303
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031634970'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Certifying phase abstraction
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: 14739
year: '2024'
...
---
APC_amount: 2748 EUR
OA_place: publisher
OA_type: hybrid
_id: '17634'
abstract:
- lang: eng
text: System behaviors are traditionally evaluated through binary classifications
of correctness, which do not suffice for properties involving quantitative aspects
of systems and executions. Quantitative automata offer a more nuanced approach,
mapping each execution to a real number by incorporating weighted transitions
and value functions generalizing acceptance conditions. In this paper, we introduce
QuAK, the first tool designed to automate the analysis of quantitative automata.
QuAK currently supports a variety of quantitative automaton types, including Inf,
Sup, LimInf, LimSup, LimInfAvg, and LimSupAvg automata, and implements decision
procedures for problems such as emptiness, universality, inclusion, equivalence,
as well as for checking whether an automaton is safe, live, or constant. Additionally,
QuAK is able to compute extremal values when possible, construct safety-liveness
decompositions, and monitor system behaviors. We demonstrate the effectiveness
of QuAK through experiments focusing on the inclusion, constant-function check,
and monitoring problems.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. N.
Mazzocchi was affiliated with ISTA when his collaboration started.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- 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: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata
Kit. In: 12th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation. Vol 15222. Springer Nature; 2024:3-20.
doi:10.1007/978-3-031-75387-9_1'
apa: 'Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2024).
QuAK: Quantitative Automata Kit. In 12th International Symposium on Leveraging
Applications of Formal Methods, Verification and Validation (Vol. 15222, pp.
3–20). Crete, Greece: Springer Nature. https://doi.org/10.1007/978-3-031-75387-9_1'
chicago: 'Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci
E Sarac. “QuAK: Quantitative Automata Kit.” In 12th International Symposium
on Leveraging Applications of Formal Methods, Verification and Validation,
15222:3–20. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-75387-9_1.'
ieee: 'M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “QuAK: Quantitative
Automata Kit,” in 12th International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation, Crete, Greece, 2024, vol. 15222,
pp. 3–20.'
ista: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2024. QuAK: Quantitative
Automata Kit. 12th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation. ISoLA: International Symposium on Leveraging
Applications, LNCS, vol. 15222, 3–20.'
mla: 'Chalupa, Marek, et al. “QuAK: Quantitative Automata Kit.” 12th International
Symposium on Leveraging Applications of Formal Methods, Verification and Validation,
vol. 15222, Springer Nature, 2024, pp. 3–20, doi:10.1007/978-3-031-75387-9_1.'
short: M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 12th International
Symposium on Leveraging Applications of Formal Methods, Verification and Validation,
Springer Nature, 2024, pp. 3–20.
conference:
end_date: 2024-10-31
location: Crete, Greece
name: 'ISoLA: International Symposium on Leveraging Applications'
start_date: 2024-10-27
corr_author: '1'
date_created: 2024-09-05T14:27:08Z
date_published: 2024-10-26T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '26'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-75387-9_1
ec_funded: 1
external_id:
arxiv:
- '2409.03569'
isi:
- '001419008700001'
file:
- access_level: open_access
checksum: 43e432f82be376434b358f3dd7a94b71
content_type: application/pdf
creator: esarac
date_created: 2024-09-05T14:26:02Z
date_updated: 2024-09-05T14:26:02Z
file_id: '17635'
file_name: isola24.pdf
file_size: 847422
relation: main_file
success: 1
- access_level: open_access
checksum: 6bc04f07bb5612c0e7ea00ac121a69b6
content_type: application/pdf
creator: dernst
date_created: 2025-01-21T14:39:49Z
date_updated: 2025-01-21T14:39:49Z
file_id: '18865'
file_name: 2024_LNCS_Chalupa.pdf
file_size: 1358706
relation: main_file
success: 1
file_date_updated: 2025-01-21T14:39:49Z
has_accepted_license: '1'
intvolume: ' 15222'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 3-20
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 12th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031753862'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'QuAK: Quantitative Automata Kit'
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: 15222
year: '2024'
...
---
_id: '14076'
abstract:
- lang: eng
text: Hyperproperties are properties that relate multiple execution traces. Previous
work on monitoring hyperproperties focused on synchronous hyperproperties, usually
specified in HyperLTL. When monitoring synchronous hyperproperties, all traces
are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers
and show how to use them for monitoring synchronous as well as, for the first
time, asynchronous hyperproperties. Prefix transducers map multiple input traces
into one or more output traces by incrementally matching prefixes of the input
traces against expressions similar to regular expressions. The prefixes of different
traces which are consumed by a single matching step of the monitor may have different
lengths. The deterministic and executable nature of prefix transducers makes them
more suitable as an intermediate formalism for runtime verification than logical
specifications, which tend to be highly non-deterministic, especially in the case
of asynchronous hyperproperties. We report on a set of experiments about monitoring
asynchronous version of observational determinism.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
authors would like to thank Ana Oliveira da Costa for commenting on a draft of the
paper.
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers.
In: 23nd International Conference on Runtime Verification. Vol 14245. Springer
Nature; 2023:168-190. doi:10.1007/978-3-031-44267-4_9'
apa: 'Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with
prefix transducers. In 23nd International Conference on Runtime Verification
(Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. https://doi.org/10.1007/978-3-031-44267-4_9'
chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with
Prefix Transducers.” In 23nd International Conference on Runtime Verification,
14245:168–90. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_9.
ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,”
in 23nd International Conference on Runtime Verification, Thessaloniki,
Greek, 2023, vol. 14245, pp. 168–190.
ista: 'Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers.
23nd International Conference on Runtime Verification. RV: Conference on Runtime
Verification, LNCS, vol. 14245, 168–190.'
mla: Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix
Transducers.” 23nd International Conference on Runtime Verification, vol.
14245, Springer Nature, 2023, pp. 168–90, doi:10.1007/978-3-031-44267-4_9.
short: M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime
Verification, Springer Nature, 2023, pp. 168–190.
conference:
end_date: 2023-10-07
location: Thessaloniki, Greek
name: 'RV: Conference on Runtime Verification'
start_date: 2023-10-04
corr_author: '1'
date_created: 2023-08-16T20:46:08Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2025-04-14T09:42:55Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-44267-4_9
ec_funded: 1
file:
- access_level: open_access
checksum: ee33bd6f1a26f4dae7a8192584869fd8
content_type: application/pdf
creator: dernst
date_created: 2023-10-16T07:15:11Z
date_updated: 2023-10-16T07:15:11Z
file_id: '14430'
file_name: 2023_LNCS_RV_Chalupa.pdf
file_size: 867256
relation: main_file
success: 1
file_date_updated: 2023-10-16T07:15:11Z
has_accepted_license: '1'
intvolume: ' 14245'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 168-190
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 23nd International Conference on Runtime Verification
publication_identifier:
eisbn:
- 978-3-031-44267-4
isbn:
- 978-3-031-44266-7
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '15035'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Monitoring hyperproperties with prefix transducers
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: 14245
year: '2023'
...
---
_id: '14242'
abstract:
- lang: eng
text: We study the problem of training and certifying adversarially robust quantized
neural networks (QNNs). Quantization is a technique for making neural networks
more efficient by running them using low-bit integer arithmetic and is therefore
commonly adopted in industry. Recent work has shown that floating-point neural
networks that have been verified to be robust can become vulnerable to adversarial
attacks after quantization, and certification of the quantized representation
is necessary to guarantee robustness. In this work, we present quantization-aware
interval bound propagation (QA-IBP), a novel method for training robust QNNs.
Inspired by advances in robust learning of non-quantized networks, our training
algorithm computes the gradient of an abstract representation of the actual network.
Unlike existing approaches, our method can handle the discrete semantics of QNNs.
Based on QA-IBP, we also develop a complete verification procedure for verifying
the adversarial robustness of QNNs, which is guaranteed to terminate and produce
a correct answer. Compared to existing approaches, the key advantage of our verification
procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate
experimentally that our approach significantly outperforms existing methods and
establish the new state-of-the-art for training and certifying the robustness
of QNNs.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. Research
was sponsored by the United\r\nStates Air Force Research Laboratory and the United
States Air Force Artificial Intelligence Accelerator and was accomplished under
Cooperative Agreement Number FA8750-19-2-\r\n1000. The views and conclusions contained
in this document are those of the authors and should not be interpreted as representing
the official policies, either expressed or implied,\r\nof the United States Air
Force or the U.S. Government. The U.S. Government is authorized to reproduce and
distribute reprints for Government purposes notwithstanding any copyright\r\nnotation
herein. The research was also funded in part by the AI2050 program at Schmidt Futures
(Grant G-22-63172) and Capgemini SE."
article_processing_charge: No
arxiv: 1
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks.
In: Proceedings of the 37th AAAI Conference on Artificial Intelligence.
Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973.
doi:10.1609/aaai.v37i12.26747'
apa: 'Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., & Rus, D.
(2023). Quantization-aware interval bound propagation for training certifiably
robust quantized neural networks. In Proceedings of the 37th AAAI Conference
on Artificial Intelligence (Vol. 37, pp. 14964–14973). Washington, DC, United
States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i12.26747'
chicago: Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, Thomas A Henzinger,
and Daniela Rus. “Quantization-Aware Interval Bound Propagation for Training Certifiably
Robust Quantized Neural Networks.” In Proceedings of the 37th AAAI Conference
on Artificial Intelligence, 37:14964–73. Association for the Advancement of
Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i12.26747.
ieee: M. Lechner, D. Zikelic, K. Chatterjee, T. A. Henzinger, and D. Rus, “Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks,”
in Proceedings of the 37th AAAI Conference on Artificial Intelligence,
Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973.
ista: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks.
Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference
on Artificial Intelligence vol. 37, 14964–14973.'
mla: Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for
Training Certifiably Robust Quantized Neural Networks.” Proceedings of the
37th AAAI Conference on Artificial Intelligence, vol. 37, no. 12, Association
for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:10.1609/aaai.v37i12.26747.
short: M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, D. Rus, in:, Proceedings
of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2023, pp. 14964–14973.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2023-08-27T22:01:17Z
date_published: 2023-06-26T00:00:00Z
date_updated: 2025-03-31T16:01:08Z
day: '26'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i12.26747
ec_funded: 1
external_id:
arxiv:
- '2211.16187'
intvolume: ' 37'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2211.16187
month: '06'
oa: 1
oa_version: Preprint
page: 14964-14973
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781577358800'
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantization-aware interval bound propagation for training certifiably robust
quantized neural networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '14243'
abstract:
- lang: eng
text: 'Two-player zero-sum "graph games" are central in logic, verification, and
multi-agent systems. The game proceeds by placing a token on a vertex of a graph,
and allowing the players to move it to produce an infinite path, which determines
the winner or payoff of the game. Traditionally, the players alternate turns in
moving the token. In "bidding games", however, the players have budgets and in
each turn, an auction (bidding) determines which player moves the token. So far,
bidding games have only been studied as full-information games. In this work we
initiate the study of partial-information bidding games: we study bidding games
in which a player''s initial budget is drawn from a known probability distribution.
We show that while for some bidding mechanisms and objectives, it is straightforward
to adapt the results from the full-information setting to the partial-information
setting, for others, the analysis is significantly more challenging, requires
new techniques, and gives rise to interesting results. Specifically, we study
games with "mean-payoff" objectives in combination with "poorman" bidding. We
construct optimal strategies for a partially-informed player who plays against
a fully-informed adversary. We show that, somewhat surprisingly, the "value" under
pure strategies does not necessarily exist in such games.'
acknowledgement: This research was supported in part by ISF grant no.1679/21, by the
ERC CoG 863818 (ForM-SMArt), and the European Union’s Horizon 2020 research and
innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
article_processing_charge: No
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Ismael R
full_name: Jecker, Ismael R
id: 85D7C63E-7D5D-11E9-9C0F-98C4E5697425
last_name: Jecker
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable
budgets. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence.
Vol 37. ; 2023:5464-5471. doi:10.1609/aaai.v37i5.25679'
apa: Avni, G., Jecker, I. R., & Zikelic, D. (2023). Bidding graph games with
partially-observable budgets. In Proceedings of the 37th AAAI Conference on
Artificial Intelligence (Vol. 37, pp. 5464–5471). Washington, DC, United States.
https://doi.org/10.1609/aaai.v37i5.25679
chicago: Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with
Partially-Observable Budgets.” In Proceedings of the 37th AAAI Conference on
Artificial Intelligence, 37:5464–71, 2023. https://doi.org/10.1609/aaai.v37i5.25679.
ieee: G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable
budgets,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence,
Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471.
ista: 'Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable
budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI:
Conference on Artificial Intelligence vol. 37, 5464–5471.'
mla: Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.”
Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol.
37, no. 5, 2023, pp. 5464–71, doi:10.1609/aaai.v37i5.25679.
short: G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference
on Artificial Intelligence, 2023, pp. 5464–5471.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2023-08-27T22:01:18Z
date_published: 2023-06-27T00:00:00Z
date_updated: 2025-03-31T16:01:08Z
day: '27'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i5.25679
ec_funded: 1
external_id:
arxiv:
- '2211.13626'
intvolume: ' 37'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1609/aaai.v37i5.25679
month: '06'
oa: 1
oa_version: Published Version
page: 5464-5471
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781577358800'
publication_status: published
quality_controlled: '1'
scopus_import: '1'
status: public
title: Bidding graph games with partially-observable budgets
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '14405'
abstract:
- lang: eng
text: We introduce hypernode automata as a new specification formalism for hyperproperties
of concurrent systems. They are finite automata with nodes labeled with hypernode
logic formulas and transitions labeled with actions. A hypernode logic formula
specifies relations between sequences of variable values in different system executions.
Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces
by constraining the values and the order of value changes of each variable without
correlating the timing of the changes. Different execution traces are synchronized
solely through the transitions of hypernode automata. Hypernode automata naturally
combine asynchronicity at the node level with synchronicity at the transition
level. We show that the model-checking problem for hypernode automata is decidable
over action-labeled Kripke structures, whose actions induce transitions of the
specification automata. For this reason, hypernode automaton is a suitable formalism
for specifying and verifying asynchronous hyperproperties, such as declassifying
observational determinism in multi-threaded programs.
acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF)
SFB project\r\nSpyCoDe F8502, by the FWF projects ZK-35 and W1255-N23, and by the
ERC Advanced Grant\r\nVAMOS 101020093."
alternative_title:
- LIPIcs
article_number: '21'
article_processing_charge: Yes
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. Hypernode automata.
In: 34th International Conference on Concurrency Theory. Vol 279. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.21'
apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A.
(2023). Hypernode automata. In 34th International Conference on Concurrency
Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.21'
chicago: Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
Costa. “Hypernode Automata.” In 34th International Conference on Concurrency
Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
https://doi.org/10.4230/LIPIcs.CONCUR.2023.21.
ieee: E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode
automata,” in 34th International Conference on Concurrency Theory, Antwerp,
Belgium, 2023, vol. 279.
ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2023. Hypernode
automata. 34th International Conference on Concurrency Theory. CONCUR: Conference
on Concurrency Theory, LIPIcs, vol. 279, 21.'
mla: Bartocci, Ezio, et al. “Hypernode Automata.” 34th International Conference
on Concurrency Theory, vol. 279, 21, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.21.
short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, 34th
International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2023.
conference:
end_date: 2023-09-22
location: Antwerp, Belgium
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2023-09-19
corr_author: '1'
date_created: 2023-10-08T22:01:16Z
date_published: 2023-09-01T00:00:00Z
date_updated: 2026-01-05T12:27:40Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2023.21
ec_funded: 1
external_id:
arxiv:
- '2305.02836'
file:
- access_level: open_access
checksum: 215765e40454d806174ac0a223e8d6fa
content_type: application/pdf
creator: dernst
date_created: 2023-10-09T07:42:45Z
date_updated: 2023-10-09T07:42:45Z
file_id: '14413'
file_name: 2023_LIPcs_Bartocci.pdf
file_size: 795790
relation: main_file
success: 1
file_date_updated: 2023-10-09T07:42:45Z
has_accepted_license: '1'
intvolume: ' 279'
language:
- iso: eng
month: '09'
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: 34th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959772990'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
record:
- id: '20866'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Hypernode 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: 279
year: '2023'
...
---
_id: '14411'
abstract:
- lang: eng
text: "Partially specified Boolean networks (PSBNs) represent a promising framework
for the qualitative modelling of biological systems in which the logic of interactions
is not completely known. Phenotype control aims to stabilise the network in states
exhibiting specific traits.\r\nIn this paper, we define the phenotype control
problem in the context of asynchronous PSBNs and propose a novel semi-symbolic
algorithm for solving this problem with permanent variable perturbations."
acknowledgement: This work was supported by the Czech Foundation grant No. GA22-10845S,
Grant Agency of Masaryk University grant No. MUNI/G/1771/2020, and the European
Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie
Grant Agreement No. 101034413.
alternative_title:
- LNBI
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
- first_name: Eva
full_name: Šmijáková, Eva
last_name: Šmijáková
citation:
ama: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. Phenotype control of partially
specified boolean networks. In: 21st International Conference on Computational
Methods in Systems Biology. Vol 14137. Springer Nature; 2023:18-35. doi:10.1007/978-3-031-42697-1_2'
apa: 'Beneš, N., Brim, L., Pastva, S., Šafránek, D., & Šmijáková, E. (2023).
Phenotype control of partially specified boolean networks. In 21st International
Conference on Computational Methods in Systems Biology (Vol. 14137, pp. 18–35).
Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-42697-1_2'
chicago: Beneš, Nikola, Luboš Brim, Samuel Pastva, David Šafránek, and Eva Šmijáková.
“Phenotype Control of Partially Specified Boolean Networks.” In 21st International
Conference on Computational Methods in Systems Biology, 14137:18–35. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-42697-1_2.
ieee: N. Beneš, L. Brim, S. Pastva, D. Šafránek, and E. Šmijáková, “Phenotype control
of partially specified boolean networks,” in 21st International Conference
on Computational Methods in Systems Biology, Luxembourg City, Luxembourg,
2023, vol. 14137, pp. 18–35.
ista: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. 2023. Phenotype control
of partially specified boolean networks. 21st International Conference on Computational
Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNBI,
vol. 14137, 18–35.'
mla: Beneš, Nikola, et al. “Phenotype Control of Partially Specified Boolean Networks.”
21st International Conference on Computational Methods in Systems Biology,
vol. 14137, Springer Nature, 2023, pp. 18–35, doi:10.1007/978-3-031-42697-1_2.
short: N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková, in:, 21st International
Conference on Computational Methods in Systems Biology, Springer Nature, 2023,
pp. 18–35.
conference:
end_date: 2023-09-15
location: Luxembourg City, Luxembourg
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2023-09-13
date_created: 2023-10-08T22:01:18Z
date_published: 2023-09-09T00:00:00Z
date_updated: 2025-09-09T14:25:46Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-42697-1_2
ec_funded: 1
external_id:
isi:
- '001156280600002'
file:
- access_level: open_access
checksum: 6f71bdaedb770b52380222fd9f4d7937
content_type: application/pdf
creator: spastva
date_created: 2024-02-16T08:26:32Z
date_updated: 2024-02-16T08:26:32Z
file_id: '14997'
file_name: cmsb2023.pdf
file_size: 691582
relation: main_file
success: 1
file_date_updated: 2024-02-16T08:26:32Z
has_accepted_license: '1'
intvolume: ' 14137'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 18-35
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 21st International Conference on Computational Methods in Systems Biology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031426964'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Phenotype control of partially specified boolean networks
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14137
year: '2023'
...
---
_id: '14454'
abstract:
- lang: eng
text: As AI and machine-learned software are used increasingly for making decisions
that affect humans, it is imperative that they remain fair and unbiased in their
decisions. To complement design-time bias mitigation measures, runtime verification
techniques have been introduced recently to monitor the algorithmic fairness of
deployed systems. Previous monitoring techniques assume full observability of
the states of the (unknown) monitored system. Moreover, they can monitor only
fairness properties that are specified as arithmetic expressions over the probabilities
of different events. In this work, we extend fairness monitoring to systems modeled
as partially observed Markov chains (POMC), and to specifications containing arithmetic
expressions over the expected values of numerical functions on event sequences.
The only assumptions we make are that the underlying POMC is aperiodic and starts
in the stationary distribution, with a bound on its mixing time being known. These
assumptions enable us to estimate a given property for the entire distribution
of possible executions of the monitored POMC, by observing only a single execution.
Our monitors observe a long run of the system and, after each new observation,
output updated PAC-estimates of how fair or biased the system is. The monitors
are computationally lightweight and, using a prototype implementation, we demonstrate
their effectiveness on several real-world examples.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG 101020093.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Henzinger TA, Kueffner K, Mallik K. Monitoring algorithmic fairness under
partial observations. In: 23rd International Conference on Runtime Verification.
Vol 14245. Springer Nature; 2023:291-311. doi:10.1007/978-3-031-44267-4_15'
apa: 'Henzinger, T. A., Kueffner, K., & Mallik, K. (2023). Monitoring algorithmic
fairness under partial observations. In 23rd International Conference on Runtime
Verification (Vol. 14245, pp. 291–311). Thessaloniki, Greece: Springer Nature.
https://doi.org/10.1007/978-3-031-44267-4_15'
chicago: Henzinger, Thomas A, Konstantin Kueffner, and Kaushik Mallik. “Monitoring
Algorithmic Fairness under Partial Observations.” In 23rd International Conference
on Runtime Verification, 14245:291–311. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_15.
ieee: T. A. Henzinger, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness
under partial observations,” in 23rd International Conference on Runtime Verification,
Thessaloniki, Greece, 2023, vol. 14245, pp. 291–311.
ista: 'Henzinger TA, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness
under partial observations. 23rd International Conference on Runtime Verification.
RV: Conference on Runtime Verification, LNCS, vol. 14245, 291–311.'
mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness under Partial
Observations.” 23rd International Conference on Runtime Verification, vol.
14245, Springer Nature, 2023, pp. 291–311, doi:10.1007/978-3-031-44267-4_15.
short: T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference
on Runtime Verification, Springer Nature, 2023, pp. 291–311.
conference:
end_date: 2023-10-06
location: Thessaloniki, Greece
name: 'RV: Conference on Runtime Verification'
start_date: 2023-10-03
corr_author: '1'
date_created: 2023-10-29T23:01:15Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2025-04-14T07:55:55Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-031-44267-4_15
ec_funded: 1
external_id:
arxiv:
- '2308.00341'
intvolume: ' 14245'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2308.00341
month: '10'
oa: 1
oa_version: Preprint
page: 291-311
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 23rd International Conference on Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031442667'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring algorithmic fairness under partial observations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14245
year: '2023'
...
---
_id: '14518'
abstract:
- lang: eng
text: We consider bidding games, a class of two-player zero-sum graph games. The
game proceeds as follows. Both players have bounded budgets. A token is placed
on a vertex of a graph, in each turn the players simultaneously submit bids, and
the higher bidder moves the token, where we break bidding ties in favor of Player
1. Player 1 wins the game iff the token visits a designated target vertex. We
consider, for the first time, poorman discrete-bidding in which the granularity
of the bids is restricted and the higher bid is paid to the bank. Previous work
either did not impose granularity restrictions or considered Richman bidding (bids
are paid to the opponent). While the latter mechanisms are technically more accessible,
the former is more appealing from a practical standpoint. Our study focuses on
threshold budgets, which is the necessary and sufficient initial budget required
for Player 1 to ensure winning against a given Player 2 budget. We first show
existence of thresholds. In DAGs, we show that threshold budgets can be approximated
with error bounds by thresholds under continuous-bidding and that they exhibit
a periodic behavior. We identify closed-form solutions in special cases. We implement
and experiment with an algorithm to find threshold budgets.
acknowledgement: This research was supported in part by ISF grant no. 1679/21, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie SkłodowskaCurie Grant Agreement No. 665385.
article_processing_charge: No
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Suman
full_name: Sadhukhan, Suman
last_name: Sadhukhan
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. Reachability poorman
discrete-bidding games. In: Frontiers in Artificial Intelligence and Applications.
Vol 372. IOS Press; 2023:141-148. doi:10.3233/FAIA230264'
apa: 'Avni, G., Meggendorfer, T., Sadhukhan, S., Tkadlec, J., & Zikelic, D.
(2023). Reachability poorman discrete-bidding games. In Frontiers in Artificial
Intelligence and Applications (Vol. 372, pp. 141–148). Krakow, Poland: IOS
Press. https://doi.org/10.3233/FAIA230264'
chicago: Avni, Guy, Tobias Meggendorfer, Suman Sadhukhan, Josef Tkadlec, and Dorde
Zikelic. “Reachability Poorman Discrete-Bidding Games.” In Frontiers in Artificial
Intelligence and Applications, 372:141–48. IOS Press, 2023. https://doi.org/10.3233/FAIA230264.
ieee: G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, and D. Zikelic, “Reachability
poorman discrete-bidding games,” in Frontiers in Artificial Intelligence and
Applications, Krakow, Poland, 2023, vol. 372, pp. 141–148.
ista: 'Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. 2023. Reachability
poorman discrete-bidding games. Frontiers in Artificial Intelligence and Applications.
ECAI: European Conference on Artificial Intelligence vol. 372, 141–148.'
mla: Avni, Guy, et al. “Reachability Poorman Discrete-Bidding Games.” Frontiers
in Artificial Intelligence and Applications, vol. 372, IOS Press, 2023, pp.
141–48, doi:10.3233/FAIA230264.
short: G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, D. Zikelic, in:, Frontiers
in Artificial Intelligence and Applications, IOS Press, 2023, pp. 141–148.
conference:
end_date: 2023-10-04
location: Krakow, Poland
name: 'ECAI: European Conference on Artificial Intelligence'
start_date: 2023-09-30
corr_author: '1'
date_created: 2023-11-12T23:00:56Z
date_published: 2023-09-28T00:00:00Z
date_updated: 2025-03-31T16:01:09Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.3233/FAIA230264
ec_funded: 1
external_id:
arxiv:
- '2307.15218'
file:
- access_level: open_access
checksum: 1390ca38480fa4cf286b0f1a42e8c12f
content_type: application/pdf
creator: dernst
date_created: 2023-11-13T10:16:10Z
date_updated: 2023-11-13T10:16:10Z
file_id: '14529'
file_name: 2023_FAIA_Avni.pdf
file_size: 501011
relation: main_file
success: 1
file_date_updated: 2023-11-13T10:16:10Z
has_accepted_license: '1'
intvolume: ' 372'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc/4.0/
month: '09'
oa: 1
oa_version: Published Version
page: 141-148
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Frontiers in Artificial Intelligence and Applications
publication_identifier:
isbn:
- '9781643684369'
issn:
- 0922-6389
publication_status: published
publisher: IOS Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reachability poorman discrete-bidding games
tmp:
image: /images/cc_by_nc.png
legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
short: CC BY-NC (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 372
year: '2023'
...
---
_id: '14559'
abstract:
- lang: eng
text: We consider the problem of learning control policies in discrete-time stochastic
systems which guarantee that the system stabilizes within some specified stabilization
region with probability 1. Our approach is based on the novel notion of stabilizing
ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome
the limitation of methods proposed in previous works whose applicability is restricted
to systems in which the stabilizing region cannot be left once entered under any
control policy. We present a learning procedure that learns a control policy together
with an sRSM that formally certifies probability 1 stability, both learned as
neural networks. We show that this procedure can also be adapted to formally verifying
that, under a given Lipschitz continuous control policy, the stochastic system
stabilizes within some stabilizing region with probability 1. Our experimental
evaluation shows that our learning procedure can successfully learn provably stabilizing
policies in practice.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Matin
full_name: Ansaripour, Matin
last_name: Ansaripour
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. Learning provably
stabilizing neural controllers for discrete-time stochastic systems. In: 21st
International Symposium on Automated Technology for Verification and Analysis.
Vol 14215. Springer Nature; 2023:357-379. doi:10.1007/978-3-031-45329-8_17'
apa: 'Ansaripour, M., Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic,
D. (2023). Learning provably stabilizing neural controllers for discrete-time
stochastic systems. In 21st International Symposium on Automated Technology
for Verification and Analysis (Vol. 14215, pp. 357–379). Singapore, Singapore:
Springer Nature. https://doi.org/10.1007/978-3-031-45329-8_17'
chicago: Ansaripour, Matin, Krishnendu Chatterjee, Thomas A Henzinger, Mathias Lechner,
and Dorde Zikelic. “Learning Provably Stabilizing Neural Controllers for Discrete-Time
Stochastic Systems.” In 21st International Symposium on Automated Technology
for Verification and Analysis, 14215:357–79. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-45329-8_17.
ieee: M. Ansaripour, K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic,
“Learning provably stabilizing neural controllers for discrete-time stochastic
systems,” in 21st International Symposium on Automated Technology for Verification
and Analysis, Singapore, Singapore, 2023, vol. 14215, pp. 357–379.
ista: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning
provably stabilizing neural controllers for discrete-time stochastic systems.
21st International Symposium on Automated Technology for Verification and Analysis.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379.'
mla: Ansaripour, Matin, et al. “Learning Provably Stabilizing Neural Controllers
for Discrete-Time Stochastic Systems.” 21st International Symposium on Automated
Technology for Verification and Analysis, vol. 14215, Springer Nature, 2023,
pp. 357–79, doi:10.1007/978-3-031-45329-8_17.
short: M. Ansaripour, K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:,
21st International Symposium on Automated Technology for Verification and Analysis,
Springer Nature, 2023, pp. 357–379.
conference:
end_date: 2023-10-27
location: Singapore, Singapore
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2023-10-24
corr_author: '1'
date_created: 2023-11-19T23:00:56Z
date_published: 2023-10-22T00:00:00Z
date_updated: 2025-09-09T13:20:26Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-031-45329-8_17
ec_funded: 1
external_id:
arxiv:
- '2210.05304'
isi:
- '001456127300017'
intvolume: ' 14215'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2210.05304'
month: '10'
oa: 1
oa_version: Preprint
page: 357-379
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: 21st International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031453281'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Learning provably stabilizing neural controllers for discrete-time stochastic
systems
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14215
year: '2023'
...
---
_id: '14718'
abstract:
- lang: eng
text: 'Binary decision diagrams (BDDs) are one of the fundamental data structures
in formal methods and computer science in general. However, the performance of
BDD-based algorithms greatly depends on memory latency due to the reliance on
large hash tables and thus, by extension, on the speed of random memory access.
This hinders the full utilisation of resources available on modern CPUs, since
the absolute memory latency has not improved significantly for at least a decade.
In this paper, we explore several implementation techniques that improve the performance
of BDD manipulation either through enhanced memory locality or by partially eliminating
random memory access. On a benchmark suite of 600+ BDDs derived from real-world
applications, we demonstrate runtime that is comparable or better than parallelising
the same operations on eight CPU cores. '
acknowledgement: "This work was supported by the European Union’s Horizon 2020 research
and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413
and the\r\n“VAMOS” grant ERC-2020-AdG 101020093."
article_processing_charge: No
author:
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- 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: 'Pastva S, Henzinger TA. Binary decision diagrams on modern hardware. In: Proceedings
of the 23rd Conference on Formal Methods in Computer-Aided Design. TU Vienna
Academic Press; 2023:122-131. doi:10.34727/2023/isbn.978-3-85448-060-0_20'
apa: 'Pastva, S., & Henzinger, T. A. (2023). Binary decision diagrams on modern
hardware. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design (pp. 122–131). Ames, IA, United States: TU Vienna Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20'
chicago: Pastva, Samuel, and Thomas A Henzinger. “Binary Decision Diagrams on Modern
Hardware.” In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design, 122–31. TU Vienna Academic Press, 2023. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20.
ieee: S. Pastva and T. A. Henzinger, “Binary decision diagrams on modern hardware,”
in Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design,
Ames, IA, United States, 2023, pp. 122–131.
ista: 'Pastva S, Henzinger TA. 2023. Binary decision diagrams on modern hardware.
Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design.
FMCAD: Formal Methods in Computer-Aided Design, 122–131.'
mla: Pastva, Samuel, and Thomas A. Henzinger. “Binary Decision Diagrams on Modern
Hardware.” Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design, TU Vienna Academic Press, 2023, pp. 122–31, doi:10.34727/2023/isbn.978-3-85448-060-0_20.
short: S. Pastva, T.A. Henzinger, in:, Proceedings of the 23rd Conference on Formal
Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–131.
conference:
end_date: 2023-10-27
location: Ames, IA, United States
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2023-10-25
corr_author: '1'
date_created: 2023-12-31T23:01:03Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2025-09-09T14:04:14Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.34727/2023/isbn.978-3-85448-060-0_20
ec_funded: 1
external_id:
isi:
- '001504402400020'
file:
- access_level: open_access
checksum: 818d6e13dd508f3a04f0941081022e5d
content_type: application/pdf
creator: dernst
date_created: 2024-01-02T08:14:23Z
date_updated: 2024-01-02T08:14:23Z
file_id: '14721'
file_name: 2023_FMCAD_Pastva.pdf
file_size: 524321
relation: main_file
success: 1
file_date_updated: 2024-01-02T08:14:23Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 122-131
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design
publication_identifier:
isbn:
- '9783854480600'
publication_status: published
publisher: TU Vienna Academic Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Binary decision diagrams on modern hardware
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2023'
...
---
_id: '12407'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of run-time monitoring. Third-party monitoring, with limited knowledge
of the monitored software, and best-effort monitoring, which keeps pace with the
monitored software, are especially valuable, yet underexplored areas of run-time
monitoring. Most existing monitoring frameworks do not support their combination
because they either require access to the monitored code for instrumentation purposes
or the processing of all observed events, or both.\r\n\r\nWe present a middleware
framework, VAMOS, for the run-time monitoring of software which is explicitly
designed to support third-party and best-effort scenarios. The design goals of
VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the
ability to monitor black-box code through a variety of different event channels,
and the connectability to monitors written in different specification languages),
and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker
and event recognition systems with aspects of stream processing systems.\r\n\r\nWe
implemented a prototype toolchain for VAMOS and conducted experiments including
a case study of monitoring for data races. The results indicate that VAMOS enables
writing useful yet efficient monitors, is compatible with a variety of event sources
and monitor specifications, and simplifies key aspects of setting up a monitoring
system from scratch."
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093. \r\nThe
authors would like to thank the anonymous FASE reviewers for their valuable feedback
and suggestions."
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for
Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria;
2023. doi:10.15479/AT:ISTA:12407'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023).
VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of
Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:12407'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of
Science and Technology Austria, 2023. https://doi.org/10.15479/AT:ISTA:12407.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, VAMOS: Middleware
for Best-Effort Third-Party Monitoring. Institute of Science and Technology
Austria, 2023.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. VAMOS: Middleware
for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria,
38p.'
mla: 'Chalupa, Marek, et al. VAMOS: Middleware for Best-Effort Third-Party Monitoring.
Institute of Science and Technology Austria, 2023, doi:10.15479/AT:ISTA:12407.'
short: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, VAMOS: Middleware
for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria,
2023.'
corr_author: '1'
date_created: 2023-01-27T03:18:08Z
date_published: 2023-01-27T00:00:00Z
date_updated: 2025-09-09T12:25:29Z
day: '27'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:12407
ec_funded: 1
file:
- access_level: open_access
checksum: 55426e463fdeafe9777fc3ff635154c7
content_type: application/pdf
creator: fmuehlbo
date_created: 2023-01-27T03:18:34Z
date_updated: 2023-01-27T03:18:34Z
file_id: '12408'
file_name: main.pdf
file_size: 662409
relation: main_file
success: 1
file_date_updated: 2023-01-27T03:18:34Z
has_accepted_license: '1'
keyword:
- runtime monitoring
- best effort
- third party
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '38'
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
eissn:
- 2664-1690
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '12856'
relation: later_version
status: public
status: public
title: 'VAMOS: Middleware for Best-Effort Third-Party Monitoring'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '12467'
abstract:
- lang: eng
text: Safety and liveness are elementary concepts of computation, and the foundation
of many verification paradigms. The safety-liveness classification of boolean
properties characterizes whether a given property can be falsified by observing
a finite prefix of an infinite computation trace (always for safety, never for
liveness). In quantitative specification and verification, properties assign not
truth values, but quantitative values to infinite traces (e.g., a cost, or the
distance to a boolean property). We introduce quantitative safety and liveness,
and we prove that our definitions induce conservative quantitative generalizations
of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness
decomposition of boolean properties. In particular, we show that every quantitative
property can be written as the pointwise minimum of a quantitative safety property
and a quantitative liveness property. Consequently, like boolean properties, also
quantitative properties can be min-decomposed into safety and liveness parts,
or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover,
quantitative properties can be approximated naturally. We prove that every quantitative
property that has both safe and co-safe approximations can be monitored arbitrarily
precisely by a monitor that uses only a finite number of states.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In:
26th International Conference Foundations of Software Science and Computation
Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative
safety and liveness. In 26th International Conference Foundations of Software
Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France:
Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative
Safety and Liveness.” In 26th International Conference Foundations of Software
Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17.
ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and
liveness,” in 26th International Conference Foundations of Software Science
and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness.
26th International Conference Foundations of Software Science and Computation
Structures. FOSSACS: Foundations of Software Science and Computation Structures,
LNCS, vol. 13992, 349–370.'
mla: Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International
Conference Foundations of Software Science and Computation Structures, vol.
13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference
Foundations of Software Science and Computation Structures, Springer Nature, 2023,
pp. 349–370.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FOSSACS: Foundations of Software Science and Computation Structures'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-01-31T07:23:56Z
date_published: 2023-04-21T00:00:00Z
date_updated: 2025-09-09T12:21:08Z
day: '21'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-30829-1_17
ec_funded: 1
external_id:
arxiv:
- '2301.11175'
isi:
- '001288609300017'
file:
- access_level: open_access
checksum: 981025aed580b6b27c426cb8856cf63e
content_type: application/pdf
creator: esarac
date_created: 2023-01-31T07:22:21Z
date_updated: 2023-01-31T07:22:21Z
file_id: '12468'
file_name: qsl.pdf
file_size: 449027
relation: main_file
success: 1
- access_level: open_access
checksum: f16e2af1e0eb243158ab0f0fe74e7d5a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T10:28:09Z
date_updated: 2023-06-19T10:28:09Z
file_id: '13153'
file_name: 2023_LNCS_HenzingerT.pdf
file_size: 1048171
relation: main_file
success: 1
file_date_updated: 2023-06-19T10:28:09Z
has_accepted_license: '1'
intvolume: ' 13992'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 349-370
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 26th International Conference Foundations of Software Science and Computation
Structures
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308284'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative safety and liveness
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13992
year: '2023'
...
---
_id: '12704'
abstract:
- lang: eng
text: Adversarial training (i.e., training on adversarially perturbed input data)
is a well-studied method for making neural networks robust to potential adversarial
attacks during inference. However, the improved robustness does not come for free
but rather is accompanied by a decrease in overall model accuracy and performance.
Recent work has shown that, in practical robot learning applications, the effects
of adversarial training do not pose a fair trade-off but inflict a net loss when
measured in holistic robot performance. This work revisits the robustness-accuracy
trade-off in robot learning by systematically analyzing if recent advances in
robust training methods and theory in conjunction with adversarial robot learning,
are capable of making adversarial training suitable for real-world robot applications.
We evaluate three different robot learning tasks ranging from autonomous driving
in a high-fidelity environment amenable to sim-to-real deployment to mobile robot
navigation and gesture recognition. Our results demonstrate that, while these
techniques make incremental improvements on the trade-off on a relative scale,
the negative impact on the nominal accuracy caused by adversarial training still
outweighs the improved robustness by an order of magnitude. We conclude that although
progress is happening, further advances in robust learning methods are necessary
before they can benefit robot learning tasks in practice.
acknowledgement: "We thank Christoph Lampert for inspiring this work. The\r\nviews
and conclusions contained in this document are those of\r\nthe authors and should
not be interpreted as representing the\r\nofficial policies, either expressed or
implied, of the United States\r\nAir Force or the U.S. Government. The U.S. Government
is\r\nauthorized to reproduce and distribute reprints for Government\r\npurposes
notwithstanding any copyright notation herein."
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- 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: Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy
tradeoff in robot learning. IEEE Robotics and Automation Letters. 2023;8(3):1595-1602.
doi:10.1109/LRA.2023.3240930
apa: Lechner, M., Amini, A., Rus, D., & Henzinger, T. A. (2023). Revisiting
the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics
and Automation Letters. Institute of Electrical and Electronics Engineers.
https://doi.org/10.1109/LRA.2023.3240930
chicago: Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger.
“Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” IEEE
Robotics and Automation Letters. Institute of Electrical and Electronics Engineers,
2023. https://doi.org/10.1109/LRA.2023.3240930.
ieee: M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial
robustness-accuracy tradeoff in robot learning,” IEEE Robotics and Automation
Letters, vol. 8, no. 3. Institute of Electrical and Electronics Engineers,
pp. 1595–1602, 2023.
ista: Lechner M, Amini A, Rus D, Henzinger TA. 2023. Revisiting the adversarial
robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters.
8(3), 1595–1602.
mla: Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff
in Robot Learning.” IEEE Robotics and Automation Letters, vol. 8, no. 3,
Institute of Electrical and Electronics Engineers, 2023, pp. 1595–602, doi:10.1109/LRA.2023.3240930.
short: M. Lechner, A. Amini, D. Rus, T.A. Henzinger, IEEE Robotics and Automation
Letters 8 (2023) 1595–1602.
date_created: 2023-03-05T23:01:04Z
date_published: 2023-03-01T00:00:00Z
date_updated: 2025-04-14T09:42:58Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/LRA.2023.3240930
external_id:
arxiv:
- '2204.07373'
isi:
- '000936534100012'
file:
- access_level: open_access
checksum: 5a75dcd326ea66685de2b1aaec259e85
content_type: application/pdf
creator: cchlebak
date_created: 2023-03-07T12:22:23Z
date_updated: 2023-03-07T12:22:23Z
file_id: '12714'
file_name: 2023_IEEERobAutLetters_Lechner.pdf
file_size: 944052
relation: main_file
success: 1
file_date_updated: 2023-03-07T12:22:23Z
has_accepted_license: '1'
intvolume: ' 8'
isi: 1
issue: '3'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: 1595-1602
publication: IEEE Robotics and Automation Letters
publication_identifier:
eissn:
- 2377-3766
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
related_material:
record:
- id: '11366'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Revisiting the adversarial robustness-accuracy tradeoff in robot learning
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 8
year: '2023'
...
---
_id: '12854'
abstract:
- lang: eng
text: "The main idea behind BUBAAK is to run multiple program analyses in parallel
and use runtime monitoring and enforcement to observe and control their progress
in real time. The analyses send information about (un)explored states of the program
and discovered invariants to a monitor. The monitor processes the received data
and can force an analysis to stop the search of certain program parts (which have
already been analyzed by other analyses), or to make it utilize a program invariant
found by another analysis.\r\nAt SV-COMP 2023, the implementation of data exchange
between the monitor and the analyses was not yet completed, which is why BUBAAK
only ran several analyses in parallel, without any coordination. Still, BUBAAK
won the meta-category FalsificationOverall and placed very well in several other
(sub)-categories of the competition."
acknowledgement: This work was supported by the ERC-2020-AdG 10102009 grant.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers.
In: Tools and Algorithms for the Construction and Analysis of Systems.
Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32'
apa: 'Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of
program verifiers. In Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32'
chicago: 'Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of
Program Verifiers.” In Tools and Algorithms for the Construction and Analysis
of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.'
ieee: 'M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,”
in Tools and Algorithms for the Construction and Analysis of Systems, Paris,
France, 2023, vol. 13994, pp. 535–540.'
ista: 'Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers.
Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994,
535–540.'
mla: 'Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program
Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.'
short: M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 535–540.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-04-20T08:22:53Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2025-09-09T12:24:56Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_32
ec_funded: 1
external_id:
isi:
- '001288698100041'
file:
- access_level: open_access
checksum: 120d2c2a38384058ad0630fdf8288312
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T06:58:36Z
date_updated: 2023-04-25T06:58:36Z
file_id: '12864'
file_name: 2023_LNCS_Chalupa.pdf
file_size: 16096413
relation: main_file
success: 1
file_date_updated: 2023-04-25T06:58:36Z
has_accepted_license: '1'
intvolume: ' 13994'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 535-540
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783031308208'
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Bubaak: Runtime monitoring of program verifiers'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13994
year: '2023'
...