---
_id: '13310'
abstract:
- lang: eng
text: Machine-learned systems are in widespread use for making decisions about humans,
and it is important that they are fair, i.e., not biased against individuals based
on sensitive attributes. We present runtime verification of algorithmic fairness
for systems whose models are unknown, but are assumed to have a Markov chain structure.
We introduce a specification language that can model many common algorithmic fairness
properties, such as demographic parity, equal opportunity, and social burden.
We build monitors that observe a long sequence of events as generated by a given
system, and output, after each observation, a quantitative estimate of how fair
or biased the system was on that run until that point in time. The estimate is
proven to be correct modulo a variable error bound and a given confidence level,
where the error bound gets tighter as the observed sequence gets longer. Our monitors
are of two types, and use, respectively, frequentist and Bayesian statistical
inference techniques. While the frequentist monitors compute estimates that are
objectively correct with respect to the ground truth, the Bayesian monitors compute
estimates that are correct subject to a given prior belief about the system’s
model. Using a prototype implementation, we show how we can monitor if a bank
is fair in giving loans to applicants from different social backgrounds, and if
a college is fair in admitting students while maintaining a reasonable financial
burden on the society. Although they exhibit different theoretical complexities
in certain cases, in our experiments, both frequentist and Bayesian monitors took
less than a millisecond to update their verdicts after each observation.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG101020093.'
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Mahyar
full_name: Karimi, Mahyar
id: f1dedef5-2f78-11ee-989a-c4c97bccf506
last_name: Karimi
orcid: 0009-0005-0820-1696
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness.
In: Computer Aided Verification. Vol 13965. Springer Nature; 2023:358–382.
doi:10.1007/978-3-031-37703-7_17'
apa: 'Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Monitoring
algorithmic fairness. In Computer Aided Verification (Vol. 13965, pp. 358–382).
Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37703-7_17'
chicago: Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik.
“Monitoring Algorithmic Fairness.” In Computer Aided Verification, 13965:358–382.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37703-7_17.
ieee: T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic
fairness,” in Computer Aided Verification, Paris, France, 2023, vol. 13965,
pp. 358–382.
ista: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Monitoring algorithmic
fairness. Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 13965, 358–382.'
mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” Computer
Aided Verification, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:10.1007/978-3-031-37703-7_17.
short: T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification,
Springer Nature, 2023, pp. 358–382.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-07-25T18:32:40Z
date_published: 2023-07-18T00:00:00Z
date_updated: 2023-09-05T15:14:00Z
day: '18'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-37703-7_17
ec_funded: 1
external_id:
arxiv:
- '2305.15979'
file:
- access_level: open_access
checksum: ccaf94bf7d658ba012c016e11869b54c
content_type: application/pdf
creator: dernst
date_created: 2023-07-31T08:11:20Z
date_updated: 2023-07-31T08:11:20Z
file_id: '13327'
file_name: 2023_LNCS_CAV_HenzingerT.pdf
file_size: 647760
relation: main_file
success: 1
file_date_updated: 2023-07-31T08:11:20Z
has_accepted_license: '1'
intvolume: ' 13965'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 358–382
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Computer Aided Verification
publication_identifier:
eisbn:
- '9783031377037'
eissn:
- 1611-3349
isbn:
- '9783031377020'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Monitoring algorithmic fairness
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13965
year: '2023'
...
---
_id: '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
date_created: 2023-08-16T20:46:08Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2024-02-28T12:33:08Z
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
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-07-14T09:09:56Z
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-07-14T09:09:56Z
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: '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.'
date_created: 2023-01-27T03:18:08Z
date_published: 2023-01-27T00:00:00Z
date_updated: 2023-04-25T07:19:06Z
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
date_created: 2023-01-31T07:23:56Z
date_published: 2023-04-21T00:00:00Z
date_updated: 2023-07-14T11:20:27Z
day: '21'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-30829-1_17
ec_funded: 1
external_id:
arxiv:
- '2301.11175'
file:
- access_level: open_access
checksum: 981025aed580b6b27c426cb8856cf63e
content_type: application/pdf
creator: esarac
date_created: 2023-01-31T07:22:21Z
date_updated: 2023-01-31T07:22:21Z
file_id: '12468'
file_name: qsl.pdf
file_size: 449027
relation: main_file
success: 1
- access_level: open_access
checksum: f16e2af1e0eb243158ab0f0fe74e7d5a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T10:28:09Z
date_updated: 2023-06-19T10:28:09Z
file_id: '13153'
file_name: 2023_LNCS_HenzingerT.pdf
file_size: 1048171
relation: main_file
success: 1
file_date_updated: 2023-06-19T10:28:09Z
has_accepted_license: '1'
intvolume: ' 13992'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 349-370
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 26th International Conference Foundations of Software Science and Computation
Structures
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308284'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative safety and liveness
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 13992
year: '2023'
...
---
_id: '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: 2023-08-01T13:36:50Z
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
date_created: 2023-04-20T08:22:53Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-04-25T07:02:43Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_32
ec_funded: 1
file:
- access_level: open_access
checksum: 120d2c2a38384058ad0630fdf8288312
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T06:58:36Z
date_updated: 2023-04-25T06:58:36Z
file_id: '12864'
file_name: 2023_LNCS_Chalupa.pdf
file_size: 16096413
relation: main_file
success: 1
file_date_updated: 2023-04-25T06:58:36Z
has_accepted_license: '1'
intvolume: ' 13994'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 535-540
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783031308208'
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: 'Bubaak: Runtime monitoring of program verifiers'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13994
year: '2023'
...
---
_id: '12856'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of run-time monitoring. Third-party monitoring, with limited knowledge
of the monitored software, and best-effort monitoring, which keeps pace with the
monitored software, are especially valuable, yet underexplored areas of run-time
monitoring. Most existing monitoring frameworks do not support their combination
because they either require access to the monitored code for instrumentation purposes
or the processing of all observed events, or both.\r\n\r\nWe present a middleware
framework, VAMOS, for the run-time monitoring of software which is explicitly
designed to support third-party and best-effort scenarios. The design goals of
VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the
ability to monitor black-box code through a variety of different event channels,
and the connectability to monitors written in different specification languages),
and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker
and event recognition systems with aspects of stream processing systems.\r\nWe
implemented a prototype toolchain for VAMOS and conducted experiments including
a case study of monitoring for data races. The results indicate that VAMOS enables
writing useful yet efficient monitors, is compatible with a variety of event sources
and monitor specifications, and simplifies key aspects of setting up a monitoring
system from scratch."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
authors would like to thank the anonymous FASE reviewers for their valuable feedback
and suggestions.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort
third-party monitoring. In: Fundamental Approaches to Software Engineering.
Vol 13991. Springer Nature; 2023:260-281. doi:10.1007/978-3-031-30826-0_15'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023).
Vamos: Middleware for best-effort third-party monitoring. In Fundamental Approaches
to Software Engineering (Vol. 13991, pp. 260–281). Paris, France: Springer
Nature. https://doi.org/10.1007/978-3-031-30826-0_15'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
“Vamos: Middleware for Best-Effort Third-Party Monitoring.” In Fundamental
Approaches to Software Engineering, 13991:260–81. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30826-0_15.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware
for best-effort third-party monitoring,” in Fundamental Approaches to Software
Engineering, Paris, France, 2023, vol. 13991, pp. 260–281.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware
for best-effort third-party monitoring. Fundamental Approaches to Software Engineering.
FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.'
mla: 'Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.”
Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature,
2023, pp. 260–81, doi:10.1007/978-3-031-30826-0_15.'
short: M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental
Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FASE: Fundamental Approaches to Software Engineering'
start_date: 2023-04-22
date_created: 2023-04-20T08:29:42Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-04-25T07:19:07Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30826-0_15
ec_funded: 1
file:
- access_level: open_access
checksum: 17a7c8e08be609cf2408d37ea55e322c
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T07:16:36Z
date_updated: 2023-04-25T07:16:36Z
file_id: '12865'
file_name: 2023_LNCS_ChalupaM.pdf
file_size: 580828
relation: main_file
success: 1
file_date_updated: 2023-04-25T07:16:36Z
has_accepted_license: '1'
intvolume: ' 13991'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 260-281
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Fundamental Approaches to Software Engineering
publication_identifier:
eisbn:
- '9783031308260'
eissn:
- 1611-3349
isbn:
- '9783031308253'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '12407'
relation: earlier_version
status: public
status: public
title: 'Vamos: Middleware for best-effort third-party monitoring'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13991
year: '2023'
...
---
_id: '12876'
abstract:
- lang: eng
text: "Motivation: The problem of model inference is of fundamental importance to
systems biology. Logical models (e.g. Boolean networks; BNs) represent a computationally
attractive approach capable of handling large biological networks. The models
are typically inferred from experimental data. However, even with a substantial
amount of experimental data supported by some prior knowledge, existing inference
methods often focus on a small sample of admissible candidate models only.\r\n\r\nResults:
We propose Boolean network sketches as a new formal instrument for the inference
of Boolean networks. A sketch integrates (typically partial) knowledge about the
network’s topology and the update logic (obtained through, e.g. a biological knowledge
base or a literature search), as well as further assumptions about the properties
of the network’s transitions (e.g. the form of its attractor landscape), and additional
restrictions on the model dynamics given by the measured experimental data. Our
new BNs inference algorithm starts with an ‘initial’ sketch, which is extended
by adding restrictions representing experimental data to a ‘data-informed’ sketch
and subsequently computes all BNs consistent with the data-informed sketch. Our
algorithm is based on a symbolic representation and coloured model-checking. Our
approach is unique in its ability to cover a broad spectrum of knowledge and efficiently
produce a compact representation of all inferred BNs. We evaluate the method on
a non-trivial collection of real-world and simulated data."
acknowledgement: This work was partially supported by GACR [grant No. GA22-10845S];
and Grant Agency of Masaryk University [grant No. MUNI/G/1771/2020]. This work was
partially supported by European Union’s Horizon 2020 research and innovation programme
under the Marie Skłodowska-Curie [Grant Agreement No. 101034413 to S.P.].
article_number: btad158
article_processing_charge: No
article_type: original
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Ondřej
full_name: Huvar, Ondřej
last_name: Huvar
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
citation:
ama: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. Boolean network sketches:
A unifying framework for logical model inference. Bioinformatics. 2023;39(4).
doi:10.1093/bioinformatics/btad158'
apa: 'Beneš, N., Brim, L., Huvar, O., Pastva, S., & Šafránek, D. (2023). Boolean
network sketches: A unifying framework for logical model inference. Bioinformatics.
Oxford Academic. https://doi.org/10.1093/bioinformatics/btad158'
chicago: 'Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek.
“Boolean Network Sketches: A Unifying Framework for Logical Model Inference.”
Bioinformatics. Oxford Academic, 2023. https://doi.org/10.1093/bioinformatics/btad158.'
ieee: 'N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “Boolean network
sketches: A unifying framework for logical model inference,” Bioinformatics,
vol. 39, no. 4. Oxford Academic, 2023.'
ista: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2023. Boolean network sketches:
A unifying framework for logical model inference. Bioinformatics. 39(4), btad158.'
mla: 'Beneš, Nikola, et al. “Boolean Network Sketches: A Unifying Framework for
Logical Model Inference.” Bioinformatics, vol. 39, no. 4, btad158, Oxford
Academic, 2023, doi:10.1093/bioinformatics/btad158.'
short: N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, Bioinformatics 39 (2023).
date_created: 2023-04-30T22:01:05Z
date_published: 2023-04-03T00:00:00Z
date_updated: 2023-08-01T14:27:28Z
day: '03'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1093/bioinformatics/btad158
ec_funded: 1
external_id:
isi:
- '000976610800001'
pmid:
- '37004199'
file:
- access_level: open_access
checksum: 2cb90ddf781baefddf47eac4b54e2a03
content_type: application/pdf
creator: dernst
date_created: 2023-05-02T07:39:04Z
date_updated: 2023-05-02T07:39:04Z
file_id: '12886'
file_name: 2023_Bioinformatics_Benes.pdf
file_size: 478740
relation: main_file
success: 1
file_date_updated: 2023-05-02T07:39:04Z
has_accepted_license: '1'
intvolume: ' 39'
isi: 1
issue: '4'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Bioinformatics
publication_identifier:
eissn:
- 1367-4811
publication_status: published
publisher: Oxford Academic
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://doi.org/10.5281/zenodo.7688740
scopus_import: '1'
status: public
title: 'Boolean network sketches: A unifying framework for logical model inference'
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: 39
year: '2023'
...
---
_id: '10774'
abstract:
- lang: eng
text: We study the problem of specifying sequential information-flow properties
of systems. Information-flow properties are hyperproperties, as they compare different
traces of a system. Sequential information-flow properties can express changes,
over time, in the information-flow constraints. For example, information-flow
constraints during an initialization phase of a system may be different from information-flow
constraints that are required during the operation phase. We formalize several
variants of interpreting sequential information-flow constraints, which arise
from different assumptions about what can be observed of the system. For this
purpose, we introduce a first-order logic, called Hypertrace Logic, with both
trace and time quantifiers for specifying linear-time hyperproperties. We prove
that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted
quantifier prefixes, cannot specify the majority of the studied variants of sequential
information flow, including all variants in which the transition between sequential
phases (such as initialization and operation) happens asynchronously. Our results
rely on new equivalences between sets of traces that cannot be distinguished by
certain classes of formulas from Hypertrace Logic. This presents a new approach
to proving inexpressiveness results for HyperLTL.
acknowledgement: This work was funded in part by the Wittgenstein Award Z211-N23 of
the Austrian Science Fund (FWF) and by the FWF project W1255-N23.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- 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 Oliveira
full_name: Da Costa, Ana Oliveira
last_name: Da Costa
citation:
ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential
information flow. In: Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
Vol 13182. Springer Nature; 2022:1-19. doi:10.1007/978-3-030-94583-1_1'
apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa,
A. O. (2022). Flavors of sequential information flow. In Lecture Notes in Computer
Science (including subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics) (Vol. 13182, pp. 1–19). Philadelphia, PA, United
States: Springer Nature. https://doi.org/10.1007/978-3-030-94583-1_1'
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), 13182:1–19. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-94583-1_1.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
“Flavors of sequential information flow,” in Lecture Notes in Computer Science
(including subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), Philadelphia, PA, United States, 2022, vol. 13182, pp.
1–19.
ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors
of sequential information flow. Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182,
1–19.'
mla: Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 13182, Springer Nature, 2022, pp.
1–19, doi:10.1007/978-3-030-94583-1_1.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp.
1–19.
conference:
end_date: 2022-01-18
location: Philadelphia, PA, United States
name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
start_date: 2022-01-16
date_created: 2022-02-20T23:01:34Z
date_published: 2022-01-14T00:00:00Z
date_updated: 2022-08-05T09:02:56Z
day: '14'
department:
- _id: ToHe
doi: 10.1007/978-3-030-94583-1_1
external_id:
arxiv:
- '2105.02013'
intvolume: ' 13182'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2105.02013'
month: '01'
oa: 1
oa_version: Preprint
page: 1-19
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783030945824'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of sequential information flow
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13182
year: '2022'
...
---
_id: '10891'
abstract:
- lang: eng
text: We present a formal framework for the online black-box monitoring of software
using monitors with quantitative verdict functions. Quantitative verdict functions
have several advantages. First, quantitative monitors can be approximate, i.e.,
the value of the verdict function does not need to correspond exactly to the value
of the property under observation. Second, quantitative monitors can be quantified
universally, i.e., for every possible observed behavior, the monitor tries to
make the best effort to estimate the value of the property under observation.
Third, quantitative monitors can watch boolean as well as quantitative properties,
such as average response time. Fourth, quantitative monitors can use non-finite-state
resources, such as counters. As a consequence, quantitative monitors can be compared
according to how many resources they use (e.g., the number of counters) and how
precisely they approximate the property under observation. This allows for a rich
spectrum of cost-precision trade-offs in monitoring software.
acknowledgement: The formal framework for quantitative monitoring which is presented
in this invited talk was defined jointly with N. Ege Saraç at LICS 2021. This work
was supported in part by the Wittgenstein Award Z211-N23 of the Austrian Science
Fund.
article_processing_charge: No
author:
- 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: 'Henzinger TA. Quantitative monitoring of software. In: Software Verification.
Vol 13124. LNCS. Springer Nature; 2022:3-6. doi:10.1007/978-3-030-95561-8_1'
apa: 'Henzinger, T. A. (2022). Quantitative monitoring of software. In Software
Verification (Vol. 13124, pp. 3–6). New Haven, CT, United States: Springer
Nature. https://doi.org/10.1007/978-3-030-95561-8_1'
chicago: Henzinger, Thomas A. “Quantitative Monitoring of Software.” In Software
Verification, 13124:3–6. LNCS. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-95561-8_1.
ieee: T. A. Henzinger, “Quantitative monitoring of software,” in Software Verification,
New Haven, CT, United States, 2022, vol. 13124, pp. 3–6.
ista: 'Henzinger TA. 2022. Quantitative monitoring of software. Software Verification.
NSV: Numerical Software VerificationLNCS vol. 13124, 3–6.'
mla: Henzinger, Thomas A. “Quantitative Monitoring of Software.” Software Verification,
vol. 13124, Springer Nature, 2022, pp. 3–6, doi:10.1007/978-3-030-95561-8_1.
short: T.A. Henzinger, in:, Software Verification, Springer Nature, 2022, pp. 3–6.
conference:
end_date: 2021-10-19
location: New Haven, CT, United States
name: 'NSV: Numerical Software Verification'
start_date: 2021-10-18
date_created: 2022-03-20T23:01:40Z
date_published: 2022-02-22T00:00:00Z
date_updated: 2023-08-03T06:11:55Z
day: '22'
department:
- _id: ToHe
doi: 10.1007/978-3-030-95561-8_1
external_id:
isi:
- '000771713200001'
intvolume: ' 13124'
isi: 1
language:
- iso: eng
month: '02'
oa_version: None
page: 3-6
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Software Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030955601'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Quantitative monitoring of software
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13124
year: '2022'
...
---
_id: '11355'
abstract:
- lang: eng
text: "Contract-based design is a promising methodology for taming the complexity
of developing sophisticated systems. A formal contract distinguishes between assumptions,
which are constraints that the designer of a component puts on the environments
in which the component can be used safely, and guarantees, which are promises
that the designer asks from the team that implements the component. A theory of
formal contracts can be formalized as an interface theory, which supports the
composition and refinement of both assumptions and guarantees.\r\nAlthough there
is a rich landscape of contract-based design methods that address functional and
extra-functional properties, we present the first interface theory that is designed
for ensuring system-wide security properties. Our framework provides a refinement
relation and a composition operation that support both incremental design and
independent implementability. We develop our theory for both stateless and stateful
interfaces. We illustrate the applicability of our framework with an example inspired
from the automotive domain."
acknowledgement: This project has received funding from the European Union’s Horizon
2020 research and innovation programme under grant agreement No 956123 and was funded
in part by the FWF project W1255-N23 and by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- 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 Oliveira
full_name: Da Costa, Ana Oliveira
last_name: Da Costa
citation:
ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow
interfaces. In: Fundamental Approaches to Software Engineering. Vol 13241.
Springer Nature; 2022:3-22. doi:10.1007/978-3-030-99429-7_1'
apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa,
A. O. (2022). Information-flow interfaces. In Fundamental Approaches to Software
Engineering (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. https://doi.org/10.1007/978-3-030-99429-7_1'
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira Da Costa. “Information-Flow Interfaces.” In Fundamental Approaches
to Software Engineering, 13241:3–22. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-99429-7_1.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
“Information-flow interfaces,” in Fundamental Approaches to Software Engineering,
Munich, Germany, 2022, vol. 13241, pp. 3–22.
ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Information-flow
interfaces. Fundamental Approaches to Software Engineering. FASE: Fundamental
Approaches to Software Engineering, LNCS, vol. 13241, 3–22.'
mla: Bartocci, Ezio, et al. “Information-Flow Interfaces.” Fundamental Approaches
to Software Engineering, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:10.1007/978-3-030-99429-7_1.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
Fundamental Approaches to Software Engineering, Springer Nature, 2022, pp. 3–22.
conference:
end_date: 2022-04-07
location: Munich, Germany
name: 'FASE: Fundamental Approaches to Software Engineering'
start_date: 2022-04-02
date_created: 2022-05-08T22:01:44Z
date_published: 2022-03-29T00:00:00Z
date_updated: 2023-08-03T07:03:40Z
day: '29'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-99429-7_1
ec_funded: 1
external_id:
isi:
- '000782393600001'
file:
- access_level: open_access
checksum: 7f6f860b20b8de2a249e9c1b4eee15cf
content_type: application/pdf
creator: dernst
date_created: 2022-05-09T06:52:44Z
date_updated: 2022-05-09T06:52:44Z
file_id: '11357'
file_name: 2022_LNCS_Bartocci.pdf
file_size: 479146
relation: main_file
success: 1
file_date_updated: 2022-05-09T06:52:44Z
has_accepted_license: '1'
intvolume: ' 13241'
isi: 1
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: 3-22
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Fundamental Approaches to Software Engineering
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030994280'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Information-flow interfaces
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13241
year: '2022'
...
---
_id: '11362'
abstract:
- lang: eng
text: "Deep learning has enabled breakthroughs in challenging computing problems
and has emerged as the standard problem-solving tool for computer vision and natural
language processing tasks.\r\nOne exception to this trend is safety-critical tasks
where robustness and resilience requirements contradict the black-box nature of
neural networks. \r\nTo deploy deep learning methods for these tasks, it is vital
to provide guarantees on neural network agents' safety and robustness criteria.
\r\nThis can be achieved by developing formal verification methods to verify the
safety and robustness properties of neural networks.\r\n\r\nOur goal is to design,
develop and assess safety verification methods for neural networks to improve
their reliability and trustworthiness in real-world applications.\r\nThis thesis
establishes techniques for the verification of compressed and adversarially trained
models as well as the design of novel neural networks for verifiably safe decision-making.\r\n\r\nFirst,
we establish the problem of verifying quantized neural networks. Quantization
is a technique that trades numerical precision for the computational efficiency
of running a neural network and is widely adopted in industry.\r\nWe show that
neglecting the reduced precision when verifying a neural network can lead to wrong
conclusions about the robustness and safety of the network, highlighting that
novel techniques for quantized network verification are necessary. We introduce
several bit-exact verification methods explicitly designed for quantized neural
networks and experimentally confirm on realistic networks that the network's robustness
and other formal properties are affected by the quantization.\r\n\r\nFurthermore,
we perform a case study providing evidence that adversarial training, a standard
technique for making neural networks more robust, has detrimental effects on the
network's performance. This robustness-accuracy tradeoff has been studied before
regarding the accuracy obtained on classification datasets where each data point
is independent of all other data points. On the other hand, we investigate the
tradeoff empirically in robot learning settings where a both, a high accuracy
and a high robustness, are desirable.\r\nOur results suggest that the negative
side-effects of adversarial training outweigh its robustness benefits in practice.\r\n\r\nFinally,
we consider the problem of verifying safety when running a Bayesian neural network
policy in a feedback loop with systems over the infinite time horizon. Bayesian
neural networks are probabilistic models for learning uncertainties in the data
and are therefore often used on robotic and healthcare applications where data
is inherently stochastic.\r\nWe introduce a method for recalibrating Bayesian
neural networks so that they yield probability distributions over safe decisions
only.\r\nOur method learns a safety certificate that guarantees safety over the
infinite time horizon to determine which decisions are safe in every possible
state of the system.\r\nWe demonstrate the effectiveness of our approach on a
series of reinforcement learning benchmarks."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
citation:
ama: Lechner M. Learning verifiable representations. 2022. doi:10.15479/at:ista:11362
apa: Lechner, M. (2022). Learning verifiable representations. Institute of
Science and Technology Austria. https://doi.org/10.15479/at:ista:11362
chicago: Lechner, Mathias. “Learning Verifiable Representations.” Institute of Science
and Technology Austria, 2022. https://doi.org/10.15479/at:ista:11362.
ieee: M. Lechner, “Learning verifiable representations,” Institute of Science and
Technology Austria, 2022.
ista: Lechner M. 2022. Learning verifiable representations. Institute of Science
and Technology Austria.
mla: Lechner, Mathias. Learning Verifiable Representations. Institute of
Science and Technology Austria, 2022, doi:10.15479/at:ista:11362.
short: M. Lechner, Learning Verifiable Representations, Institute of Science and
Technology Austria, 2022.
date_created: 2022-05-12T07:14:01Z
date_published: 2022-05-12T00:00:00Z
date_updated: 2025-07-14T09:10:11Z
day: '12'
ddc:
- '004'
degree_awarded: PhD
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/at:ista:11362
ec_funded: 1
file:
- access_level: closed
checksum: 8eefa9c7c10ca7e1a2ccdd731962a645
content_type: application/zip
creator: mlechner
date_created: 2022-05-13T12:33:26Z
date_updated: 2022-05-13T12:49:00Z
file_id: '11378'
file_name: src.zip
file_size: 13210143
relation: source_file
- access_level: open_access
checksum: 1b9e1e5a9a83ed9d89dad2f5133dc026
content_type: application/pdf
creator: mlechner
date_created: 2022-05-16T08:02:28Z
date_updated: 2022-05-17T15:19:39Z
file_id: '11382'
file_name: thesis_main-a2.pdf
file_size: 2732536
relation: main_file
file_date_updated: 2022-05-17T15:19:39Z
has_accepted_license: '1'
keyword:
- neural networks
- verification
- machine learning
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: '124'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
isbn:
- 978-3-99078-017-6
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '11366'
relation: part_of_dissertation
status: public
- id: '7808'
relation: part_of_dissertation
status: public
- id: '10666'
relation: part_of_dissertation
status: public
- id: '10665'
relation: part_of_dissertation
status: public
- id: '10667'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Learning verifiable representations
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '11366'
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\r\ncome 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\r\nbut 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\r\nconjunction with adversarial robot learning
can make adversarial training suitable for real-world robot applications. We evaluate
a wide variety of robot learning tasks ranging from autonomous driving in a high-fidelity
environment\r\namenable to sim-to-real deployment, to mobile robot gesture recognition.
Our results demonstrate that, while these techniques make incremental improvements
on the trade-off on a relative scale, the negative side-effects caused by\r\nadversarial
training still outweigh the improvements by an order of magnitude. We conclude
that more substantial advances in robust learning methods are necessary before
they can benefit robot learning tasks in practice."
acknowledgement: "This work was supported in parts by the ERC-2020-AdG 101020093,
National Science Foundation (NSF), and JP\r\nMorgan Graduate Fellowships. We thank
Christoph Lampert for inspiring this work.\r\n"
article_number: '2204.07373'
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: 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. arXiv. doi:10.48550/arXiv.2204.07373
apa: Lechner, M., Amini, A., Rus, D., & Henzinger, T. A. (n.d.). Revisiting
the adversarial robustness-accuracy tradeoff in robot learning. arXiv.
https://doi.org/10.48550/arXiv.2204.07373
chicago: Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger.
“Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” ArXiv,
n.d. https://doi.org/10.48550/arXiv.2204.07373.
ieee: M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial
robustness-accuracy tradeoff in robot learning,” arXiv. .
ista: Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy
tradeoff in robot learning. arXiv, 2204.07373.
mla: Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff
in Robot Learning.” ArXiv, 2204.07373, doi:10.48550/arXiv.2204.07373.
short: M. Lechner, A. Amini, D. Rus, T.A. Henzinger, ArXiv (n.d.).
date_created: 2022-05-12T13:20:17Z
date_published: 2022-04-15T00:00:00Z
date_updated: 2023-08-01T13:36:50Z
day: '15'
department:
- _id: ToHe
doi: 10.48550/arXiv.2204.07373
ec_funded: 1
external_id:
arxiv:
- '2204.07373'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2204.07373
month: '04'
oa: 1
oa_version: Preprint
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: arXiv
publication_status: submitted
related_material:
record:
- id: '11362'
relation: dissertation_contains
status: public
- id: '12704'
relation: later_version
status: public
status: public
title: Revisiting the adversarial robustness-accuracy tradeoff in robot learning
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2022'
...
---
_id: '11775'
abstract:
- lang: eng
text: 'Quantitative monitoring can be universal and approximate: For every finite
sequence of observations, the specification provides a value and the monitor outputs
a best-effort approximation of it. The quality of the approximation may depend
on the resources that are available to the monitor. By taking to the limit the
sequences of specification values and monitor outputs, we obtain precision-resource
trade-offs also for limit monitoring. This paper provides a formal framework for
studying such trade-offs using an abstract interpretation for monitors: For each
natural number n, the aggregate semantics of a monitor at time n is an equivalence
relation over all sequences of at most n observations so that two equivalent sequences
are indistinguishable to the monitor and thus mapped to the same output. This
abstract interpretation of quantitative monitors allows us to measure the number
of equivalence classes (or “resource use”) that is necessary for a certain precision
up to a certain time, or at any time. Our framework offers several insights. For
example, we identify a family of specifications for which any resource-optimal
exact limit monitor is independent of any error permitted over finite traces.
Moreover, we present a specification for which any resource-optimal approximate
limit monitor does not minimize its resource use at any time. '
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: Yes
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. Abstract monitors for quantitative specifications.
In: 22nd International Conference on Runtime Verification. Vol 13498. Springer
Nature; 2022:200-220. doi:10.1007/978-3-031-17196-3_11'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2022). Abstract monitors
for quantitative specifications. In 22nd International Conference on Runtime
Verification (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature.
https://doi.org/10.1007/978-3-031-17196-3_11'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract
Monitors for Quantitative Specifications.” In 22nd International Conference
on Runtime Verification, 13498:200–220. Springer Nature, 2022. https://doi.org/10.1007/978-3-031-17196-3_11.
ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for
quantitative specifications,” in 22nd International Conference on Runtime Verification,
Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2022. Abstract monitors for quantitative
specifications. 22nd International Conference on Runtime Verification. RV: Runtime
Verification, LNCS, vol. 13498, 200–220.'
mla: Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.”
22nd International Conference on Runtime Verification, vol. 13498, Springer
Nature, 2022, pp. 200–20, doi:10.1007/978-3-031-17196-3_11.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference
on Runtime Verification, Springer Nature, 2022, pp. 200–220.
conference:
end_date: 2022-09-30
location: Tbilisi, Georgia
name: 'RV: Runtime Verification'
start_date: 2022-09-28
date_created: 2022-08-08T17:09:09Z
date_published: 2022-09-23T00:00:00Z
date_updated: 2023-08-03T13:38:46Z
day: '23'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-17196-3_11
ec_funded: 1
external_id:
isi:
- '000866539700011'
file:
- access_level: open_access
checksum: 05c7dcfbb9053a98f46441fb2eccb213
content_type: application/pdf
creator: dernst
date_created: 2023-01-20T07:34:50Z
date_updated: 2023-01-20T07:34:50Z
file_id: '12317'
file_name: 2022_LNCS_RV_Henzinger.pdf
file_size: 477110
relation: main_file
success: 1
file_date_updated: 2023-01-20T07:34:50Z
has_accepted_license: '1'
intvolume: ' 13498'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 200-220
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 22nd International Conference on Runtime Verification
publication_identifier:
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstract monitors for quantitative specifications
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13498
year: '2022'
...
---
_id: '14600'
abstract:
- lang: eng
text: We study the problem of learning controllers for discrete-time non-linear
stochastic dynamical systems with formal reach-avoid guarantees. This work presents
the first method for providing formal reach-avoid guarantees, which combine and
generalize stability and safety guarantees, with a tolerable probability threshold
$p\in[0,1]$ over the infinite time horizon. Our method leverages advances in machine
learning literature and it represents formal certificates as neural networks.
In particular, we learn a certificate in the form of a reach-avoid supermartingale
(RASM), a novel notion that we introduce in this work. Our RASMs provide reachability
and avoidance guarantees by imposing constraints on what can be viewed as a stochastic
extension of level sets of Lyapunov functions for deterministic systems. Our approach
solves several important problems -- it can be used to learn a control policy
from scratch, to verify a reach-avoid specification for a fixed control policy,
or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification.
We validate our approach on $3$ stochastic non-linear reinforcement learning tasks.
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- 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: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. arXiv. doi:10.48550/ARXIV.2210.05308
apa: Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (n.d.). Learning
control policies for stochastic systems with reach-avoid guarantees. arXiv.
https://doi.org/10.48550/ARXIV.2210.05308
chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee.
“Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.”
ArXiv, n.d. https://doi.org/10.48550/ARXIV.2210.05308.
ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control
policies for stochastic systems with reach-avoid guarantees,” arXiv. .
ista: Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. arXiv, 10.48550/ARXIV.2210.05308.
mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with
Reach-Avoid Guarantees.” ArXiv, doi:10.48550/ARXIV.2210.05308.
short: D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, ArXiv (n.d.).
date_created: 2023-11-24T13:10:09Z
date_published: 2022-11-29T00:00:00Z
date_updated: 2025-07-14T09:10:02Z
day: '29'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/ARXIV.2210.05308
ec_funded: 1
external_id:
arxiv:
- '2210.05308'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-sa/4.0/
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2210.05308
month: '11'
oa: 1
oa_version: Preprint
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: arXiv
publication_status: submitted
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
- id: '14830'
relation: later_version
status: public
status: public
title: Learning control policies for stochastic systems with reach-avoid guarantees
tmp:
image: /images/cc_by_sa.png
legal_code_url: https://creativecommons.org/licenses/by-sa/4.0/legalcode
name: Creative Commons Attribution-ShareAlike 4.0 International Public License (CC
BY-SA 4.0)
short: CC BY-SA (4.0)
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '14601'
abstract:
- lang: eng
text: "In this work, we address the problem of learning provably stable neural\r\nnetwork
policies for stochastic control systems. While recent work has\r\ndemonstrated
the feasibility of certifying given policies using martingale\r\ntheory, the problem
of how to learn such policies is little explored. Here, we\r\nstudy the effectiveness
of jointly learning a policy together with a martingale\r\ncertificate that proves
its stability using a single learning algorithm. We\r\nobserve that the joint
optimization problem becomes easily stuck in local\r\nminima when starting from
a randomly initialized policy. Our results suggest\r\nthat some form of pre-training
of the policy is required for the joint\r\noptimization to repair and verify the
policy successfully."
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- 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
citation:
ama: Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies
in stochastic control systems. arXiv. doi:10.48550/arXiv.2205.11991
apa: Zikelic, D., Lechner, M., Chatterjee, K., & Henzinger, T. A. (n.d.). Learning
stabilizing policies in stochastic control systems. arXiv. https://doi.org/10.48550/arXiv.2205.11991
chicago: Zikelic, Dorde, Mathias Lechner, Krishnendu Chatterjee, and Thomas A Henzinger.
“Learning Stabilizing Policies in Stochastic Control Systems.” ArXiv, n.d.
https://doi.org/10.48550/arXiv.2205.11991.
ieee: D. Zikelic, M. Lechner, K. Chatterjee, and T. A. Henzinger, “Learning stabilizing
policies in stochastic control systems,” arXiv. .
ista: Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies
in stochastic control systems. arXiv, 10.48550/arXiv.2205.11991.
mla: Zikelic, Dorde, et al. “Learning Stabilizing Policies in Stochastic Control
Systems.” ArXiv, doi:10.48550/arXiv.2205.11991.
short: D. Zikelic, M. Lechner, K. Chatterjee, T.A. Henzinger, ArXiv (n.d.).
date_created: 2023-11-24T13:22:30Z
date_published: 2022-05-24T00:00:00Z
date_updated: 2025-07-14T09:10:00Z
day: '24'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/arXiv.2205.11991
ec_funded: 1
external_id:
arxiv:
- '2205.11991'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2205.11991
month: '05'
oa: 1
oa_version: Preprint
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: arXiv
publication_status: submitted
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
status: public
title: Learning stabilizing policies in stochastic control systems
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '12010'
abstract:
- lang: eng
text: World models learn behaviors in a latent imagination space to enhance the
sample-efficiency of deep reinforcement learning (RL) algorithms. While learning
world models for high-dimensional observations (e.g., pixel inputs) has become
practicable on standard RL benchmarks and some games, their effectiveness in real-world
robotics applications has not been explored. In this paper, we investigate how
such agents generalize to real-world autonomous vehicle control tasks, where advanced
model-free deep RL algorithms fail. In particular, we set up a series of time-lap
tasks for an F1TENTH racing robot, equipped with a high-dimensional LiDAR sensor,
on a set of test tracks with a gradual increase in their complexity. In this continuous-control
setting, we show that model-based agents capable of learning in imagination substantially
outperform model-free agents with respect to performance, sample efficiency, successful
task completion, and generalization. Moreover, we show that the generalization
ability of model-based agents strongly depends on the choice of their observation
model. We provide extensive empirical evidence for the effectiveness of world
models provided with long enough memory horizons in sim2real tasks.
acknowledgement: L.B. was supported by the Doctoral College Resilient Embedded Systems.
M.L. was supported in part by the ERC2020-AdG 101020093 and the Austrian Science
Fund (FWF) under grant Z211-N23 (Wittgenstein Award). R.H. and D.R. were supported
by The Boeing Company and the Office of Naval Research (ONR) Grant N00014-18-1-2830.
R.G. was partially supported by the Horizon-2020 ECSEL Project grant No. 783163
(iDev40) and A.B. by FFG Project ADEX.
article_processing_charge: No
arxiv: 1
author:
- first_name: Axel
full_name: Brunnbauer, Axel
last_name: Brunnbauer
- first_name: Luigi
full_name: Berducci, Luigi
last_name: Berducci
- first_name: Andreas
full_name: Brandstatter, Andreas
last_name: Brandstatter
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Brunnbauer A, Berducci L, Brandstatter A, et al. Latent imagination facilitates
zero-shot transfer in autonomous racing. In: 2022 International Conference
on Robotics and Automation. IEEE; 2022:7513-7520. doi:10.1109/ICRA46639.2022.9811650'
apa: 'Brunnbauer, A., Berducci, L., Brandstatter, A., Lechner, M., Hasani, R., Rus,
D., & Grosu, R. (2022). Latent imagination facilitates zero-shot transfer
in autonomous racing. In 2022 International Conference on Robotics and Automation
(pp. 7513–7520). Philadelphia, PA, United States: IEEE. https://doi.org/10.1109/ICRA46639.2022.9811650'
chicago: Brunnbauer, Axel, Luigi Berducci, Andreas Brandstatter, Mathias Lechner,
Ramin Hasani, Daniela Rus, and Radu Grosu. “Latent Imagination Facilitates Zero-Shot
Transfer in Autonomous Racing.” In 2022 International Conference on Robotics
and Automation, 7513–20. IEEE, 2022. https://doi.org/10.1109/ICRA46639.2022.9811650.
ieee: A. Brunnbauer et al., “Latent imagination facilitates zero-shot transfer
in autonomous racing,” in 2022 International Conference on Robotics and Automation,
Philadelphia, PA, United States, 2022, pp. 7513–7520.
ista: 'Brunnbauer A, Berducci L, Brandstatter A, Lechner M, Hasani R, Rus D, Grosu
R. 2022. Latent imagination facilitates zero-shot transfer in autonomous racing.
2022 International Conference on Robotics and Automation. ICRA: International
Conference on Robotics and Automation, 7513–7520.'
mla: Brunnbauer, Axel, et al. “Latent Imagination Facilitates Zero-Shot Transfer
in Autonomous Racing.” 2022 International Conference on Robotics and Automation,
IEEE, 2022, pp. 7513–20, doi:10.1109/ICRA46639.2022.9811650.
short: A. Brunnbauer, L. Berducci, A. Brandstatter, M. Lechner, R. Hasani, D. Rus,
R. Grosu, in:, 2022 International Conference on Robotics and Automation, IEEE,
2022, pp. 7513–7520.
conference:
end_date: 2022-05-27
location: Philadelphia, PA, United States
name: 'ICRA: International Conference on Robotics and Automation'
start_date: 2022-05-23
date_created: 2022-09-04T22:02:02Z
date_published: 2022-07-12T00:00:00Z
date_updated: 2022-09-05T08:46:12Z
day: '12'
department:
- _id: ToHe
doi: 10.1109/ICRA46639.2022.9811650
ec_funded: 1
external_id:
arxiv:
- '2103.04909'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2103.04909
month: '07'
oa: 1
oa_version: Preprint
page: 7513-7520
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 2022 International Conference on Robotics and Automation
publication_identifier:
isbn:
- '9781728196817'
issn:
- 1050-4729
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Latent imagination facilitates zero-shot transfer in autonomous racing
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2022'
...
---
_id: '12147'
abstract:
- lang: eng
text: Continuous-time neural networks are a class of machine learning systems that
can tackle representation learning on spatiotemporal decision-making tasks. These
models are typically represented by continuous differential equations. However,
their expressive power when they are deployed on computers is bottlenecked by
numerical differential equation solvers. This limitation has notably slowed down
the scaling and understanding of numerous natural physical phenomena such as the
dynamics of nervous systems. Ideally, we would circumvent this bottleneck by solving
the given dynamical system in closed form. This is known to be intractable in
general. Here, we show that it is possible to closely approximate the interaction
between neurons and synapses—the building blocks of natural and artificial neural
networks—constructed by liquid time-constant networks efficiently in closed form.
To this end, we compute a tightly bounded approximation of the solution of an
integral appearing in liquid time-constant dynamics that has had no known closed-form
solution so far. This closed-form solution impacts the design of continuous-time
and continuous-depth neural models. For instance, since time appears explicitly
in closed form, the formulation relaxes the need for complex numerical solvers.
Consequently, we obtain models that are between one and five orders of magnitude
faster in training and inference compared with differential equation-based counterparts.
More importantly, in contrast to ordinary differential equation-based continuous
networks, closed-form networks can scale remarkably well compared with other deep
learning instances. Lastly, as these models are derived from liquid networks,
they show good performance in time-series modelling compared with advanced recurrent
neural network models.
acknowledgement: This research was supported in part by the AI2050 program at Schmidt
Futures (grant G-22-63172), the Boeing Company, and the United States Air Force
Research Laboratory and the United States Air Force Artificial Intelligence Accelerator
and was accomplished under cooperative agreement number FA8750-19-2-1000. 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,
of 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 notation herein. This work was further supported by The Boeing Company
and Office of Naval Research grant N00014-18-1-2830. M.T. is supported by the Poul
Due Jensen Foundation, grant 883901. M.L. was supported in part by the Austrian
Science Fund under grant Z211-N23 (Wittgenstein Award). A.A. was supported by the
National Science Foundation Graduate Research Fellowship Program. We thank T.-H.
Wang, P. Kao, M. Chahine, W. Xiao, X. Li, L. Yin and Y. Ben for useful suggestions
and for testing of CfC models to confirm the results across other domains.
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- 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: Lucas
full_name: Liebenwein, Lucas
last_name: Liebenwein
- first_name: Aaron
full_name: Ray, Aaron
last_name: Ray
- first_name: Max
full_name: Tschaikowski, Max
last_name: Tschaikowski
- first_name: Gerald
full_name: Teschl, Gerald
last_name: Teschl
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: Hasani R, Lechner M, Amini A, et al. Closed-form continuous-time neural networks.
Nature Machine Intelligence. 2022;4(11):992-1003. doi:10.1038/s42256-022-00556-7
apa: Hasani, R., Lechner, M., Amini, A., Liebenwein, L., Ray, A., Tschaikowski,
M., … Rus, D. (2022). Closed-form continuous-time neural networks. Nature Machine
Intelligence. Springer Nature. https://doi.org/10.1038/s42256-022-00556-7
chicago: Hasani, Ramin, Mathias Lechner, Alexander Amini, Lucas Liebenwein, Aaron
Ray, Max Tschaikowski, Gerald Teschl, and Daniela Rus. “Closed-Form Continuous-Time
Neural Networks.” Nature Machine Intelligence. Springer Nature, 2022. https://doi.org/10.1038/s42256-022-00556-7.
ieee: R. Hasani et al., “Closed-form continuous-time neural networks,” Nature
Machine Intelligence, vol. 4, no. 11. Springer Nature, pp. 992–1003, 2022.
ista: Hasani R, Lechner M, Amini A, Liebenwein L, Ray A, Tschaikowski M, Teschl
G, Rus D. 2022. Closed-form continuous-time neural networks. Nature Machine Intelligence.
4(11), 992–1003.
mla: Hasani, Ramin, et al. “Closed-Form Continuous-Time Neural Networks.” Nature
Machine Intelligence, vol. 4, no. 11, Springer Nature, 2022, pp. 992–1003,
doi:10.1038/s42256-022-00556-7.
short: R. Hasani, M. Lechner, A. Amini, L. Liebenwein, A. Ray, M. Tschaikowski,
G. Teschl, D. Rus, Nature Machine Intelligence 4 (2022) 992–1003.
date_created: 2023-01-12T12:07:21Z
date_published: 2022-11-15T00:00:00Z
date_updated: 2023-08-04T09:00:10Z
day: '15'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1038/s42256-022-00556-7
external_id:
arxiv:
- '2106.13898'
isi:
- '000884215600003'
file:
- access_level: open_access
checksum: b4789122ce04bfb4ac042390f59aaa8b
content_type: application/pdf
creator: dernst
date_created: 2023-01-24T09:49:44Z
date_updated: 2023-01-24T09:49:44Z
file_id: '12355'
file_name: 2022_NatureMachineIntelligence_Hasani.pdf
file_size: 3259553
relation: main_file
success: 1
file_date_updated: 2023-01-24T09:49:44Z
has_accepted_license: '1'
intvolume: ' 4'
isi: 1
issue: '11'
keyword:
- Artificial Intelligence
- Computer Networks and Communications
- Computer Vision and Pattern Recognition
- Human-Computer Interaction
- Software
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: 992-1003
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Nature Machine Intelligence
publication_identifier:
issn:
- 2522-5839
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
link:
- relation: erratum
url: https://doi.org/10.1038/s42256-022-00597-y
scopus_import: '1'
status: public
title: Closed-form continuous-time neural 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: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 4
year: '2022'
...