---
_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
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: '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'
...
---
_id: '8912'
abstract:
- lang: eng
text: "For automata, synchronization, the problem of bringing an automaton to a
particular state regardless of its initial state, is important. It has several
applications in practice and is related to a fifty-year-old conjecture on the
length of the shortest synchronizing word. Although using shorter words increases
the effectiveness in practice, finding a shortest one (which is not necessarily
unique) is NP-hard. For this reason, there exist various heuristics in the literature.
However, high-quality heuristics such as SynchroP producing relatively shorter
sequences are very expensive and can take hours when the automaton has tens of
thousands of states. The SynchroP heuristic has been frequently used as a benchmark
to evaluate the performance of the new heuristics. In this work, we first improve
the runtime of SynchroP and its variants by using algorithmic techniques. We then
focus on adapting SynchroP for many-core architectures,\r\nand overall, we obtain
more than 1000× speedup on GPUs compared to naive sequential implementation that
has been frequently used as a benchmark to evaluate new heuristics in the literature.
We also propose two SynchroP variants and evaluate their performance."
acknowledgement: This work was supported by The Scientific and Technological Research
Council of Turkey (TUBITAK) [grant number 114E569]. This research was supported
in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).
We would like to thank the authors of (Roman & Szykula, 2015) for providing their
heuristics implementations, which we used to compare our SynchroP implementation
as given in Table 11.
article_number: '114203'
article_processing_charge: No
article_type: original
author:
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
- first_name: Ömer Faruk
full_name: Altun, Ömer Faruk
last_name: Altun
- first_name: Kamil Tolga
full_name: Atam, Kamil Tolga
last_name: Atam
- first_name: Sertac
full_name: Karahoda, Sertac
last_name: Karahoda
- first_name: Kamer
full_name: Kaya, Kamer
last_name: Kaya
- first_name: Hüsnü
full_name: Yenigün, Hüsnü
last_name: Yenigün
citation:
ama: Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. Boosting expensive
synchronizing heuristics. Expert Systems with Applications. 2021;167(4).
doi:10.1016/j.eswa.2020.114203
apa: Sarac, N. E., Altun, Ö. F., Atam, K. T., Karahoda, S., Kaya, K., & Yenigün,
H. (2021). Boosting expensive synchronizing heuristics. Expert Systems with
Applications. Elsevier. https://doi.org/10.1016/j.eswa.2020.114203
chicago: Sarac, Naci E, Ömer Faruk Altun, Kamil Tolga Atam, Sertac Karahoda, Kamer
Kaya, and Hüsnü Yenigün. “Boosting Expensive Synchronizing Heuristics.” Expert
Systems with Applications. Elsevier, 2021. https://doi.org/10.1016/j.eswa.2020.114203.
ieee: N. E. Sarac, Ö. F. Altun, K. T. Atam, S. Karahoda, K. Kaya, and H. Yenigün,
“Boosting expensive synchronizing heuristics,” Expert Systems with Applications,
vol. 167, no. 4. Elsevier, 2021.
ista: Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. 2021. Boosting
expensive synchronizing heuristics. Expert Systems with Applications. 167(4),
114203.
mla: Sarac, Naci E., et al. “Boosting Expensive Synchronizing Heuristics.” Expert
Systems with Applications, vol. 167, no. 4, 114203, Elsevier, 2021, doi:10.1016/j.eswa.2020.114203.
short: N.E. Sarac, Ö.F. Altun, K.T. Atam, S. Karahoda, K. Kaya, H. Yenigün, Expert
Systems with Applications 167 (2021).
date_created: 2020-12-02T13:34:25Z
date_published: 2021-04-01T00:00:00Z
date_updated: 2023-08-04T11:19:00Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.eswa.2020.114203
external_id:
isi:
- '000640531100038'
file:
- access_level: open_access
checksum: 600c2f81bc898a725bcfa7cf26ff4fed
content_type: application/pdf
creator: esarac
date_created: 2020-12-02T13:33:51Z
date_updated: 2020-12-02T13:33:51Z
file_id: '8913'
file_name: synchroPaperRevised.pdf
file_size: 634967
relation: main_file
file_date_updated: 2020-12-02T13:33:51Z
has_accepted_license: '1'
intvolume: ' 167'
isi: 1
issue: '4'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Expert Systems with Applications
publication_identifier:
issn:
- '09574174'
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Boosting expensive synchronizing heuristics
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 167
year: '2021'
...
---
_id: '9200'
abstract:
- lang: eng
text: Formal design of embedded and cyber-physical systems relies on mathematical
modeling. In this paper, we consider the model class of hybrid automata whose
dynamics are defined by affine differential equations. Given a set of time-series
data, we present an algorithmic approach to synthesize a hybrid automaton exhibiting
behavior that is close to the data, up to a specified precision, and changes in
synchrony with the data. A fundamental problem in our synthesis algorithm is to
check membership of a time series in a hybrid automaton. Our solution integrates
reachability and optimization techniques for affine dynamical systems to obtain
both a sufficient and a necessary condition for membership, combined in a refinement
framework. The algorithm processes one time series at a time and hence can be
interrupted, provide an intermediate result, and be resumed. We report experimental
results demonstrating the applicability of our synthesis approach.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award) and the European Union’s Horizon
2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement
No. 754411.
article_processing_charge: No
arxiv: 1
author:
- first_name: Miriam
full_name: Garcia Soto, Miriam
id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
last_name: Garcia Soto
orcid: 0000-0003-2936-5719
- 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: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Garcia Soto M, Henzinger TA, Schilling C. Synthesis of hybrid automata with
affine dynamics from time-series data. In: HSCC ’21: Proceedings of the 24th
International Conference on Hybrid Systems: Computation and Control. Association
for Computing Machinery; 2021:2102.12734. doi:10.1145/3447928.3456704'
apa: 'Garcia Soto, M., Henzinger, T. A., & Schilling, C. (2021). Synthesis of
hybrid automata with affine dynamics from time-series data. In HSCC ’21: Proceedings
of the 24th International Conference on Hybrid Systems: Computation and Control
(p. 2102.12734). Nashville, TN, United States: Association for Computing Machinery.
https://doi.org/10.1145/3447928.3456704'
chicago: 'Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis
of Hybrid Automata with Affine Dynamics from Time-Series Data.” In HSCC ’21:
Proceedings of the 24th International Conference on Hybrid Systems: Computation
and Control, 2102.12734. Association for Computing Machinery, 2021. https://doi.org/10.1145/3447928.3456704.'
ieee: 'M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of hybrid automata
with affine dynamics from time-series data,” in HSCC ’21: Proceedings of the
24th International Conference on Hybrid Systems: Computation and Control,
Nashville, TN, United States, 2021, p. 2102.12734.'
ista: 'Garcia Soto M, Henzinger TA, Schilling C. 2021. Synthesis of hybrid automata
with affine dynamics from time-series data. HSCC ’21: Proceedings of the 24th
International Conference on Hybrid Systems: Computation and Control. HSCC: International
Conference on Hybrid Systems Computation and Control, 2102.12734.'
mla: 'Garcia Soto, Miriam, et al. “Synthesis of Hybrid Automata with Affine Dynamics
from Time-Series Data.” HSCC ’21: Proceedings of the 24th International Conference
on Hybrid Systems: Computation and Control, Association for Computing Machinery,
2021, p. 2102.12734, doi:10.1145/3447928.3456704.'
short: 'M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, HSCC ’21: Proceedings
of the 24th International Conference on Hybrid Systems: Computation and Control,
Association for Computing Machinery, 2021, p. 2102.12734.'
conference:
end_date: 2021-05-21
location: Nashville, TN, United States
name: 'HSCC: International Conference on Hybrid Systems Computation and Control'
start_date: 2021-05-19
date_created: 2021-02-26T16:30:39Z
date_published: 2021-05-01T00:00:00Z
date_updated: 2023-08-07T13:49:33Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3447928.3456704
ec_funded: 1
external_id:
arxiv:
- '2102.12734'
isi:
- '000932821700028'
file:
- access_level: open_access
checksum: 4c1202c1abf71384c3ee6fea88c2f80e
content_type: application/pdf
creator: kschuh
date_created: 2021-05-25T13:53:22Z
date_updated: 2021-05-25T13:53:22Z
file_id: '9424'
file_name: 2021_HSCC_Soto.pdf
file_size: 1474786
relation: main_file
success: 1
file_date_updated: 2021-05-25T13:53:22Z
has_accepted_license: '1'
isi: 1
keyword:
- hybrid automaton
- membership
- system identification
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: '2102.12734'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: 'HSCC ''21: Proceedings of the 24th International Conference on Hybrid
Systems: Computation and Control'
publication_identifier:
isbn:
- '9781450383394'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of hybrid automata with affine dynamics from time-series data
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
year: '2021'
...
---
_id: '9239'
abstract:
- lang: eng
text: 'A graph game proceeds as follows: two players move a token through a graph
to produce a finite or infinite path, which determines the payoff of the game.
We study bidding games in which in each turn, an auction determines which player
moves the token. Bidding games were largely studied in combination with two variants
of first-price auctions called “Richman” and “poorman” bidding. We study taxman
bidding, which span the spectrum between the two. The game is parameterized by
a constant : portion τ of the winning bid is paid to the other player, and portion to
the bank. While finite-duration (reachability) taxman games have been studied
before, we present, for the first time, results on infinite-duration taxman games:
we unify, generalize, and simplify previous equivalences between bidding games
and a class of stochastic games called random-turn games.'
article_processing_charge: No
article_type: original
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Đorđe
full_name: Žikelić, Đorđe
last_name: Žikelić
citation:
ama: Avni G, Henzinger TA, Žikelić Đ. Bidding mechanisms in graph games. Journal
of Computer and System Sciences. 2021;119(8):133-144. doi:10.1016/j.jcss.2021.02.008
apa: Avni, G., Henzinger, T. A., & Žikelić, Đ. (2021). Bidding mechanisms in
graph games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2021.02.008
chicago: Avni, Guy, Thomas A Henzinger, and Đorđe Žikelić. “Bidding Mechanisms in
Graph Games.” Journal of Computer and System Sciences. Elsevier, 2021.
https://doi.org/10.1016/j.jcss.2021.02.008.
ieee: G. Avni, T. A. Henzinger, and Đ. Žikelić, “Bidding mechanisms in graph games,”
Journal of Computer and System Sciences, vol. 119, no. 8. Elsevier, pp.
133–144, 2021.
ista: Avni G, Henzinger TA, Žikelić Đ. 2021. Bidding mechanisms in graph games.
Journal of Computer and System Sciences. 119(8), 133–144.
mla: Avni, Guy, et al. “Bidding Mechanisms in Graph Games.” Journal of Computer
and System Sciences, vol. 119, no. 8, Elsevier, 2021, pp. 133–44, doi:10.1016/j.jcss.2021.02.008.
short: G. Avni, T.A. Henzinger, Đ. Žikelić, Journal of Computer and System Sciences
119 (2021) 133–144.
date_created: 2021-03-14T23:01:32Z
date_published: 2021-03-03T00:00:00Z
date_updated: 2023-08-07T14:08:34Z
day: '03'
department:
- _id: ToHe
doi: 10.1016/j.jcss.2021.02.008
external_id:
arxiv:
- '1905.03835'
isi:
- '000634149800009'
intvolume: ' 119'
isi: 1
issue: '8'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.1905.03835
month: '03'
oa: 1
oa_version: Preprint
page: 133-144
publication: Journal of Computer and System Sciences
publication_identifier:
eissn:
- 1090-2724
issn:
- 0022-0000
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '6884'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Bidding mechanisms in graph games
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 119
year: '2021'
...
---
_id: '9281'
abstract:
- lang: eng
text: We comment on two formal proofs of Fermat's sum of two squares theorem, written
using the Mathematical Components libraries of the Coq proof assistant. The first
one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's
recent new proof relying on partition-theoretic arguments. Both formal proofs
rely on a general property of involutions of finite sets, of independent interest.
The proof technique consists for the most part of automating recurrent tasks (such
as case distinctions and computations on natural numbers) via ad hoc tactics.
article_number: '2103.11389'
article_processing_charge: No
arxiv: 1
author:
- first_name: Guillaume
full_name: Dubach, Guillaume
id: D5C6A458-10C4-11EA-ABF4-A4B43DDC885E
last_name: Dubach
orcid: 0000-0001-6892-8137
- 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
citation:
ama: Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv.
doi:10.48550/arXiv.2103.11389
apa: Dubach, G., & Mühlböck, F. (n.d.). Formal verification of Zagier’s one-sentence
proof. arXiv. https://doi.org/10.48550/arXiv.2103.11389
chicago: Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s
One-Sentence Proof.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2103.11389.
ieee: G. Dubach and F. Mühlböck, “Formal verification of Zagier’s one-sentence proof,”
arXiv. .
ista: Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof.
arXiv, 2103.11389.
mla: Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence
Proof.” ArXiv, 2103.11389, doi:10.48550/arXiv.2103.11389.
short: G. Dubach, F. Mühlböck, ArXiv (n.d.).
date_created: 2021-03-23T05:38:48Z
date_published: 2021-03-21T00:00:00Z
date_updated: 2023-05-03T10:26:45Z
day: '21'
department:
- _id: LaEr
- _id: ToHe
doi: 10.48550/arXiv.2103.11389
ec_funded: 1
external_id:
arxiv:
- '2103.11389'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2103.11389
month: '03'
oa: 1
oa_version: Preprint
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: arXiv
publication_status: submitted
related_material:
record:
- id: '9946'
relation: other
status: public
status: public
title: Formal verification of Zagier's one-sentence proof
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2021'
...
---
_id: '9356'
abstract:
- lang: eng
text: 'In runtime verification, a monitor watches a trace of a system and, if possible,
decides after observing each finite prefix whether or not the unknown infinite
trace satisfies a given specification. We generalize the theory of runtime verification
to monitors that attempt to estimate numerical values of quantitative trace properties
(instead of attempting to conclude boolean values of trace specifications), such
as maximal or average response time along a trace. Quantitative monitors are approximate:
with every finite prefix, they can improve their estimate of the infinite trace''s
unknown property value. Consequently, quantitative monitors can be compared with
regard to a precision-cost trade-off: better approximations of the property value
require more monitor resources, such as states (in the case of finite-state monitors)
or registers, and additional resources yield better approximations. We introduce
a formal framework for quantitative and approximate monitoring, show how it conservatively
generalizes the classical boolean setting for monitoring, and give several precision-cost
trade-offs for monitors. For example, we prove that there are quantitative properties
for which every additional register improves monitoring precision.'
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23
(Wittgenstein Award).
article_number: '9470547'
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: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Sarac NE. Quantitative and approximate monitoring. In: Proceedings
of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. Institute
of Electrical and Electronics Engineers; 2021. doi:10.1109/LICS52264.2021.9470547'
apa: 'Henzinger, T. A., & Sarac, N. E. (2021). Quantitative and approximate
monitoring. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in
Computer Science. Online: Institute of Electrical and Electronics Engineers.
https://doi.org/10.1109/LICS52264.2021.9470547'
chicago: Henzinger, Thomas A, and Naci E Sarac. “Quantitative and Approximate Monitoring.”
In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science.
Institute of Electrical and Electronics Engineers, 2021. https://doi.org/10.1109/LICS52264.2021.9470547.
ieee: T. A. Henzinger and N. E. Sarac, “Quantitative and approximate monitoring,”
in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science,
Online, 2021.
ista: 'Henzinger TA, Sarac NE. 2021. Quantitative and approximate monitoring. Proceedings
of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium
on Logic in Computer Science, 9470547.'
mla: Henzinger, Thomas A., and Naci E. Sarac. “Quantitative and Approximate Monitoring.”
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science,
9470547, Institute of Electrical and Electronics Engineers, 2021, doi:10.1109/LICS52264.2021.9470547.
short: T.A. Henzinger, N.E. Sarac, in:, Proceedings of the 36th Annual ACM/IEEE
Symposium on Logic in Computer Science, Institute of Electrical and Electronics
Engineers, 2021.
conference:
end_date: 2021-07-02
location: Online
name: 'LICS: Symposium on Logic in Computer Science'
start_date: 2021-06-29
date_created: 2021-04-30T17:30:47Z
date_published: 2021-06-29T00:00:00Z
date_updated: 2023-08-08T13:52:56Z
day: '29'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1109/LICS52264.2021.9470547
external_id:
arxiv:
- '2105.08353'
isi:
- '000947350400021'
file:
- access_level: open_access
checksum: 6e4cba3f72775f479c5b1b75d1a4a0c4
content_type: application/pdf
creator: esarac
date_created: 2021-06-16T08:23:54Z
date_updated: 2021-06-16T08:23:54Z
file_id: '9557'
file_name: qam.pdf
file_size: 641990
relation: main_file
success: 1
file_date_updated: 2021-06-16T08:23:54Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
Science
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative and approximate monitoring
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '10108'
abstract:
- lang: eng
text: We argue that the time is ripe to investigate differential monitoring, in
which the specification of a program's behavior is implicitly given by a second
program implementing the same informal specification. Similar ideas have been
proposed before, and are currently implemented in restricted form for testing
and specialized run-time analyses, aspects of which we combine. We discuss the
challenges of implementing differential monitoring as a general-purpose, black-box
run-time monitoring framework, and present promising results of a preliminary
implementation, showing low monitoring overheads for diverse programs.
acknowledgement: The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer,
Adrian Francalanza, Owolabi Legunsen, Mae Milano, Manuel Rigger, Cesar Sanchez,
and the members of the IST Verification Seminar for their helpful comments and insights
on various stages of this work, as well as the reviewers of RV’21 for their helpful
suggestions on the actual paper.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Mühlböck F, Henzinger TA. Differential monitoring. In: International Conference
on Runtime Verification. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:10.1007/978-3-030-88494-9_12'
apa: 'Mühlböck, F., & Henzinger, T. A. (2021). Differential monitoring. In International
Conference on Runtime Verification (Vol. 12974, pp. 231–243). Cham: Springer
Nature. https://doi.org/10.1007/978-3-030-88494-9_12'
chicago: 'Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In
International Conference on Runtime Verification, 12974:231–43. Cham: Springer
Nature, 2021. https://doi.org/10.1007/978-3-030-88494-9_12.'
ieee: F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in International
Conference on Runtime Verification, Virtual, 2021, vol. 12974, pp. 231–243.
ista: 'Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference
on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 231–243.'
mla: Mühlböck, Fabian, and Thomas A. Henzinger. “Differential Monitoring.” International
Conference on Runtime Verification, vol. 12974, Springer Nature, 2021, pp.
231–43, doi:10.1007/978-3-030-88494-9_12.
short: F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification,
Springer Nature, Cham, 2021, pp. 231–243.
conference:
end_date: 2021-10-14
location: Virtual
name: 'RV: Runtime Verification'
start_date: 2021-10-11
date_created: 2021-10-07T23:30:10Z
date_published: 2021-10-06T00:00:00Z
date_updated: 2023-08-14T07:20:30Z
day: '06'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-030-88494-9_12
external_id:
isi:
- '000719383800012'
file:
- access_level: open_access
checksum: 554c7fdb259eda703a8b6328a6dad55a
content_type: application/pdf
creator: fmuehlbo
date_created: 2021-10-07T23:32:18Z
date_updated: 2021-10-07T23:32:18Z
file_id: '10109'
file_name: differentialmonitoring-cameraready-openaccess.pdf
file_size: 350632
relation: main_file
success: 1
file_date_updated: 2021-10-07T23:32:18Z
has_accepted_license: '1'
intvolume: ' 12974'
isi: 1
keyword:
- run-time verification
- software engineering
- implicit specification
language:
- iso: eng
month: '10'
oa: 1
oa_version: Preprint
page: 231-243
place: Cham
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: International Conference on Runtime Verification
publication_identifier:
eisbn:
- 978-3-030-88494-9
eissn:
- 1611-3349
isbn:
- 978-3-030-88493-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '9946'
relation: extended_version
status: public
scopus_import: '1'
status: public
title: Differential monitoring
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 12974
year: '2021'
...
---
_id: '10153'
abstract:
- lang: eng
text: "Gradual typing is a principled means for mixing typed and untyped code. But
typed and untyped code often exhibit different programming patterns. There is
already substantial research investigating gradually giving types to code exhibiting
typical untyped patterns, and some research investigating gradually removing types
from code exhibiting typical typed patterns. This paper investigates how to extend
these established gradual-typing concepts to give formal guarantees not only about
how to change types as code evolves but also about how to change such programming
patterns as well.\r\n\r\nIn particular, we explore mixing untyped \"structural\"
code with typed \"nominal\" code in an object-oriented language. But whereas previous
work only allowed \"nominal\" objects to be treated as \"structural\" objects,
we also allow \"structural\" objects to dynamically acquire certain nominal types,
namely interfaces. We present a calculus that supports such \"cross-paradigm\"
code migration and interoperation in a manner satisfying both the static and dynamic
gradual guarantees, and demonstrate that the calculus can be implemented efficiently."
acknowledgement: "We thank the reviewers for their valuable suggestions towards improving
the paper. We also \r\nthank Mae Milano and Adrian Sampson, as well as the members
of the Programming Languages Discussion Group at Cornell University and of the Programming
Research Laboratory at Northeastern University, for their helpful feedback on preliminary
findings of this work.\r\n\r\nThis material is based upon work supported in part
by the National Science Foundation (NSF) through grant CCF-1350182 and the Austrian
Science Fund (FWF) through grant Z211-N23 (Wittgenstein~Award).\r\nAny opinions,
findings, and conclusions or recommendations expressed in this material are those
of the authors and do not necessarily reflect the views of the NSF or the FWF."
article_number: '127'
article_processing_charge: No
article_type: original
author:
- 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: Ross
full_name: Tate, Ross
last_name: Tate
citation:
ama: Mühlböck F, Tate R. Transitioning from structural to nominal code with efficient
gradual typing. Proceedings of the ACM on Programming Languages. 2021;5.
doi:10.1145/3485504
apa: 'Mühlböck, F., & Tate, R. (2021). Transitioning from structural to nominal
code with efficient gradual typing. Proceedings of the ACM on Programming Languages.
Chicago, IL, United States: Association for Computing Machinery. https://doi.org/10.1145/3485504'
chicago: Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal
Code with Efficient Gradual Typing.” Proceedings of the ACM on Programming
Languages. Association for Computing Machinery, 2021. https://doi.org/10.1145/3485504.
ieee: F. Mühlböck and R. Tate, “Transitioning from structural to nominal code with
efficient gradual typing,” Proceedings of the ACM on Programming Languages,
vol. 5. Association for Computing Machinery, 2021.
ista: Mühlböck F, Tate R. 2021. Transitioning from structural to nominal code with
efficient gradual typing. Proceedings of the ACM on Programming Languages. 5,
127.
mla: Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal
Code with Efficient Gradual Typing.” Proceedings of the ACM on Programming
Languages, vol. 5, 127, Association for Computing Machinery, 2021, doi:10.1145/3485504.
short: F. Mühlböck, R. Tate, Proceedings of the ACM on Programming Languages 5 (2021).
conference:
end_date: 2021-10-23
location: Chicago, IL, United States
name: 'OOPSLA: Object-Oriented Programming, Systems, Languages, and Applications'
start_date: 2021-10-17
date_created: 2021-10-19T12:48:44Z
date_published: 2021-10-15T00:00:00Z
date_updated: 2021-11-12T11:30:07Z
day: '15'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/3485504
file:
- access_level: open_access
checksum: 71011efd2da771cafdec7f0d9693f8c1
content_type: application/pdf
creator: fmuehlbo
date_created: 2021-10-19T12:52:23Z
date_updated: 2021-10-19T12:52:23Z
file_id: '10154'
file_name: monnom-oopsla21.pdf
file_size: 770269
relation: main_file
success: 1
file_date_updated: 2021-10-19T12:52:23Z
has_accepted_license: '1'
intvolume: ' 5'
keyword:
- gradual typing
- gradual guarantee
- nominal
- structural
- call tags
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
status: public
title: Transitioning from structural to nominal code with efficient gradual typing
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: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 5
year: '2021'
...
---
_id: '10206'
abstract:
- lang: eng
text: Neural-network classifiers achieve high accuracy when predicting the class
of an input that they were trained to identify. Maintaining this accuracy in dynamic
environments, where inputs frequently fall outside the fixed set of initially
known classes, remains a challenge. The typical approach is to detect inputs from
novel classes and retrain the classifier on an augmented dataset. However, not
only the classifier but also the detection mechanism needs to adapt in order to
distinguish between newly learned and yet unknown input classes. To address this
challenge, we introduce an algorithmic framework for active monitoring of a neural
network. A monitor wrapped in our framework operates in parallel with the neural
network and interacts with a human user via a series of interpretable labeling
queries for incremental adaptation. In addition, we propose an adaptive quantitative
monitor to improve precision. An experimental evaluation on a diverse set of benchmarks
with varying numbers of classes confirms the benefits of our active monitoring
framework in dynamic scenarios.
acknowledgement: We thank Christoph Lampert and Alex Greengold for fruitful discussions.
This research was supported in part by the Simons Institute for the Theory of Computing,
the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), and the
European Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie grant agreement No. 754411.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Anna
full_name: Lukina, Anna
id: CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425
last_name: Lukina
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- 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: 'Lukina A, Schilling C, Henzinger TA. Into the unknown: active monitoring of neural
networks. In: 21st International Conference on Runtime Verification. Vol
12974. Cham: Springer Nature; 2021:42-61. doi:10.1007/978-3-030-88494-9_3'
apa: 'Lukina, A., Schilling, C., & Henzinger, T. A. (2021). Into the unknown:
active monitoring of neural networks. In 21st International Conference on Runtime
Verification (Vol. 12974, pp. 42–61). Cham: Springer Nature. https://doi.org/10.1007/978-3-030-88494-9_3'
chicago: 'Lukina, Anna, Christian Schilling, and Thomas A Henzinger. “Into the Unknown:
Active Monitoring of Neural Networks.” In 21st International Conference on
Runtime Verification, 12974:42–61. Cham: Springer Nature, 2021. https://doi.org/10.1007/978-3-030-88494-9_3.'
ieee: 'A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: active monitoring
of neural networks,” in 21st International Conference on Runtime Verification,
Virtual, 2021, vol. 12974, pp. 42–61.'
ista: 'Lukina A, Schilling C, Henzinger TA. 2021. Into the unknown: active monitoring
of neural networks. 21st International Conference on Runtime Verification. RV:
Runtime Verification, LNCS, vol. 12974, 42–61.'
mla: 'Lukina, Anna, et al. “Into the Unknown: Active Monitoring of Neural Networks.”
21st International Conference on Runtime Verification, vol. 12974, Springer
Nature, 2021, pp. 42–61, doi:10.1007/978-3-030-88494-9_3.'
short: A. Lukina, C. Schilling, T.A. Henzinger, in:, 21st International Conference
on Runtime Verification, Springer Nature, Cham, 2021, pp. 42–61.
conference:
end_date: 2021-10-14
location: Virtual
name: 'RV: Runtime Verification'
start_date: 2021-10-11
date_created: 2021-10-31T23:01:31Z
date_published: 2021-10-06T00:00:00Z
date_updated: 2024-01-30T12:06:56Z
day: '06'
department:
- _id: ToHe
doi: 10.1007/978-3-030-88494-9_3
ec_funded: 1
external_id:
arxiv:
- '2009.06429'
isi:
- '000719383800003'
isi: 1
keyword:
- monitoring
- neural networks
- novelty detection
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2009.06429
month: '10'
oa: 1
oa_version: Preprint
page: 42-61
place: Cham
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 21st International Conference on Runtime Verification
publication_identifier:
eisbn:
- 978-3-030-88494-9
eissn:
- 1611-3349
isbn:
- 9-783-0308-8493-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '13234'
relation: extended_version
status: public
scopus_import: '1'
status: public
title: 'Into the unknown: active monitoring of neural networks'
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: '12974 '
year: '2021'
...
---
_id: '10404'
abstract:
- lang: eng
text: While convolutional neural networks (CNNs) have found wide adoption as state-of-the-art
models for image-related tasks, their predictions are often highly sensitive to
small input perturbations, which the human vision is robust against. This paper
presents Perturber, a web-based application that allows users to instantaneously
explore how CNN activations and predictions evolve when a 3D input scene is interactively
perturbed. Perturber offers a large variety of scene modifications, such as camera
controls, lighting and shading effects, background modifications, object morphing,
as well as adversarial attacks, to facilitate the discovery of potential vulnerabilities.
Fine-tuned model versions can be directly compared for qualitative evaluation
of their robustness. Case studies with machine learning experts have shown that
Perturber helps users to quickly generate hypotheses about model vulnerabilities
and to qualitatively compare model behavior. Using quantitative analyses, we could
replicate users’ insights with other CNN architectures and input images, yielding
new insights about the vulnerability of adversarially trained models.
acknowledgement: "We thank Robert Geirhos and Roland Zimmermann for their participation
in the case study and valuable feedback, Chris Olah and Nick Cammarata for valuable
discussions in the early phase of the project, as well as the Distill Slack workspace
as a platform for discussions. M.L. is supported in part by the Austrian Science
Fund (FWF) under grant Z211-N23 (Wittgenstein Award). J.B. is supported by the German
Federal Ministry of Education and Research\r\n(BMBF) through the Competence Center
for Machine Learning (TUE.AI, FKZ 01IS18039A) and the International Max Planck Research
School for Intelligent Systems (IMPRS-IS). R.H. is partially supported by Boeing
and Horizon-2020 ECSEL (grant 783163, iDev40).\r\n"
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Stefan
full_name: Sietzen, Stefan
last_name: Sietzen
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Judy
full_name: Borowski, Judy
last_name: Borowski
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Manuela
full_name: Waldner, Manuela
last_name: Waldner
citation:
ama: Sietzen S, Lechner M, Borowski J, Hasani R, Waldner M. Interactive analysis
of CNN robustness. Computer Graphics Forum. 2021;40(7):253-264. doi:10.1111/cgf.14418
apa: Sietzen, S., Lechner, M., Borowski, J., Hasani, R., & Waldner, M. (2021).
Interactive analysis of CNN robustness. Computer Graphics Forum. Wiley.
https://doi.org/10.1111/cgf.14418
chicago: Sietzen, Stefan, Mathias Lechner, Judy Borowski, Ramin Hasani, and Manuela
Waldner. “Interactive Analysis of CNN Robustness.” Computer Graphics Forum.
Wiley, 2021. https://doi.org/10.1111/cgf.14418.
ieee: S. Sietzen, M. Lechner, J. Borowski, R. Hasani, and M. Waldner, “Interactive
analysis of CNN robustness,” Computer Graphics Forum, vol. 40, no. 7. Wiley,
pp. 253–264, 2021.
ista: Sietzen S, Lechner M, Borowski J, Hasani R, Waldner M. 2021. Interactive analysis
of CNN robustness. Computer Graphics Forum. 40(7), 253–264.
mla: Sietzen, Stefan, et al. “Interactive Analysis of CNN Robustness.” Computer
Graphics Forum, vol. 40, no. 7, Wiley, 2021, pp. 253–64, doi:10.1111/cgf.14418.
short: S. Sietzen, M. Lechner, J. Borowski, R. Hasani, M. Waldner, Computer Graphics
Forum 40 (2021) 253–264.
date_created: 2021-12-05T23:01:40Z
date_published: 2021-11-27T00:00:00Z
date_updated: 2023-08-14T13:11:42Z
day: '27'
department:
- _id: ToHe
doi: 10.1111/cgf.14418
external_id:
arxiv:
- '2110.07667'
isi:
- '000722952000024'
intvolume: ' 40'
isi: 1
issue: '7'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2110.07667
month: '11'
oa: 1
oa_version: Preprint
page: 253-264
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Computer Graphics Forum
publication_identifier:
eissn:
- 1467-8659
issn:
- 0167-7055
publication_status: published
publisher: Wiley
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interactive analysis of CNN robustness
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 40
year: '2021'
...
---
_id: '10665'
abstract:
- lang: eng
text: "Formal verification of neural networks is an active topic of research, and
recent advances have significantly increased the size of the networks that verification
tools can handle. However, most methods are designed for verification of an idealized
model of the actual network which works over real arithmetic and ignores rounding
imprecisions. This idealization is in stark contrast to network quantization,
which is a technique that trades numerical precision for computational efficiency
and is, therefore, often applied in practice. Neglecting rounding errors of such
low-bit quantized neural networks has been shown to lead to wrong conclusions
about the network’s correctness. Thus, the desired approach for verifying quantized
neural networks would be one that takes these rounding errors\r\ninto account.
In this paper, we show that verifying the bitexact implementation of quantized
neural networks with bitvector specifications is PSPACE-hard, even though verifying
idealized real-valued networks and satisfiability of bit-vector specifications
alone are each in NP. Furthermore, we explore several practical heuristics toward
closing the complexity gap between idealized and bit-exact verification. In particular,
we propose three techniques for making SMT-based verification of quantized neural
networks more scalable. Our experiments demonstrate that our proposed methods
allow a speedup of up to three orders of magnitude over existing approaches."
acknowledgement: "This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein\r\nAward), 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.\r\n"
alternative_title:
- Technical Tracks
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: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Henzinger TA, Lechner M, Zikelic D. Scalable verification of quantized neural
networks. In: Proceedings of the AAAI Conference on Artificial Intelligence.
Vol 35. AAAI Press; 2021:3787-3795.'
apa: 'Henzinger, T. A., Lechner, M., & Zikelic, D. (2021). Scalable verification
of quantized neural networks. In Proceedings of the AAAI Conference on Artificial
Intelligence (Vol. 35, pp. 3787–3795). Virtual: AAAI Press.'
chicago: Henzinger, Thomas A, Mathias Lechner, and Dorde Zikelic. “Scalable Verification
of Quantized Neural Networks.” In Proceedings of the AAAI Conference on Artificial
Intelligence, 35:3787–95. AAAI Press, 2021.
ieee: T. A. Henzinger, M. Lechner, and D. Zikelic, “Scalable verification of quantized
neural networks,” in Proceedings of the AAAI Conference on Artificial Intelligence,
Virtual, 2021, vol. 35, no. 5A, pp. 3787–3795.
ista: 'Henzinger TA, Lechner M, Zikelic D. 2021. Scalable verification of quantized
neural networks. Proceedings of the AAAI Conference on Artificial Intelligence.
AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks,
vol. 35, 3787–3795.'
mla: Henzinger, Thomas A., et al. “Scalable Verification of Quantized Neural Networks.”
Proceedings of the AAAI Conference on Artificial Intelligence, vol. 35,
no. 5A, AAAI Press, 2021, pp. 3787–95.
short: T.A. Henzinger, M. Lechner, D. Zikelic, in:, Proceedings of the AAAI Conference
on Artificial Intelligence, AAAI Press, 2021, pp. 3787–3795.
conference:
end_date: 2021-02-09
location: Virtual
name: 'AAAI: Association for the Advancement of Artificial Intelligence'
start_date: 2021-02-02
date_created: 2022-01-25T15:15:02Z
date_published: 2021-05-28T00:00:00Z
date_updated: 2025-07-14T09:10:11Z
day: '28'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
ec_funded: 1
external_id:
arxiv:
- '2012.08185'
file:
- access_level: open_access
checksum: 2bc8155b2526a70fba5b7301bc89dbd1
content_type: application/pdf
creator: mlechner
date_created: 2022-01-26T07:41:16Z
date_updated: 2022-01-26T07:41:16Z
file_id: '10684'
file_name: 16496-Article Text-19990-1-2-20210518 (1).pdf
file_size: 137235
relation: main_file
success: 1
file_date_updated: 2022-01-26T07:41:16Z
has_accepted_license: '1'
intvolume: ' 35'
issue: 5A
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://ojs.aaai.org/index.php/AAAI/article/view/16496
month: '05'
oa: 1
oa_version: Published Version
page: 3787-3795
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- 978-1-57735-866-4
issn:
- 2159-5399
publication_status: published
publisher: AAAI Press
quality_controlled: '1'
related_material:
record:
- id: '11362'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Scalable verification of quantized neural networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 35
year: '2021'
...
---
_id: '10666'
abstract:
- lang: eng
text: Adversarial training is an effective method to train deep learning models
that are resilient to norm-bounded perturbations, with the cost of nominal performance
drop. While adversarial training appears to enhance the robustness and safety
of a deep model deployed in open-world decision-critical applications, counterintuitively,
it induces undesired behaviors in robot learning settings. In this paper, we show
theoretically and experimentally that neural controllers obtained via adversarial
training are subjected to three types of defects, namely transient, systematic,
and conditional errors. We first generalize adversarial training to a safety-domain
optimization scheme allowing for more generic specifications. We then prove that
such a learning process tends to cause certain error profiles. We support our
theoretical results by a thorough experimental safety analysis in a robot-learning
task. Our results suggest that adversarial training is not yet ready for robot
learning.
acknowledgement: M.L. and T.A.H. are supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award). R.H. and D.R. are supported by
Boeing and R.G. by Horizon-2020 ECSEL Project grant no. 783163 (iDev40).
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: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- 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, Hasani R, Grosu R, Rus D, Henzinger TA. Adversarial training is
not ready for robot learning. In: 2021 IEEE International Conference on Robotics
and Automation. ICRA. ; 2021:4140-4147. doi:10.1109/ICRA48506.2021.9561036'
apa: Lechner, M., Hasani, R., Grosu, R., Rus, D., & Henzinger, T. A. (2021).
Adversarial training is not ready for robot learning. In 2021 IEEE International
Conference on Robotics and Automation (pp. 4140–4147). Xi’an, China. https://doi.org/10.1109/ICRA48506.2021.9561036
chicago: Lechner, Mathias, Ramin Hasani, Radu Grosu, Daniela Rus, and Thomas A Henzinger.
“Adversarial Training Is Not Ready for Robot Learning.” In 2021 IEEE International
Conference on Robotics and Automation, 4140–47. ICRA, 2021. https://doi.org/10.1109/ICRA48506.2021.9561036.
ieee: M. Lechner, R. Hasani, R. Grosu, D. Rus, and T. A. Henzinger, “Adversarial
training is not ready for robot learning,” in 2021 IEEE International Conference
on Robotics and Automation, Xi’an, China, 2021, pp. 4140–4147.
ista: 'Lechner M, Hasani R, Grosu R, Rus D, Henzinger TA. 2021. Adversarial training
is not ready for robot learning. 2021 IEEE International Conference on Robotics
and Automation. ICRA: International Conference on Robotics and AutomationICRA,
4140–4147.'
mla: Lechner, Mathias, et al. “Adversarial Training Is Not Ready for Robot Learning.”
2021 IEEE International Conference on Robotics and Automation, 2021, pp.
4140–47, doi:10.1109/ICRA48506.2021.9561036.
short: M. Lechner, R. Hasani, R. Grosu, D. Rus, T.A. Henzinger, in:, 2021 IEEE International
Conference on Robotics and Automation, 2021, pp. 4140–4147.
conference:
end_date: 2021-06-05
location: Xi'an, China
name: 'ICRA: International Conference on Robotics and Automation'
start_date: 2021-05-30
date_created: 2022-01-25T15:44:54Z
date_published: 2021-01-01T00:00:00Z
date_updated: 2023-08-17T06:58:38Z
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1109/ICRA48506.2021.9561036
external_id:
arxiv:
- '2103.08187'
isi:
- '000765738803040'
has_accepted_license: '1'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/3.0/
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2103.08187
oa: 1
oa_version: None
page: 4140-4147
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 2021 IEEE International Conference on Robotics and Automation
publication_identifier:
eisbn:
- 978-1-7281-9077-8
eissn:
- 2577-087X
isbn:
- 978-1-7281-9078-5
issn:
- 1050-4729
publication_status: published
quality_controlled: '1'
related_material:
record:
- id: '11362'
relation: dissertation_contains
status: public
series_title: ICRA
status: public
title: Adversarial training is not ready for robot learning
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND
3.0)
short: CC BY-NC-ND (3.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '10667'
abstract:
- lang: eng
text: Bayesian neural networks (BNNs) place distributions over the weights of a
neural network to model uncertainty in the data and the network's prediction.
We consider the problem of verifying safety when running a Bayesian neural network
policy in a feedback loop with infinite time horizon systems. Compared to the
existing sampling-based approaches, which are inapplicable to the infinite time
horizon setting, we train a separate deterministic neural network that serves
as an infinite time horizon safety certificate. In particular, we show that the
certificate network guarantees the safety of the system over a subset of the BNN
weight posterior's support. Our method first computes a safe weight set and then
alters the BNN's weight posterior to reject samples outside this set. Moreover,
we show how to extend our approach to a safe-exploration reinforcement learning
setting, in order to avoid unsafe trajectories during the training of the policy.
We evaluate our approach on a series of reinforcement learning benchmarks, including
non-Lyapunovian safety specifications.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and
the European Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- ' Advances in Neural Information Processing Systems'
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: Ðorđe
full_name: Žikelić, Ðorđe
last_name: Žikelić
- 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: 'Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. Infinite time horizon safety
of Bayesian neural networks. In: 35th Conference on Neural Information Processing
Systems. ; 2021. doi:10.48550/arXiv.2111.03165'
apa: Lechner, M., Žikelić, Ð., Chatterjee, K., & Henzinger, T. A. (2021). Infinite
time horizon safety of Bayesian neural networks. In 35th Conference on Neural
Information Processing Systems. Virtual. https://doi.org/10.48550/arXiv.2111.03165
chicago: Lechner, Mathias, Ðorđe Žikelić, Krishnendu Chatterjee, and Thomas A Henzinger.
“Infinite Time Horizon Safety of Bayesian Neural Networks.” In 35th Conference
on Neural Information Processing Systems, 2021. https://doi.org/10.48550/arXiv.2111.03165.
ieee: M. Lechner, Ð. Žikelić, K. Chatterjee, and T. A. Henzinger, “Infinite time
horizon safety of Bayesian neural networks,” in 35th Conference on Neural Information
Processing Systems, Virtual, 2021.
ista: 'Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. 2021. Infinite time horizon
safety of Bayesian neural networks. 35th Conference on Neural Information Processing
Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information
Processing Systems, .'
mla: Lechner, Mathias, et al. “Infinite Time Horizon Safety of Bayesian Neural Networks.”
35th Conference on Neural Information Processing Systems, 2021, doi:10.48550/arXiv.2111.03165.
short: M. Lechner, Ð. Žikelić, K. Chatterjee, T.A. Henzinger, in:, 35th Conference
on Neural Information Processing Systems, 2021.
conference:
end_date: 2021-12-10
location: Virtual
name: 'NeurIPS: Neural Information Processing Systems'
start_date: 2021-12-06
date_created: 2022-01-25T15:45:58Z
date_published: 2021-12-01T00:00:00Z
date_updated: 2025-07-14T09:10:12Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
- _id: KrCh
doi: 10.48550/arXiv.2111.03165
ec_funded: 1
external_id:
arxiv:
- '2111.03165'
file:
- access_level: open_access
checksum: 0fc0f852525c10dda9cc9ffea07fb4e4
content_type: application/pdf
creator: mlechner
date_created: 2022-01-26T07:39:59Z
date_updated: 2022-01-26T07:39:59Z
file_id: '10682'
file_name: infinite_time_horizon_safety_o.pdf
file_size: 452492
relation: main_file
success: 1
file_date_updated: 2022-01-26T07:39:59Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://proceedings.neurips.cc/paper/2021/hash/544defa9fddff50c53b71c43e0da72be-Abstract.html
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 35th Conference on Neural Information Processing Systems
publication_status: published
quality_controlled: '1'
related_material:
record:
- id: '11362'
relation: dissertation_contains
status: public
status: public
title: Infinite time horizon safety of Bayesian neural networks
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND
3.0)
short: CC BY-NC-ND (3.0)
type: conference
user_id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
year: '2021'
...
---
_id: '10668'
abstract:
- lang: eng
text: 'Robustness to variations in lighting conditions is a key objective for any
deep vision system. To this end, our paper extends the receptive field of convolutional
neural networks with two residual components, ubiquitous in the visual processing
system of vertebrates: On-center and off-center pathways, with an excitatory center
and inhibitory surround; OOCS for short. The On-center pathway is excited by the
presence of a light stimulus in its center, but not in its surround, whereas the
Off-center pathway is excited by the absence of a light stimulus in its center,
but not in its surround. We design OOCS pathways via a difference of Gaussians,
with their variance computed analytically from the size of the receptive fields.
OOCS pathways complement each other in their response to light stimuli, ensuring
this way a strong edge-detection capability, and as a result an accurate and robust
inference under challenging lighting conditions. We provide extensive empirical
evidence showing that networks supplied with OOCS pathways gain accuracy and illumination-robustness
from the novel edge representation, compared to other baselines.'
acknowledgement: Z.B. is supported by the Doctoral College Resilient Embedded Systems,
which is run jointly by the TU Wien’s Faculty of Informatics and the UAS Technikum
Wien. R.G. is partially supported by the Horizon 2020 Era-Permed project Persorad,
and ECSEL Project grant no. 783163 (iDev40). R.H and D.R were partially supported
by Boeing and MIT. M.L. is supported in part by the Austrian Science Fund (FWF)
under grant Z211-N23 (Wittgenstein Award).
alternative_title:
- PMLR
article_processing_charge: No
author:
- first_name: Zahra
full_name: Babaiee, Zahra
last_name: Babaiee
- 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: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Babaiee Z, Hasani R, Lechner M, Rus D, Grosu R. On-off center-surround receptive
fields for accurate and robust image classification. In: Proceedings of the
38th International Conference on Machine Learning. Vol 139. ML Research Press;
2021:478-489.'
apa: 'Babaiee, Z., Hasani, R., Lechner, M., Rus, D., & Grosu, R. (2021). On-off
center-surround receptive fields for accurate and robust image classification.
In Proceedings of the 38th International Conference on Machine Learning
(Vol. 139, pp. 478–489). Virtual: ML Research Press.'
chicago: Babaiee, Zahra, Ramin Hasani, Mathias Lechner, Daniela Rus, and Radu Grosu.
“On-off Center-Surround Receptive Fields for Accurate and Robust Image Classification.”
In Proceedings of the 38th International Conference on Machine Learning,
139:478–89. ML Research Press, 2021.
ieee: Z. Babaiee, R. Hasani, M. Lechner, D. Rus, and R. Grosu, “On-off center-surround
receptive fields for accurate and robust image classification,” in Proceedings
of the 38th International Conference on Machine Learning, Virtual, 2021, vol.
139, pp. 478–489.
ista: 'Babaiee Z, Hasani R, Lechner M, Rus D, Grosu R. 2021. On-off center-surround
receptive fields for accurate and robust image classification. Proceedings of
the 38th International Conference on Machine Learning. ML: Machine Learning, PMLR,
vol. 139, 478–489.'
mla: Babaiee, Zahra, et al. “On-off Center-Surround Receptive Fields for Accurate
and Robust Image Classification.” Proceedings of the 38th International Conference
on Machine Learning, vol. 139, ML Research Press, 2021, pp. 478–89.
short: Z. Babaiee, R. Hasani, M. Lechner, D. Rus, R. Grosu, in:, Proceedings of
the 38th International Conference on Machine Learning, ML Research Press, 2021,
pp. 478–489.
conference:
end_date: 2021-07-24
location: Virtual
name: 'ML: Machine Learning'
start_date: 2021-07-18
date_created: 2022-01-25T15:46:33Z
date_published: 2021-07-01T00:00:00Z
date_updated: 2022-05-04T15:02:27Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
file:
- access_level: open_access
checksum: d30eae62561bb517d9f978437d7677db
content_type: application/pdf
creator: mlechner
date_created: 2022-01-26T07:38:32Z
date_updated: 2022-01-26T07:38:32Z
file_id: '10681'
file_name: babaiee21a.pdf
file_size: 4246561
relation: main_file
success: 1
file_date_updated: 2022-01-26T07:38:32Z
has_accepted_license: '1'
intvolume: ' 139'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://proceedings.mlr.press/v139/babaiee21a
month: '07'
oa: 1
oa_version: Published Version
page: 478-489
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 38th International Conference on Machine Learning
publication_identifier:
issn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
status: public
title: On-off center-surround receptive fields for accurate and robust image classification
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND
3.0)
short: CC BY-NC-ND (3.0)
type: conference
user_id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
volume: 139
year: '2021'
...