---
_id: '12511'
abstract:
- lang: eng
text: "We consider the problem of formally verifying almost-sure (a.s.) asymptotic
stability in discrete-time nonlinear stochastic control systems. While verifying
stability in deterministic control systems is extensively studied in the literature,
verifying stability in stochastic control systems is an open problem. The few
existing works on this topic either consider only specialized forms of stochasticity
or make restrictive assumptions on the system, rendering them inapplicable to
learning algorithms with neural network policies. \r\n In this work, we present
an approach for general nonlinear stochastic control problems with two novel aspects:
(a) instead of classical stochastic extensions of Lyapunov functions, we use ranking
supermartingales (RSMs) to certify a.s. asymptotic stability, and (b) we present
a method for learning neural network RSMs. \r\n We prove that our approach guarantees
a.s. asymptotic stability of the system and\r\n provides the first method to obtain
bounds on the stabilization time, which stochastic Lyapunov functions do not.\r\n
Finally, we validate our approach experimentally on a set of nonlinear stochastic
reinforcement learning environments with neural network policies."
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme\r\nunder the Marie Skłodowska-Curie Grant Agreement No. 665385."
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Lechner M, Zikelic D, Chatterjee K, Henzinger TA. Stability verification in
stochastic control systems via neural network supermartingales. Proceedings
of the AAAI Conference on Artificial Intelligence. 2022;36(7):7326-7336. doi:10.1609/aaai.v36i7.20695
apa: Lechner, M., Zikelic, D., Chatterjee, K., & Henzinger, T. A. (2022). Stability
verification in stochastic control systems via neural network supermartingales.
Proceedings of the AAAI Conference on Artificial Intelligence. Association
for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v36i7.20695
chicago: Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A Henzinger.
“Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.”
Proceedings of the AAAI Conference on Artificial Intelligence. Association
for the Advancement of Artificial Intelligence, 2022. https://doi.org/10.1609/aaai.v36i7.20695.
ieee: M. Lechner, D. Zikelic, K. Chatterjee, and T. A. Henzinger, “Stability verification
in stochastic control systems via neural network supermartingales,” Proceedings
of the AAAI Conference on Artificial Intelligence, vol. 36, no. 7. Association
for the Advancement of Artificial Intelligence, pp. 7326–7336, 2022.
ista: Lechner M, Zikelic D, Chatterjee K, Henzinger TA. 2022. Stability verification
in stochastic control systems via neural network supermartingales. Proceedings
of the AAAI Conference on Artificial Intelligence. 36(7), 7326–7336.
mla: Lechner, Mathias, et al. “Stability Verification in Stochastic Control Systems
via Neural Network Supermartingales.” Proceedings of the AAAI Conference on
Artificial Intelligence, vol. 36, no. 7, Association for the Advancement of
Artificial Intelligence, 2022, pp. 7326–36, doi:10.1609/aaai.v36i7.20695.
short: M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, Proceedings of the
AAAI Conference on Artificial Intelligence 36 (2022) 7326–7336.
corr_author: '1'
date_created: 2023-02-05T17:29:50Z
date_published: 2022-06-28T00:00:00Z
date_updated: 2026-04-07T13:27:55Z
day: '28'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v36i7.20695
ec_funded: 1
external_id:
arxiv:
- '2112.09495'
intvolume: ' 36'
issue: '7'
keyword:
- General Medicine
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2112.09495
month: '06'
oa: 1
oa_version: Preprint
page: 7326-7336
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- '9781577358350'
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Stability verification in stochastic control systems via neural network supermartingales
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 36
year: '2022'
...
---
OA_place: repository
_id: '14600'
abstract:
- lang: eng
text: We study the problem of learning controllers for discrete-time non-linear
stochastic dynamical systems with formal reach-avoid guarantees. This work presents
the first method for providing formal reach-avoid guarantees, which combine and
generalize stability and safety guarantees, with a tolerable probability threshold
$p\in[0,1]$ over the infinite time horizon. Our method leverages advances in machine
learning literature and it represents formal certificates as neural networks.
In particular, we learn a certificate in the form of a reach-avoid supermartingale
(RASM), a novel notion that we introduce in this work. Our RASMs provide reachability
and avoidance guarantees by imposing constraints on what can be viewed as a stochastic
extension of level sets of Lyapunov functions for deterministic systems. Our approach
solves several important problems -- it can be used to learn a control policy
from scratch, to verify a reach-avoid specification for a fixed control policy,
or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification.
We validate our approach on $3$ stochastic non-linear reinforcement learning tasks.
article_number: '2210.05308'
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. arXiv. doi:10.48550/ARXIV.2210.05308
apa: Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (n.d.). Learning
control policies for stochastic systems with reach-avoid guarantees. arXiv.
https://doi.org/10.48550/ARXIV.2210.05308
chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee.
“Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.”
ArXiv, n.d. https://doi.org/10.48550/ARXIV.2210.05308.
ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control
policies for stochastic systems with reach-avoid guarantees,” arXiv. .
ista: Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. arXiv, 2210.05308.
mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with
Reach-Avoid Guarantees.” ArXiv, 2210.05308, doi:10.48550/ARXIV.2210.05308.
short: D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, ArXiv (n.d.).
corr_author: '1'
date_created: 2023-11-24T13:10:09Z
date_published: 2022-11-29T00:00:00Z
date_updated: 2026-04-07T13:27:56Z
day: '29'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/ARXIV.2210.05308
ec_funded: 1
external_id:
arxiv:
- '2210.05308'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-sa/4.0/
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2210.05308
month: '11'
oa: 1
oa_version: Preprint
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: arXiv
publication_status: draft
related_material:
record:
- id: '14830'
relation: later_version
status: public
- id: '14539'
relation: dissertation_contains
status: public
status: public
title: Learning control policies for stochastic systems with reach-avoid guarantees
tmp:
image: /images/cc_by_sa.png
legal_code_url: https://creativecommons.org/licenses/by-sa/4.0/legalcode
name: Creative Commons Attribution-ShareAlike 4.0 International Public License (CC
BY-SA 4.0)
short: CC BY-SA (4.0)
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2022'
...
---
OA_place: repository
_id: '14601'
abstract:
- lang: eng
text: "In this work, we address the problem of learning provably stable neural\r\nnetwork
policies for stochastic control systems. While recent work has\r\ndemonstrated
the feasibility of certifying given policies using martingale\r\ntheory, the problem
of how to learn such policies is little explored. Here, we\r\nstudy the effectiveness
of jointly learning a policy together with a martingale\r\ncertificate that proves
its stability using a single learning algorithm. We\r\nobserve that the joint
optimization problem becomes easily stuck in local\r\nminima when starting from
a randomly initialized policy. Our results suggest\r\nthat some form of pre-training
of the policy is required for the joint\r\noptimization to repair and verify the
policy successfully."
article_number: '2205.11991'
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies
in stochastic control systems. arXiv. doi:10.48550/arXiv.2205.11991
apa: Zikelic, D., Lechner, M., Chatterjee, K., & Henzinger, T. A. (n.d.). Learning
stabilizing policies in stochastic control systems. arXiv. https://doi.org/10.48550/arXiv.2205.11991
chicago: Zikelic, Dorde, Mathias Lechner, Krishnendu Chatterjee, and Thomas A Henzinger.
“Learning Stabilizing Policies in Stochastic Control Systems.” ArXiv, n.d.
https://doi.org/10.48550/arXiv.2205.11991.
ieee: D. Zikelic, M. Lechner, K. Chatterjee, and T. A. Henzinger, “Learning stabilizing
policies in stochastic control systems,” arXiv. .
ista: Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies
in stochastic control systems. arXiv, 2205.11991.
mla: Zikelic, Dorde, et al. “Learning Stabilizing Policies in Stochastic Control
Systems.” ArXiv, 2205.11991, doi:10.48550/arXiv.2205.11991.
short: D. Zikelic, M. Lechner, K. Chatterjee, T.A. Henzinger, ArXiv (n.d.).
corr_author: '1'
date_created: 2023-11-24T13:22:30Z
date_published: 2022-05-24T00:00:00Z
date_updated: 2026-04-07T13:27:56Z
day: '24'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/arXiv.2205.11991
ec_funded: 1
external_id:
arxiv:
- '2205.11991'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2205.11991
month: '05'
oa: 1
oa_version: Preprint
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: arXiv
publication_status: draft
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
status: public
title: Learning stabilizing policies in stochastic control systems
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2022'
...
---
_id: '10774'
abstract:
- lang: eng
text: We study the problem of specifying sequential information-flow properties
of systems. Information-flow properties are hyperproperties, as they compare different
traces of a system. Sequential information-flow properties can express changes,
over time, in the information-flow constraints. For example, information-flow
constraints during an initialization phase of a system may be different from information-flow
constraints that are required during the operation phase. We formalize several
variants of interpreting sequential information-flow constraints, which arise
from different assumptions about what can be observed of the system. For this
purpose, we introduce a first-order logic, called Hypertrace Logic, with both
trace and time quantifiers for specifying linear-time hyperproperties. We prove
that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted
quantifier prefixes, cannot specify the majority of the studied variants of sequential
information flow, including all variants in which the transition between sequential
phases (such as initialization and operation) happens asynchronously. Our results
rely on new equivalences between sets of traces that cannot be distinguished by
certain classes of formulas from Hypertrace Logic. This presents a new approach
to proving inexpressiveness results for HyperLTL.
acknowledgement: This work was funded in part by the Wittgenstein Award Z211-N23 of
the Austrian Science Fund (FWF) and by the FWF project W1255-N23.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana Oliveira
full_name: Da Costa, Ana Oliveira
last_name: Da Costa
citation:
ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential
information flow. In: Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
Vol 13182. Springer Nature; 2022:1-19. doi:10.1007/978-3-030-94583-1_1'
apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa,
A. O. (2022). Flavors of sequential information flow. In Lecture Notes in Computer
Science (including subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics) (Vol. 13182, pp. 1–19). Philadelphia, PA, United
States: Springer Nature. https://doi.org/10.1007/978-3-030-94583-1_1'
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), 13182:1–19. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-94583-1_1.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
“Flavors of sequential information flow,” in Lecture Notes in Computer Science
(including subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), Philadelphia, PA, United States, 2022, vol. 13182, pp.
1–19.
ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors
of sequential information flow. Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182,
1–19.'
mla: Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 13182, Springer Nature, 2022, pp.
1–19, doi:10.1007/978-3-030-94583-1_1.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp.
1–19.
conference:
end_date: 2022-01-18
location: Philadelphia, PA, United States
name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
start_date: 2022-01-16
date_created: 2022-02-20T23:01:34Z
date_published: 2022-01-14T00:00:00Z
date_updated: 2026-04-16T09:13:43Z
day: '14'
department:
- _id: ToHe
doi: 10.1007/978-3-030-94583-1_1
external_id:
arxiv:
- '2105.02013'
isi:
- '001059208500001'
intvolume: ' 13182'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2105.02013'
month: '01'
oa: 1
oa_version: Preprint
page: 1-19
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eisbn:
- '9783030945831'
eissn:
- 1611-3349
isbn:
- '9783030945824'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of sequential information flow
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 13182
year: '2022'
...
---
_id: '12508'
abstract:
- lang: eng
text: "We explore the notion of history-determinism in the context of timed automata
(TA). History-deterministic automata are those in which nondeterminism can be
resolved on the fly, based on the run constructed thus far. History-determinism
is a robust property that admits different game-based characterisations, and history-deterministic
specifications allow for game-based verification without an expensive determinization
step.\r\nWe show yet another characterisation of history-determinism in terms
of fair simulation, at the general level of labelled transition systems: a system
is history-deterministic precisely if and only if it fairly simulates all language
smaller systems.\r\nFor timed automata over infinite timed words it is known that
universality is undecidable for Büchi TA. We show that for history-deterministic
TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis
all remain decidable and are ExpTime-complete.\r\nFor the subclass of TA with
safety or reachability acceptance, we show that checking whether such an automaton
is history-deterministic is decidable (in ExpTime), and history-deterministic
TA with safety acceptance are effectively determinizable without introducing new
automata states."
acknowledgement: "Thomas A. Henzinger: This work was supported in part by the ERC-2020-AdG
101020093.\r\nPatrick Totzke: acknowledges support from the EPSRC, project no. EP/V025848/1.\r\n"
alternative_title:
- LIPIcs
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
- first_name: Karoliina
full_name: Lehtinen, Karoliina
last_name: Lehtinen
- first_name: Patrick
full_name: Totzke, Patrick
last_name: Totzke
citation:
ama: 'Henzinger TA, Lehtinen K, Totzke P. History-deterministic timed automata.
In: 33rd International Conference on Concurrency Theory. Vol 243. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2022:14:1-14:21. doi:10.4230/LIPIcs.CONCUR.2022.14'
apa: 'Henzinger, T. A., Lehtinen, K., & Totzke, P. (2022). History-deterministic
timed automata. In 33rd International Conference on Concurrency Theory
(Vol. 243, p. 14:1-14:21). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.14'
chicago: Henzinger, Thomas A, Karoliina Lehtinen, and Patrick Totzke. “History-Deterministic
Timed Automata.” In 33rd International Conference on Concurrency Theory,
243:14:1-14:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.CONCUR.2022.14.
ieee: T. A. Henzinger, K. Lehtinen, and P. Totzke, “History-deterministic timed
automata,” in 33rd International Conference on Concurrency Theory, Warsaw,
Poland, 2022, vol. 243, p. 14:1-14:21.
ista: 'Henzinger TA, Lehtinen K, Totzke P. 2022. History-deterministic timed automata.
33rd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency
Theory, LIPIcs, vol. 243, 14:1-14:21.'
mla: Henzinger, Thomas A., et al. “History-Deterministic Timed Automata.” 33rd
International Conference on Concurrency Theory, vol. 243, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2022, p. 14:1-14:21, doi:10.4230/LIPIcs.CONCUR.2022.14.
short: T.A. Henzinger, K. Lehtinen, P. Totzke, in:, 33rd International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022,
p. 14:1-14:21.
conference:
end_date: 2022-09-16
location: Warsaw, Poland
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2022-09-13
corr_author: '1'
das_tickbox: '1'
date_created: 2023-02-05T17:24:23Z
date_published: 2022-09-06T00:00:00Z
date_updated: 2026-07-07T13:37:45Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2022.14
ec_funded: 1
file:
- access_level: open_access
checksum: 9e97e15628f66b2ad77f535bb0327dee
content_type: application/pdf
creator: dernst
date_created: 2023-02-06T09:21:09Z
date_updated: 2023-02-06T09:21:09Z
file_id: '12520'
file_name: 2022_LIPICs_Henzinger2.pdf
file_size: 717940
relation: main_file
success: 1
file_date_updated: 2023-02-06T09:21:09Z
has_accepted_license: '1'
intvolume: ' 243'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 14:1-14:21
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 33rd International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959772464'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
record:
- id: '18530'
relation: later_version
status: public
scopus_import: '1'
status: public
title: History-deterministic timed automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 243
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
corr_author: '1'
date_created: 2022-08-08T17:09:09Z
date_published: 2022-09-23T00:00:00Z
date_updated: 2026-07-27T12:48:18Z
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'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
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'
...
---
OA_place: repository
_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.).
corr_author: '1'
date_created: 2022-05-12T13:20:17Z
date_published: 2022-04-15T00:00:00Z
date_updated: 2026-08-12T06:40:15Z
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: draft
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'
...
---
OA_place: publisher
_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.
corr_author: '1'
date_created: 2022-05-12T07:14:01Z
date_published: 2022-05-12T00:00:00Z
date_updated: 2026-08-19T09:28:05Z
day: '12'
ddc:
- '004'
degree_awarded: PhD
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/at:ista:11362
ec_funded: 1
file:
- access_level: closed
checksum: 8eefa9c7c10ca7e1a2ccdd731962a645
content_type: application/zip
creator: mlechner
date_created: 2022-05-13T12:33:26Z
date_updated: 2022-05-13T12:49:00Z
file_id: '11378'
file_name: src.zip
file_size: 13210143
relation: source_file
- access_level: open_access
checksum: 1b9e1e5a9a83ed9d89dad2f5133dc026
content_type: application/pdf
creator: mlechner
date_created: 2022-05-16T08:02:28Z
date_updated: 2022-05-17T15:19:39Z
file_id: '11382'
file_name: thesis_main-a2.pdf
file_size: 2732536
relation: main_file
file_date_updated: 2022-05-17T15:19:39Z
has_accepted_license: '1'
keyword:
- neural networks
- verification
- machine learning
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: '124'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
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: '10667'
relation: part_of_dissertation
status: public
- id: '10665'
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: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2022'
...
---
_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
corr_author: '1'
date_created: 2021-10-07T23:30:10Z
date_published: 2021-10-06T00:00:00Z
date_updated: 2025-04-15T06:26:12Z
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: Formal methods for the design and analysis of complex systems
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: 2025-04-15T06:25:55Z
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: Formal methods for the design and analysis of complex systems
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '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
corr_author: '1'
date_created: 2021-10-31T23:01:31Z
date_published: 2021-10-06T00:00:00Z
date_updated: 2025-04-15T06:26:14Z
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: Formal methods for the design and analysis of complex systems
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: 2025-04-15T06:25:55Z
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: Formal methods for the design and analysis of complex systems
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: '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
arxiv: 1
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: 2025-05-19T11:28:08Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
external_id:
arxiv:
- '2106.07091'
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
license: https://creativecommons.org/licenses/by-nc-nd/3.0/
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: Formal methods for the design and analysis of complex systems
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 139
year: '2021'
...
---
_id: '10688'
abstract:
- lang: eng
text: "Civl is a static verifier for concurrent programs designed around the conceptual
framework of layered refinement,\r\nwhich views the task of verifying a program
as a sequence of program simplification steps each justified by its own invariant.
Civl verifies a layered concurrent program that compactly expresses all the programs
in this sequence and the supporting invariants. This paper presents the design
and implementation of the Civl verifier."
acknowledgement: This research was performed while Bernhard Kragl was at IST Austria,
supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein
Award).
alternative_title:
- Conference Series
article_processing_charge: No
author:
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: 'Kragl B, Qadeer S. The Civl verifier. In: Ruzica P, Whalen MW, eds. Proceedings
of the 21st Conference on Formal Methods in Computer-Aided Design. Vol 2.
TU Wien Academic Press; 2021:143–152. doi:10.34727/2021/isbn.978-3-85448-046-4_23'
apa: 'Kragl, B., & Qadeer, S. (2021). The Civl verifier. In P. Ruzica &
M. W. Whalen (Eds.), Proceedings of the 21st Conference on Formal Methods in
Computer-Aided Design (Vol. 2, pp. 143–152). Virtual: TU Wien Academic Press.
https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23'
chicago: Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” In Proceedings
of the 21st Conference on Formal Methods in Computer-Aided Design, edited
by Piskac Ruzica and Michael W. Whalen, 2:143–152. TU Wien Academic Press, 2021.
https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23.
ieee: B. Kragl and S. Qadeer, “The Civl verifier,” in Proceedings of the 21st
Conference on Formal Methods in Computer-Aided Design, Virtual, 2021, vol.
2, pp. 143–152.
ista: 'Kragl B, Qadeer S. 2021. The Civl verifier. Proceedings of the 21st Conference
on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided
Design, Conference Series, vol. 2, 143–152.'
mla: Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” Proceedings of the
21st Conference on Formal Methods in Computer-Aided Design, edited by Piskac
Ruzica and Michael W. Whalen, vol. 2, TU Wien Academic Press, 2021, pp. 143–152,
doi:10.34727/2021/isbn.978-3-85448-046-4_23.
short: B. Kragl, S. Qadeer, in:, P. Ruzica, M.W. Whalen (Eds.), Proceedings of the
21st Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press,
2021, pp. 143–152.
conference:
end_date: 2021-10-22
location: Virtual
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2021-10-20
corr_author: '1'
date_created: 2022-01-26T08:01:30Z
date_published: 2021-10-01T00:00:00Z
date_updated: 2025-04-15T06:25:56Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.34727/2021/isbn.978-3-85448-046-4_23
editor:
- first_name: Piskac
full_name: Ruzica, Piskac
last_name: Ruzica
- first_name: Michael W.
full_name: Whalen, Michael W.
last_name: Whalen
file:
- access_level: open_access
checksum: 35438ac9f9750340b7f8ae4ae3220d9f
content_type: application/pdf
creator: cchlebak
date_created: 2022-01-26T08:04:29Z
date_updated: 2022-01-26T08:04:29Z
file_id: '10689'
file_name: 2021_FCAD2021_Kragl.pdf
file_size: 390555
relation: main_file
success: 1
file_date_updated: 2022-01-26T08:04:29Z
has_accepted_license: '1'
intvolume: ' 2'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 143–152
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: Proceedings of the 21st Conference on Formal Methods in Computer-Aided
Design
publication_identifier:
isbn:
- 978-3-85448-046-4
publication_status: published
publisher: TU Wien Academic Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: The Civl verifier
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2021'
...
---
_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).
corr_author: '1'
date_created: 2020-12-02T13:34:25Z
date_published: 2021-04-01T00:00:00Z
date_updated: 2026-04-16T09:15:47Z
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: Formal methods for the design and analysis of complex systems
publication: Expert Systems with Applications
publication_identifier:
eissn:
- 1873-6793
issn:
- 0957-4174
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Boosting expensive synchronizing heuristics
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
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: 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: Hybrid Systems - Computation and Control'
start_date: 2021-05-19
corr_author: '1'
date_created: 2021-02-26T16:30:39Z
date_published: 2021-05-01T00:00:00Z
date_updated: 2025-07-10T12:01:40Z
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: Formal methods for the design and analysis of complex systems
- _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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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: 2025-07-10T11:53:57Z
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.).
corr_author: '1'
date_created: 2021-03-23T05:38:48Z
date_published: 2021-03-21T00:00:00Z
date_updated: 2025-04-15T06:26:12Z
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: '9647'
abstract:
- lang: eng
text: 'Gene expression is regulated by the set of transcription factors (TFs) that
bind to the promoter. The ensuing regulating function is often represented as
a combinational logic circuit, where output (gene expression) is determined by
current input values (promoter bound TFs) only. However, the simultaneous arrival
of TFs is a strong assumption, since transcription and translation of genes introduce
intrinsic time delays and there is no global synchronisation among the arrival
times of different molecular species at their targets. We present an experimentally
implementable genetic circuit with two inputs and one output, which in the presence
of small delays in input arrival, exhibits qualitatively distinct population-level
phenotypes, over timescales that are longer than typical cell doubling times.
From a dynamical systems point of view, these phenotypes represent long-lived
transients: although they converge to the same value eventually, they do so after
a very long time span. The key feature of this toy model genetic circuit is that,
despite having only two inputs and one output, it is regulated by twenty-three
distinct DNA-TF configurations, two of which are more stable than others (DNA
looped states), one promoting and another blocking the expression of the output
gene. Small delays in input arrival time result in a majority of cells in the
population quickly reaching the stable state associated with the first input,
while exiting of this stable state occurs at a slow timescale. In order to mechanistically
model the behaviour of this genetic circuit, we used a rule-based modelling language,
and implemented a grid-search to find parameter combinations giving rise to long-lived
transients. Our analysis shows that in the absence of feedback, there exist path-dependent
gene regulatory mechanisms based on the long timescale of transients. The behaviour
of this toy model circuit suggests that gene regulatory networks can exploit event
timing to create phenotypes, and it opens the possibility that they could use
event timing to memorise events, without regulatory feedback. The model reveals
the importance of (i) mechanistically modelling the transitions between the different
DNA-TF states, and (ii) employing transient analysis thereof.'
acknowledgement: 'Tatjana Petrov’s research was supported in part by SNSF Advanced
Postdoctoral Mobility Fellowship grant number P300P2 161067, the Ministry of Science,
Research and the Arts of the state of Baden-Wurttemberg, and the DFG Centre of Excellence
2117 ‘Centre for the Advanced Study of Collective Behaviour’ (ID: 422037984). Claudia
Igler is the recipient of a DOC Fellowship of the Austrian Academy of Sciences.
Thomas A. Henzinger’s research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award).'
article_processing_charge: No
article_type: original
author:
- first_name: Tatjana
full_name: Petrov, Tatjana
last_name: Petrov
- first_name: Claudia
full_name: Igler, Claudia
id: 46613666-F248-11E8-B48F-1D18A9856A87
last_name: Igler
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
- 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: Calin C
full_name: Guet, Calin C
id: 47F8433E-F248-11E8-B48F-1D18A9856A87
last_name: Guet
orcid: 0000-0001-6220-2052
citation:
ama: Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. Long lived transients in
gene regulation. Theoretical Computer Science. 2021;893:1-16. doi:10.1016/j.tcs.2021.05.023
apa: Petrov, T., Igler, C., Sezgin, A., Henzinger, T. A., & Guet, C. C. (2021).
Long lived transients in gene regulation. Theoretical Computer Science.
Elsevier. https://doi.org/10.1016/j.tcs.2021.05.023
chicago: Petrov, Tatjana, Claudia Igler, Ali Sezgin, Thomas A Henzinger, and Calin
C Guet. “Long Lived Transients in Gene Regulation.” Theoretical Computer Science.
Elsevier, 2021. https://doi.org/10.1016/j.tcs.2021.05.023.
ieee: T. Petrov, C. Igler, A. Sezgin, T. A. Henzinger, and C. C. Guet, “Long lived
transients in gene regulation,” Theoretical Computer Science, vol. 893.
Elsevier, pp. 1–16, 2021.
ista: Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. 2021. Long lived transients
in gene regulation. Theoretical Computer Science. 893, 1–16.
mla: Petrov, Tatjana, et al. “Long Lived Transients in Gene Regulation.” Theoretical
Computer Science, vol. 893, Elsevier, 2021, pp. 1–16, doi:10.1016/j.tcs.2021.05.023.
short: T. Petrov, C. Igler, A. Sezgin, T.A. Henzinger, C.C. Guet, Theoretical Computer
Science 893 (2021) 1–16.
corr_author: '1'
date_created: 2021-07-11T22:01:18Z
date_published: 2021-06-04T00:00:00Z
date_updated: 2025-04-15T06:25:56Z
day: '04'
ddc:
- '004'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1016/j.tcs.2021.05.023
external_id:
isi:
- '000710180500002'
file:
- access_level: open_access
checksum: d3aef34cfb13e53bba4cf44d01680793
content_type: application/pdf
creator: dernst
date_created: 2022-05-12T12:13:27Z
date_updated: 2022-05-12T12:13:27Z
file_id: '11364'
file_name: 2021_TheoreticalComputerScience_Petrov.pdf
file_size: 2566504
relation: main_file
success: 1
file_date_updated: 2022-05-12T12:13:27Z
has_accepted_license: '1'
intvolume: ' 893'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 1-16
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: Theoretical Computer Science
publication_identifier:
issn:
- 0304-3975
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Long lived transients in gene regulation
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 893
year: '2021'
...
---
_id: '9946'
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, Matthew 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:
- IST Austria Technical Report
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. IST Austria; 2021.
doi:10.15479/AT:ISTA:9946
apa: Mühlböck, F., & Henzinger, T. A. (2021). Differential monitoring.
IST Austria. https://doi.org/10.15479/AT:ISTA:9946
chicago: Mühlböck, Fabian, and Thomas A Henzinger. Differential Monitoring.
IST Austria, 2021. https://doi.org/10.15479/AT:ISTA:9946.
ieee: F. Mühlböck and T. A. Henzinger, Differential monitoring. IST Austria,
2021.
ista: Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.
mla: Mühlböck, Fabian, and Thomas A. Henzinger. Differential Monitoring.
IST Austria, 2021, doi:10.15479/AT:ISTA:9946.
short: F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021.
date_created: 2021-08-20T20:00:37Z
date_published: 2021-09-01T00:00:00Z
date_updated: 2025-04-15T06:55:00Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:9946
file:
- access_level: open_access
checksum: 0f9aafd59444cb6bdca6925d163ab946
content_type: application/pdf
creator: fmuehlbo
date_created: 2021-08-20T19:59:44Z
date_updated: 2021-09-03T12:34:28Z
file_id: '9948'
file_name: differentialmonitoring-techreport.pdf
file_size: '320453'
relation: main_file
file_date_updated: 2021-09-03T12:34:28Z
has_accepted_license: '1'
keyword:
- run-time verification
- software engineering
- implicit specification
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '17'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
related_material:
record:
- id: '10108'
relation: shorter_version
status: public
- id: '9281'
relation: other
status: public
status: public
title: Differential monitoring
type: technical_report
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2021'
...