---
_id: '12854'
abstract:
- lang: eng
text: "The main idea behind BUBAAK is to run multiple program analyses in parallel
and use runtime monitoring and enforcement to observe and control their progress
in real time. The analyses send information about (un)explored states of the program
and discovered invariants to a monitor. The monitor processes the received data
and can force an analysis to stop the search of certain program parts (which have
already been analyzed by other analyses), or to make it utilize a program invariant
found by another analysis.\r\nAt SV-COMP 2023, the implementation of data exchange
between the monitor and the analyses was not yet completed, which is why BUBAAK
only ran several analyses in parallel, without any coordination. Still, BUBAAK
won the meta-category FalsificationOverall and placed very well in several other
(sub)-categories of the competition."
acknowledgement: This work was supported by the ERC-2020-AdG 10102009 grant.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers.
In: Tools and Algorithms for the Construction and Analysis of Systems.
Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32'
apa: 'Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of
program verifiers. In Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32'
chicago: 'Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of
Program Verifiers.” In Tools and Algorithms for the Construction and Analysis
of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.'
ieee: 'M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,”
in Tools and Algorithms for the Construction and Analysis of Systems, Paris,
France, 2023, vol. 13994, pp. 535–540.'
ista: 'Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers.
Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994,
535–540.'
mla: 'Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program
Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.'
short: M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 535–540.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-04-20T08:22:53Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-04-25T07:02:43Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_32
ec_funded: 1
file:
- access_level: open_access
checksum: 120d2c2a38384058ad0630fdf8288312
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T06:58:36Z
date_updated: 2023-04-25T06:58:36Z
file_id: '12864'
file_name: 2023_LNCS_Chalupa.pdf
file_size: 16096413
relation: main_file
success: 1
file_date_updated: 2023-04-25T06:58:36Z
has_accepted_license: '1'
intvolume: ' 13994'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 535-540
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783031308208'
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: 'Bubaak: Runtime monitoring of program verifiers'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13994
year: '2023'
...
---
_id: '12856'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of run-time monitoring. Third-party monitoring, with limited knowledge
of the monitored software, and best-effort monitoring, which keeps pace with the
monitored software, are especially valuable, yet underexplored areas of run-time
monitoring. Most existing monitoring frameworks do not support their combination
because they either require access to the monitored code for instrumentation purposes
or the processing of all observed events, or both.\r\n\r\nWe present a middleware
framework, VAMOS, for the run-time monitoring of software which is explicitly
designed to support third-party and best-effort scenarios. The design goals of
VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the
ability to monitor black-box code through a variety of different event channels,
and the connectability to monitors written in different specification languages),
and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker
and event recognition systems with aspects of stream processing systems.\r\nWe
implemented a prototype toolchain for VAMOS and conducted experiments including
a case study of monitoring for data races. The results indicate that VAMOS enables
writing useful yet efficient monitors, is compatible with a variety of event sources
and monitor specifications, and simplifies key aspects of setting up a monitoring
system from scratch."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
authors would like to thank the anonymous FASE reviewers for their valuable feedback
and suggestions.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort
third-party monitoring. In: Fundamental Approaches to Software Engineering.
Vol 13991. Springer Nature; 2023:260-281. doi:10.1007/978-3-031-30826-0_15'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023).
Vamos: Middleware for best-effort third-party monitoring. In Fundamental Approaches
to Software Engineering (Vol. 13991, pp. 260–281). Paris, France: Springer
Nature. https://doi.org/10.1007/978-3-031-30826-0_15'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
“Vamos: Middleware for Best-Effort Third-Party Monitoring.” In Fundamental
Approaches to Software Engineering, 13991:260–81. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30826-0_15.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware
for best-effort third-party monitoring,” in Fundamental Approaches to Software
Engineering, Paris, France, 2023, vol. 13991, pp. 260–281.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware
for best-effort third-party monitoring. Fundamental Approaches to Software Engineering.
FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.'
mla: 'Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.”
Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature,
2023, pp. 260–81, doi:10.1007/978-3-031-30826-0_15.'
short: M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental
Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FASE: Fundamental Approaches to Software Engineering'
start_date: 2023-04-22
date_created: 2023-04-20T08:29:42Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-04-25T07:19:07Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30826-0_15
ec_funded: 1
file:
- access_level: open_access
checksum: 17a7c8e08be609cf2408d37ea55e322c
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T07:16:36Z
date_updated: 2023-04-25T07:16:36Z
file_id: '12865'
file_name: 2023_LNCS_ChalupaM.pdf
file_size: 580828
relation: main_file
success: 1
file_date_updated: 2023-04-25T07:16:36Z
has_accepted_license: '1'
intvolume: ' 13991'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 260-281
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Fundamental Approaches to Software Engineering
publication_identifier:
eisbn:
- '9783031308260'
eissn:
- 1611-3349
isbn:
- '9783031308253'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '12407'
relation: earlier_version
status: public
status: public
title: 'Vamos: Middleware for best-effort third-party monitoring'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13991
year: '2023'
...
---
_id: '12407'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of run-time monitoring. Third-party monitoring, with limited knowledge
of the monitored software, and best-effort monitoring, which keeps pace with the
monitored software, are especially valuable, yet underexplored areas of run-time
monitoring. Most existing monitoring frameworks do not support their combination
because they either require access to the monitored code for instrumentation purposes
or the processing of all observed events, or both.\r\n\r\nWe present a middleware
framework, VAMOS, for the run-time monitoring of software which is explicitly
designed to support third-party and best-effort scenarios. The design goals of
VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the
ability to monitor black-box code through a variety of different event channels,
and the connectability to monitors written in different specification languages),
and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker
and event recognition systems with aspects of stream processing systems.\r\n\r\nWe
implemented a prototype toolchain for VAMOS and conducted experiments including
a case study of monitoring for data races. The results indicate that VAMOS enables
writing useful yet efficient monitors, is compatible with a variety of event sources
and monitor specifications, and simplifies key aspects of setting up a monitoring
system from scratch."
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093. \r\nThe
authors would like to thank the anonymous FASE reviewers for their valuable feedback
and suggestions."
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for
Best-Effort Third-Party Monitoring. Institute of Science and Technology Austria;
2023. doi:10.15479/AT:ISTA:12407'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023).
VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of
Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:12407'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
VAMOS: Middleware for Best-Effort Third-Party Monitoring. Institute of
Science and Technology Austria, 2023. https://doi.org/10.15479/AT:ISTA:12407.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, VAMOS: Middleware
for Best-Effort Third-Party Monitoring. Institute of Science and Technology
Austria, 2023.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. VAMOS: Middleware
for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria,
38p.'
mla: 'Chalupa, Marek, et al. VAMOS: Middleware for Best-Effort Third-Party Monitoring.
Institute of Science and Technology Austria, 2023, doi:10.15479/AT:ISTA:12407.'
short: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, VAMOS: Middleware
for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria,
2023.'
date_created: 2023-01-27T03:18:08Z
date_published: 2023-01-27T00:00:00Z
date_updated: 2023-04-25T07:19:06Z
day: '27'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:12407
ec_funded: 1
file:
- access_level: open_access
checksum: 55426e463fdeafe9777fc3ff635154c7
content_type: application/pdf
creator: fmuehlbo
date_created: 2023-01-27T03:18:34Z
date_updated: 2023-01-27T03:18:34Z
file_id: '12408'
file_name: main.pdf
file_size: 662409
relation: main_file
success: 1
file_date_updated: 2023-01-27T03:18:34Z
has_accepted_license: '1'
keyword:
- runtime monitoring
- best effort
- third party
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '38'
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
eissn:
- 2664-1690
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '12856'
relation: later_version
status: public
status: public
title: 'VAMOS: Middleware for Best-Effort Third-Party Monitoring'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '13142'
abstract:
- lang: eng
text: Reinforcement learning has received much attention for learning controllers
of deterministic systems. We consider a learner-verifier framework for stochastic
control systems and survey recent methods that formally guarantee a conjunction
of reachability and safety properties. Given a property and a lower bound on the
probability of the property being satisfied, our framework jointly learns a control
policy and a formal certificate to ensure the satisfaction of the property with
a desired probability threshold. Both the control policy and the formal certificate
are continuous functions from states to reals, which are learned as parameterized
neural networks. While in the deterministic case, the certificates are invariant
and barrier functions for safety, or Lyapunov and ranking functions for liveness,
in the stochastic case the certificates are supermartingales. For certificate
verification, we use interval arithmetic abstract interpretation to bound the
expected values of neural network functions.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
citation:
ama: 'Chatterjee K, Henzinger TA, Lechner M, Zikelic D. A learner-verifier framework
for neural network controllers and certificates of stochastic systems. In: Tools
and Algorithms for the Construction and Analysis of Systems . Vol 13993. Springer
Nature; 2023:3-25. doi:10.1007/978-3-031-30823-9_1'
apa: 'Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic, D. (2023). A
learner-verifier framework for neural network controllers and certificates of
stochastic systems. In Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13993, pp. 3–25). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_1'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Mathias Lechner, and Dorde
Zikelic. “A Learner-Verifier Framework for Neural Network Controllers and Certificates
of Stochastic Systems.” In Tools and Algorithms for the Construction and Analysis
of Systems , 13993:3–25. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_1.
ieee: K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic, “A learner-verifier
framework for neural network controllers and certificates of stochastic systems,”
in Tools and Algorithms for the Construction and Analysis of Systems ,
Paris, France, 2023, vol. 13993, pp. 3–25.
ista: 'Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier
framework for neural network controllers and certificates of stochastic systems.
Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993,
3–25.'
mla: Chatterjee, Krishnendu, et al. “A Learner-Verifier Framework for Neural Network
Controllers and Certificates of Stochastic Systems.” Tools and Algorithms for
the Construction and Analysis of Systems , vol. 13993, Springer Nature, 2023,
pp. 3–25, doi:10.1007/978-3-031-30823-9_1.
short: K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:, Tools and Algorithms
for the Construction and Analysis of Systems , Springer Nature, 2023, pp. 3–25.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-06-18T22:00:47Z
date_published: 2023-04-22T00:00:00Z
date_updated: 2023-06-19T08:30:54Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-031-30823-9_1
ec_funded: 1
file:
- access_level: open_access
checksum: 3d8a8bb24d211bc83360dfc2fd744307
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T08:29:30Z
date_updated: 2023-06-19T08:29:30Z
file_id: '13150'
file_name: 2023_LNCS_Chatterjee.pdf
file_size: 528455
relation: main_file
success: 1
file_date_updated: 2023-06-19T08:29:30Z
has_accepted_license: '1'
intvolume: ' 13993'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 3-25
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: 'Tools and Algorithms for the Construction and Analysis of Systems '
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308222'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: A learner-verifier framework for neural network controllers and certificates
of stochastic systems
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: 13993
year: '2023'
...
---
_id: '13141'
abstract:
- lang: eng
text: "We automatically compute a new class of environment assumptions in two-player
turn-based finite graph games which characterize an “adequate cooperation” needed
from the environment to allow the system player to win. Given an ω-regular winning
condition Φ for the system player, we compute an ω-regular assumption Ψ for the
environment player, such that (i) every environment strategy compliant with Ψ
allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the
environment for every strategy of the system (implementability), and (iii) Ψ does
not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games,
which are canonical representations of ω-regular games, we present a polynomial-time
algorithm for the symbolic computation of adequately permissive assumptions and
show that our algorithm runs faster and produces better assumptions than existing
approaches—both theoretically and empirically. To the best of our knowledge, for
ω\r\n-regular games, we provide the first algorithm to compute sufficient and
implementable environment assumptions that are also permissive."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ashwani
full_name: Anand, Ashwani
last_name: Anand
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Satya Prakash
full_name: Nayak, Satya Prakash
last_name: Nayak
- first_name: Anne Kathrin
full_name: Schmuck, Anne Kathrin
last_name: Schmuck
citation:
ama: 'Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions
for synthesis. In: TACAS 2023: Tools and Algorithms for the Construction and
Analysis of Systems. Vol 13994. Springer Nature; 2023:211-228. doi:10.1007/978-3-031-30820-8_15'
apa: 'Anand, A., Mallik, K., Nayak, S. P., & Schmuck, A. K. (2023). Computing
adequately permissive assumptions for synthesis. In TACAS 2023: Tools and Algorithms
for the Construction and Analysis of Systems (Vol. 13994, pp. 211–228). Paris,
France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_15'
chicago: 'Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin
Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In TACAS
2023: Tools and Algorithms for the Construction and Analysis of Systems, 13994:211–28.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_15.'
ieee: 'A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately
permissive assumptions for synthesis,” in TACAS 2023: Tools and Algorithms
for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994,
pp. 211–228.'
ista: 'Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive
assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of Systems, LNCS, vol. 13994, 211–228.'
mla: 'Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.”
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 211–28, doi:10.1007/978-3-031-30820-8_15.'
short: 'A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and
Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023,
pp. 211–228.'
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-06-18T22:00:47Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2023-06-19T08:49:46Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_15
file:
- access_level: open_access
checksum: 60dcafc1b4f6f070be43bad3fe877974
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T08:43:21Z
date_updated: 2023-06-19T08:43:21Z
file_id: '13151'
file_name: 2023_LNCS_Anand.pdf
file_size: 521425
relation: main_file
success: 1
file_date_updated: 2023-06-19T08:43:21Z
has_accepted_license: '1'
intvolume: ' 13994'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 211-228
publication: 'TACAS 2023: Tools and Algorithms for the Construction and Analysis of
Systems'
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing adequately permissive assumptions for synthesis
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13994
year: '2023'
...
---
_id: '12467'
abstract:
- lang: eng
text: Safety and liveness are elementary concepts of computation, and the foundation
of many verification paradigms. The safety-liveness classification of boolean
properties characterizes whether a given property can be falsified by observing
a finite prefix of an infinite computation trace (always for safety, never for
liveness). In quantitative specification and verification, properties assign not
truth values, but quantitative values to infinite traces (e.g., a cost, or the
distance to a boolean property). We introduce quantitative safety and liveness,
and we prove that our definitions induce conservative quantitative generalizations
of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness
decomposition of boolean properties. In particular, we show that every quantitative
property can be written as the pointwise minimum of a quantitative safety property
and a quantitative liveness property. Consequently, like boolean properties, also
quantitative properties can be min-decomposed into safety and liveness parts,
or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover,
quantitative properties can be approximated naturally. We prove that every quantitative
property that has both safe and co-safe approximations can be monitored arbitrarily
precisely by a monitor that uses only a finite number of states.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In:
26th International Conference Foundations of Software Science and Computation
Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative
safety and liveness. In 26th International Conference Foundations of Software
Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France:
Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative
Safety and Liveness.” In 26th International Conference Foundations of Software
Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17.
ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and
liveness,” in 26th International Conference Foundations of Software Science
and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness.
26th International Conference Foundations of Software Science and Computation
Structures. FOSSACS: Foundations of Software Science and Computation Structures,
LNCS, vol. 13992, 349–370.'
mla: Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International
Conference Foundations of Software Science and Computation Structures, vol.
13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference
Foundations of Software Science and Computation Structures, Springer Nature, 2023,
pp. 349–370.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FOSSACS: Foundations of Software Science and Computation Structures'
start_date: 2023-04-22
date_created: 2023-01-31T07:23:56Z
date_published: 2023-04-21T00:00:00Z
date_updated: 2023-07-14T11:20:27Z
day: '21'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-30829-1_17
ec_funded: 1
external_id:
arxiv:
- '2301.11175'
file:
- access_level: open_access
checksum: 981025aed580b6b27c426cb8856cf63e
content_type: application/pdf
creator: esarac
date_created: 2023-01-31T07:22:21Z
date_updated: 2023-01-31T07:22:21Z
file_id: '12468'
file_name: qsl.pdf
file_size: 449027
relation: main_file
success: 1
- access_level: open_access
checksum: f16e2af1e0eb243158ab0f0fe74e7d5a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T10:28:09Z
date_updated: 2023-06-19T10:28:09Z
file_id: '13153'
file_name: 2023_LNCS_HenzingerT.pdf
file_size: 1048171
relation: main_file
success: 1
file_date_updated: 2023-06-19T10:28:09Z
has_accepted_license: '1'
intvolume: ' 13992'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 349-370
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 26th International Conference Foundations of Software Science and Computation
Structures
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308284'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative safety and liveness
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 13992
year: '2023'
...
---
_id: '13292'
abstract:
- lang: eng
text: The operator precedence languages (OPLs) represent the largest known subclass
of the context-free languages which enjoys all desirable closure and decidability
properties. This includes the decidability of language inclusion, which is the
ultimate verification problem. Operator precedence grammars, automata, and logics
have been investigated and used, for example, to verify programs with arithmetic
expressions and exceptions (both of which are deterministic pushdown but lie outside
the scope of the visibly pushdown languages). In this paper, we complete the picture
and give, for the first time, an algebraic characterization of the class of OPLs
in the form of a syntactic congruence that has finitely many equivalence classes
exactly for the operator precedence languages. This is a generalization of the
celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of
the consequences, we show that universality and language inclusion for nondeterministic
operator precedence automata can be solved by an antichain algorithm. Antichain
algorithms avoid determinization and complementation through an explicit subset
construction, by leveraging a quasi-order on words, which allows the pruning of
the search space for counterexample words without sacrificing completeness. Antichain
algorithms can be implemented symbolically, and these implementations are today
the best-performing algorithms in practice for the inclusion of finite automata.
We give a generic construction of the quasi-order needed for antichain algorithms
from a finite syntactic congruence. This yields the first antichain algorithm
for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem
for OPLs in exponential time.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe
thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful
comments.\r\n"
alternative_title:
- LIPIcs
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: Pavol
full_name: Kebis, Pavol
last_name: Kebis
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator
precedence languages. In: 50th International Colloquium on Automata, Languages,
and Programming. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2023:129:1--129:20. doi:10.4230/LIPIcs.ICALP.2023.129'
apa: 'Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2023).
Regular methods for operator precedence languages. In 50th International Colloquium
on Automata, Languages, and Programming (Vol. 261, p. 129:1--129:20). Paderborn,
Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.129'
chicago: Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E
Sarac. “Regular Methods for Operator Precedence Languages.” In 50th International
Colloquium on Automata, Languages, and Programming, 261:129:1--129:20. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.ICALP.2023.129.
ieee: T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Regular methods
for operator precedence languages,” in 50th International Colloquium on Automata,
Languages, and Programming, Paderborn, Germany, 2023, vol. 261, p. 129:1--129:20.
ista: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2023. Regular methods for
operator precedence languages. 50th International Colloquium on Automata, Languages,
and Programming. ICALP: International Colloquium on Automata, Languages, and Programming,
LIPIcs, vol. 261, 129:1--129:20.'
mla: Henzinger, Thomas A., et al. “Regular Methods for Operator Precedence Languages.”
50th International Colloquium on Automata, Languages, and Programming,
vol. 261, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 129:1--129:20,
doi:10.4230/LIPIcs.ICALP.2023.129.
short: T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 50th International
Colloquium on Automata, Languages, and Programming, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2023, p. 129:1--129:20.
conference:
end_date: 2023-07-14
location: Paderborn, Germany
name: 'ICALP: International Colloquium on Automata, Languages, and Programming'
start_date: 2023-07-10
date_created: 2023-07-24T15:11:41Z
date_published: 2023-07-05T00:00:00Z
date_updated: 2023-07-31T08:38:38Z
day: '05'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.4230/LIPIcs.ICALP.2023.129
ec_funded: 1
external_id:
arxiv:
- '2305.03447'
file:
- access_level: open_access
checksum: 5d4c8932ef3450615a53b9bb15d92eb2
content_type: application/pdf
creator: esarac
date_created: 2023-07-24T15:11:05Z
date_updated: 2023-07-24T15:11:05Z
file_id: '13293'
file_name: icalp23.pdf
file_size: 859379
relation: main_file
success: 1
file_date_updated: 2023-07-24T15:11:05Z
has_accepted_license: '1'
intvolume: ' 261'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 129:1--129:20
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 50th International Colloquium on Automata, Languages, and Programming
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959772785'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
status: public
title: Regular methods for operator precedence languages
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: 261
year: '2023'
...
---
_id: '12704'
abstract:
- lang: eng
text: Adversarial training (i.e., training on adversarially perturbed input data)
is a well-studied method for making neural networks robust to potential adversarial
attacks during inference. However, the improved robustness does not come for free
but rather is accompanied by a decrease in overall model accuracy and performance.
Recent work has shown that, in practical robot learning applications, the effects
of adversarial training do not pose a fair trade-off but inflict a net loss when
measured in holistic robot performance. This work revisits the robustness-accuracy
trade-off in robot learning by systematically analyzing if recent advances in
robust training methods and theory in conjunction with adversarial robot learning,
are capable of making adversarial training suitable for real-world robot applications.
We evaluate three different robot learning tasks ranging from autonomous driving
in a high-fidelity environment amenable to sim-to-real deployment to mobile robot
navigation and gesture recognition. Our results demonstrate that, while these
techniques make incremental improvements on the trade-off on a relative scale,
the negative impact on the nominal accuracy caused by adversarial training still
outweighs the improved robustness by an order of magnitude. We conclude that although
progress is happening, further advances in robust learning methods are necessary
before they can benefit robot learning tasks in practice.
acknowledgement: "We thank Christoph Lampert for inspiring this work. The\r\nviews
and conclusions contained in this document are those of\r\nthe authors and should
not be interpreted as representing the\r\nofficial policies, either expressed or
implied, of the United States\r\nAir Force or the U.S. Government. The U.S. Government
is\r\nauthorized to reproduce and distribute reprints for Government\r\npurposes
notwithstanding any copyright notation herein."
article_processing_charge: No
article_type: original
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy
tradeoff in robot learning. IEEE Robotics and Automation Letters. 2023;8(3):1595-1602.
doi:10.1109/LRA.2023.3240930
apa: Lechner, M., Amini, A., Rus, D., & Henzinger, T. A. (2023). Revisiting
the adversarial robustness-accuracy tradeoff in robot learning. IEEE Robotics
and Automation Letters. Institute of Electrical and Electronics Engineers.
https://doi.org/10.1109/LRA.2023.3240930
chicago: Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger.
“Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” IEEE
Robotics and Automation Letters. Institute of Electrical and Electronics Engineers,
2023. https://doi.org/10.1109/LRA.2023.3240930.
ieee: M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial
robustness-accuracy tradeoff in robot learning,” IEEE Robotics and Automation
Letters, vol. 8, no. 3. Institute of Electrical and Electronics Engineers,
pp. 1595–1602, 2023.
ista: Lechner M, Amini A, Rus D, Henzinger TA. 2023. Revisiting the adversarial
robustness-accuracy tradeoff in robot learning. IEEE Robotics and Automation Letters.
8(3), 1595–1602.
mla: Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff
in Robot Learning.” IEEE Robotics and Automation Letters, vol. 8, no. 3,
Institute of Electrical and Electronics Engineers, 2023, pp. 1595–602, doi:10.1109/LRA.2023.3240930.
short: M. Lechner, A. Amini, D. Rus, T.A. Henzinger, IEEE Robotics and Automation
Letters 8 (2023) 1595–1602.
date_created: 2023-03-05T23:01:04Z
date_published: 2023-03-01T00:00:00Z
date_updated: 2023-08-01T13:36:50Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/LRA.2023.3240930
external_id:
arxiv:
- '2204.07373'
isi:
- '000936534100012'
file:
- access_level: open_access
checksum: 5a75dcd326ea66685de2b1aaec259e85
content_type: application/pdf
creator: cchlebak
date_created: 2023-03-07T12:22:23Z
date_updated: 2023-03-07T12:22:23Z
file_id: '12714'
file_name: 2023_IEEERobAutLetters_Lechner.pdf
file_size: 944052
relation: main_file
success: 1
file_date_updated: 2023-03-07T12:22:23Z
has_accepted_license: '1'
intvolume: ' 8'
isi: 1
issue: '3'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: 1595-1602
publication: IEEE Robotics and Automation Letters
publication_identifier:
eissn:
- 2377-3766
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
related_material:
record:
- id: '11366'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Revisiting the adversarial robustness-accuracy tradeoff in robot learning
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 8
year: '2023'
...
---
_id: '12876'
abstract:
- lang: eng
text: "Motivation: The problem of model inference is of fundamental importance to
systems biology. Logical models (e.g. Boolean networks; BNs) represent a computationally
attractive approach capable of handling large biological networks. The models
are typically inferred from experimental data. However, even with a substantial
amount of experimental data supported by some prior knowledge, existing inference
methods often focus on a small sample of admissible candidate models only.\r\n\r\nResults:
We propose Boolean network sketches as a new formal instrument for the inference
of Boolean networks. A sketch integrates (typically partial) knowledge about the
network’s topology and the update logic (obtained through, e.g. a biological knowledge
base or a literature search), as well as further assumptions about the properties
of the network’s transitions (e.g. the form of its attractor landscape), and additional
restrictions on the model dynamics given by the measured experimental data. Our
new BNs inference algorithm starts with an ‘initial’ sketch, which is extended
by adding restrictions representing experimental data to a ‘data-informed’ sketch
and subsequently computes all BNs consistent with the data-informed sketch. Our
algorithm is based on a symbolic representation and coloured model-checking. Our
approach is unique in its ability to cover a broad spectrum of knowledge and efficiently
produce a compact representation of all inferred BNs. We evaluate the method on
a non-trivial collection of real-world and simulated data."
acknowledgement: This work was partially supported by GACR [grant No. GA22-10845S];
and Grant Agency of Masaryk University [grant No. MUNI/G/1771/2020]. This work was
partially supported by European Union’s Horizon 2020 research and innovation programme
under the Marie Skłodowska-Curie [Grant Agreement No. 101034413 to S.P.].
article_number: btad158
article_processing_charge: No
article_type: original
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Ondřej
full_name: Huvar, Ondřej
last_name: Huvar
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
citation:
ama: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. Boolean network sketches:
A unifying framework for logical model inference. Bioinformatics. 2023;39(4).
doi:10.1093/bioinformatics/btad158'
apa: 'Beneš, N., Brim, L., Huvar, O., Pastva, S., & Šafránek, D. (2023). Boolean
network sketches: A unifying framework for logical model inference. Bioinformatics.
Oxford Academic. https://doi.org/10.1093/bioinformatics/btad158'
chicago: 'Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek.
“Boolean Network Sketches: A Unifying Framework for Logical Model Inference.”
Bioinformatics. Oxford Academic, 2023. https://doi.org/10.1093/bioinformatics/btad158.'
ieee: 'N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “Boolean network
sketches: A unifying framework for logical model inference,” Bioinformatics,
vol. 39, no. 4. Oxford Academic, 2023.'
ista: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2023. Boolean network sketches:
A unifying framework for logical model inference. Bioinformatics. 39(4), btad158.'
mla: 'Beneš, Nikola, et al. “Boolean Network Sketches: A Unifying Framework for
Logical Model Inference.” Bioinformatics, vol. 39, no. 4, btad158, Oxford
Academic, 2023, doi:10.1093/bioinformatics/btad158.'
short: N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, Bioinformatics 39 (2023).
date_created: 2023-04-30T22:01:05Z
date_published: 2023-04-03T00:00:00Z
date_updated: 2023-08-01T14:27:28Z
day: '03'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1093/bioinformatics/btad158
ec_funded: 1
external_id:
isi:
- '000976610800001'
pmid:
- '37004199'
file:
- access_level: open_access
checksum: 2cb90ddf781baefddf47eac4b54e2a03
content_type: application/pdf
creator: dernst
date_created: 2023-05-02T07:39:04Z
date_updated: 2023-05-02T07:39:04Z
file_id: '12886'
file_name: 2023_Bioinformatics_Benes.pdf
file_size: 478740
relation: main_file
success: 1
file_date_updated: 2023-05-02T07:39:04Z
has_accepted_license: '1'
intvolume: ' 39'
isi: 1
issue: '4'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Bioinformatics
publication_identifier:
eissn:
- 1367-4811
publication_status: published
publisher: Oxford Academic
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://doi.org/10.5281/zenodo.7688740
scopus_import: '1'
status: public
title: 'Boolean network sketches: A unifying framework for logical model inference'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 39
year: '2023'
...
---
_id: '14242'
abstract:
- lang: eng
text: We study the problem of training and certifying adversarially robust quantized
neural networks (QNNs). Quantization is a technique for making neural networks
more efficient by running them using low-bit integer arithmetic and is therefore
commonly adopted in industry. Recent work has shown that floating-point neural
networks that have been verified to be robust can become vulnerable to adversarial
attacks after quantization, and certification of the quantized representation
is necessary to guarantee robustness. In this work, we present quantization-aware
interval bound propagation (QA-IBP), a novel method for training robust QNNs.
Inspired by advances in robust learning of non-quantized networks, our training
algorithm computes the gradient of an abstract representation of the actual network.
Unlike existing approaches, our method can handle the discrete semantics of QNNs.
Based on QA-IBP, we also develop a complete verification procedure for verifying
the adversarial robustness of QNNs, which is guaranteed to terminate and produce
a correct answer. Compared to existing approaches, the key advantage of our verification
procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate
experimentally that our approach significantly outperforms existing methods and
establish the new state-of-the-art for training and certifying the robustness
of QNNs.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385. Research
was sponsored by the United\r\nStates Air Force Research Laboratory and the United
States Air Force Artificial Intelligence Accelerator and was accomplished under
Cooperative Agreement Number FA8750-19-2-\r\n1000. The views and conclusions contained
in this document are those of the authors and should not be interpreted as representing
the official policies, either expressed or implied,\r\nof the United States Air
Force or the U.S. Government. The U.S. Government is authorized to reproduce and
distribute reprints for Government purposes notwithstanding any copyright\r\nnotation
herein. The research was also funded in part by the AI2050 program at Schmidt Futures
(Grant G-22-63172) and Capgemini SE."
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks.
In: Proceedings of the 37th AAAI Conference on Artificial Intelligence.
Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973.
doi:10.1609/aaai.v37i12.26747'
apa: 'Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T. A., & Rus, D.
(2023). Quantization-aware interval bound propagation for training certifiably
robust quantized neural networks. In Proceedings of the 37th AAAI Conference
on Artificial Intelligence (Vol. 37, pp. 14964–14973). Washington, DC, United
States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v37i12.26747'
chicago: Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, Thomas A Henzinger,
and Daniela Rus. “Quantization-Aware Interval Bound Propagation for Training Certifiably
Robust Quantized Neural Networks.” In Proceedings of the 37th AAAI Conference
on Artificial Intelligence, 37:14964–73. Association for the Advancement of
Artificial Intelligence, 2023. https://doi.org/10.1609/aaai.v37i12.26747.
ieee: M. Lechner, D. Zikelic, K. Chatterjee, T. A. Henzinger, and D. Rus, “Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks,”
in Proceedings of the 37th AAAI Conference on Artificial Intelligence,
Washington, DC, United States, 2023, vol. 37, no. 12, pp. 14964–14973.
ista: 'Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware
interval bound propagation for training certifiably robust quantized neural networks.
Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference
on Artificial Intelligence vol. 37, 14964–14973.'
mla: Lechner, Mathias, et al. “Quantization-Aware Interval Bound Propagation for
Training Certifiably Robust Quantized Neural Networks.” Proceedings of the
37th AAAI Conference on Artificial Intelligence, vol. 37, no. 12, Association
for the Advancement of Artificial Intelligence, 2023, pp. 14964–73, doi:10.1609/aaai.v37i12.26747.
short: M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, D. Rus, in:, Proceedings
of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2023, pp. 14964–14973.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2023-08-27T22:01:17Z
date_published: 2023-06-26T00:00:00Z
date_updated: 2023-09-05T07:06:14Z
day: '26'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i12.26747
ec_funded: 1
external_id:
arxiv:
- '2211.16187'
intvolume: ' 37'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2211.16187
month: '06'
oa: 1
oa_version: Preprint
page: 14964-14973
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781577358800'
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantization-aware interval bound propagation for training certifiably robust
quantized neural networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '14243'
abstract:
- lang: eng
text: 'Two-player zero-sum "graph games" are central in logic, verification, and
multi-agent systems. The game proceeds by placing a token on a vertex of a graph,
and allowing the players to move it to produce an infinite path, which determines
the winner or payoff of the game. Traditionally, the players alternate turns in
moving the token. In "bidding games", however, the players have budgets and in
each turn, an auction (bidding) determines which player moves the token. So far,
bidding games have only been studied as full-information games. In this work we
initiate the study of partial-information bidding games: we study bidding games
in which a player''s initial budget is drawn from a known probability distribution.
We show that while for some bidding mechanisms and objectives, it is straightforward
to adapt the results from the full-information setting to the partial-information
setting, for others, the analysis is significantly more challenging, requires
new techniques, and gives rise to interesting results. Specifically, we study
games with "mean-payoff" objectives in combination with "poorman" bidding. We
construct optimal strategies for a partially-informed player who plays against
a fully-informed adversary. We show that, somewhat surprisingly, the "value" under
pure strategies does not necessarily exist in such games.'
acknowledgement: This research was supported in part by ISF grant no.1679/21, by the
ERC CoG 863818 (ForM-SMArt), and the European Union’s Horizon 2020 research and
innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Ismael R
full_name: Jecker, Ismael R
id: 85D7C63E-7D5D-11E9-9C0F-98C4E5697425
last_name: Jecker
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable
budgets. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence.
Vol 37. ; 2023:5464-5471. doi:10.1609/aaai.v37i5.25679'
apa: Avni, G., Jecker, I. R., & Zikelic, D. (2023). Bidding graph games with
partially-observable budgets. In Proceedings of the 37th AAAI Conference on
Artificial Intelligence (Vol. 37, pp. 5464–5471). Washington, DC, United States.
https://doi.org/10.1609/aaai.v37i5.25679
chicago: Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with
Partially-Observable Budgets.” In Proceedings of the 37th AAAI Conference on
Artificial Intelligence, 37:5464–71, 2023. https://doi.org/10.1609/aaai.v37i5.25679.
ieee: G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable
budgets,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence,
Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471.
ista: 'Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable
budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI:
Conference on Artificial Intelligence vol. 37, 5464–5471.'
mla: Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.”
Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol.
37, no. 5, 2023, pp. 5464–71, doi:10.1609/aaai.v37i5.25679.
short: G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference
on Artificial Intelligence, 2023, pp. 5464–5471.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2023-08-27T22:01:18Z
date_published: 2023-06-27T00:00:00Z
date_updated: 2023-09-05T08:37:00Z
day: '27'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i5.25679
ec_funded: 1
external_id:
arxiv:
- '2211.13626'
intvolume: ' 37'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1609/aaai.v37i5.25679
month: '06'
oa: 1
oa_version: Published Version
page: 5464-5471
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
isbn:
- '9781577358800'
publication_status: published
quality_controlled: '1'
scopus_import: '1'
status: public
title: Bidding graph games with partially-observable budgets
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '13310'
abstract:
- lang: eng
text: Machine-learned systems are in widespread use for making decisions about humans,
and it is important that they are fair, i.e., not biased against individuals based
on sensitive attributes. We present runtime verification of algorithmic fairness
for systems whose models are unknown, but are assumed to have a Markov chain structure.
We introduce a specification language that can model many common algorithmic fairness
properties, such as demographic parity, equal opportunity, and social burden.
We build monitors that observe a long sequence of events as generated by a given
system, and output, after each observation, a quantitative estimate of how fair
or biased the system was on that run until that point in time. The estimate is
proven to be correct modulo a variable error bound and a given confidence level,
where the error bound gets tighter as the observed sequence gets longer. Our monitors
are of two types, and use, respectively, frequentist and Bayesian statistical
inference techniques. While the frequentist monitors compute estimates that are
objectively correct with respect to the ground truth, the Bayesian monitors compute
estimates that are correct subject to a given prior belief about the system’s
model. Using a prototype implementation, we show how we can monitor if a bank
is fair in giving loans to applicants from different social backgrounds, and if
a college is fair in admitting students while maintaining a reasonable financial
burden on the society. Although they exhibit different theoretical complexities
in certain cases, in our experiments, both frequentist and Bayesian monitors took
less than a millisecond to update their verdicts after each observation.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG101020093.'
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Mahyar
full_name: Karimi, Mahyar
id: f1dedef5-2f78-11ee-989a-c4c97bccf506
last_name: Karimi
orcid: 0009-0005-0820-1696
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness.
In: Computer Aided Verification. Vol 13965. Springer Nature; 2023:358–382.
doi:10.1007/978-3-031-37703-7_17'
apa: 'Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Monitoring
algorithmic fairness. In Computer Aided Verification (Vol. 13965, pp. 358–382).
Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37703-7_17'
chicago: Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik.
“Monitoring Algorithmic Fairness.” In Computer Aided Verification, 13965:358–382.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37703-7_17.
ieee: T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic
fairness,” in Computer Aided Verification, Paris, France, 2023, vol. 13965,
pp. 358–382.
ista: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Monitoring algorithmic
fairness. Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 13965, 358–382.'
mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” Computer
Aided Verification, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:10.1007/978-3-031-37703-7_17.
short: T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification,
Springer Nature, 2023, pp. 358–382.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2023-07-25T18:32:40Z
date_published: 2023-07-18T00:00:00Z
date_updated: 2023-09-05T15:14:00Z
day: '18'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-37703-7_17
ec_funded: 1
external_id:
arxiv:
- '2305.15979'
file:
- access_level: open_access
checksum: ccaf94bf7d658ba012c016e11869b54c
content_type: application/pdf
creator: dernst
date_created: 2023-07-31T08:11:20Z
date_updated: 2023-07-31T08:11:20Z
file_id: '13327'
file_name: 2023_LNCS_CAV_HenzingerT.pdf
file_size: 647760
relation: main_file
success: 1
file_date_updated: 2023-07-31T08:11:20Z
has_accepted_license: '1'
intvolume: ' 13965'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 358–382
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Computer Aided Verification
publication_identifier:
eisbn:
- '9783031377037'
eissn:
- 1611-3349
isbn:
- '9783031377020'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Monitoring algorithmic fairness
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13965
year: '2023'
...
---
_id: '13221'
abstract:
- lang: eng
text: The safety-liveness dichotomy is a fundamental concept in formal languages
which plays a key role in verification. Recently, this dichotomy has been lifted
to quantitative properties, which are arbitrary functions from infinite words
to partially-ordered domains. We look into harnessing the dichotomy for the specific
classes of quantitative properties expressed by quantitative automata. These automata
contain finitely many states and rational-valued transition weights, and their
common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum
map infinite words into the totallyordered domain of real numbers. In this automata-theoretic
setting, we establish a connection between quantitative safety and topological
continuity and provide an alternative characterization of quantitative safety
and liveness in terms of their boolean counterparts. For all common value functions,
we show how the safety closure of a quantitative automaton can be constructed
in PTime, and we provide PSpace-complete checks of whether a given quantitative
automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata,
for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf,
and LimSup automata, we give PTime decompositions into safe and live automata.
These decompositions enable the separation of techniques for safety and liveness
verification for quantitative specifications.
acknowledgement: We thank Christof Löding for pointing us to some results on PSpace-hardess
of universality problems and the anonymous reviewers for their helpful comments.
This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science
Foundation grant 2410/22.
alternative_title:
- LIPIcs
article_number: '17'
article_processing_charge: No
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative
automata. In: 34th International Conference on Concurrency Theory. Vol
279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.17'
apa: 'Boker, U., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023).
Safety and liveness of quantitative automata. In 34th International Conference
on Concurrency Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17'
chicago: Boker, Udi, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac.
“Safety and Liveness of Quantitative Automata.” In 34th International Conference
on Concurrency Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2023. https://doi.org/10.4230/LIPIcs.CONCUR.2023.17.
ieee: U. Boker, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Safety and liveness
of quantitative automata,” in 34th International Conference on Concurrency
Theory, Antwerp, Belgium, 2023, vol. 279.
ista: 'Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Safety and liveness
of quantitative automata. 34th International Conference on Concurrency Theory.
CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 279, 17.'
mla: Boker, Udi, et al. “Safety and Liveness of Quantitative Automata.” 34th
International Conference on Concurrency Theory, vol. 279, 17, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.17.
short: U. Boker, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 34th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2023.
conference:
end_date: 2023-09-23
location: Antwerp, Belgium
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2023-09-18
date_created: 2023-07-14T10:00:15Z
date_published: 2023-09-01T00:00:00Z
date_updated: 2023-10-09T07:14:03Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2023.17
ec_funded: 1
external_id:
arxiv:
- '2307.06016'
file:
- access_level: open_access
checksum: d40e57a04448ea5c77d7e1cfb9590a81
content_type: application/pdf
creator: esarac
date_created: 2023-07-14T12:03:48Z
date_updated: 2023-07-14T12:03:48Z
file_id: '13224'
file_name: CONCUR23.pdf
file_size: 755529
relation: main_file
success: 1
file_date_updated: 2023-07-14T12:03:48Z
has_accepted_license: '1'
intvolume: ' 279'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 34th International Conference on Concurrency Theory
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959772990'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
status: public
title: Safety and liveness of quantitative automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 279
year: '2023'
...
---
_id: '14405'
abstract:
- lang: eng
text: We introduce hypernode automata as a new specification formalism for hyperproperties
of concurrent systems. They are finite automata with nodes labeled with hypernode
logic formulas and transitions labeled with actions. A hypernode logic formula
specifies relations between sequences of variable values in different system executions.
Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces
by constraining the values and the order of value changes of each variable without
correlating the timing of the changes. Different execution traces are synchronized
solely through the transitions of hypernode automata. Hypernode automata naturally
combine asynchronicity at the node level with synchronicity at the transition
level. We show that the model-checking problem for hypernode automata is decidable
over action-labeled Kripke structures, whose actions induce transitions of the
specification automata. For this reason, hypernode automaton is a suitable formalism
for specifying and verifying asynchronous hyperproperties, such as declassifying
observational determinism in multi-threaded programs.
acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF)
SFB project\r\nSpyCoDe F8502, by the FWF projects ZK-35 and W1255-N23, and by the
ERC Advanced Grant\r\nVAMOS 101020093."
alternative_title:
- LIPIcs
article_number: '21'
article_processing_charge: Yes
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata.
In: 34th International Conference on Concurrency Theory. Vol 279. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.21'
apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A.
(2023). Hypernode automata. In 34th International Conference on Concurrency
Theory (Vol. 279). Antwerp, Belgium: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.21'
chicago: Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
Costa. “Hypernode Automata.” In 34th International Conference on Concurrency
Theory, Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
https://doi.org/10.4230/LIPIcs.CONCUR.2023.21.
ieee: E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode
automata,” in 34th International Conference on Concurrency Theory, Antwerp,
Belgium, 2023, vol. 279.
ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2023. Hypernode
automata. 34th International Conference on Concurrency Theory. CONCUR: Conference
on Concurrency Theory, LIPIcs, vol. 279, 21.'
mla: Bartocci, Ezio, et al. “Hypernode Automata.” 34th International Conference
on Concurrency Theory, vol. 279, 21, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2023, doi:10.4230/LIPIcs.CONCUR.2023.21.
short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, 34th
International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2023.
conference:
end_date: 2023-09-22
location: Antwerp, Belgium
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2023-09-19
date_created: 2023-10-08T22:01:16Z
date_published: 2023-09-01T00:00:00Z
date_updated: 2023-10-09T07:43:44Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2023.21
ec_funded: 1
external_id:
arxiv:
- '2305.02836'
file:
- access_level: open_access
checksum: 215765e40454d806174ac0a223e8d6fa
content_type: application/pdf
creator: dernst
date_created: 2023-10-09T07:42:45Z
date_updated: 2023-10-09T07:42:45Z
file_id: '14413'
file_name: 2023_LIPcs_Bartocci.pdf
file_size: 795790
relation: main_file
success: 1
file_date_updated: 2023-10-09T07:42:45Z
has_accepted_license: '1'
intvolume: ' 279'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 34th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959772990'
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Hypernode automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 279
year: '2023'
...
---
_id: '14454'
abstract:
- lang: eng
text: As AI and machine-learned software are used increasingly for making decisions
that affect humans, it is imperative that they remain fair and unbiased in their
decisions. To complement design-time bias mitigation measures, runtime verification
techniques have been introduced recently to monitor the algorithmic fairness of
deployed systems. Previous monitoring techniques assume full observability of
the states of the (unknown) monitored system. Moreover, they can monitor only
fairness properties that are specified as arithmetic expressions over the probabilities
of different events. In this work, we extend fairness monitoring to systems modeled
as partially observed Markov chains (POMC), and to specifications containing arithmetic
expressions over the expected values of numerical functions on event sequences.
The only assumptions we make are that the underlying POMC is aperiodic and starts
in the stationary distribution, with a bound on its mixing time being known. These
assumptions enable us to estimate a given property for the entire distribution
of possible executions of the monitored POMC, by observing only a single execution.
Our monitors observe a long run of the system and, after each new observation,
output updated PAC-estimates of how fair or biased the system is. The monitors
are computationally lightweight and, using a prototype implementation, we demonstrate
their effectiveness on several real-world examples.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG 101020093.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Henzinger TA, Kueffner K, Mallik K. Monitoring algorithmic fairness under
partial observations. In: 23rd International Conference on Runtime Verification.
Vol 14245. Springer Nature; 2023:291-311. doi:10.1007/978-3-031-44267-4_15'
apa: 'Henzinger, T. A., Kueffner, K., & Mallik, K. (2023). Monitoring algorithmic
fairness under partial observations. In 23rd International Conference on Runtime
Verification (Vol. 14245, pp. 291–311). Thessaloniki, Greece: Springer Nature.
https://doi.org/10.1007/978-3-031-44267-4_15'
chicago: Henzinger, Thomas A, Konstantin Kueffner, and Kaushik Mallik. “Monitoring
Algorithmic Fairness under Partial Observations.” In 23rd International Conference
on Runtime Verification, 14245:291–311. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_15.
ieee: T. A. Henzinger, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness
under partial observations,” in 23rd International Conference on Runtime Verification,
Thessaloniki, Greece, 2023, vol. 14245, pp. 291–311.
ista: 'Henzinger TA, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness
under partial observations. 23rd International Conference on Runtime Verification.
RV: Conference on Runtime Verification, LNCS, vol. 14245, 291–311.'
mla: Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness under Partial
Observations.” 23rd International Conference on Runtime Verification, vol.
14245, Springer Nature, 2023, pp. 291–311, doi:10.1007/978-3-031-44267-4_15.
short: T.A. Henzinger, K. Kueffner, K. Mallik, in:, 23rd International Conference
on Runtime Verification, Springer Nature, 2023, pp. 291–311.
conference:
end_date: 2023-10-06
location: Thessaloniki, Greece
name: 'RV: Conference on Runtime Verification'
start_date: 2023-10-03
date_created: 2023-10-29T23:01:15Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2023-10-31T11:48:20Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-031-44267-4_15
ec_funded: 1
external_id:
arxiv:
- '2308.00341'
intvolume: ' 14245'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2308.00341
month: '10'
oa: 1
oa_version: Preprint
page: 291-311
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 23rd International Conference on Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031442667'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring algorithmic fairness under partial observations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14245
year: '2023'
...
---
_id: '14518'
abstract:
- lang: eng
text: We consider bidding games, a class of two-player zero-sum graph games. The
game proceeds as follows. Both players have bounded budgets. A token is placed
on a vertex of a graph, in each turn the players simultaneously submit bids, and
the higher bidder moves the token, where we break bidding ties in favor of Player
1. Player 1 wins the game iff the token visits a designated target vertex. We
consider, for the first time, poorman discrete-bidding in which the granularity
of the bids is restricted and the higher bid is paid to the bank. Previous work
either did not impose granularity restrictions or considered Richman bidding (bids
are paid to the opponent). While the latter mechanisms are technically more accessible,
the former is more appealing from a practical standpoint. Our study focuses on
threshold budgets, which is the necessary and sufficient initial budget required
for Player 1 to ensure winning against a given Player 2 budget. We first show
existence of thresholds. In DAGs, we show that threshold budgets can be approximated
with error bounds by thresholds under continuous-bidding and that they exhibit
a periodic behavior. We identify closed-form solutions in special cases. We implement
and experiment with an algorithm to find threshold budgets.
acknowledgement: This research was supported in part by ISF grant no. 1679/21, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie SkłodowskaCurie Grant Agreement No. 665385.
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Suman
full_name: Sadhukhan, Suman
last_name: Sadhukhan
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. Reachability poorman
discrete-bidding games. In: Frontiers in Artificial Intelligence and Applications.
Vol 372. IOS Press; 2023:141-148. doi:10.3233/FAIA230264'
apa: 'Avni, G., Meggendorfer, T., Sadhukhan, S., Tkadlec, J., & Zikelic, D.
(2023). Reachability poorman discrete-bidding games. In Frontiers in Artificial
Intelligence and Applications (Vol. 372, pp. 141–148). Krakow, Poland: IOS
Press. https://doi.org/10.3233/FAIA230264'
chicago: Avni, Guy, Tobias Meggendorfer, Suman Sadhukhan, Josef Tkadlec, and Dorde
Zikelic. “Reachability Poorman Discrete-Bidding Games.” In Frontiers in Artificial
Intelligence and Applications, 372:141–48. IOS Press, 2023. https://doi.org/10.3233/FAIA230264.
ieee: G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, and D. Zikelic, “Reachability
poorman discrete-bidding games,” in Frontiers in Artificial Intelligence and
Applications, Krakow, Poland, 2023, vol. 372, pp. 141–148.
ista: 'Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. 2023. Reachability
poorman discrete-bidding games. Frontiers in Artificial Intelligence and Applications.
ECAI: European Conference on Artificial Intelligence vol. 372, 141–148.'
mla: Avni, Guy, et al. “Reachability Poorman Discrete-Bidding Games.” Frontiers
in Artificial Intelligence and Applications, vol. 372, IOS Press, 2023, pp.
141–48, doi:10.3233/FAIA230264.
short: G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, D. Zikelic, in:, Frontiers
in Artificial Intelligence and Applications, IOS Press, 2023, pp. 141–148.
conference:
end_date: 2023-10-04
location: Krakow, Poland
name: 'ECAI: European Conference on Artificial Intelligence'
start_date: 2023-09-30
date_created: 2023-11-12T23:00:56Z
date_published: 2023-09-28T00:00:00Z
date_updated: 2023-11-13T10:18:45Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.3233/FAIA230264
ec_funded: 1
external_id:
arxiv:
- '2307.15218'
file:
- access_level: open_access
checksum: 1390ca38480fa4cf286b0f1a42e8c12f
content_type: application/pdf
creator: dernst
date_created: 2023-11-13T10:16:10Z
date_updated: 2023-11-13T10:16:10Z
file_id: '14529'
file_name: 2023_FAIA_Avni.pdf
file_size: 501011
relation: main_file
success: 1
file_date_updated: 2023-11-13T10:16:10Z
has_accepted_license: '1'
intvolume: ' 372'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc/4.0/
month: '09'
oa: 1
oa_version: Published Version
page: 141-148
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Frontiers in Artificial Intelligence and Applications
publication_identifier:
isbn:
- '9781643684369'
issn:
- 0922-6389
publication_status: published
publisher: IOS Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reachability poorman discrete-bidding games
tmp:
image: /images/cc_by_nc.png
legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
short: CC BY-NC (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 372
year: '2023'
...
---
_id: '14559'
abstract:
- lang: eng
text: We consider the problem of learning control policies in discrete-time stochastic
systems which guarantee that the system stabilizes within some specified stabilization
region with probability 1. Our approach is based on the novel notion of stabilizing
ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome
the limitation of methods proposed in previous works whose applicability is restricted
to systems in which the stabilizing region cannot be left once entered under any
control policy. We present a learning procedure that learns a control policy together
with an sRSM that formally certifies probability 1 stability, both learned as
neural networks. We show that this procedure can also be adapted to formally verifying
that, under a given Lipschitz continuous control policy, the stochastic system
stabilizes within some stabilizing region with probability 1. Our experimental
evaluation shows that our learning procedure can successfully learn provably stabilizing
policies in practice.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Matin
full_name: Ansaripour, Matin
last_name: Ansaripour
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. Learning provably
stabilizing neural controllers for discrete-time stochastic systems. In: 21st
International Symposium on Automated Technology for Verification and Analysis.
Vol 14215. Springer Nature; 2023:357-379. doi:10.1007/978-3-031-45329-8_17'
apa: 'Ansaripour, M., Chatterjee, K., Henzinger, T. A., Lechner, M., & Zikelic,
D. (2023). Learning provably stabilizing neural controllers for discrete-time
stochastic systems. In 21st International Symposium on Automated Technology
for Verification and Analysis (Vol. 14215, pp. 357–379). Singapore, Singapore:
Springer Nature. https://doi.org/10.1007/978-3-031-45329-8_17'
chicago: Ansaripour, Matin, Krishnendu Chatterjee, Thomas A Henzinger, Mathias Lechner,
and Dorde Zikelic. “Learning Provably Stabilizing Neural Controllers for Discrete-Time
Stochastic Systems.” In 21st International Symposium on Automated Technology
for Verification and Analysis, 14215:357–79. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-45329-8_17.
ieee: M. Ansaripour, K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic,
“Learning provably stabilizing neural controllers for discrete-time stochastic
systems,” in 21st International Symposium on Automated Technology for Verification
and Analysis, Singapore, Singapore, 2023, vol. 14215, pp. 357–379.
ista: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning
provably stabilizing neural controllers for discrete-time stochastic systems.
21st International Symposium on Automated Technology for Verification and Analysis.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379.'
mla: Ansaripour, Matin, et al. “Learning Provably Stabilizing Neural Controllers
for Discrete-Time Stochastic Systems.” 21st International Symposium on Automated
Technology for Verification and Analysis, vol. 14215, Springer Nature, 2023,
pp. 357–79, doi:10.1007/978-3-031-45329-8_17.
short: M. Ansaripour, K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:,
21st International Symposium on Automated Technology for Verification and Analysis,
Springer Nature, 2023, pp. 357–379.
conference:
end_date: 2023-10-27
location: Singapore, Singapore
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2023-10-24
date_created: 2023-11-19T23:00:56Z
date_published: 2023-10-22T00:00:00Z
date_updated: 2023-11-20T08:30:20Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-031-45329-8_17
ec_funded: 1
intvolume: ' 14215'
language:
- iso: eng
month: '10'
oa_version: None
page: 357-379
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: 21st International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031453281'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Learning provably stabilizing neural controllers for discrete-time stochastic
systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14215
year: '2023'
...
---
_id: '13228'
abstract:
- lang: eng
text: A machine-learned system that is fair in static decision-making tasks may
have biased societal impacts in the long-run. This may happen when the system
interacts with humans and feedback patterns emerge, reinforcing old biases in
the system and creating new biases. While existing works try to identify and mitigate
long-run biases through smart system design, we introduce techniques for monitoring
fairness in real time. Our goal is to build and deploy a monitor that will continuously
observe a long sequence of events generated by the system in the wild, and will
output, with each event, a verdict on how fair the system is at the current point
in time. The advantages of monitoring are two-fold. Firstly, fairness is evaluated
at run-time, which is important because unfair behaviors may not be eliminated
a priori, at design-time, due to partial knowledge about the system and the environment,
as well as uncertainties and dynamic changes in the system and the environment,
such as the unpredictability of human behavior. Secondly, monitors are by design
oblivious to how the monitored system is constructed, which makes them suitable
to be used as trusted third-party fairness watchdogs. They function as computationally
lightweight statistical estimators, and their correctness proofs rely on the rigorous
analysis of the stochastic process that models the assumptions about the underlying
dynamics of the system. We show, both in theory and experiments, how monitors
can warn us (1) if a bank’s credit policy over time has created an unfair distribution
of credit scores among the population, and (2) if a resource allocator’s allocation
policy over time has made unfair allocations. Our experiments demonstrate that
the monitors introduce very low overhead. We believe that runtime monitoring is
an important and mathematically rigorous new addition to the fairness toolbox.
acknowledgement: 'The authors would like to thank the anonymous reviewers for their
valuable comments and helpful suggestions. This work is supported by the European
Research Council under Grant No.: ERC-2020-AdG 101020093.'
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: Mahyar
full_name: Karimi, Mahyar
last_name: Karimi
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. Runtime monitoring of dynamic
fairness properties. In: FAccT ’23: Proceedings of the 2023 ACM Conference
on Fairness, Accountability, and Transparency. Association for Computing Machinery;
2023:604-614. doi:10.1145/3593013.3594028'
apa: 'Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023). Runtime
monitoring of dynamic fairness properties. In FAccT ’23: Proceedings of the
2023 ACM Conference on Fairness, Accountability, and Transparency (pp. 604–614).
Chicago, IL, United States: Association for Computing Machinery. https://doi.org/10.1145/3593013.3594028'
chicago: 'Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik.
“Runtime Monitoring of Dynamic Fairness Properties.” In FAccT ’23: Proceedings
of the 2023 ACM Conference on Fairness, Accountability, and Transparency,
604–14. Association for Computing Machinery, 2023. https://doi.org/10.1145/3593013.3594028.'
ieee: 'T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Runtime monitoring
of dynamic fairness properties,” in FAccT ’23: Proceedings of the 2023 ACM
Conference on Fairness, Accountability, and Transparency, Chicago, IL, United
States, 2023, pp. 604–614.'
ista: 'Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Runtime monitoring of
dynamic fairness properties. FAccT ’23: Proceedings of the 2023 ACM Conference
on Fairness, Accountability, and Transparency. FAccT: Conference on Fairness,
Accountability and Transparency, 604–614.'
mla: 'Henzinger, Thomas A., et al. “Runtime Monitoring of Dynamic Fairness Properties.”
FAccT ’23: Proceedings of the 2023 ACM Conference on Fairness, Accountability,
and Transparency, Association for Computing Machinery, 2023, pp. 604–14, doi:10.1145/3593013.3594028.'
short: 'T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, FAccT ’23: Proceedings
of the 2023 ACM Conference on Fairness, Accountability, and Transparency, Association
for Computing Machinery, 2023, pp. 604–614.'
conference:
end_date: 2023-06-15
location: Chicago, IL, United States
name: 'FAccT: Conference on Fairness, Accountability and Transparency'
start_date: 2023-06-12
date_created: 2023-07-16T22:01:09Z
date_published: 2023-06-12T00:00:00Z
date_updated: 2023-12-13T11:30:31Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3593013.3594028
ec_funded: 1
external_id:
arxiv:
- '2305.04699'
isi:
- '001062819300057'
file:
- access_level: open_access
checksum: 96c759db9cdf94b81e37871a66a6ff48
content_type: application/pdf
creator: dernst
date_created: 2023-07-18T07:43:10Z
date_updated: 2023-07-18T07:43:10Z
file_id: '13245'
file_name: 2023_ACM_HenzingerT.pdf
file_size: 4100596
relation: main_file
success: 1
file_date_updated: 2023-07-18T07:43:10Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 604-614
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 'FAccT ''23: Proceedings of the 2023 ACM Conference on Fairness, Accountability,
and Transparency'
publication_identifier:
isbn:
- '9781450372527'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Runtime monitoring of dynamic fairness properties
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '13263'
abstract:
- lang: eng
text: "Motivation: Boolean networks are simple but efficient mathematical formalism
for modelling complex biological systems. However, having only two levels of activation
is sometimes not enough to fully capture the dynamics of real-world biological
systems. Hence, the need for multi-valued networks (MVNs), a generalization of
Boolean networks. Despite the importance of MVNs for modelling biological systems,
only limited progress has been made on developing theories, analysis methods,
and tools that can support them. In particular, the recent use of trap spaces
in Boolean networks made a great impact on the field of systems biology, but there
has been no similar concept defined and studied for MVNs to date.\r\n\r\nResults:
In this work, we generalize the concept of trap spaces in Boolean networks to
that in MVNs. We then develop the theory and the analysis methods for trap spaces
in MVNs. In particular, we implement all proposed methods in a Python package
called trapmvn. Not only showing the applicability of our approach via a realistic
case study, we also evaluate the time efficiency of the method on a large collection
of real-world models. The experimental results confirm the time efficiency, which
we believe enables more accurate analysis on larger and more complex multi-valued
models."
acknowledgement: This work was supported by L’Institut Carnot STAR, Marseille, France,
and by the European Union’s Horizon 2020 research and innovation programme under
the Marie Skłodowska-Curie Grant Agreement No. [101034413].
article_processing_charge: Yes
article_type: original
author:
- first_name: Van Giang
full_name: Trinh, Van Giang
last_name: Trinh
- first_name: Belaid
full_name: Benhamou, Belaid
last_name: Benhamou
- 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: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
citation:
ama: 'Trinh VG, Benhamou B, Henzinger TA, Pastva S. Trap spaces of multi-valued
networks: Definition, computation, and applications. Bioinformatics. 2023;39(Supplement_1):i513-i522.
doi:10.1093/bioinformatics/btad262'
apa: 'Trinh, V. G., Benhamou, B., Henzinger, T. A., & Pastva, S. (2023). Trap
spaces of multi-valued networks: Definition, computation, and applications. Bioinformatics.
Oxford Academic. https://doi.org/10.1093/bioinformatics/btad262'
chicago: 'Trinh, Van Giang, Belaid Benhamou, Thomas A Henzinger, and Samuel Pastva.
“Trap Spaces of Multi-Valued Networks: Definition, Computation, and Applications.”
Bioinformatics. Oxford Academic, 2023. https://doi.org/10.1093/bioinformatics/btad262.'
ieee: 'V. G. Trinh, B. Benhamou, T. A. Henzinger, and S. Pastva, “Trap spaces of
multi-valued networks: Definition, computation, and applications,” Bioinformatics,
vol. 39, no. Supplement_1. Oxford Academic, pp. i513–i522, 2023.'
ista: 'Trinh VG, Benhamou B, Henzinger TA, Pastva S. 2023. Trap spaces of multi-valued
networks: Definition, computation, and applications. Bioinformatics. 39(Supplement_1),
i513–i522.'
mla: 'Trinh, Van Giang, et al. “Trap Spaces of Multi-Valued Networks: Definition,
Computation, and Applications.” Bioinformatics, vol. 39, no. Supplement_1,
Oxford Academic, 2023, pp. i513–22, doi:10.1093/bioinformatics/btad262.'
short: V.G. Trinh, B. Benhamou, T.A. Henzinger, S. Pastva, Bioinformatics 39 (2023)
i513–i522.
date_created: 2023-07-23T22:01:12Z
date_published: 2023-06-30T00:00:00Z
date_updated: 2023-12-13T11:41:52Z
day: '30'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1093/bioinformatics/btad262
ec_funded: 1
external_id:
isi:
- '001027457000060'
pmid:
- '37387165'
file:
- access_level: open_access
checksum: ba3abe1171df1958413b7c7f957f5486
content_type: application/pdf
creator: dernst
date_created: 2023-07-31T11:09:05Z
date_updated: 2023-07-31T11:09:05Z
file_id: '13335'
file_name: 2023_Bioinformatics_Trinh.pdf
file_size: 641736
relation: main_file
success: 1
file_date_updated: 2023-07-31T11:09:05Z
has_accepted_license: '1'
intvolume: ' 39'
isi: 1
issue: Supplement_1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: i513-i522
pmid: 1
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Bioinformatics
publication_identifier:
eissn:
- 1367-4811
issn:
- 1367-4803
publication_status: published
publisher: Oxford Academic
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/giang-trinh/trap-mvn
scopus_import: '1'
status: public
title: 'Trap spaces of multi-valued networks: Definition, computation, and applications'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 39
year: '2023'
...
---
_id: '14400'
abstract:
- lang: eng
text: "We consider the problem of computing the maximal probability of satisfying
an \r\n-regular specification for stochastic, continuous-state, nonlinear systems
evolving in discrete time. The problem reduces, after automata-theoretic constructions,
to finding the maximal probability of satisfying a parity condition on a (possibly
hybrid) state space. While characterizing the exact satisfaction probability is
open, we show that a lower bound on this probability can be obtained by (I) computing
an under-approximation of the qualitative winning region, i.e., states from which
the parity condition can be enforced almost surely, and (II) computing the maximal
probability of reaching this qualitative winning region.\r\nThe heart of our approach
is a technique to symbolically compute the under-approximation of the qualitative
winning region in step (I) via a finite-state abstraction of the original system
as a \r\n-player parity game. Our abstraction procedure uses only the support
of the probabilistic evolution; it does not use precise numerical transition probabilities.
We prove that the winning set in the abstract -player game induces an under-approximation
of the qualitative winning region in the original synthesis problem, along with
a policy to solve it. By combining these contributions with (a) a symbolic fixpoint
algorithm to solve \r\n-player games and (b) existing techniques for reachability
policy synthesis in stochastic nonlinear systems, we get an abstraction-based
algorithm for finding a lower bound on the maximal satisfaction probability.\r\nWe
have implemented the abstraction-based algorithm in Mascot-SDS, where we combined
the outlined abstraction step with our tool Genie (Majumdar et al., 2023) that
solves \r\n-player parity games (through a reduction to Rabin games) more efficiently
than existing algorithms. We evaluated our implementation on the nonlinear model
of a perturbed bistable switch from the literature. We show empirically that the
lower bound on the winning region computed by our approach is precise, by comparing
against an over-approximation of the qualitative winning region. Moreover, our
implementation outperforms a recently proposed tool for solving this problem by
a large margin."
acknowledgement: "We thank Daniel Hausmann and Nir Piterman for their valuable comments
on an earlier version of the manuscript of our other paper [22] where we present,
among other things, the parity fixpoint for 2 1/2-player games (for a slightly more
general class of games) with a different and indirect proof of correctness. Based
on their comments we observed that, unlike the other fixpoints that we present in
[22], the parity fixpoint does not follow the exact same structure as its counterpart
for 2-player games, which we also use int his paper.\r\nWe also thank Thejaswini
Raghavan for observing that our symbolic parity fixpoint algorithm can be solved
in quasi-polynomial time using recent improved algorithms for solving \r\n-calculus
expressions. This significantly improved the complexity bounds of our algorithm
in this paper.\r\nThe work of R. Majumdar and A.-K. Schmuck are partially supported
by DFG, Germany project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded
through DFG, Germany project (SCHM 3541/1-1). K. Mallik is supported by the ERC
project ERC-2020-AdG 101020093. S. Soudjani is supported by the following projects:
EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047."
article_number: '101430'
article_processing_charge: No
article_type: original
author:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Anne Kathrin
full_name: Schmuck, Anne Kathrin
last_name: Schmuck
- first_name: Sadegh
full_name: Soudjani, Sadegh
last_name: Soudjani
citation:
ama: 'Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic
systems via finite parity games. Nonlinear Analysis: Hybrid Systems. 2023;51.
doi:10.1016/j.nahs.2023.101430'
apa: 'Majumdar, R., Mallik, K., Schmuck, A. K., & Soudjani, S. (2023). Symbolic
control for stochastic systems via finite parity games. Nonlinear Analysis:
Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2023.101430'
chicago: 'Majumdar, Rupak, Kaushik Mallik, Anne Kathrin Schmuck, and Sadegh Soudjani.
“Symbolic Control for Stochastic Systems via Finite Parity Games.” Nonlinear
Analysis: Hybrid Systems. Elsevier, 2023. https://doi.org/10.1016/j.nahs.2023.101430.'
ieee: 'R. Majumdar, K. Mallik, A. K. Schmuck, and S. Soudjani, “Symbolic control
for stochastic systems via finite parity games,” Nonlinear Analysis: Hybrid
Systems, vol. 51. Elsevier, 2023.'
ista: 'Majumdar R, Mallik K, Schmuck AK, Soudjani S. 2023. Symbolic control for
stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems.
51, 101430.'
mla: 'Majumdar, Rupak, et al. “Symbolic Control for Stochastic Systems via Finite
Parity Games.” Nonlinear Analysis: Hybrid Systems, vol. 51, 101430, Elsevier,
2023, doi:10.1016/j.nahs.2023.101430.'
short: 'R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid
Systems 51 (2023).'
date_created: 2023-10-08T22:01:15Z
date_published: 2023-09-27T00:00:00Z
date_updated: 2023-12-13T12:58:56Z
day: '27'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2023.101430
ec_funded: 1
external_id:
arxiv:
- '2101.00834'
isi:
- '001093188100001'
intvolume: ' 51'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.nahs.2023.101430
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_identifier:
issn:
- 1751-570X
publication_status: epub_ahead
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic control for stochastic systems via finite parity games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 51
year: '2023'
...
---
_id: '14718'
abstract:
- lang: eng
text: 'Binary decision diagrams (BDDs) are one of the fundamental data structures
in formal methods and computer science in general. However, the performance of
BDD-based algorithms greatly depends on memory latency due to the reliance on
large hash tables and thus, by extension, on the speed of random memory access.
This hinders the full utilisation of resources available on modern CPUs, since
the absolute memory latency has not improved significantly for at least a decade.
In this paper, we explore several implementation techniques that improve the performance
of BDD manipulation either through enhanced memory locality or by partially eliminating
random memory access. On a benchmark suite of 600+ BDDs derived from real-world
applications, we demonstrate runtime that is comparable or better than parallelising
the same operations on eight CPU cores. '
acknowledgement: "This work was supported by the European Union’s Horizon 2020 research
and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413
and the\r\n“VAMOS” grant ERC-2020-AdG 101020093."
article_processing_charge: No
author:
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Pastva S, Henzinger TA. Binary decision diagrams on modern hardware. In: Proceedings
of the 23rd Conference on Formal Methods in Computer-Aided Design. TU Vienna
Academic Press; 2023:122-131. doi:10.34727/2023/isbn.978-3-85448-060-0_20'
apa: 'Pastva, S., & Henzinger, T. A. (2023). Binary decision diagrams on modern
hardware. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design (pp. 122–131). Ames, IA, United States: TU Vienna Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20'
chicago: Pastva, Samuel, and Thomas A Henzinger. “Binary Decision Diagrams on Modern
Hardware.” In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design, 122–31. TU Vienna Academic Press, 2023. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20.
ieee: S. Pastva and T. A. Henzinger, “Binary decision diagrams on modern hardware,”
in Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design,
Ames, IA, United States, 2023, pp. 122–131.
ista: 'Pastva S, Henzinger TA. 2023. Binary decision diagrams on modern hardware.
Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design.
FMCAD: Conference on Formal Methods in Computer-aided design, 122–131.'
mla: Pastva, Samuel, and Thomas A. Henzinger. “Binary Decision Diagrams on Modern
Hardware.” Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design, TU Vienna Academic Press, 2023, pp. 122–31, doi:10.34727/2023/isbn.978-3-85448-060-0_20.
short: S. Pastva, T.A. Henzinger, in:, Proceedings of the 23rd Conference on Formal
Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–131.
conference:
end_date: 2023-10-27
location: Ames, IA, United States
name: 'FMCAD: Conference on Formal Methods in Computer-aided design'
start_date: 2023-10-25
date_created: 2023-12-31T23:01:03Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2024-01-02T08:16:28Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.34727/2023/isbn.978-3-85448-060-0_20
ec_funded: 1
file:
- access_level: open_access
checksum: 818d6e13dd508f3a04f0941081022e5d
content_type: application/pdf
creator: dernst
date_created: 2024-01-02T08:14:23Z
date_updated: 2024-01-02T08:14:23Z
file_id: '14721'
file_name: 2023_FMCAD_Pastva.pdf
file_size: 524321
relation: main_file
success: 1
file_date_updated: 2024-01-02T08:14:23Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 122-131
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
Design
publication_identifier:
isbn:
- '9783854480600'
publication_status: published
publisher: TU Vienna Academic Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Binary decision diagrams on modern hardware
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '14830'
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.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC
CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
article_processing_charge: No
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. In: Proceedings of the
37th AAAI Conference on Artificial Intelligence. Vol 37. Association for the
Advancement of Artificial Intelligence; 2023:11926-11935. doi:10.1609/aaai.v37i10.26407'
apa: 'Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (2023). Learning
control policies for stochastic systems with reach-avoid guarantees. In Proceedings
of the 37th AAAI Conference on Artificial Intelligence (Vol. 37, pp. 11926–11935).
Washington, DC, United States: Association for the Advancement of Artificial Intelligence.
https://doi.org/10.1609/aaai.v37i10.26407'
chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee.
“Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.”
In Proceedings of the 37th AAAI Conference on Artificial Intelligence,
37:11926–35. Association for the Advancement of Artificial Intelligence, 2023.
https://doi.org/10.1609/aaai.v37i10.26407.
ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control
policies for stochastic systems with reach-avoid guarantees,” in Proceedings
of the 37th AAAI Conference on Artificial Intelligence, Washington, DC, United
States, 2023, vol. 37, no. 10, pp. 11926–11935.
ista: 'Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control
policies for stochastic systems with reach-avoid guarantees. Proceedings of the
37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial
Intelligence vol. 37, 11926–11935.'
mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with
Reach-Avoid Guarantees.” Proceedings of the 37th AAAI Conference on Artificial
Intelligence, vol. 37, no. 10, Association for the Advancement of Artificial
Intelligence, 2023, pp. 11926–35, doi:10.1609/aaai.v37i10.26407.
short: D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of
the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement
of Artificial Intelligence, 2023, pp. 11926–11935.
conference:
end_date: 2023-02-14
location: Washington, DC, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2023-02-07
date_created: 2024-01-18T07:44:31Z
date_published: 2023-06-26T00:00:00Z
date_updated: 2024-01-22T14:08:29Z
day: '26'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v37i10.26407
ec_funded: 1
external_id:
arxiv:
- '2210.05308'
intvolume: ' 37'
issue: '10'
keyword:
- General Medicine
language:
- iso: eng
month: '06'
oa_version: Preprint
page: 11926-11935
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: Proceedings of the 37th AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
related_material:
record:
- id: '14600'
relation: earlier_version
status: public
status: public
title: Learning control policies for stochastic systems with reach-avoid guarantees
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2023'
...
---
_id: '13234'
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. We consider the problem of monitoring the
classification decisions of neural networks in the presence of novel classes.
For this purpose, we generalize our recently proposed abstraction-based monitor
from binary output to real-valued quantitative output. This quantitative output
enables new applications, two of which we investigate in the paper. As our first
application, we introduce an algorithmic framework for active monitoring of a
neural network, which allows us to learn new classes dynamically and yet maintain
high monitoring performance. As our second application, we present an offline
procedure to retrain the neural network to improve the monitor’s detection performance
without deteriorating the network’s classification accuracy. Our experimental
evaluation demonstrates both the benefits of our active monitoring framework in
dynamic scenarios and the effectiveness of the retraining procedure.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, by
DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS.
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- 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: 'Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active
monitoring of neural networks (extended version). International Journal on
Software Tools for Technology Transfer. 2023;25:575-592. doi:10.1007/s10009-023-00711-4'
apa: 'Kueffner, K., Lukina, A., Schilling, C., & Henzinger, T. A. (2023). Into
the unknown: Active monitoring of neural networks (extended version). International
Journal on Software Tools for Technology Transfer. Springer Nature. https://doi.org/10.1007/s10009-023-00711-4'
chicago: 'Kueffner, Konstantin, Anna Lukina, Christian Schilling, and Thomas A Henzinger.
“Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” International
Journal on Software Tools for Technology Transfer. Springer Nature, 2023.
https://doi.org/10.1007/s10009-023-00711-4.'
ieee: 'K. Kueffner, A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown:
Active monitoring of neural networks (extended version),” International Journal
on Software Tools for Technology Transfer, vol. 25. Springer Nature, pp. 575–592,
2023.'
ista: 'Kueffner K, Lukina A, Schilling C, Henzinger TA. 2023. Into the unknown:
Active monitoring of neural networks (extended version). International Journal
on Software Tools for Technology Transfer. 25, 575–592.'
mla: 'Kueffner, Konstantin, et al. “Into the Unknown: Active Monitoring of Neural
Networks (Extended Version).” International Journal on Software Tools for Technology
Transfer, vol. 25, Springer Nature, 2023, pp. 575–92, doi:10.1007/s10009-023-00711-4.'
short: K. Kueffner, A. Lukina, C. Schilling, T.A. Henzinger, International Journal
on Software Tools for Technology Transfer 25 (2023) 575–592.
date_created: 2023-07-16T22:01:11Z
date_published: 2023-08-01T00:00:00Z
date_updated: 2024-01-30T12:06:57Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s10009-023-00711-4
ec_funded: 1
external_id:
arxiv:
- '2009.06429'
isi:
- '001020160000001'
file:
- access_level: open_access
checksum: 3c4b347f39412a76872f9a6f30101f94
content_type: application/pdf
creator: dernst
date_created: 2024-01-30T12:06:07Z
date_updated: 2024-01-30T12:06:07Z
file_id: '14903'
file_name: 2023_JourSoftwareTools_Kueffner.pdf
file_size: 13387667
relation: main_file
success: 1
file_date_updated: 2024-01-30T12:06:07Z
has_accepted_license: '1'
intvolume: ' 25'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 575-592
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: International Journal on Software Tools for Technology Transfer
publication_identifier:
eissn:
- 1433-2787
issn:
- 1433-2779
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '10206'
relation: shorter_version
status: public
scopus_import: '1'
status: public
title: 'Into the unknown: Active monitoring of neural networks (extended version)'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 25
year: '2023'
...
---
_id: '14920'
abstract:
- lang: eng
text: "We consider fixpoint algorithms for two-player games on graphs with $\\omega$-regular
winning conditions, where the environment is constrained by a strong transition
fairness assumption. Strong transition fairness is a widely occurring special
case of strong fairness, which requires that any execution is strongly fair with
respect to a specified set of live edges: whenever the\r\nsource vertex of a live
edge is visited infinitely often along a play, the edge itself is traversed infinitely
often along the play as well. We show that, surprisingly, strong transition fairness
retains the algorithmic characteristics of the fixpoint algorithms for $\\omega$-regular
games -- the new algorithms have the same alternation depth as the classical algorithms
but invoke a new type of predecessor operator. For Rabin games with $k$ pairs,
the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is
independent of the number of live edges in the strong transition fairness assumption.
Further, we show that GR(1) specifications with strong transition fairness assumptions
can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm.
In contrast, strong fairness necessarily requires increasing the alternation depth
depending on the number of fairness assumptions. We get symbolic algorithms for
(generalized) Rabin, parity and GR(1) objectives under strong transition fairness
assumptions as well as a direct symbolic algorithm for qualitative winning in
stochastic\r\n$\\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps,
improving the state of the art. Finally, we have implemented a BDD-based synthesis
engine based on our algorithm. We show on a set of synthetic and real benchmarks
that our algorithm is scalable, parallelizable, and outperforms previous algorithms
by orders of magnitude."
acknowledgement: A previous version of this paper has appeared in TACAS 2022. Authors
ordered alphabetically. T. Banerjee was interning with MPI-SWS when this research
was conducted. R. Majumdar and A.-K. Schmuck are partially supported by DFG project
389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded through DFG project
(SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093.
article_number: '4'
article_processing_charge: Yes
article_type: original
author:
- first_name: Tamajit
full_name: Banerjee, Tamajit
last_name: Banerjee
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Anne-Kathrin
full_name: Schmuck, Anne-Kathrin
last_name: Schmuck
- first_name: Sadegh
full_name: Soudjani, Sadegh
last_name: Soudjani
citation:
ama: Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. Fast symbolic algorithms
for mega-regular games under strong transition fairness. TheoretiCS. 2023;2.
doi:10.46298/theoretics.23.4
apa: Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A.-K., & Soudjani, S.
(2023). Fast symbolic algorithms for mega-regular games under strong transition
fairness. TheoretiCS. EPI Sciences. https://doi.org/10.46298/theoretics.23.4
chicago: Banerjee, Tamajit, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck,
and Sadegh Soudjani. “Fast Symbolic Algorithms for Mega-Regular Games under Strong
Transition Fairness.” TheoretiCS. EPI Sciences, 2023. https://doi.org/10.46298/theoretics.23.4.
ieee: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani, “Fast
symbolic algorithms for mega-regular games under strong transition fairness,”
TheoretiCS, vol. 2. EPI Sciences, 2023.
ista: Banerjee T, Majumdar R, Mallik K, Schmuck A-K, Soudjani S. 2023. Fast symbolic
algorithms for mega-regular games under strong transition fairness. TheoretiCS.
2, 4.
mla: Banerjee, Tamajit, et al. “Fast Symbolic Algorithms for Mega-Regular Games
under Strong Transition Fairness.” TheoretiCS, vol. 2, 4, EPI Sciences,
2023, doi:10.46298/theoretics.23.4.
short: T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, S. Soudjani, TheoretiCS
2 (2023).
date_created: 2024-01-31T13:40:49Z
date_published: 2023-02-24T00:00:00Z
date_updated: 2024-02-05T10:21:51Z
day: '24'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.46298/theoretics.23.4
ec_funded: 1
external_id:
arxiv:
- '2202.07480'
file:
- access_level: open_access
checksum: 2972d531122a6f15727b396110fb3f5c
content_type: application/pdf
creator: dernst
date_created: 2024-02-05T10:19:35Z
date_updated: 2024-02-05T10:19:35Z
file_id: '14940'
file_name: 2023_TheoretiCS_Banerjee.pdf
file_size: 917076
relation: main_file
success: 1
file_date_updated: 2024-02-05T10:19:35Z
has_accepted_license: '1'
intvolume: ' 2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: TheoretiCS
publication_identifier:
issn:
- 2751-4838
publication_status: published
publisher: EPI Sciences
quality_controlled: '1'
status: public
title: Fast symbolic algorithms for mega-regular games under strong transition fairness
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2023'
...
---
_id: '14411'
abstract:
- lang: eng
text: "Partially specified Boolean networks (PSBNs) represent a promising framework
for the qualitative modelling of biological systems in which the logic of interactions
is not completely known. Phenotype control aims to stabilise the network in states
exhibiting specific traits.\r\nIn this paper, we define the phenotype control
problem in the context of asynchronous PSBNs and propose a novel semi-symbolic
algorithm for solving this problem with permanent variable perturbations."
acknowledgement: This work was supported by the Czech Foundation grant No. GA22-10845S,
Grant Agency of Masaryk University grant No. MUNI/G/1771/2020, and the European
Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie
Grant Agreement No. 101034413.
alternative_title:
- LNBI
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
- first_name: Eva
full_name: Šmijáková, Eva
last_name: Šmijáková
citation:
ama: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. Phenotype control of partially
specified boolean networks. In: 21st International Conference on Computational
Methods in Systems Biology. Vol 14137. Springer Nature; 2023:18-35. doi:10.1007/978-3-031-42697-1_2'
apa: 'Beneš, N., Brim, L., Pastva, S., Šafránek, D., & Šmijáková, E. (2023).
Phenotype control of partially specified boolean networks. In 21st International
Conference on Computational Methods in Systems Biology (Vol. 14137, pp. 18–35).
Luxembourg City, Luxembourg: Springer Nature. https://doi.org/10.1007/978-3-031-42697-1_2'
chicago: Beneš, Nikola, Luboš Brim, Samuel Pastva, David Šafránek, and Eva Šmijáková.
“Phenotype Control of Partially Specified Boolean Networks.” In 21st International
Conference on Computational Methods in Systems Biology, 14137:18–35. Springer
Nature, 2023. https://doi.org/10.1007/978-3-031-42697-1_2.
ieee: N. Beneš, L. Brim, S. Pastva, D. Šafránek, and E. Šmijáková, “Phenotype control
of partially specified boolean networks,” in 21st International Conference
on Computational Methods in Systems Biology, Luxembourg City, Luxembourg,
2023, vol. 14137, pp. 18–35.
ista: 'Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. 2023. Phenotype control
of partially specified boolean networks. 21st International Conference on Computational
Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNBI,
vol. 14137, 18–35.'
mla: Beneš, Nikola, et al. “Phenotype Control of Partially Specified Boolean Networks.”
21st International Conference on Computational Methods in Systems Biology,
vol. 14137, Springer Nature, 2023, pp. 18–35, doi:10.1007/978-3-031-42697-1_2.
short: N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková, in:, 21st International
Conference on Computational Methods in Systems Biology, Springer Nature, 2023,
pp. 18–35.
conference:
end_date: 2023-09-15
location: Luxembourg City, Luxembourg
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2023-09-13
date_created: 2023-10-08T22:01:18Z
date_published: 2023-09-09T00:00:00Z
date_updated: 2024-02-20T09:02:04Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-42697-1_2
ec_funded: 1
file:
- access_level: open_access
checksum: 6f71bdaedb770b52380222fd9f4d7937
content_type: application/pdf
creator: spastva
date_created: 2024-02-16T08:26:32Z
date_updated: 2024-02-16T08:26:32Z
file_id: '14997'
file_name: cmsb2023.pdf
file_size: 691582
relation: main_file
success: 1
file_date_updated: 2024-02-16T08:26:32Z
has_accepted_license: '1'
intvolume: ' 14137'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 18-35
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 21st International Conference on Computational Methods in Systems Biology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031426964'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Phenotype control of partially specified boolean networks
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14137
year: '2023'
...
---
_id: '14758'
abstract:
- lang: eng
text: 'We present a flexible and efficient toolchain to symbolically solve (standard)
Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin
games. To our best knowledge, our tools are the first ones to be able to solve
these problems. Furthermore, using these flexible game solvers as a back-end,
we implemented a tool for computing correct-by-construction controllers for stochastic
dynamical systems under LTL specifications. Our implementations use the recent
theoretical result that all of these games can be solved using the same symbolic
fixpoint algorithm but utilizing different, domain specific calculations of the
involved predecessor operators. The main feature of our toolchain is the utilization
of two programming abstractions: one to separate the symbolic fixpoint computations
from the predecessor calculations, and another one to allow the integration of
different BDD libraries as back-ends. In particular, we employ a multi-threaded
execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan,
which leads to enormous computational savings.'
acknowledgement: 'Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are
partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally
funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project
ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1.
S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802,
and ERC 101089047.'
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Mateusz
full_name: Rychlicki, Mateusz
last_name: Rychlicki
- first_name: Anne-Kathrin
full_name: Schmuck, Anne-Kathrin
last_name: Schmuck
- first_name: Sadegh
full_name: Soudjani, Sadegh
last_name: Soudjani
citation:
ama: 'Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain
for symbolic rabin games under fair and stochastic uncertainties. In: 35th
International Conference on Computer Aided Verification. Vol 13966. Springer
Nature; 2023:3-15. doi:10.1007/978-3-031-37709-9_1'
apa: 'Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., & Soudjani, S.
(2023). A flexible toolchain for symbolic rabin games under fair and stochastic
uncertainties. In 35th International Conference on Computer Aided Verification
(Vol. 13966, pp. 3–15). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-37709-9_1'
chicago: Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck,
and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair
and Stochastic Uncertainties.” In 35th International Conference on Computer
Aided Verification, 13966:3–15. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-37709-9_1.
ieee: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible
toolchain for symbolic rabin games under fair and stochastic uncertainties,” in
35th International Conference on Computer Aided Verification, Paris, France,
2023, vol. 13966, pp. 3–15.
ista: 'Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible
toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th
International Conference on Computer Aided Verification. CAV: Computer Aided Verification,
LNCS, vol. 13966, 3–15.'
mla: Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under
Fair and Stochastic Uncertainties.” 35th International Conference on Computer
Aided Verification, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:10.1007/978-3-031-37709-9_1.
short: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th
International Conference on Computer Aided Verification, Springer Nature, 2023,
pp. 3–15.
conference:
end_date: 2023-07-22
location: Paris, France
name: 'CAV: Computer Aided Verification'
start_date: 2023-07-17
date_created: 2024-01-08T13:18:00Z
date_published: 2023-07-16T00:00:00Z
date_updated: 2024-02-27T07:39:51Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-37709-9_1
ec_funded: 1
file:
- access_level: open_access
checksum: 1a361d83db0244fd32c03b544c294b5a
content_type: application/pdf
creator: dernst
date_created: 2024-01-09T10:01:07Z
date_updated: 2024-01-09T10:01:07Z
file_id: '14765'
file_name: 2023_LNCSCAV_Majumdar.pdf
file_size: 405147
relation: main_file
success: 1
file_date_updated: 2024-01-09T10:01:07Z
has_accepted_license: '1'
intvolume: ' 13966'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 3-15
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 35th International Conference on Computer Aided Verification
publication_identifier:
eisbn:
- '9783031377099'
eissn:
- 1611-3349
isbn:
- '9783031377082'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14994'
relation: research_data
status: public
scopus_import: '1'
status: public
title: A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties
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: 13966
year: '2023'
...
---
_id: '14994'
abstract:
- lang: eng
text: This resource contains the artifacts for reproducing the experimental results
presented in the paper titled "A Flexible Toolchain for Symbolic Rabin Games under
Fair and Stochastic Uncertainties" that has been submitted in CAV 2023.
article_processing_charge: No
author:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Mateusz
full_name: Rychlicki, Mateusz
last_name: Rychlicki
- first_name: Anne-Kathrin
full_name: Schmuck, Anne-Kathrin
last_name: Schmuck
- first_name: Sadegh
full_name: Soudjani, Sadegh
last_name: Soudjani
citation:
ama: Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain
for symbolic rabin games under fair and stochastic uncertainties. 2023. doi:10.5281/ZENODO.7877790
apa: Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., & Soudjani, S.
(2023). A flexible toolchain for symbolic rabin games under fair and stochastic
uncertainties. Zenodo. https://doi.org/10.5281/ZENODO.7877790
chicago: Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck,
and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair
and Stochastic Uncertainties.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.7877790.
ieee: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible
toolchain for symbolic rabin games under fair and stochastic uncertainties.” Zenodo,
2023.
ista: Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible
toolchain for symbolic rabin games under fair and stochastic uncertainties, Zenodo,
10.5281/ZENODO.7877790.
mla: Majumdar, Rupak, et al. A Flexible Toolchain for Symbolic Rabin Games under
Fair and Stochastic Uncertainties. Zenodo, 2023, doi:10.5281/ZENODO.7877790.
short: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, (2023).
date_created: 2024-02-14T15:13:00Z
date_published: 2023-04-28T00:00:00Z
date_updated: 2024-02-27T07:39:51Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.5281/ZENODO.7877790
has_accepted_license: '1'
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/zenodo.7877790
month: '04'
oa: 1
oa_version: Published Version
publisher: Zenodo
related_material:
record:
- id: '14758'
relation: used_in_publication
status: public
status: public
title: A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties
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: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '15023'
abstract:
- lang: eng
text: Reinforcement learning has shown promising results in learning neural network
policies for complicated control tasks. However, the lack of formal guarantees
about the behavior of such policies remains an impediment to their deployment.
We propose a novel method for learning a composition of neural network policies
in stochastic environments, along with a formal certificate which guarantees that
a specification over the policy's behavior is satisfied with the desired probability.
Unlike prior work on verifiable RL, our approach leverages the compositional nature
of logical specifications provided in SpectRL, to learn over graphs of probabilistic
reach-avoid specifications. The formal guarantees are provided by learning neural
network policies together with reach-avoid supermartingales (RASM) for the graph’s
sub-tasks and then composing them into a global policy. We also derive a tighter
lower bound compared to previous work on the probability of reach-avoidance implied
by a RASM, which is required to find a compositional policy with an acceptable
probabilistic threshold for complex tasks with multiple edge policies. We implement
a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS)
and the ERC-2020-\r\nCoG 863818 (FoRM-SMArt)."
article_processing_charge: No
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: Abhinav
full_name: Verma, Abhinav
id: a235593c-d7fa-11eb-a0c5-b22ca3c66ee6
last_name: Verma
- 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, Verma A, Chatterjee K, Henzinger TA. Compositional policy
learning in stochastic control systems with formal guarantees. In: 37th Conference
on Neural Information Processing Systems. ; 2023.'
apa: Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., & Henzinger, T. A.
(2023). Compositional policy learning in stochastic control systems with formal
guarantees. In 37th Conference on Neural Information Processing Systems.
New Orleans, LO, United States.
chicago: Zikelic, Dorde, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee,
and Thomas A Henzinger. “Compositional Policy Learning in Stochastic Control Systems
with Formal Guarantees.” In 37th Conference on Neural Information Processing
Systems, 2023.
ieee: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, and T. A. Henzinger, “Compositional
policy learning in stochastic control systems with formal guarantees,” in 37th
Conference on Neural Information Processing Systems, New Orleans, LO, United
States, 2023.
ista: 'Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional
policy learning in stochastic control systems with formal guarantees. 37th Conference
on Neural Information Processing Systems. NeurIPS: Neural Information Processing
Systems.'
mla: Zikelic, Dorde, et al. “Compositional Policy Learning in Stochastic Control
Systems with Formal Guarantees.” 37th Conference on Neural Information Processing
Systems, 2023.
short: D. Zikelic, M. Lechner, A. Verma, K. Chatterjee, T.A. Henzinger, in:, 37th
Conference on Neural Information Processing Systems, 2023.
conference:
end_date: 2023-12-16
location: New Orleans, LO, United States
name: 'NeurIPS: Neural Information Processing Systems'
start_date: 2023-12-10
date_created: 2024-02-25T09:23:24Z
date_published: 2023-12-15T00:00:00Z
date_updated: 2024-02-28T12:20:11Z
day: '15'
department:
- _id: ToHe
- _id: KrCh
ec_funded: 1
external_id:
arxiv:
- '2312.01456'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2312.01456
month: '12'
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
publication: 37th Conference on Neural Information Processing Systems
publication_status: epub_ahead
quality_controlled: '1'
status: public
title: Compositional policy learning in stochastic control systems with formal guarantees
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '14076'
abstract:
- lang: eng
text: Hyperproperties are properties that relate multiple execution traces. Previous
work on monitoring hyperproperties focused on synchronous hyperproperties, usually
specified in HyperLTL. When monitoring synchronous hyperproperties, all traces
are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers
and show how to use them for monitoring synchronous as well as, for the first
time, asynchronous hyperproperties. Prefix transducers map multiple input traces
into one or more output traces by incrementally matching prefixes of the input
traces against expressions similar to regular expressions. The prefixes of different
traces which are consumed by a single matching step of the monitor may have different
lengths. The deterministic and executable nature of prefix transducers makes them
more suitable as an intermediate formalism for runtime verification than logical
specifications, which tend to be highly non-deterministic, especially in the case
of asynchronous hyperproperties. We report on a set of experiments about monitoring
asynchronous version of observational determinism.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
authors would like to thank Ana Oliveira da Costa for commenting on a draft of the
paper.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers.
In: 23nd International Conference on Runtime Verification. Vol 14245. Springer
Nature; 2023:168-190. doi:10.1007/978-3-031-44267-4_9'
apa: 'Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with
prefix transducers. In 23nd International Conference on Runtime Verification
(Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. https://doi.org/10.1007/978-3-031-44267-4_9'
chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with
Prefix Transducers.” In 23nd International Conference on Runtime Verification,
14245:168–90. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-44267-4_9.
ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,”
in 23nd International Conference on Runtime Verification, Thessaloniki,
Greek, 2023, vol. 14245, pp. 168–190.
ista: 'Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers.
23nd International Conference on Runtime Verification. RV: Conference on Runtime
Verification, LNCS, vol. 14245, 168–190.'
mla: Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix
Transducers.” 23nd International Conference on Runtime Verification, vol.
14245, Springer Nature, 2023, pp. 168–90, doi:10.1007/978-3-031-44267-4_9.
short: M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime
Verification, Springer Nature, 2023, pp. 168–190.
conference:
end_date: 2023-10-07
location: Thessaloniki, Greek
name: 'RV: Conference on Runtime Verification'
start_date: 2023-10-04
date_created: 2023-08-16T20:46:08Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2024-02-28T12:33:08Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-44267-4_9
ec_funded: 1
file:
- access_level: open_access
checksum: ee33bd6f1a26f4dae7a8192584869fd8
content_type: application/pdf
creator: dernst
date_created: 2023-10-16T07:15:11Z
date_updated: 2023-10-16T07:15:11Z
file_id: '14430'
file_name: 2023_LNCS_RV_Chalupa.pdf
file_size: 867256
relation: main_file
success: 1
file_date_updated: 2023-10-16T07:15:11Z
has_accepted_license: '1'
intvolume: ' 14245'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 168-190
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 23nd International Conference on Runtime Verification
publication_identifier:
eisbn:
- 978-3-031-44267-4
isbn:
- 978-3-031-44266-7
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '15035'
relation: research_data
status: public
status: public
title: Monitoring hyperproperties with prefix transducers
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14245
year: '2023'
...
---
_id: '15035'
abstract:
- lang: eng
text: "This artifact aims to reproduce experiments from the paper Monitoring Hyperproperties
With Prefix Transducers accepted at RV'23, and give further pointers to implementation
of prefix transducers.\r\nIt has two parts: a pre-compiled docker image and sources
that one can use to compile (locally or in docker) the software and run the experiments."
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers.
2023. doi:10.5281/ZENODO.8191723
apa: Chalupa, M., & Henzinger, T. A. (2023). Monitoring hyperproperties with
prefix transducers. Zenodo. https://doi.org/10.5281/ZENODO.8191723
chicago: Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with
Prefix Transducers.” Zenodo, 2023. https://doi.org/10.5281/ZENODO.8191723.
ieee: M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers.”
Zenodo, 2023.
ista: Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers,
Zenodo, 10.5281/ZENODO.8191723.
mla: Chalupa, Marek, and Thomas A. Henzinger. Monitoring Hyperproperties with
Prefix Transducers. Zenodo, 2023, doi:10.5281/ZENODO.8191723.
short: M. Chalupa, T.A. Henzinger, (2023).
date_created: 2024-02-28T07:34:34Z
date_published: 2023-07-28T00:00:00Z
date_updated: 2024-02-28T12:33:09Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.5281/ZENODO.8191723
ec_funded: 1
has_accepted_license: '1'
main_file_link:
- open_access: '1'
url: https://doi.org/10.5281/zenodo.8191722
month: '07'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publisher: Zenodo
related_material:
record:
- id: '14076'
relation: used_in_publication
status: public
status: public
title: Monitoring hyperproperties with prefix transducers
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: research_data_reference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '10774'
abstract:
- lang: eng
text: We study the problem of specifying sequential information-flow properties
of systems. Information-flow properties are hyperproperties, as they compare different
traces of a system. Sequential information-flow properties can express changes,
over time, in the information-flow constraints. For example, information-flow
constraints during an initialization phase of a system may be different from information-flow
constraints that are required during the operation phase. We formalize several
variants of interpreting sequential information-flow constraints, which arise
from different assumptions about what can be observed of the system. For this
purpose, we introduce a first-order logic, called Hypertrace Logic, with both
trace and time quantifiers for specifying linear-time hyperproperties. We prove
that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted
quantifier prefixes, cannot specify the majority of the studied variants of sequential
information flow, including all variants in which the transition between sequential
phases (such as initialization and operation) happens asynchronously. Our results
rely on new equivalences between sets of traces that cannot be distinguished by
certain classes of formulas from Hypertrace Logic. This presents a new approach
to proving inexpressiveness results for HyperLTL.
acknowledgement: This work was funded in part by the Wittgenstein Award Z211-N23 of
the Austrian Science Fund (FWF) and by the FWF project W1255-N23.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana Oliveira
full_name: Da Costa, Ana Oliveira
last_name: Da Costa
citation:
ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential
information flow. In: Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
Vol 13182. Springer Nature; 2022:1-19. doi:10.1007/978-3-030-94583-1_1'
apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa,
A. O. (2022). Flavors of sequential information flow. In Lecture Notes in Computer
Science (including subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics) (Vol. 13182, pp. 1–19). Philadelphia, PA, United
States: Springer Nature. https://doi.org/10.1007/978-3-030-94583-1_1'
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), 13182:1–19. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-94583-1_1.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
“Flavors of sequential information flow,” in Lecture Notes in Computer Science
(including subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), Philadelphia, PA, United States, 2022, vol. 13182, pp.
1–19.
ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors
of sequential information flow. Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182,
1–19.'
mla: Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 13182, Springer Nature, 2022, pp.
1–19, doi:10.1007/978-3-030-94583-1_1.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp.
1–19.
conference:
end_date: 2022-01-18
location: Philadelphia, PA, United States
name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
start_date: 2022-01-16
date_created: 2022-02-20T23:01:34Z
date_published: 2022-01-14T00:00:00Z
date_updated: 2022-08-05T09:02:56Z
day: '14'
department:
- _id: ToHe
doi: 10.1007/978-3-030-94583-1_1
external_id:
arxiv:
- '2105.02013'
intvolume: ' 13182'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2105.02013'
month: '01'
oa: 1
oa_version: Preprint
page: 1-19
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783030945824'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of sequential information flow
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13182
year: '2022'
...
---
_id: '12010'
abstract:
- lang: eng
text: World models learn behaviors in a latent imagination space to enhance the
sample-efficiency of deep reinforcement learning (RL) algorithms. While learning
world models for high-dimensional observations (e.g., pixel inputs) has become
practicable on standard RL benchmarks and some games, their effectiveness in real-world
robotics applications has not been explored. In this paper, we investigate how
such agents generalize to real-world autonomous vehicle control tasks, where advanced
model-free deep RL algorithms fail. In particular, we set up a series of time-lap
tasks for an F1TENTH racing robot, equipped with a high-dimensional LiDAR sensor,
on a set of test tracks with a gradual increase in their complexity. In this continuous-control
setting, we show that model-based agents capable of learning in imagination substantially
outperform model-free agents with respect to performance, sample efficiency, successful
task completion, and generalization. Moreover, we show that the generalization
ability of model-based agents strongly depends on the choice of their observation
model. We provide extensive empirical evidence for the effectiveness of world
models provided with long enough memory horizons in sim2real tasks.
acknowledgement: L.B. was supported by the Doctoral College Resilient Embedded Systems.
M.L. was supported in part by the ERC2020-AdG 101020093 and the Austrian Science
Fund (FWF) under grant Z211-N23 (Wittgenstein Award). R.H. and D.R. were supported
by The Boeing Company and the Office of Naval Research (ONR) Grant N00014-18-1-2830.
R.G. was partially supported by the Horizon-2020 ECSEL Project grant No. 783163
(iDev40) and A.B. by FFG Project ADEX.
article_processing_charge: No
author:
- first_name: Axel
full_name: Brunnbauer, Axel
last_name: Brunnbauer
- first_name: Luigi
full_name: Berducci, Luigi
last_name: Berducci
- first_name: Andreas
full_name: Brandstatter, Andreas
last_name: Brandstatter
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Brunnbauer A, Berducci L, Brandstatter A, et al. Latent imagination facilitates
zero-shot transfer in autonomous racing. In: 2022 International Conference
on Robotics and Automation. IEEE; 2022:7513-7520. doi:10.1109/ICRA46639.2022.9811650'
apa: 'Brunnbauer, A., Berducci, L., Brandstatter, A., Lechner, M., Hasani, R., Rus,
D., & Grosu, R. (2022). Latent imagination facilitates zero-shot transfer
in autonomous racing. In 2022 International Conference on Robotics and Automation
(pp. 7513–7520). Philadelphia, PA, United States: IEEE. https://doi.org/10.1109/ICRA46639.2022.9811650'
chicago: Brunnbauer, Axel, Luigi Berducci, Andreas Brandstatter, Mathias Lechner,
Ramin Hasani, Daniela Rus, and Radu Grosu. “Latent Imagination Facilitates Zero-Shot
Transfer in Autonomous Racing.” In 2022 International Conference on Robotics
and Automation, 7513–20. IEEE, 2022. https://doi.org/10.1109/ICRA46639.2022.9811650.
ieee: A. Brunnbauer et al., “Latent imagination facilitates zero-shot transfer
in autonomous racing,” in 2022 International Conference on Robotics and Automation,
Philadelphia, PA, United States, 2022, pp. 7513–7520.
ista: 'Brunnbauer A, Berducci L, Brandstatter A, Lechner M, Hasani R, Rus D, Grosu
R. 2022. Latent imagination facilitates zero-shot transfer in autonomous racing.
2022 International Conference on Robotics and Automation. ICRA: International
Conference on Robotics and Automation, 7513–7520.'
mla: Brunnbauer, Axel, et al. “Latent Imagination Facilitates Zero-Shot Transfer
in Autonomous Racing.” 2022 International Conference on Robotics and Automation,
IEEE, 2022, pp. 7513–20, doi:10.1109/ICRA46639.2022.9811650.
short: A. Brunnbauer, L. Berducci, A. Brandstatter, M. Lechner, R. Hasani, D. Rus,
R. Grosu, in:, 2022 International Conference on Robotics and Automation, IEEE,
2022, pp. 7513–7520.
conference:
end_date: 2022-05-27
location: Philadelphia, PA, United States
name: 'ICRA: International Conference on Robotics and Automation'
start_date: 2022-05-23
date_created: 2022-09-04T22:02:02Z
date_published: 2022-07-12T00:00:00Z
date_updated: 2022-09-05T08:46:12Z
day: '12'
department:
- _id: ToHe
doi: 10.1109/ICRA46639.2022.9811650
ec_funded: 1
external_id:
arxiv:
- '2103.04909'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2103.04909
month: '07'
oa: 1
oa_version: Preprint
page: 7513-7520
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 2022 International Conference on Robotics and Automation
publication_identifier:
isbn:
- '9781728196817'
issn:
- 1050-4729
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Latent imagination facilitates zero-shot transfer in autonomous racing
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2022'
...
---
_id: '12171'
abstract:
- lang: eng
text: 'We propose an algorithmic approach for synthesizing linear hybrid automata
from time-series data. Unlike existing approaches, our approach provides a whole
family of models with the same discrete structure but different dynamics. Each
model in the family is guaranteed to capture the input data up to a precision
error ε, in the following sense: For each time series, the model contains an execution
that is ε-close to the data points. Our construction allows to effectively choose
a model from this family with minimal precision error ε. We demonstrate the algorithm’s
efficiency and its ability to find precise models in two case studies.'
acknowledgement: This work was supported in part by the European Union’s Horizon 2020
research and innovation programme under the Marie Skłodowska-Curie grant agreement
no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark,
and by the Villum Investigator Grant S4OS.
alternative_title:
- LNCS
article_processing_charge: No
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 parametric hybrid automata
from time series. In: 20th International Symposium on Automated Technology
for Verification and Analysis. Vol 13505. Springer Nature; 2022:337-353. doi:10.1007/978-3-031-19992-9_22'
apa: 'Garcia Soto, M., Henzinger, T. A., & Schilling, C. (2022). Synthesis of parametric
hybrid automata from time series. In 20th International Symposium on Automated
Technology for Verification and Analysis (Vol. 13505, pp. 337–353). Virtual:
Springer Nature. https://doi.org/10.1007/978-3-031-19992-9_22'
chicago: Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis
of Parametric Hybrid Automata from Time Series.” In 20th International Symposium
on Automated Technology for Verification and Analysis, 13505:337–53. Springer
Nature, 2022. https://doi.org/10.1007/978-3-031-19992-9_22.
ieee: M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric
hybrid automata from time series,” in 20th International Symposium on Automated
Technology for Verification and Analysis, Virtual, 2022, vol. 13505, pp. 337–353.
ista: 'Garcia Soto M, Henzinger TA, Schilling C. 2022. Synthesis of parametric hybrid
automata from time series. 20th International Symposium on Automated Technology
for Verification and Analysis. ATVA: Automated Technology for Verification and
Analysis, LNCS, vol. 13505, 337–353.'
mla: Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time
Series.” 20th International Symposium on Automated Technology for Verification
and Analysis, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:10.1007/978-3-031-19992-9_22.
short: M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium
on Automated Technology for Verification and Analysis, Springer Nature, 2022,
pp. 337–353.
conference:
end_date: 2022-10-28
location: Virtual
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2022-10-25
date_created: 2023-01-12T12:11:16Z
date_published: 2022-10-21T00:00:00Z
date_updated: 2023-02-13T09:27:55Z
day: '21'
department:
- _id: ToHe
doi: 10.1007/978-3-031-19992-9_22
ec_funded: 1
external_id:
arxiv:
- '2208.06383'
intvolume: ' 13505'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2208.06383
month: '10'
oa: 1
oa_version: Preprint
page: 337-353
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 20th International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eisbn:
- '9783031199929'
eissn:
- 1611-3349
isbn:
- '9783031199912'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of parametric hybrid automata from time series
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13505
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
date_created: 2023-02-05T17:24:23Z
date_published: 2022-09-06T00:00:00Z
date_updated: 2023-02-06T09:23:31Z
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'
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: '12509'
abstract:
- lang: eng
text: A graph game is a two-player zero-sum game in which the players move a token
throughout a graph to produce an infinite path, which determines the winner or
payoff of the game. In bidding games, both players have budgets, and in each turn,
we hold an "auction" (bidding) to determine which player moves the token. In this
survey, we consider several bidding mechanisms and their effect on the properties
of the game. Specifically, bidding games, and in particular bidding games of infinite
duration, have an intriguing equivalence with random-turn games in which in each
turn, the player who moves is chosen randomly. We summarize how minor changes
in the bidding mechanism lead to unexpected differences in the equivalence with
random-turn games.
acknowledgement: "Guy Avni: Work partially supported by the Israel Science Foundation,
ISF grant agreement\r\nno 1679/21.\r\nThomas A. Henzinger: This work was supported
in part by the ERC-2020-AdG 101020093.\r\nWe would like to thank all our collaborators
Milad Aghajohari, Ventsislav Chonev, Rasmus Ibsen-Jensen, Ismäel Jecker, Petr Novotný,
Josef Tkadlec, and Ðorđe Žikelić; we hope the collaboration was as fun and meaningful
for you as it was for us."
article_processing_charge: No
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
citation:
ama: 'Avni G, Henzinger TA. An updated survey of bidding games on graphs. In: 47th
International Symposium on Mathematical Foundations of Computer Science. Vol
241. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022:3:1-3:6. doi:10.4230/LIPIcs.MFCS.2022.3'
apa: 'Avni, G., & Henzinger, T. A. (2022). An updated survey of bidding games
on graphs. In 47th International Symposium on Mathematical Foundations of Computer
Science (Vol. 241, p. 3:1-3:6). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2022.3'
chicago: 'Avni, Guy, and Thomas A Henzinger. “An Updated Survey of Bidding Games
on Graphs.” In 47th International Symposium on Mathematical Foundations of
Computer Science, 241:3:1-3:6. Leibniz International Proceedings in Informatics
(LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2022. https://doi.org/10.4230/LIPIcs.MFCS.2022.3.'
ieee: G. Avni and T. A. Henzinger, “An updated survey of bidding games on graphs,”
in 47th International Symposium on Mathematical Foundations of Computer Science,
Vienna, Austria, 2022, vol. 241, p. 3:1-3:6.
ista: 'Avni G, Henzinger TA. 2022. An updated survey of bidding games on graphs.
47th International Symposium on Mathematical Foundations of Computer Science.
MFCS: Symposium on Mathematical Foundations of Computer ScienceLeibniz International
Proceedings in Informatics (LIPIcs) vol. 241, 3:1-3:6.'
mla: Avni, Guy, and Thomas A. Henzinger. “An Updated Survey of Bidding Games on
Graphs.” 47th International Symposium on Mathematical Foundations of Computer
Science, vol. 241, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022,
p. 3:1-3:6, doi:10.4230/LIPIcs.MFCS.2022.3.
short: G. Avni, T.A. Henzinger, in:, 47th International Symposium on Mathematical
Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
Dagstuhl, Germany, 2022, p. 3:1-3:6.
conference:
end_date: 2022-08-26
location: Vienna, Austria
name: 'MFCS: Symposium on Mathematical Foundations of Computer Science'
start_date: 2022-08-22
date_created: 2023-02-05T17:26:01Z
date_published: 2022-08-22T00:00:00Z
date_updated: 2023-02-06T09:16:54Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2022.3
ec_funded: 1
file:
- access_level: open_access
checksum: 1888ec9421622f9526fbec2de035f132
content_type: application/pdf
creator: dernst
date_created: 2023-02-06T09:13:04Z
date_updated: 2023-02-06T09:13:04Z
file_id: '12519'
file_name: 2022_LIPICs_Avni.pdf
file_size: 624586
relation: main_file
success: 1
file_date_updated: 2023-02-06T09:13:04Z
has_accepted_license: '1'
intvolume: ' 241'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 3:1-3:6
place: Dagstuhl, Germany
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 47th International Symposium on Mathematical Foundations of Computer
Science
publication_identifier:
isbn:
- '9783959772563'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
series_title: Leibniz International Proceedings in Informatics (LIPIcs)
status: public
title: An updated survey of bidding games on graphs
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: 241
year: '2022'
...
---
_id: '11366'
abstract:
- lang: eng
text: "Adversarial training (i.e., training on adversarially perturbed input data)
is a well-studied method for making neural networks robust to potential adversarial
attacks during inference. However, the improved robustness does not\r\ncome for
free but rather is accompanied by a decrease in overall model accuracy and performance.
Recent work has shown that, in practical robot learning applications, the effects
of adversarial training do not pose a fair trade-off\r\nbut inflict a net loss
when measured in holistic robot performance. This work revisits the robustness-accuracy
trade-off in robot learning by systematically analyzing if recent advances in
robust training methods and theory in\r\nconjunction with adversarial robot learning
can make adversarial training suitable for real-world robot applications. We evaluate
a wide variety of robot learning tasks ranging from autonomous driving in a high-fidelity
environment\r\namenable to sim-to-real deployment, to mobile robot gesture recognition.
Our results demonstrate that, while these techniques make incremental improvements
on the trade-off on a relative scale, the negative side-effects caused by\r\nadversarial
training still outweigh the improvements by an order of magnitude. We conclude
that more substantial advances in robust learning methods are necessary before
they can benefit robot learning tasks in practice."
acknowledgement: "This work was supported in parts by the ERC-2020-AdG 101020093,
National Science Foundation (NSF), and JP\r\nMorgan Graduate Fellowships. We thank
Christoph Lampert for inspiring this work.\r\n"
article_number: '2204.07373'
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy
tradeoff in robot learning. arXiv. doi:10.48550/arXiv.2204.07373
apa: Lechner, M., Amini, A., Rus, D., & Henzinger, T. A. (n.d.). Revisiting
the adversarial robustness-accuracy tradeoff in robot learning. arXiv.
https://doi.org/10.48550/arXiv.2204.07373
chicago: Lechner, Mathias, Alexander Amini, Daniela Rus, and Thomas A Henzinger.
“Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning.” ArXiv,
n.d. https://doi.org/10.48550/arXiv.2204.07373.
ieee: M. Lechner, A. Amini, D. Rus, and T. A. Henzinger, “Revisiting the adversarial
robustness-accuracy tradeoff in robot learning,” arXiv. .
ista: Lechner M, Amini A, Rus D, Henzinger TA. Revisiting the adversarial robustness-accuracy
tradeoff in robot learning. arXiv, 2204.07373.
mla: Lechner, Mathias, et al. “Revisiting the Adversarial Robustness-Accuracy Tradeoff
in Robot Learning.” ArXiv, 2204.07373, doi:10.48550/arXiv.2204.07373.
short: M. Lechner, A. Amini, D. Rus, T.A. Henzinger, ArXiv (n.d.).
date_created: 2022-05-12T13:20:17Z
date_published: 2022-04-15T00:00:00Z
date_updated: 2023-08-01T13:36:50Z
day: '15'
department:
- _id: ToHe
doi: 10.48550/arXiv.2204.07373
ec_funded: 1
external_id:
arxiv:
- '2204.07373'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2204.07373
month: '04'
oa: 1
oa_version: Preprint
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: arXiv
publication_status: submitted
related_material:
record:
- id: '11362'
relation: dissertation_contains
status: public
- id: '12704'
relation: later_version
status: public
status: public
title: Revisiting the adversarial robustness-accuracy tradeoff in robot learning
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2022'
...
---
_id: '10891'
abstract:
- lang: eng
text: We present a formal framework for the online black-box monitoring of software
using monitors with quantitative verdict functions. Quantitative verdict functions
have several advantages. First, quantitative monitors can be approximate, i.e.,
the value of the verdict function does not need to correspond exactly to the value
of the property under observation. Second, quantitative monitors can be quantified
universally, i.e., for every possible observed behavior, the monitor tries to
make the best effort to estimate the value of the property under observation.
Third, quantitative monitors can watch boolean as well as quantitative properties,
such as average response time. Fourth, quantitative monitors can use non-finite-state
resources, such as counters. As a consequence, quantitative monitors can be compared
according to how many resources they use (e.g., the number of counters) and how
precisely they approximate the property under observation. This allows for a rich
spectrum of cost-precision trade-offs in monitoring software.
acknowledgement: The formal framework for quantitative monitoring which is presented
in this invited talk was defined jointly with N. Ege Saraç at LICS 2021. This work
was supported in part by the Wittgenstein Award Z211-N23 of the Austrian Science
Fund.
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Henzinger TA. Quantitative monitoring of software. In: Software Verification.
Vol 13124. LNCS. Springer Nature; 2022:3-6. doi:10.1007/978-3-030-95561-8_1'
apa: 'Henzinger, T. A. (2022). Quantitative monitoring of software. In Software
Verification (Vol. 13124, pp. 3–6). New Haven, CT, United States: Springer
Nature. https://doi.org/10.1007/978-3-030-95561-8_1'
chicago: Henzinger, Thomas A. “Quantitative Monitoring of Software.” In Software
Verification, 13124:3–6. LNCS. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-95561-8_1.
ieee: T. A. Henzinger, “Quantitative monitoring of software,” in Software Verification,
New Haven, CT, United States, 2022, vol. 13124, pp. 3–6.
ista: 'Henzinger TA. 2022. Quantitative monitoring of software. Software Verification.
NSV: Numerical Software VerificationLNCS vol. 13124, 3–6.'
mla: Henzinger, Thomas A. “Quantitative Monitoring of Software.” Software Verification,
vol. 13124, Springer Nature, 2022, pp. 3–6, doi:10.1007/978-3-030-95561-8_1.
short: T.A. Henzinger, in:, Software Verification, Springer Nature, 2022, pp. 3–6.
conference:
end_date: 2021-10-19
location: New Haven, CT, United States
name: 'NSV: Numerical Software Verification'
start_date: 2021-10-18
date_created: 2022-03-20T23:01:40Z
date_published: 2022-02-22T00:00:00Z
date_updated: 2023-08-03T06:11:55Z
day: '22'
department:
- _id: ToHe
doi: 10.1007/978-3-030-95561-8_1
external_id:
isi:
- '000771713200001'
intvolume: ' 13124'
isi: 1
language:
- iso: eng
month: '02'
oa_version: None
page: 3-6
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Software Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030955601'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Quantitative monitoring of software
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13124
year: '2022'
...
---
_id: '11355'
abstract:
- lang: eng
text: "Contract-based design is a promising methodology for taming the complexity
of developing sophisticated systems. A formal contract distinguishes between assumptions,
which are constraints that the designer of a component puts on the environments
in which the component can be used safely, and guarantees, which are promises
that the designer asks from the team that implements the component. A theory of
formal contracts can be formalized as an interface theory, which supports the
composition and refinement of both assumptions and guarantees.\r\nAlthough there
is a rich landscape of contract-based design methods that address functional and
extra-functional properties, we present the first interface theory that is designed
for ensuring system-wide security properties. Our framework provides a refinement
relation and a composition operation that support both incremental design and
independent implementability. We develop our theory for both stateless and stateful
interfaces. We illustrate the applicability of our framework with an example inspired
from the automotive domain."
acknowledgement: This project has received funding from the European Union’s Horizon
2020 research and innovation programme under grant agreement No 956123 and was funded
in part by the FWF project W1255-N23 and by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana Oliveira
full_name: Da Costa, Ana Oliveira
last_name: Da Costa
citation:
ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow
interfaces. In: Fundamental Approaches to Software Engineering. Vol 13241.
Springer Nature; 2022:3-22. doi:10.1007/978-3-030-99429-7_1'
apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Da Costa,
A. O. (2022). Information-flow interfaces. In Fundamental Approaches to Software
Engineering (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. https://doi.org/10.1007/978-3-030-99429-7_1'
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira Da Costa. “Information-Flow Interfaces.” In Fundamental Approaches
to Software Engineering, 13241:3–22. Springer Nature, 2022. https://doi.org/10.1007/978-3-030-99429-7_1.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
“Information-flow interfaces,” in Fundamental Approaches to Software Engineering,
Munich, Germany, 2022, vol. 13241, pp. 3–22.
ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Information-flow
interfaces. Fundamental Approaches to Software Engineering. FASE: Fundamental
Approaches to Software Engineering, LNCS, vol. 13241, 3–22.'
mla: Bartocci, Ezio, et al. “Information-Flow Interfaces.” Fundamental Approaches
to Software Engineering, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:10.1007/978-3-030-99429-7_1.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
Fundamental Approaches to Software Engineering, Springer Nature, 2022, pp. 3–22.
conference:
end_date: 2022-04-07
location: Munich, Germany
name: 'FASE: Fundamental Approaches to Software Engineering'
start_date: 2022-04-02
date_created: 2022-05-08T22:01:44Z
date_published: 2022-03-29T00:00:00Z
date_updated: 2023-08-03T07:03:40Z
day: '29'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-99429-7_1
ec_funded: 1
external_id:
isi:
- '000782393600001'
file:
- access_level: open_access
checksum: 7f6f860b20b8de2a249e9c1b4eee15cf
content_type: application/pdf
creator: dernst
date_created: 2022-05-09T06:52:44Z
date_updated: 2022-05-09T06:52:44Z
file_id: '11357'
file_name: 2022_LNCS_Bartocci.pdf
file_size: 479146
relation: main_file
success: 1
file_date_updated: 2022-05-09T06:52:44Z
has_accepted_license: '1'
intvolume: ' 13241'
isi: 1
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: 3-22
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Fundamental Approaches to Software Engineering
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030994280'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Information-flow interfaces
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13241
year: '2022'
...
---
_id: '11775'
abstract:
- lang: eng
text: 'Quantitative monitoring can be universal and approximate: For every finite
sequence of observations, the specification provides a value and the monitor outputs
a best-effort approximation of it. The quality of the approximation may depend
on the resources that are available to the monitor. By taking to the limit the
sequences of specification values and monitor outputs, we obtain precision-resource
trade-offs also for limit monitoring. This paper provides a formal framework for
studying such trade-offs using an abstract interpretation for monitors: For each
natural number n, the aggregate semantics of a monitor at time n is an equivalence
relation over all sequences of at most n observations so that two equivalent sequences
are indistinguishable to the monitor and thus mapped to the same output. This
abstract interpretation of quantitative monitors allows us to measure the number
of equivalence classes (or “resource use”) that is necessary for a certain precision
up to a certain time, or at any time. Our framework offers several insights. For
example, we identify a family of specifications for which any resource-optimal
exact limit monitor is independent of any error permitted over finite traces.
Moreover, we present a specification for which any resource-optimal approximate
limit monitor does not minimize its resource use at any time. '
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: Yes
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Abstract monitors for quantitative specifications.
In: 22nd International Conference on Runtime Verification. Vol 13498. Springer
Nature; 2022:200-220. doi:10.1007/978-3-031-17196-3_11'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2022). Abstract monitors
for quantitative specifications. In 22nd International Conference on Runtime
Verification (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature.
https://doi.org/10.1007/978-3-031-17196-3_11'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract
Monitors for Quantitative Specifications.” In 22nd International Conference
on Runtime Verification, 13498:200–220. Springer Nature, 2022. https://doi.org/10.1007/978-3-031-17196-3_11.
ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for
quantitative specifications,” in 22nd International Conference on Runtime Verification,
Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2022. Abstract monitors for quantitative
specifications. 22nd International Conference on Runtime Verification. RV: Runtime
Verification, LNCS, vol. 13498, 200–220.'
mla: Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.”
22nd International Conference on Runtime Verification, vol. 13498, Springer
Nature, 2022, pp. 200–20, doi:10.1007/978-3-031-17196-3_11.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference
on Runtime Verification, Springer Nature, 2022, pp. 200–220.
conference:
end_date: 2022-09-30
location: Tbilisi, Georgia
name: 'RV: Runtime Verification'
start_date: 2022-09-28
date_created: 2022-08-08T17:09:09Z
date_published: 2022-09-23T00:00:00Z
date_updated: 2023-08-03T13:38:46Z
day: '23'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-17196-3_11
ec_funded: 1
external_id:
isi:
- '000866539700011'
file:
- access_level: open_access
checksum: 05c7dcfbb9053a98f46441fb2eccb213
content_type: application/pdf
creator: dernst
date_created: 2023-01-20T07:34:50Z
date_updated: 2023-01-20T07:34:50Z
file_id: '12317'
file_name: 2022_LNCS_RV_Henzinger.pdf
file_size: 477110
relation: main_file
success: 1
file_date_updated: 2023-01-20T07:34:50Z
has_accepted_license: '1'
intvolume: ' 13498'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 200-220
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 22nd International Conference on Runtime Verification
publication_identifier:
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstract monitors for quantitative specifications
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13498
year: '2022'
...
---
_id: '12147'
abstract:
- lang: eng
text: Continuous-time neural networks are a class of machine learning systems that
can tackle representation learning on spatiotemporal decision-making tasks. These
models are typically represented by continuous differential equations. However,
their expressive power when they are deployed on computers is bottlenecked by
numerical differential equation solvers. This limitation has notably slowed down
the scaling and understanding of numerous natural physical phenomena such as the
dynamics of nervous systems. Ideally, we would circumvent this bottleneck by solving
the given dynamical system in closed form. This is known to be intractable in
general. Here, we show that it is possible to closely approximate the interaction
between neurons and synapses—the building blocks of natural and artificial neural
networks—constructed by liquid time-constant networks efficiently in closed form.
To this end, we compute a tightly bounded approximation of the solution of an
integral appearing in liquid time-constant dynamics that has had no known closed-form
solution so far. This closed-form solution impacts the design of continuous-time
and continuous-depth neural models. For instance, since time appears explicitly
in closed form, the formulation relaxes the need for complex numerical solvers.
Consequently, we obtain models that are between one and five orders of magnitude
faster in training and inference compared with differential equation-based counterparts.
More importantly, in contrast to ordinary differential equation-based continuous
networks, closed-form networks can scale remarkably well compared with other deep
learning instances. Lastly, as these models are derived from liquid networks,
they show good performance in time-series modelling compared with advanced recurrent
neural network models.
acknowledgement: This research was supported in part by the AI2050 program at Schmidt
Futures (grant G-22-63172), the Boeing Company, and the United States Air Force
Research Laboratory and the United States Air Force Artificial Intelligence Accelerator
and was accomplished under cooperative agreement number FA8750-19-2-1000. The views
and conclusions contained in this document are those of the authors and should not
be interpreted as representing the official policies, either expressed or implied,
of the United States Air Force or the U.S. Government. The U.S. Government is authorized
to reproduce and distribute reprints for Government purposes, notwithstanding any
copyright notation herein. This work was further supported by The Boeing Company
and Office of Naval Research grant N00014-18-1-2830. M.T. is supported by the Poul
Due Jensen Foundation, grant 883901. M.L. was supported in part by the Austrian
Science Fund under grant Z211-N23 (Wittgenstein Award). A.A. was supported by the
National Science Foundation Graduate Research Fellowship Program. We thank T.-H.
Wang, P. Kao, M. Chahine, W. Xiao, X. Li, L. Yin and Y. Ben for useful suggestions
and for testing of CfC models to confirm the results across other domains.
article_processing_charge: No
article_type: original
author:
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Lucas
full_name: Liebenwein, Lucas
last_name: Liebenwein
- first_name: Aaron
full_name: Ray, Aaron
last_name: Ray
- first_name: Max
full_name: Tschaikowski, Max
last_name: Tschaikowski
- first_name: Gerald
full_name: Teschl, Gerald
last_name: Teschl
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: Hasani R, Lechner M, Amini A, et al. Closed-form continuous-time neural networks.
Nature Machine Intelligence. 2022;4(11):992-1003. doi:10.1038/s42256-022-00556-7
apa: Hasani, R., Lechner, M., Amini, A., Liebenwein, L., Ray, A., Tschaikowski,
M., … Rus, D. (2022). Closed-form continuous-time neural networks. Nature Machine
Intelligence. Springer Nature. https://doi.org/10.1038/s42256-022-00556-7
chicago: Hasani, Ramin, Mathias Lechner, Alexander Amini, Lucas Liebenwein, Aaron
Ray, Max Tschaikowski, Gerald Teschl, and Daniela Rus. “Closed-Form Continuous-Time
Neural Networks.” Nature Machine Intelligence. Springer Nature, 2022. https://doi.org/10.1038/s42256-022-00556-7.
ieee: R. Hasani et al., “Closed-form continuous-time neural networks,” Nature
Machine Intelligence, vol. 4, no. 11. Springer Nature, pp. 992–1003, 2022.
ista: Hasani R, Lechner M, Amini A, Liebenwein L, Ray A, Tschaikowski M, Teschl
G, Rus D. 2022. Closed-form continuous-time neural networks. Nature Machine Intelligence.
4(11), 992–1003.
mla: Hasani, Ramin, et al. “Closed-Form Continuous-Time Neural Networks.” Nature
Machine Intelligence, vol. 4, no. 11, Springer Nature, 2022, pp. 992–1003,
doi:10.1038/s42256-022-00556-7.
short: R. Hasani, M. Lechner, A. Amini, L. Liebenwein, A. Ray, M. Tschaikowski,
G. Teschl, D. Rus, Nature Machine Intelligence 4 (2022) 992–1003.
date_created: 2023-01-12T12:07:21Z
date_published: 2022-11-15T00:00:00Z
date_updated: 2023-08-04T09:00:10Z
day: '15'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1038/s42256-022-00556-7
external_id:
arxiv:
- '2106.13898'
isi:
- '000884215600003'
file:
- access_level: open_access
checksum: b4789122ce04bfb4ac042390f59aaa8b
content_type: application/pdf
creator: dernst
date_created: 2023-01-24T09:49:44Z
date_updated: 2023-01-24T09:49:44Z
file_id: '12355'
file_name: 2022_NatureMachineIntelligence_Hasani.pdf
file_size: 3259553
relation: main_file
success: 1
file_date_updated: 2023-01-24T09:49:44Z
has_accepted_license: '1'
intvolume: ' 4'
isi: 1
issue: '11'
keyword:
- Artificial Intelligence
- Computer Networks and Communications
- Computer Vision and Pattern Recognition
- Human-Computer Interaction
- Software
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: 992-1003
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Nature Machine Intelligence
publication_identifier:
issn:
- 2522-5839
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
link:
- relation: erratum
url: https://doi.org/10.1038/s42256-022-00597-y
scopus_import: '1'
status: public
title: Closed-form continuous-time neural networks
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 4
year: '2022'
...
---
_id: '11362'
abstract:
- lang: eng
text: "Deep learning has enabled breakthroughs in challenging computing problems
and has emerged as the standard problem-solving tool for computer vision and natural
language processing tasks.\r\nOne exception to this trend is safety-critical tasks
where robustness and resilience requirements contradict the black-box nature of
neural networks. \r\nTo deploy deep learning methods for these tasks, it is vital
to provide guarantees on neural network agents' safety and robustness criteria.
\r\nThis can be achieved by developing formal verification methods to verify the
safety and robustness properties of neural networks.\r\n\r\nOur goal is to design,
develop and assess safety verification methods for neural networks to improve
their reliability and trustworthiness in real-world applications.\r\nThis thesis
establishes techniques for the verification of compressed and adversarially trained
models as well as the design of novel neural networks for verifiably safe decision-making.\r\n\r\nFirst,
we establish the problem of verifying quantized neural networks. Quantization
is a technique that trades numerical precision for the computational efficiency
of running a neural network and is widely adopted in industry.\r\nWe show that
neglecting the reduced precision when verifying a neural network can lead to wrong
conclusions about the robustness and safety of the network, highlighting that
novel techniques for quantized network verification are necessary. We introduce
several bit-exact verification methods explicitly designed for quantized neural
networks and experimentally confirm on realistic networks that the network's robustness
and other formal properties are affected by the quantization.\r\n\r\nFurthermore,
we perform a case study providing evidence that adversarial training, a standard
technique for making neural networks more robust, has detrimental effects on the
network's performance. This robustness-accuracy tradeoff has been studied before
regarding the accuracy obtained on classification datasets where each data point
is independent of all other data points. On the other hand, we investigate the
tradeoff empirically in robot learning settings where a both, a high accuracy
and a high robustness, are desirable.\r\nOur results suggest that the negative
side-effects of adversarial training outweigh its robustness benefits in practice.\r\n\r\nFinally,
we consider the problem of verifying safety when running a Bayesian neural network
policy in a feedback loop with systems over the infinite time horizon. Bayesian
neural networks are probabilistic models for learning uncertainties in the data
and are therefore often used on robotic and healthcare applications where data
is inherently stochastic.\r\nWe introduce a method for recalibrating Bayesian
neural networks so that they yield probability distributions over safe decisions
only.\r\nOur method learns a safety certificate that guarantees safety over the
infinite time horizon to determine which decisions are safe in every possible
state of the system.\r\nWe demonstrate the effectiveness of our approach on a
series of reinforcement learning benchmarks."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
citation:
ama: Lechner M. Learning verifiable representations. 2022. doi:10.15479/at:ista:11362
apa: Lechner, M. (2022). Learning verifiable representations. Institute of
Science and Technology Austria. https://doi.org/10.15479/at:ista:11362
chicago: Lechner, Mathias. “Learning Verifiable Representations.” Institute of Science
and Technology Austria, 2022. https://doi.org/10.15479/at:ista:11362.
ieee: M. Lechner, “Learning verifiable representations,” Institute of Science and
Technology Austria, 2022.
ista: Lechner M. 2022. Learning verifiable representations. Institute of Science
and Technology Austria.
mla: Lechner, Mathias. Learning Verifiable Representations. Institute of
Science and Technology Austria, 2022, doi:10.15479/at:ista:11362.
short: M. Lechner, Learning Verifiable Representations, Institute of Science and
Technology Austria, 2022.
date_created: 2022-05-12T07:14:01Z
date_published: 2022-05-12T00:00:00Z
date_updated: 2023-08-17T06:58:38Z
day: '12'
ddc:
- '004'
degree_awarded: PhD
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/at:ista:11362
ec_funded: 1
file:
- access_level: closed
checksum: 8eefa9c7c10ca7e1a2ccdd731962a645
content_type: application/zip
creator: mlechner
date_created: 2022-05-13T12:33:26Z
date_updated: 2022-05-13T12:49:00Z
file_id: '11378'
file_name: src.zip
file_size: 13210143
relation: source_file
- access_level: open_access
checksum: 1b9e1e5a9a83ed9d89dad2f5133dc026
content_type: application/pdf
creator: mlechner
date_created: 2022-05-16T08:02:28Z
date_updated: 2022-05-17T15:19:39Z
file_id: '11382'
file_name: thesis_main-a2.pdf
file_size: 2732536
relation: main_file
file_date_updated: 2022-05-17T15:19:39Z
has_accepted_license: '1'
keyword:
- neural networks
- verification
- machine learning
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: '124'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
isbn:
- 978-3-99078-017-6
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '10665'
relation: part_of_dissertation
status: public
- id: '10667'
relation: part_of_dissertation
status: public
- id: '11366'
relation: part_of_dissertation
status: public
- id: '7808'
relation: part_of_dissertation
status: public
- id: '10666'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Learning verifiable representations
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '12302'
abstract:
- lang: eng
text: 'We propose a novel algorithm to decide the language inclusion between (nondeterministic)
Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage
a notion of quasiorder to prune the search for a counterexample by discarding
candidates which are subsumed by others for the quasiorder. Discarded candidates
are guaranteed to not compromise the completeness of the algorithm. The novelty
of our work lies in the quasiorder used to discard candidates. We introduce FORQs
(family of right quasiorders) that we obtain by adapting the notion of family
of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based
inclusion algorithm which we prove correct and instantiate it for a specific FORQ,
called the structural FORQ, induced by the Büchi automaton to the right of the
inclusion sign. The resulting implementation, called FORKLIFT, scales up better
than the state-of-the-art on a variety of benchmarks including benchmarks from
program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870'
acknowledgement: This work was partially funded by the ESF Investing in your future,
the Madrid regional project S2018/TCS-4339 BLOQUES, the Spanish project PGC2018-102210-B-I00
BOSCO, the Ramón y Cajal fellowship RYC-2016-20281, and the ERC grant PR1001ERC02.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Kyveli
full_name: Doveri, Kyveli
last_name: Doveri
- first_name: Pierre
full_name: Ganty, Pierre
last_name: Ganty
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
citation:
ama: 'Doveri K, Ganty P, Mazzocchi NA. FORQ-based language inclusion formal testing.
In: Computer Aided Verification. Vol 13372. Springer Nature; 2022:109-129.
doi:10.1007/978-3-031-13188-2_6'
apa: 'Doveri, K., Ganty, P., & Mazzocchi, N. A. (2022). FORQ-based language
inclusion formal testing. In Computer Aided Verification (Vol. 13372, pp.
109–129). Haifa, Israel: Springer Nature. https://doi.org/10.1007/978-3-031-13188-2_6'
chicago: Doveri, Kyveli, Pierre Ganty, and Nicolas Adrien Mazzocchi. “FORQ-Based
Language Inclusion Formal Testing.” In Computer Aided Verification, 13372:109–29.
Springer Nature, 2022. https://doi.org/10.1007/978-3-031-13188-2_6.
ieee: K. Doveri, P. Ganty, and N. A. Mazzocchi, “FORQ-based language inclusion formal
testing,” in Computer Aided Verification, Haifa, Israel, 2022, vol. 13372,
pp. 109–129.
ista: 'Doveri K, Ganty P, Mazzocchi NA. 2022. FORQ-based language inclusion formal
testing. Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 13372, 109–129.'
mla: Doveri, Kyveli, et al. “FORQ-Based Language Inclusion Formal Testing.” Computer
Aided Verification, vol. 13372, Springer Nature, 2022, pp. 109–29, doi:10.1007/978-3-031-13188-2_6.
short: K. Doveri, P. Ganty, N.A. Mazzocchi, in:, Computer Aided Verification, Springer
Nature, 2022, pp. 109–129.
conference:
end_date: 2022-08-10
location: Haifa, Israel
name: 'CAV: Computer Aided Verification'
start_date: 2022-08-07
date_created: 2023-01-16T10:06:31Z
date_published: 2022-08-06T00:00:00Z
date_updated: 2023-09-05T15:13:36Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-13188-2_6
ec_funded: 1
external_id:
arxiv:
- '2207.13549'
isi:
- '000870310500006'
file:
- access_level: open_access
checksum: edc363b1be5447a09063e115c247918a
content_type: application/pdf
creator: dernst
date_created: 2023-01-30T12:51:02Z
date_updated: 2023-01-30T12:51:02Z
file_id: '12465'
file_name: 2022_LNCS_Doveri.pdf
file_size: 497682
relation: main_file
success: 1
file_date_updated: 2023-01-30T12:51:02Z
has_accepted_license: '1'
intvolume: ' 13372'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 109-129
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Computer Aided Verification
publication_identifier:
eisbn:
- '9783031131882'
eissn:
- 1611-3349
isbn:
- '9783031131875'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: FORQ-based language inclusion formal testing
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13372
year: '2022'
...
---
_id: '12175'
abstract:
- lang: eng
text: An automaton is history-deterministic (HD) if one can safely resolve its non-deterministic
choices on the fly. In a recent paper, Henzinger, Lehtinen and Totzke studied
this in the context of Timed Automata [9], where it was conjectured that the class
of timed ω-languages recognised by HD-timed automata strictly extends that of
deterministic ones. We provide a proof for this fact.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, the
EPSRC project EP/V025848/1, and the EPSRC project EP/X017796/1.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sougata
full_name: Bose, Sougata
last_name: Bose
- 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: Sven
full_name: Schewe, Sven
last_name: Schewe
- first_name: Patrick
full_name: Totzke, Patrick
last_name: Totzke
citation:
ama: 'Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic
timed automata are not determinizable. In: 16th International Conference on
Reachability Problems. Vol 13608. Springer Nature; 2022:67-76. doi:10.1007/978-3-031-19135-0_5'
apa: 'Bose, S., Henzinger, T. A., Lehtinen, K., Schewe, S., & Totzke, P. (2022).
History-deterministic timed automata are not determinizable. In 16th International
Conference on Reachability Problems (Vol. 13608, pp. 67–76). Kaiserslautern,
Germany: Springer Nature. https://doi.org/10.1007/978-3-031-19135-0_5'
chicago: Bose, Sougata, Thomas A Henzinger, Karoliina Lehtinen, Sven Schewe, and
Patrick Totzke. “History-Deterministic Timed Automata Are Not Determinizable.”
In 16th International Conference on Reachability Problems, 13608:67–76.
Springer Nature, 2022. https://doi.org/10.1007/978-3-031-19135-0_5.
ieee: S. Bose, T. A. Henzinger, K. Lehtinen, S. Schewe, and P. Totzke, “History-deterministic
timed automata are not determinizable,” in 16th International Conference on
Reachability Problems, Kaiserslautern, Germany, 2022, vol. 13608, pp. 67–76.
ista: 'Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. 2022. History-deterministic
timed automata are not determinizable. 16th International Conference on Reachability
Problems. RC: Reachability Problems, LNCS, vol. 13608, 67–76.'
mla: Bose, Sougata, et al. “History-Deterministic Timed Automata Are Not Determinizable.”
16th International Conference on Reachability Problems, vol. 13608, Springer
Nature, 2022, pp. 67–76, doi:10.1007/978-3-031-19135-0_5.
short: S. Bose, T.A. Henzinger, K. Lehtinen, S. Schewe, P. Totzke, in:, 16th International
Conference on Reachability Problems, Springer Nature, 2022, pp. 67–76.
conference:
end_date: 2022-10-21
location: Kaiserslautern, Germany
name: 'RC: Reachability Problems'
start_date: 2022-10-17
date_created: 2023-01-12T12:11:57Z
date_published: 2022-10-12T00:00:00Z
date_updated: 2023-09-05T15:12:08Z
day: '12'
department:
- _id: ToHe
doi: 10.1007/978-3-031-19135-0_5
ec_funded: 1
intvolume: ' 13608'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://hal.science/hal-03849398/
month: '10'
oa: 1
oa_version: Preprint
page: 67-76
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 16th International Conference on Reachability Problems
publication_identifier:
eisbn:
- '9783031191350'
eissn:
- 1611-3349
isbn:
- '9783031191343'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: History-deterministic timed automata are not determinizable
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13608
year: '2022'
...
---
_id: '12510'
abstract:
- lang: eng
text: "We introduce a new statistical verification algorithm that formally quantifies
the behavioral robustness of any time-continuous process formulated as a continuous-depth
model. Our algorithm solves a set of global optimization (Go) problems over a
given time horizon to construct a tight enclosure (Tube) of the set of all process
executions starting from a ball of initial states. We call our algorithm GoTube.
Through its construction, GoTube ensures that the bounding tube is conservative
up to a desired probability and up to a desired tightness.\r\n GoTube is implemented
in JAX and optimized to scale to complex continuous-depth neural network models.
Compared to advanced reachability analysis tools for time-continuous neural networks,
GoTube does not accumulate overapproximation errors between time steps and avoids
the infamous wrapping effect inherent in symbolic techniques. We show that GoTube
substantially outperforms state-of-the-art verification tools in terms of the
size of the initial ball, speed, time-horizon, task completion, and scalability
on a large set of experiments.\r\n GoTube is stable and sets the state-of-the-art
in terms of its ability to scale to time horizons well beyond what has been previously
possible."
acknowledgement: SG is funded by the Austrian Science Fund (FWF) project number W1255-N23.
ML and TH are supported in part by FWF under grant Z211-N23 (Wittgenstein Award)
and the ERC-2020-AdG 101020093. SS is supported by NSF awards DCL-2040599, CCF-1918225,
and CPS-1446832. RH and DR are partially supported by Boeing. RG is partially supported
by Horizon-2020 ECSEL Project grant No. 783163 (iDev40).
article_processing_charge: No
article_type: original
author:
- first_name: Sophie A.
full_name: Gruenbacher, Sophie A.
last_name: Gruenbacher
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Scott A.
full_name: Smolka, Scott A.
last_name: Smolka
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Gruenbacher SA, Lechner M, Hasani R, et al. GoTube: Scalable statistical verification
of continuous-depth models. Proceedings of the AAAI Conference on Artificial
Intelligence. 2022;36(6):6755-6764. doi:10.1609/aaai.v36i6.20631'
apa: 'Gruenbacher, S. A., Lechner, M., Hasani, R., Rus, D., Henzinger, T. A., Smolka,
S. A., & Grosu, R. (2022). GoTube: Scalable statistical verification of continuous-depth
models. Proceedings of the AAAI Conference on Artificial Intelligence.
Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v36i6.20631'
chicago: 'Gruenbacher, Sophie A., Mathias Lechner, Ramin Hasani, Daniela Rus, Thomas
A Henzinger, Scott A. Smolka, and Radu Grosu. “GoTube: Scalable Statistical Verification
of Continuous-Depth Models.” Proceedings of the AAAI Conference on Artificial
Intelligence. Association for the Advancement of Artificial Intelligence,
2022. https://doi.org/10.1609/aaai.v36i6.20631.'
ieee: 'S. A. Gruenbacher et al., “GoTube: Scalable statistical verification
of continuous-depth models,” Proceedings of the AAAI Conference on Artificial
Intelligence, vol. 36, no. 6. Association for the Advancement of Artificial
Intelligence, pp. 6755–6764, 2022.'
ista: 'Gruenbacher SA, Lechner M, Hasani R, Rus D, Henzinger TA, Smolka SA, Grosu
R. 2022. GoTube: Scalable statistical verification of continuous-depth models.
Proceedings of the AAAI Conference on Artificial Intelligence. 36(6), 6755–6764.'
mla: 'Gruenbacher, Sophie A., et al. “GoTube: Scalable Statistical Verification
of Continuous-Depth Models.” Proceedings of the AAAI Conference on Artificial
Intelligence, vol. 36, no. 6, Association for the Advancement of Artificial
Intelligence, 2022, pp. 6755–64, doi:10.1609/aaai.v36i6.20631.'
short: S.A. Gruenbacher, M. Lechner, R. Hasani, D. Rus, T.A. Henzinger, S.A. Smolka,
R. Grosu, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022)
6755–6764.
date_created: 2023-02-05T17:27:42Z
date_published: 2022-06-28T00:00:00Z
date_updated: 2023-09-26T10:46:59Z
day: '28'
department:
- _id: ToHe
doi: 10.1609/aaai.v36i6.20631
ec_funded: 1
external_id:
arxiv:
- '2107.08467'
intvolume: ' 36'
issue: '6'
keyword:
- General Medicine
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2107.08467
month: '06'
oa: 1
oa_version: Preprint
page: 6755-6764
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- '978577358350'
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'GoTube: Scalable statistical verification of continuous-depth models'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 36
year: '2022'
...
---
_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
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.
date_created: 2023-02-05T17:29:50Z
date_published: 2022-06-28T00:00:00Z
date_updated: 2023-11-30T10:55:37Z
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'
...
---
_id: '14601'
abstract:
- lang: eng
text: "In this work, we address the problem of learning provably stable neural\r\nnetwork
policies for stochastic control systems. While recent work has\r\ndemonstrated
the feasibility of certifying given policies using martingale\r\ntheory, the problem
of how to learn such policies is little explored. Here, we\r\nstudy the effectiveness
of jointly learning a policy together with a martingale\r\ncertificate that proves
its stability using a single learning algorithm. We\r\nobserve that the joint
optimization problem becomes easily stuck in local\r\nminima when starting from
a randomly initialized policy. Our results suggest\r\nthat some form of pre-training
of the policy is required for the joint\r\noptimization to repair and verify the
policy successfully."
article_processing_charge: No
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies
in stochastic control systems. arXiv. doi:10.48550/arXiv.2205.11991
apa: Zikelic, D., Lechner, M., Chatterjee, K., & Henzinger, T. A. (n.d.). Learning
stabilizing policies in stochastic control systems. arXiv. https://doi.org/10.48550/arXiv.2205.11991
chicago: Zikelic, Dorde, Mathias Lechner, Krishnendu Chatterjee, and Thomas A Henzinger.
“Learning Stabilizing Policies in Stochastic Control Systems.” ArXiv, n.d.
https://doi.org/10.48550/arXiv.2205.11991.
ieee: D. Zikelic, M. Lechner, K. Chatterjee, and T. A. Henzinger, “Learning stabilizing
policies in stochastic control systems,” arXiv. .
ista: Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies
in stochastic control systems. arXiv, 10.48550/arXiv.2205.11991.
mla: Zikelic, Dorde, et al. “Learning Stabilizing Policies in Stochastic Control
Systems.” ArXiv, doi:10.48550/arXiv.2205.11991.
short: D. Zikelic, M. Lechner, K. Chatterjee, T.A. Henzinger, ArXiv (n.d.).
date_created: 2023-11-24T13:22:30Z
date_published: 2022-05-24T00:00:00Z
date_updated: 2023-11-30T10:55:37Z
day: '24'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/arXiv.2205.11991
ec_funded: 1
external_id:
arxiv:
- '2205.11991'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2205.11991
month: '05'
oa: 1
oa_version: Preprint
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: arXiv
publication_status: submitted
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
status: public
title: Learning stabilizing policies in stochastic control systems
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '14600'
abstract:
- lang: eng
text: We study the problem of learning controllers for discrete-time non-linear
stochastic dynamical systems with formal reach-avoid guarantees. This work presents
the first method for providing formal reach-avoid guarantees, which combine and
generalize stability and safety guarantees, with a tolerable probability threshold
$p\in[0,1]$ over the infinite time horizon. Our method leverages advances in machine
learning literature and it represents formal certificates as neural networks.
In particular, we learn a certificate in the form of a reach-avoid supermartingale
(RASM), a novel notion that we introduce in this work. Our RASMs provide reachability
and avoidance guarantees by imposing constraints on what can be viewed as a stochastic
extension of level sets of Lyapunov functions for deterministic systems. Our approach
solves several important problems -- it can be used to learn a control policy
from scratch, to verify a reach-avoid specification for a fixed control policy,
or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification.
We validate our approach on $3$ stochastic non-linear reinforcement learning tasks.
article_processing_charge: No
author:
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. arXiv. doi:10.48550/ARXIV.2210.05308
apa: Zikelic, D., Lechner, M., Henzinger, T. A., & Chatterjee, K. (n.d.). Learning
control policies for stochastic systems with reach-avoid guarantees. arXiv.
https://doi.org/10.48550/ARXIV.2210.05308
chicago: Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee.
“Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.”
ArXiv, n.d. https://doi.org/10.48550/ARXIV.2210.05308.
ieee: D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control
policies for stochastic systems with reach-avoid guarantees,” arXiv. .
ista: Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies
for stochastic systems with reach-avoid guarantees. arXiv, 10.48550/ARXIV.2210.05308.
mla: Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with
Reach-Avoid Guarantees.” ArXiv, doi:10.48550/ARXIV.2210.05308.
short: D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, ArXiv (n.d.).
date_created: 2023-11-24T13:10:09Z
date_published: 2022-11-29T00:00:00Z
date_updated: 2024-01-22T14:08:29Z
day: '29'
department:
- _id: KrCh
- _id: ToHe
doi: 10.48550/ARXIV.2210.05308
ec_funded: 1
external_id:
arxiv:
- '2210.05308'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-sa/4.0/
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2210.05308
month: '11'
oa: 1
oa_version: Preprint
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
publication: arXiv
publication_status: submitted
related_material:
record:
- id: '14539'
relation: dissertation_contains
status: public
- id: '14830'
relation: later_version
status: public
status: public
title: Learning control policies for stochastic systems with reach-avoid guarantees
tmp:
image: /images/cc_by_sa.png
legal_code_url: https://creativecommons.org/licenses/by-sa/4.0/legalcode
name: Creative Commons Attribution-ShareAlike 4.0 International Public License (CC
BY-SA 4.0)
short: CC BY-SA (4.0)
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '10153'
abstract:
- lang: eng
text: "Gradual typing is a principled means for mixing typed and untyped code. But
typed and untyped code often exhibit different programming patterns. There is
already substantial research investigating gradually giving types to code exhibiting
typical untyped patterns, and some research investigating gradually removing types
from code exhibiting typical typed patterns. This paper investigates how to extend
these established gradual-typing concepts to give formal guarantees not only about
how to change types as code evolves but also about how to change such programming
patterns as well.\r\n\r\nIn particular, we explore mixing untyped \"structural\"
code with typed \"nominal\" code in an object-oriented language. But whereas previous
work only allowed \"nominal\" objects to be treated as \"structural\" objects,
we also allow \"structural\" objects to dynamically acquire certain nominal types,
namely interfaces. We present a calculus that supports such \"cross-paradigm\"
code migration and interoperation in a manner satisfying both the static and dynamic
gradual guarantees, and demonstrate that the calculus can be implemented efficiently."
acknowledgement: "We thank the reviewers for their valuable suggestions towards improving
the paper. We also \r\nthank Mae Milano and Adrian Sampson, as well as the members
of the Programming Languages Discussion Group at Cornell University and of the Programming
Research Laboratory at Northeastern University, for their helpful feedback on preliminary
findings of this work.\r\n\r\nThis material is based upon work supported in part
by the National Science Foundation (NSF) through grant CCF-1350182 and the Austrian
Science Fund (FWF) through grant Z211-N23 (Wittgenstein~Award).\r\nAny opinions,
findings, and conclusions or recommendations expressed in this material are those
of the authors and do not necessarily reflect the views of the NSF or the FWF."
article_number: '127'
article_processing_charge: No
article_type: original
author:
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Ross
full_name: Tate, Ross
last_name: Tate
citation:
ama: Mühlböck F, Tate R. Transitioning from structural to nominal code with efficient
gradual typing. Proceedings of the ACM on Programming Languages. 2021;5.
doi:10.1145/3485504
apa: 'Mühlböck, F., & Tate, R. (2021). Transitioning from structural to nominal
code with efficient gradual typing. Proceedings of the ACM on Programming Languages.
Chicago, IL, United States: Association for Computing Machinery. https://doi.org/10.1145/3485504'
chicago: Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal
Code with Efficient Gradual Typing.” Proceedings of the ACM on Programming
Languages. Association for Computing Machinery, 2021. https://doi.org/10.1145/3485504.
ieee: F. Mühlböck and R. Tate, “Transitioning from structural to nominal code with
efficient gradual typing,” Proceedings of the ACM on Programming Languages,
vol. 5. Association for Computing Machinery, 2021.
ista: Mühlböck F, Tate R. 2021. Transitioning from structural to nominal code with
efficient gradual typing. Proceedings of the ACM on Programming Languages. 5,
127.
mla: Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal
Code with Efficient Gradual Typing.” Proceedings of the ACM on Programming
Languages, vol. 5, 127, Association for Computing Machinery, 2021, doi:10.1145/3485504.
short: F. Mühlböck, R. Tate, Proceedings of the ACM on Programming Languages 5 (2021).
conference:
end_date: 2021-10-23
location: Chicago, IL, United States
name: 'OOPSLA: Object-Oriented Programming, Systems, Languages, and Applications'
start_date: 2021-10-17
date_created: 2021-10-19T12:48:44Z
date_published: 2021-10-15T00:00:00Z
date_updated: 2021-11-12T11:30:07Z
day: '15'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/3485504
file:
- access_level: open_access
checksum: 71011efd2da771cafdec7f0d9693f8c1
content_type: application/pdf
creator: fmuehlbo
date_created: 2021-10-19T12:52:23Z
date_updated: 2021-10-19T12:52:23Z
file_id: '10154'
file_name: monnom-oopsla21.pdf
file_size: 770269
relation: main_file
success: 1
file_date_updated: 2021-10-19T12:52:23Z
has_accepted_license: '1'
intvolume: ' 5'
keyword:
- gradual typing
- gradual guarantee
- nominal
- structural
- call tags
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
status: public
title: Transitioning from structural to nominal code with efficient gradual typing
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 5
year: '2021'
...
---
_id: '10669'
abstract:
- lang: eng
text: "We show that Neural ODEs, an emerging class of timecontinuous neural networks,
can be verified by solving a set of global-optimization problems. For this purpose,
we introduce Stochastic Lagrangian Reachability (SLR), an\r\nabstraction-based
technique for constructing a tight Reachtube (an over-approximation of the set
of reachable states\r\nover a given time-horizon), and provide stochastic guarantees
in the form of confidence intervals for the Reachtube bounds. SLR inherently avoids
the infamous wrapping effect (accumulation of over-approximation errors) by performing
local optimization steps to expand safe regions instead of repeatedly forward-propagating
them as is done by deterministic reachability methods. To enable fast local optimizations,
we introduce a novel forward-mode adjoint sensitivity method to compute gradients
without the need for backpropagation. Finally, we establish asymptotic and non-asymptotic
convergence rates for SLR."
acknowledgement: "The authors would like to thank the reviewers for their insightful
comments. RH and RG were partially supported by\r\nHorizon-2020 ECSEL Project grant
No. 783163 (iDev40). RH was partially supported by Boeing. ML was supported\r\nin
part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).
SG was funded by FWF\r\nproject W1255-N23. JC was partially supported by NAWA Polish
Returns grant PPN/PPO/2018/1/00029. SS was supported by NSF awards DCL-2040599,
CCF-1918225, and CPS-1446832.\r\n"
alternative_title:
- Technical Tracks
article_processing_charge: No
author:
- first_name: Sophie
full_name: Grunbacher, Sophie
last_name: Grunbacher
- 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: Jacek
full_name: Cyranka, Jacek
last_name: Cyranka
- first_name: Scott A
full_name: Smolka, Scott A
last_name: Smolka
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Grunbacher S, Hasani R, Lechner M, Cyranka J, Smolka SA, Grosu R. On the verification
of neural ODEs with stochastic guarantees. In: Proceedings of the AAAI Conference
on Artificial Intelligence. Vol 35. AAAI Press; 2021:11525-11535.'
apa: 'Grunbacher, S., Hasani, R., Lechner, M., Cyranka, J., Smolka, S. A., &
Grosu, R. (2021). On the verification of neural ODEs with stochastic guarantees.
In Proceedings of the AAAI Conference on Artificial Intelligence (Vol.
35, pp. 11525–11535). Virtual: AAAI Press.'
chicago: Grunbacher, Sophie, Ramin Hasani, Mathias Lechner, Jacek Cyranka, Scott
A Smolka, and Radu Grosu. “On the Verification of Neural ODEs with Stochastic
Guarantees.” In Proceedings of the AAAI Conference on Artificial Intelligence,
35:11525–35. AAAI Press, 2021.
ieee: S. Grunbacher, R. Hasani, M. Lechner, J. Cyranka, S. A. Smolka, and R. Grosu,
“On the verification of neural ODEs with stochastic guarantees,” in Proceedings
of the AAAI Conference on Artificial Intelligence, Virtual, 2021, vol. 35,
no. 13, pp. 11525–11535.
ista: 'Grunbacher S, Hasani R, Lechner M, Cyranka J, Smolka SA, Grosu R. 2021. On
the verification of neural ODEs with stochastic guarantees. Proceedings of the
AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement
of Artificial Intelligence, Technical Tracks, vol. 35, 11525–11535.'
mla: Grunbacher, Sophie, et al. “On the Verification of Neural ODEs with Stochastic
Guarantees.” Proceedings of the AAAI Conference on Artificial Intelligence,
vol. 35, no. 13, AAAI Press, 2021, pp. 11525–35.
short: S. Grunbacher, R. Hasani, M. Lechner, J. Cyranka, S.A. Smolka, R. Grosu,
in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press,
2021, pp. 11525–11535.
conference:
end_date: 2021-02-09
location: Virtual
name: 'AAAI: Association for the Advancement of Artificial Intelligence'
start_date: 2021-02-02
date_created: 2022-01-25T15:47:20Z
date_published: 2021-05-28T00:00:00Z
date_updated: 2022-05-24T06:33:14Z
day: '28'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
external_id:
arxiv:
- '2012.08863'
file:
- access_level: open_access
checksum: 468d07041e282a1d46ffdae92f709630
content_type: application/pdf
creator: mlechner
date_created: 2022-01-26T07:38:08Z
date_updated: 2022-01-26T07:38:08Z
file_id: '10680'
file_name: 17372-Article Text-20866-1-2-20210518.pdf
file_size: 286906
relation: main_file
success: 1
file_date_updated: 2022-01-26T07:38:08Z
has_accepted_license: '1'
intvolume: ' 35'
issue: '13'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://ojs.aaai.org/index.php/AAAI/article/view/17372
month: '05'
oa: 1
oa_version: Published Version
page: 11525-11535
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- 978-1-57735-866-4
issn:
- 2159-5399
publication_status: published
publisher: AAAI Press
quality_controlled: '1'
status: public
title: On the verification of neural ODEs with stochastic guarantees
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 35
year: '2021'
...
---
_id: '10671'
abstract:
- lang: eng
text: We introduce a new class of time-continuous recurrent neural network models.
Instead of declaring a learning system’s dynamics by implicit nonlinearities,
we construct networks of linear first-order dynamical systems modulated via nonlinear
interlinked gates. The resulting models represent dynamical systems with varying
(i.e., liquid) time-constants coupled to their hidden state, with outputs being
computed by numerical differential equation solvers. These neural networks exhibit
stable and bounded behavior, yield superior expressivity within the family of
neural ordinary differential equations, and give rise to improved performance
on time-series prediction tasks. To demonstrate these properties, we first take
a theoretical approach to find bounds over their dynamics, and compute their expressive
power by the trajectory length measure in a latent trajectory space. We then conduct
a series of time-series prediction experiments to manifest the approximation capability
of Liquid Time-Constant Networks (LTCs) compared to classical and modern RNNs.
acknowledgement: "R.H. and D.R. are partially supported by Boeing. R.H. and R.G. were
partially supported by the Horizon-2020 ECSEL\r\nProject grant No. 783163 (iDev40).
M.L. was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23
(Wittgenstein Award). A.A. is supported by the National Science Foundation (NSF)
Graduate Research Fellowship Program. This research work is partially drawn from
the PhD dissertation of R.H."
alternative_title:
- Technical Tracks
article_processing_charge: No
author:
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Hasani R, Lechner M, Amini A, Rus D, Grosu R. Liquid time-constant networks.
In: Proceedings of the AAAI Conference on Artificial Intelligence. Vol
35. AAAI Press; 2021:7657-7666.'
apa: 'Hasani, R., Lechner, M., Amini, A., Rus, D., & Grosu, R. (2021). Liquid
time-constant networks. In Proceedings of the AAAI Conference on Artificial
Intelligence (Vol. 35, pp. 7657–7666). Virtual: AAAI Press.'
chicago: Hasani, Ramin, Mathias Lechner, Alexander Amini, Daniela Rus, and Radu
Grosu. “Liquid Time-Constant Networks.” In Proceedings of the AAAI Conference
on Artificial Intelligence, 35:7657–66. AAAI Press, 2021.
ieee: R. Hasani, M. Lechner, A. Amini, D. Rus, and R. Grosu, “Liquid time-constant
networks,” in Proceedings of the AAAI Conference on Artificial Intelligence,
Virtual, 2021, vol. 35, no. 9, pp. 7657–7666.
ista: 'Hasani R, Lechner M, Amini A, Rus D, Grosu R. 2021. Liquid time-constant
networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI:
Association for the Advancement of Artificial Intelligence, Technical Tracks,
vol. 35, 7657–7666.'
mla: Hasani, Ramin, et al. “Liquid Time-Constant Networks.” Proceedings of the
AAAI Conference on Artificial Intelligence, vol. 35, no. 9, AAAI Press, 2021,
pp. 7657–66.
short: R. Hasani, M. Lechner, A. Amini, D. Rus, R. Grosu, in:, Proceedings of the
AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 7657–7666.
conference:
end_date: 2021-02-09
location: Virtual
name: 'AAAI: Association for the Advancement of Artificial Intelligence'
start_date: 2021-02-02
date_created: 2022-01-25T15:48:36Z
date_published: 2021-05-28T00:00:00Z
date_updated: 2022-05-24T06:36:54Z
day: '28'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
external_id:
arxiv:
- '2006.04439'
file:
- access_level: open_access
checksum: 0f06995fba06dbcfa7ed965fc66027ff
content_type: application/pdf
creator: mlechner
date_created: 2022-01-26T07:36:03Z
date_updated: 2022-01-26T07:36:03Z
file_id: '10678'
file_name: 16936-Article Text-20430-1-2-20210518 (1).pdf
file_size: 4302669
relation: main_file
success: 1
file_date_updated: 2022-01-26T07:36:03Z
has_accepted_license: '1'
intvolume: ' 35'
issue: '9'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://ojs.aaai.org/index.php/AAAI/article/view/16936
month: '05'
oa: 1
oa_version: Published Version
page: 7657-7666
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- 978-1-57735-866-4
issn:
- 2159-5399
publication_status: published
publisher: AAAI Press
quality_controlled: '1'
status: public
title: Liquid time-constant networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 35
year: '2021'
...