---
_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
arxiv: 1
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: '10670'
abstract:
- lang: eng
text: "Imitation learning enables high-fidelity, vision-based learning of policies
within rich, photorealistic environments. However, such techniques often rely
on traditional discrete-time neural models and face difficulties in generalizing
to domain shifts by failing to account for the causal relationships between the
agent and the environment. In this paper, we propose a theoretical and experimental
framework for learning causal representations using continuous-time neural networks,
specifically over their discrete-time counterparts. We evaluate our method in
the context of visual-control learning of drones over a series of complex tasks,
ranging from short- and long-term navigation, to chasing static and dynamic objects
through photorealistic environments. Our results demonstrate that causal continuous-time\r\ndeep
models can perform robust navigation tasks, where advanced recurrent models fail.
These models learn complex causal control representations directly from raw visual
inputs and scale to solve a variety of tasks using imitation learning."
acknowledgement: "C.V., R.H. A.A. and D.R. are partially supported by Boeing and MIT.
A.A. is supported by the National Science Foundation (NSF) Graduate Research Fellowship
Program. M.L. is supported in part by the Austrian Science Fund (FWF) under grant
Z211-N23 (Wittgenstein Award). Research was sponsored by 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\r\nand 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.\r\n"
alternative_title:
- ' Advances in Neural Information Processing Systems'
article_processing_charge: No
arxiv: 1
author:
- first_name: Charles J
full_name: Vorbach, Charles J
last_name: Vorbach
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: 'Vorbach CJ, Hasani R, Amini A, Lechner M, Rus D. Causal navigation by continuous-time
neural networks. In: 35th Conference on Neural Information Processing Systems.
; 2021.'
apa: Vorbach, C. J., Hasani, R., Amini, A., Lechner, M., & Rus, D. (2021). Causal
navigation by continuous-time neural networks. In 35th Conference on Neural
Information Processing Systems. Virtual.
chicago: Vorbach, Charles J, Ramin Hasani, Alexander Amini, Mathias Lechner, and
Daniela Rus. “Causal Navigation by Continuous-Time Neural Networks.” In 35th
Conference on Neural Information Processing Systems, 2021.
ieee: C. J. Vorbach, R. Hasani, A. Amini, M. Lechner, and D. Rus, “Causal navigation
by continuous-time neural networks,” in 35th Conference on Neural Information
Processing Systems, Virtual, 2021.
ista: 'Vorbach CJ, Hasani R, Amini A, Lechner M, Rus D. 2021. Causal navigation
by continuous-time neural networks. 35th Conference on Neural Information Processing
Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information
Processing Systems, .'
mla: Vorbach, Charles J., et al. “Causal Navigation by Continuous-Time Neural Networks.”
35th Conference on Neural Information Processing Systems, 2021.
short: C.J. Vorbach, R. Hasani, A. Amini, M. Lechner, D. Rus, in:, 35th Conference
on Neural Information Processing Systems, 2021.
conference:
end_date: 2021-12-10
location: Virtual
name: 'NeurIPS: Neural Information Processing Systems'
start_date: 2021-12-06
date_created: 2022-01-25T15:47:50Z
date_published: 2021-12-01T00:00:00Z
date_updated: 2022-01-26T14:33:31Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
external_id:
arxiv:
- '2106.08314'
file:
- access_level: open_access
checksum: be81f0ade174a8c9b2d4fe09590b2021
content_type: application/pdf
creator: mlechner
date_created: 2022-01-26T07:37:24Z
date_updated: 2022-01-26T07:37:24Z
file_id: '10679'
file_name: NeurIPS-2021-causal-navigation-by-continuous-time-neural-networks-Paper.pdf
file_size: 6841228
relation: main_file
success: 1
file_date_updated: 2022-01-26T07:37:24Z
has_accepted_license: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/3.0/
main_file_link:
- open_access: '1'
url: https://proceedings.neurips.cc/paper/2021/hash/67ba02d73c54f0b83c05507b7fb7267f-Abstract.html
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 35th Conference on Neural Information Processing Systems
publication_status: published
quality_controlled: '1'
status: public
title: Causal navigation by continuous-time neural networks
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND
3.0)
short: CC BY-NC-ND (3.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
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
arxiv: 1
author:
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: 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'
...
---
_id: '10674'
abstract:
- lang: eng
text: 'In two-player games on graphs, the players move a token through a graph to
produce an infinite path, which determines the winner of the game. Such games
are central in formal methods since they model the interaction between a non-terminating
system and its environment. In bidding games the players bid for the right to
move the token: in each round, the players simultaneously submit bids, and the
higher bidder moves the token and pays the other player. Bidding games are known
to have a clean and elegant mathematical structure that relies on the ability
of the players to submit arbitrarily small bids. Many applications, however, require
a fixed granularity for the bids, which can represent, for example, the monetary
value expressed in cents. We study, for the first time, the combination of discrete-bidding
and infinite-duration games. Our most important result proves that these games
form a large determined subclass of concurrent games, where determinacy is the
strong property that there always exists exactly one player who can guarantee
winning the game. In particular, we show that, in contrast to non-discrete bidding
games, the mechanism with which tied bids are resolved plays an important role
in discrete-bidding games. We study several natural tie-breaking mechanisms and
show that, while some do not admit determinacy, most natural mechanisms imply
determinacy for every pair of initial budgets.'
acknowledgement: "This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M
2369-N33 (Meitner fellowship).\r\n"
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Milad
full_name: Aghajohari, Milad
last_name: Aghajohari
- 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: Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration
games. Logical Methods in Computer Science. 2021;17(1):10:1-10:23. doi:10.23638/LMCS-17(1:10)2021
apa: Aghajohari, M., Avni, G., & Henzinger, T. A. (2021). Determinacy in discrete-bidding
infinite-duration games. Logical Methods in Computer Science. International
Federation for Computational Logic. https://doi.org/10.23638/LMCS-17(1:10)2021
chicago: Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding
Infinite-Duration Games.” Logical Methods in Computer Science. International
Federation for Computational Logic, 2021. https://doi.org/10.23638/LMCS-17(1:10)2021.
ieee: M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding
infinite-duration games,” Logical Methods in Computer Science, vol. 17,
no. 1. International Federation for Computational Logic, p. 10:1-10:23, 2021.
ista: Aghajohari M, Avni G, Henzinger TA. 2021. Determinacy in discrete-bidding
infinite-duration games. Logical Methods in Computer Science. 17(1), 10:1-10:23.
mla: Aghajohari, Milad, et al. “Determinacy in Discrete-Bidding Infinite-Duration
Games.” Logical Methods in Computer Science, vol. 17, no. 1, International
Federation for Computational Logic, 2021, p. 10:1-10:23, doi:10.23638/LMCS-17(1:10)2021.
short: M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science
17 (2021) 10:1-10:23.
date_created: 2022-01-25T16:32:13Z
date_published: 2021-02-03T00:00:00Z
date_updated: 2023-08-17T06:56:42Z
day: '03'
ddc:
- '510'
department:
- _id: ToHe
doi: 10.23638/LMCS-17(1:10)2021
external_id:
arxiv:
- '1905.03588'
isi:
- '000658724600010'
file:
- access_level: open_access
checksum: b35586a50ed1ca8f44767de116d18d81
content_type: application/pdf
creator: alisjak
date_created: 2022-01-26T08:04:50Z
date_updated: 2022-01-26T08:04:50Z
file_id: '10690'
file_name: 2021_LMCS_AGHAJOHAR.pdf
file_size: 819878
relation: main_file
success: 1
file_date_updated: 2022-01-26T08:04:50Z
has_accepted_license: '1'
intvolume: ' 17'
isi: 1
issue: '1'
keyword:
- computer science
- computer science and game theory
- logic in computer science
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: 10:1-10:23
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Logical Methods in Computer Science
publication_identifier:
eissn:
- 1860-5974
publication_status: published
publisher: International Federation for Computational Logic
quality_controlled: '1'
scopus_import: '1'
status: public
title: Determinacy in discrete-bidding infinite-duration games
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: 17
year: '2021'
...
---
_id: '10688'
abstract:
- lang: eng
text: "Civl is a static verifier for concurrent programs designed around the conceptual
framework of layered refinement,\r\nwhich views the task of verifying a program
as a sequence of program simplification steps each justified by its own invariant.
Civl verifies a layered concurrent program that compactly expresses all the programs
in this sequence and the supporting invariants. This paper presents the design
and implementation of the Civl verifier."
acknowledgement: This research was performed while Bernhard Kragl was at IST Austria,
supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein
Award).
alternative_title:
- Conference Series
article_processing_charge: No
author:
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: 'Kragl B, Qadeer S. The Civl verifier. In: Ruzica P, Whalen MW, eds. Proceedings
of the 21st Conference on Formal Methods in Computer-Aided Design. Vol 2.
TU Wien Academic Press; 2021:143–152. doi:10.34727/2021/isbn.978-3-85448-046-4_23'
apa: 'Kragl, B., & Qadeer, S. (2021). The Civl verifier. In P. Ruzica &
M. W. Whalen (Eds.), Proceedings of the 21st Conference on Formal Methods in
Computer-Aided Design (Vol. 2, pp. 143–152). Virtual: TU Wien Academic Press.
https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23'
chicago: Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” In Proceedings
of the 21st Conference on Formal Methods in Computer-Aided Design, edited
by Piskac Ruzica and Michael W. Whalen, 2:143–152. TU Wien Academic Press, 2021.
https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23.
ieee: B. Kragl and S. Qadeer, “The Civl verifier,” in Proceedings of the 21st
Conference on Formal Methods in Computer-Aided Design, Virtual, 2021, vol.
2, pp. 143–152.
ista: 'Kragl B, Qadeer S. 2021. The Civl verifier. Proceedings of the 21st Conference
on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided
Design, Conference Series, vol. 2, 143–152.'
mla: Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” Proceedings of the
21st Conference on Formal Methods in Computer-Aided Design, edited by Piskac
Ruzica and Michael W. Whalen, vol. 2, TU Wien Academic Press, 2021, pp. 143–152,
doi:10.34727/2021/isbn.978-3-85448-046-4_23.
short: B. Kragl, S. Qadeer, in:, P. Ruzica, M.W. Whalen (Eds.), Proceedings of the
21st Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press,
2021, pp. 143–152.
conference:
end_date: 2021-10-22
location: Virtual
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2021-10-20
date_created: 2022-01-26T08:01:30Z
date_published: 2021-10-01T00:00:00Z
date_updated: 2022-01-26T08:20:41Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.34727/2021/isbn.978-3-85448-046-4_23
editor:
- first_name: Piskac
full_name: Ruzica, Piskac
last_name: Ruzica
- first_name: Michael W.
full_name: Whalen, Michael W.
last_name: Whalen
file:
- access_level: open_access
checksum: 35438ac9f9750340b7f8ae4ae3220d9f
content_type: application/pdf
creator: cchlebak
date_created: 2022-01-26T08:04:29Z
date_updated: 2022-01-26T08:04:29Z
file_id: '10689'
file_name: 2021_FCAD2021_Kragl.pdf
file_size: 390555
relation: main_file
success: 1
file_date_updated: 2022-01-26T08:04:29Z
has_accepted_license: '1'
intvolume: ' 2'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 143–152
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 21st Conference on Formal Methods in Computer-Aided
Design
publication_identifier:
isbn:
- 978-3-85448-046-4
publication_status: published
publisher: TU Wien Academic Press
quality_controlled: '1'
status: public
title: The Civl verifier
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2021'
...
---
_id: '9647'
abstract:
- lang: eng
text: 'Gene expression is regulated by the set of transcription factors (TFs) that
bind to the promoter. The ensuing regulating function is often represented as
a combinational logic circuit, where output (gene expression) is determined by
current input values (promoter bound TFs) only. However, the simultaneous arrival
of TFs is a strong assumption, since transcription and translation of genes introduce
intrinsic time delays and there is no global synchronisation among the arrival
times of different molecular species at their targets. We present an experimentally
implementable genetic circuit with two inputs and one output, which in the presence
of small delays in input arrival, exhibits qualitatively distinct population-level
phenotypes, over timescales that are longer than typical cell doubling times.
From a dynamical systems point of view, these phenotypes represent long-lived
transients: although they converge to the same value eventually, they do so after
a very long time span. The key feature of this toy model genetic circuit is that,
despite having only two inputs and one output, it is regulated by twenty-three
distinct DNA-TF configurations, two of which are more stable than others (DNA
looped states), one promoting and another blocking the expression of the output
gene. Small delays in input arrival time result in a majority of cells in the
population quickly reaching the stable state associated with the first input,
while exiting of this stable state occurs at a slow timescale. In order to mechanistically
model the behaviour of this genetic circuit, we used a rule-based modelling language,
and implemented a grid-search to find parameter combinations giving rise to long-lived
transients. Our analysis shows that in the absence of feedback, there exist path-dependent
gene regulatory mechanisms based on the long timescale of transients. The behaviour
of this toy model circuit suggests that gene regulatory networks can exploit event
timing to create phenotypes, and it opens the possibility that they could use
event timing to memorise events, without regulatory feedback. The model reveals
the importance of (i) mechanistically modelling the transitions between the different
DNA-TF states, and (ii) employing transient analysis thereof.'
acknowledgement: 'Tatjana Petrov’s research was supported in part by SNSF Advanced
Postdoctoral Mobility Fellowship grant number P300P2 161067, the Ministry of Science,
Research and the Arts of the state of Baden-Wurttemberg, and the DFG Centre of Excellence
2117 ‘Centre for the Advanced Study of Collective Behaviour’ (ID: 422037984). Claudia
Igler is the recipient of a DOC Fellowship of the Austrian Academy of Sciences.
Thomas A. Henzinger’s research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award).'
article_processing_charge: No
article_type: original
author:
- first_name: Tatjana
full_name: Petrov, Tatjana
last_name: Petrov
- first_name: Claudia
full_name: Igler, Claudia
id: 46613666-F248-11E8-B48F-1D18A9856A87
last_name: Igler
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Calin C
full_name: Guet, Calin C
id: 47F8433E-F248-11E8-B48F-1D18A9856A87
last_name: Guet
orcid: 0000-0001-6220-2052
citation:
ama: Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. Long lived transients in
gene regulation. Theoretical Computer Science. 2021;893:1-16. doi:10.1016/j.tcs.2021.05.023
apa: Petrov, T., Igler, C., Sezgin, A., Henzinger, T. A., & Guet, C. C. (2021).
Long lived transients in gene regulation. Theoretical Computer Science.
Elsevier. https://doi.org/10.1016/j.tcs.2021.05.023
chicago: Petrov, Tatjana, Claudia Igler, Ali Sezgin, Thomas A Henzinger, and Calin
C Guet. “Long Lived Transients in Gene Regulation.” Theoretical Computer Science.
Elsevier, 2021. https://doi.org/10.1016/j.tcs.2021.05.023.
ieee: T. Petrov, C. Igler, A. Sezgin, T. A. Henzinger, and C. C. Guet, “Long lived
transients in gene regulation,” Theoretical Computer Science, vol. 893.
Elsevier, pp. 1–16, 2021.
ista: Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. 2021. Long lived transients
in gene regulation. Theoretical Computer Science. 893, 1–16.
mla: Petrov, Tatjana, et al. “Long Lived Transients in Gene Regulation.” Theoretical
Computer Science, vol. 893, Elsevier, 2021, pp. 1–16, doi:10.1016/j.tcs.2021.05.023.
short: T. Petrov, C. Igler, A. Sezgin, T.A. Henzinger, C.C. Guet, Theoretical Computer
Science 893 (2021) 1–16.
date_created: 2021-07-11T22:01:18Z
date_published: 2021-06-04T00:00:00Z
date_updated: 2023-08-10T14:11:19Z
day: '04'
ddc:
- '004'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1016/j.tcs.2021.05.023
external_id:
isi:
- '000710180500002'
file:
- access_level: open_access
checksum: d3aef34cfb13e53bba4cf44d01680793
content_type: application/pdf
creator: dernst
date_created: 2022-05-12T12:13:27Z
date_updated: 2022-05-12T12:13:27Z
file_id: '11364'
file_name: 2021_TheoreticalComputerScience_Petrov.pdf
file_size: 2566504
relation: main_file
success: 1
file_date_updated: 2022-05-12T12:13:27Z
has_accepted_license: '1'
intvolume: ' 893'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 1-16
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Theoretical Computer Science
publication_identifier:
issn:
- 0304-3975
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Long lived transients in gene regulation
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 893
year: '2021'
...
---
_id: '9946'
abstract:
- lang: eng
text: We argue that the time is ripe to investigate differential monitoring, in
which the specification of a program's behavior is implicitly given by a second
program implementing the same informal specification. Similar ideas have been
proposed before, and are currently implemented in restricted form for testing
and specialized run-time analyses, aspects of which we combine. We discuss the
challenges of implementing differential monitoring as a general-purpose, black-box
run-time monitoring framework, and present promising results of a preliminary
implementation, showing low monitoring overheads for diverse programs.
acknowledgement: The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer,
Adrian Francalanza, Owolabi Legunsen, Matthew Milano, Manuel Rigger, Cesar Sanchez,
and the members of the IST Verification Seminar for their helpful comments and insights
on various stages of this work, as well as the reviewers of RV’21 for their helpful
suggestions on the actual paper.
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: Mühlböck F, Henzinger TA. Differential Monitoring. IST Austria; 2021.
doi:10.15479/AT:ISTA:9946
apa: Mühlböck, F., & Henzinger, T. A. (2021). Differential monitoring.
IST Austria. https://doi.org/10.15479/AT:ISTA:9946
chicago: Mühlböck, Fabian, and Thomas A Henzinger. Differential Monitoring.
IST Austria, 2021. https://doi.org/10.15479/AT:ISTA:9946.
ieee: F. Mühlböck and T. A. Henzinger, Differential monitoring. IST Austria,
2021.
ista: Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.
mla: Mühlböck, Fabian, and Thomas A. Henzinger. Differential Monitoring.
IST Austria, 2021, doi:10.15479/AT:ISTA:9946.
short: F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021.
date_created: 2021-08-20T20:00:37Z
date_published: 2021-09-01T00:00:00Z
date_updated: 2023-08-14T07:20:29Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:9946
file:
- access_level: open_access
checksum: 0f9aafd59444cb6bdca6925d163ab946
content_type: application/pdf
creator: fmuehlbo
date_created: 2021-08-20T19:59:44Z
date_updated: 2021-09-03T12:34:28Z
file_id: '9948'
file_name: differentialmonitoring-techreport.pdf
file_size: '320453'
relation: main_file
file_date_updated: 2021-09-03T12:34:28Z
has_accepted_license: '1'
keyword:
- run-time verification
- software engineering
- implicit specification
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '17'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
related_material:
record:
- id: '9281'
relation: other
status: public
- id: '10108'
relation: shorter_version
status: public
status: public
title: Differential monitoring
type: technical_report
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2021'
...
---
_id: '8287'
abstract:
- lang: eng
text: Reachability analysis aims at identifying states reachable by a system within
a given time horizon. This task is known to be computationally expensive for linear
hybrid systems. Reachability analysis works by iteratively applying continuous
and discrete post operators to compute states reachable according to continuous
and discrete dynamics, respectively. In this paper, we enhance both of these operators
and make sure that most of the involved computations are performed in low-dimensional
state space. In particular, we improve the continuous-post operator by performing
computations in high-dimensional state space only for time intervals relevant
for the subsequent application of the discrete-post operator. Furthermore, the
new discrete-post operator performs low-dimensional computations by leveraging
the structure of the guard and assignment of a considered transition. We illustrate
the potential of our approach on a number of challenging benchmarks.
article_processing_charge: No
arxiv: 1
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
last_name: Bogomolov
- first_name: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Kostiantyn
full_name: Potomkin, Kostiantyn
last_name: Potomkin
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis
of linear hybrid systems via block decomposition. In: Proceedings of the International
Conference on Embedded Software. ; 2020.'
apa: Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2020).
Reachability analysis of linear hybrid systems via block decomposition. In Proceedings
of the International Conference on Embedded Software. Virtual .
chicago: Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and
Christian Schilling. “Reachability Analysis of Linear Hybrid Systems via Block
Decomposition.” In Proceedings of the International Conference on Embedded
Software, 2020.
ieee: S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “Reachability
analysis of linear hybrid systems via block decomposition,” in Proceedings
of the International Conference on Embedded Software, Virtual , 2020.
ista: 'Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2020. Reachability
analysis of linear hybrid systems via block decomposition. Proceedings of the
International Conference on Embedded Software. EMSOFT: International Conference
on Embedded Software.'
mla: Bogomolov, Sergiy, et al. “Reachability Analysis of Linear Hybrid Systems via
Block Decomposition.” Proceedings of the International Conference on Embedded
Software, 2020.
short: S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings
of the International Conference on Embedded Software, 2020.
conference:
end_date: 2020-09-25
location: 'Virtual '
name: 'EMSOFT: International Conference on Embedded Software'
start_date: 2020-09-20
date_created: 2020-08-24T12:56:20Z
date_published: 2020-01-01T00:00:00Z
date_updated: 2023-08-22T13:27:32Z
ddc:
- '000'
department:
- _id: ToHe
ec_funded: 1
external_id:
arxiv:
- '1905.02458'
file:
- access_level: open_access
checksum: d19e97d0f8a3a441dc078ec812297d75
content_type: application/pdf
creator: cschilli
date_created: 2020-08-24T12:53:15Z
date_updated: 2020-08-24T12:53:15Z
file_id: '8288'
file_name: 2020EMSOFT.pdf
file_size: 696384
relation: main_file
success: 1
file_date_updated: 2020-08-24T12:53:15Z
has_accepted_license: '1'
keyword:
- reachability
- hybrid systems
- decomposition
language:
- iso: eng
oa: 1
oa_version: Preprint
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25C5A090-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z00312
name: The Wittgenstein Prize
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: Proceedings of the International Conference on Embedded Software
publication_status: published
quality_controlled: '1'
related_material:
record:
- id: '8790'
relation: later_version
status: public
status: public
title: Reachability analysis of linear hybrid systems via block decomposition
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
year: '2020'
...
---
_id: '8332'
abstract:
- lang: eng
text: "Designing and verifying concurrent programs is a notoriously challenging,
time consuming, and error prone task, even for experts. This is due to the sheer
number of possible interleavings of a concurrent program, all of which have to
be tracked and accounted for in a formal proof. Inventing an inductive invariant
that captures all interleavings of a low-level implementation is theoretically
possible, but practically intractable. We develop a refinement-based verification
framework that provides mechanisms to simplify proof construction by decomposing
the verification task into smaller subtasks.\r\n\r\nIn a first line of work, we
present a foundation for refinement reasoning over structured concurrent programs.
We introduce layered concurrent programs as a compact notation to represent multi-layer
refinement proofs. A layered concurrent program specifies a sequence of connected
concurrent programs, from most concrete to most abstract, such that common parts
of different programs are written exactly once. Each program in this sequence
is expressed as structured concurrent program, i.e., a program over (potentially
recursive) procedures, imperative control flow, gated atomic actions, structured
parallelism, and asynchronous concurrency. This is in contrast to existing refinement-based
verifiers, which represent concurrent systems as flat transition relations. We
present a powerful refinement proof rule that decomposes refinement checking over
structured programs into modular verification conditions. Refinement checking
is supported by a new form of modular, parameterized invariants, called yield
invariants, and a linear permission system to enhance local reasoning.\r\n\r\nIn
a second line of work, we present two new reduction-based program transformations
that target asynchronous programs. These transformations reduce the number of
interleavings that need to be considered, thus reducing the complexity of invariants.
Synchronization simplifies the verification of asynchronous programs by introducing
the fiction, for proof purposes, that asynchronous operations complete synchronously.
Synchronization summarizes an asynchronous computation as immediate atomic effect.
Inductive sequentialization establishes sequential reductions that captures every
behavior of the original program up to reordering of coarse-grained commutative
actions. A sequential reduction of a concurrent program is easy to reason about
since it corresponds to a simple execution of the program in an idealized synchronous
environment, where processes act in a fixed order and at the same speed.\r\n\r\nOur
approach is implemented the CIVL verifier, which has been successfully used for
the verification of several complex concurrent programs. In our methodology, the
overall correctness of a program is established piecemeal by focusing on the invariant
required for each refinement step separately. While the programmer does the creative
work of specifying the chain of programs and the inductive invariant justifying
each link in the chain, the tool automatically constructs the verification conditions
underlying each refinement step."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
citation:
ama: 'Kragl B. Verifying concurrent programs: Refinement, synchronization, sequentialization.
2020. doi:10.15479/AT:ISTA:8332'
apa: 'Kragl, B. (2020). Verifying concurrent programs: Refinement, synchronization,
sequentialization. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:8332'
chicago: 'Kragl, Bernhard. “Verifying Concurrent Programs: Refinement, Synchronization,
Sequentialization.” Institute of Science and Technology Austria, 2020. https://doi.org/10.15479/AT:ISTA:8332.'
ieee: 'B. Kragl, “Verifying concurrent programs: Refinement, synchronization, sequentialization,”
Institute of Science and Technology Austria, 2020.'
ista: 'Kragl B. 2020. Verifying concurrent programs: Refinement, synchronization,
sequentialization. Institute of Science and Technology Austria.'
mla: 'Kragl, Bernhard. Verifying Concurrent Programs: Refinement, Synchronization,
Sequentialization. Institute of Science and Technology Austria, 2020, doi:10.15479/AT:ISTA:8332.'
short: 'B. Kragl, Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization,
Institute of Science and Technology Austria, 2020.'
date_created: 2020-09-04T12:24:12Z
date_published: 2020-09-03T00:00:00Z
date_updated: 2023-09-13T08:45:08Z
day: '03'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:8332
file:
- access_level: open_access
checksum: 26fe261550f691280bda4c454bf015c7
content_type: application/pdf
creator: bkragl
date_created: 2020-09-04T12:17:47Z
date_updated: 2020-09-04T12:17:47Z
file_id: '8333'
file_name: kragl-thesis.pdf
file_size: 1348815
relation: main_file
- access_level: closed
checksum: b9694ce092b7c55557122adba8337ebc
content_type: application/zip
creator: bkragl
date_created: 2020-09-04T13:00:17Z
date_updated: 2020-09-04T13:00:17Z
file_id: '8335'
file_name: kragl-thesis.zip
file_size: 372312
relation: source_file
file_date_updated: 2020-09-04T13:00:17Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '120'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '133'
relation: part_of_dissertation
status: public
- id: '8012'
relation: part_of_dissertation
status: public
- id: '8195'
relation: part_of_dissertation
status: public
- id: '160'
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: 'Verifying concurrent programs: Refinement, synchronization, sequentialization'
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2020'
...
---
_id: '8571'
abstract:
- lang: eng
text: We present the results of a friendly competition for formal verification of
continuous and hybrid systems with nonlinear continuous dynamics. The friendly
competition took place as part of the workshop Applied Verification for Continuous
and Hybrid Systems (ARCH) in 2020. This year, 6 tools Ariadne, CORA, DynIbex,
Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. These
tools are applied to solve reachability analysis problems on six benchmark problems,
two of them featuring hybrid dynamics. We do not rank the tools based on the results,
but show the current status and discover the potential advantages of different
tools.
acknowledgement: Christian Schilling acknowledges support in part by the Austrian
Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award) and the European Union’s
Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie
grant agreement No. 754411.
article_processing_charge: No
author:
- first_name: Luca
full_name: Geretti, Luca
last_name: Geretti
- first_name: Julien
full_name: Alexandre Dit Sandretto, Julien
last_name: Alexandre Dit Sandretto
- first_name: Matthias
full_name: Althoff, Matthias
last_name: Althoff
- first_name: Luis
full_name: Benet, Luis
last_name: Benet
- first_name: Alexandre
full_name: Chapoutot, Alexandre
last_name: Chapoutot
- first_name: Xin
full_name: Chen, Xin
last_name: Chen
- first_name: Pieter
full_name: Collins, Pieter
last_name: Collins
- first_name: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Daniel
full_name: Freire, Daniel
last_name: Freire
- first_name: Fabian
full_name: Immler, Fabian
last_name: Immler
- first_name: Niklas
full_name: Kochdumper, Niklas
last_name: Kochdumper
- first_name: David
full_name: Sanders, David
last_name: Sanders
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Geretti L, Alexandre Dit Sandretto J, Althoff M, et al. ARCH-COMP20 Category
Report: Continuous and hybrid systems with nonlinear dynamics. In: EPiC Series
in Computing. Vol 74. EasyChair; 2020:49-75. doi:10.29007/zkf6'
apa: 'Geretti, L., Alexandre Dit Sandretto, J., Althoff, M., Benet, L., Chapoutot,
A., Chen, X., … Schilling, C. (2020). ARCH-COMP20 Category Report: Continuous
and hybrid systems with nonlinear dynamics. In EPiC Series in Computing
(Vol. 74, pp. 49–75). EasyChair. https://doi.org/10.29007/zkf6'
chicago: 'Geretti, Luca, Julien Alexandre Dit Sandretto, Matthias Althoff, Luis
Benet, Alexandre Chapoutot, Xin Chen, Pieter Collins, et al. “ARCH-COMP20 Category
Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” In EPiC Series
in Computing, 74:49–75. EasyChair, 2020. https://doi.org/10.29007/zkf6.'
ieee: 'L. Geretti et al., “ARCH-COMP20 Category Report: Continuous and hybrid
systems with nonlinear dynamics,” in EPiC Series in Computing, 2020, vol.
74, pp. 49–75.'
ista: 'Geretti L, Alexandre Dit Sandretto J, Althoff M, Benet L, Chapoutot A, Chen
X, Collins P, Forets M, Freire D, Immler F, Kochdumper N, Sanders D, Schilling
C. 2020. ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear
dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification
on Continuous and Hybrid Systems vol. 74, 49–75.'
mla: 'Geretti, Luca, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid
Systems with Nonlinear Dynamics.” EPiC Series in Computing, vol. 74, EasyChair,
2020, pp. 49–75, doi:10.29007/zkf6.'
short: L. Geretti, J. Alexandre Dit Sandretto, M. Althoff, L. Benet, A. Chapoutot,
X. Chen, P. Collins, M. Forets, D. Freire, F. Immler, N. Kochdumper, D. Sanders,
C. Schilling, in:, EPiC Series in Computing, EasyChair, 2020, pp. 49–75.
conference:
end_date: 2020-07-12
name: 'ARCH: International Workshop on Applied Verification on Continuous and Hybrid
Systems'
start_date: 2020-07-12
date_created: 2020-09-26T14:41:29Z
date_published: 2020-09-25T00:00:00Z
date_updated: 2021-01-12T08:20:06Z
day: '25'
department:
- _id: ToHe
doi: 10.29007/zkf6
ec_funded: 1
intvolume: ' 74'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://easychair.org/publications/download/nrdD
month: '09'
oa: 1
oa_version: Published Version
page: 49-75
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: EPiC Series in Computing
publication_status: published
publisher: EasyChair
quality_controlled: '1'
status: public
title: 'ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear
dynamics'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 74
year: '2020'
...
---
_id: '8572'
abstract:
- lang: eng
text: 'We present the results of the ARCH 2020 friendly competition for formal verification
of continuous and hybrid systems with linear continuous dynamics. In its fourth
edition, eight tools have been applied to solve eight different benchmark problems
in the category for linear continuous dynamics (in alphabetical order): CORA,
C2E2, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report
is a snapshot of the current landscape of tools and the types of benchmarks they
are particularly suited for. Due to the diversity of problems, we are not ranking
tools, yet the presented results provide one of the most complete assessments
of tools for the safety verification of continuous and hybrid systems with linear
continuous dynamics up to this date.'
acknowledgement: "The authors gratefully acknowledge financial support by the European
Commission project\r\njustITSELF under grant number 817629, by the Austrian Science
Fund (FWF) under grant\r\nZ211-N23 (Wittgenstein Award), by the European Union’s
Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie
grant agreement No. 754411, and by the\r\nScience and Engineering Research Board
(SERB) project with file number IMP/2018/000523.\r\nThis material is based upon
work supported by the Air Force Office of Scientific Research under\r\naward number
FA9550-19-1-0288. Any opinions, finding, and conclusions or recommendations\r\nexpressed
in this material are those of the author(s) and do not necessarily reflect the views
of\r\nthe United States Air Force."
article_processing_charge: No
author:
- first_name: Matthias
full_name: Althoff, Matthias
last_name: Althoff
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Zongnan
full_name: Bao, Zongnan
last_name: Bao
- first_name: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Daniel
full_name: Freire, Daniel
last_name: Freire
- first_name: Niklas
full_name: Kochdumper, Niklas
last_name: Kochdumper
- first_name: Yangge
full_name: Li, Yangge
last_name: Li
- first_name: Sayan
full_name: Mitra, Sayan
last_name: Mitra
- first_name: Rajarshi
full_name: Ray, Rajarshi
last_name: Ray
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Stefan
full_name: Schupp, Stefan
last_name: Schupp
- first_name: Mark
full_name: Wetzlinger, Mark
last_name: Wetzlinger
citation:
ama: 'Althoff M, Bak S, Bao Z, et al. ARCH-COMP20 Category Report: Continuous and
hybrid systems with linear dynamics. In: EPiC Series in Computing. Vol
74. EasyChair; 2020:16-48. doi:10.29007/7dt2'
apa: 'Althoff, M., Bak, S., Bao, Z., Forets, M., Frehse, G., Freire, D., … Wetzlinger,
M. (2020). ARCH-COMP20 Category Report: Continuous and hybrid systems with linear
dynamics. In EPiC Series in Computing (Vol. 74, pp. 16–48). EasyChair.
https://doi.org/10.29007/7dt2'
chicago: 'Althoff, Matthias, Stanley Bak, Zongnan Bao, Marcelo Forets, Goran Frehse,
Daniel Freire, Niklas Kochdumper, et al. “ARCH-COMP20 Category Report: Continuous
and Hybrid Systems with Linear Dynamics.” In EPiC Series in Computing,
74:16–48. EasyChair, 2020. https://doi.org/10.29007/7dt2.'
ieee: 'M. Althoff et al., “ARCH-COMP20 Category Report: Continuous and hybrid
systems with linear dynamics,” in EPiC Series in Computing, 2020, vol.
74, pp. 16–48.'
ista: 'Althoff M, Bak S, Bao Z, Forets M, Frehse G, Freire D, Kochdumper N, Li Y,
Mitra S, Ray R, Schilling C, Schupp S, Wetzlinger M. 2020. ARCH-COMP20 Category
Report: Continuous and hybrid systems with linear dynamics. EPiC Series in Computing.
ARCH: International Workshop on Applied Verification on Continuous and Hybrid
Systems vol. 74, 16–48.'
mla: 'Althoff, Matthias, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid
Systems with Linear Dynamics.” EPiC Series in Computing, vol. 74, EasyChair,
2020, pp. 16–48, doi:10.29007/7dt2.'
short: M. Althoff, S. Bak, Z. Bao, M. Forets, G. Frehse, D. Freire, N. Kochdumper,
Y. Li, S. Mitra, R. Ray, C. Schilling, S. Schupp, M. Wetzlinger, in:, EPiC Series
in Computing, EasyChair, 2020, pp. 16–48.
conference:
end_date: 2020-07-12
name: 'ARCH: International Workshop on Applied Verification on Continuous and Hybrid
Systems'
start_date: 2020-07-12
date_created: 2020-09-26T14:49:43Z
date_published: 2020-09-25T00:00:00Z
date_updated: 2021-01-12T08:20:06Z
day: '25'
department:
- _id: ToHe
doi: 10.29007/7dt2
ec_funded: 1
intvolume: ' 74'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://easychair.org/publications/download/DRpS
month: '09'
oa: 1
oa_version: Published Version
page: 16-48
project:
- _id: 25C5A090-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z00312
name: The Wittgenstein Prize
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: EPiC Series in Computing
publication_status: published
publisher: EasyChair
quality_controlled: '1'
status: public
title: 'ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 74
year: '2020'
...
---
_id: '8599'
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 study 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 show how minor changes in the
bidding mechanism lead to unexpected differences in the equivalence with random-turn
games.
acknowledgement: We 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.
alternative_title:
- LIPIcs
article_number: '2'
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. A survey of bidding games on graphs. In: 31st International
Conference on Concurrency Theory. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2020. doi:10.4230/LIPIcs.CONCUR.2020.2'
apa: 'Avni, G., & Henzinger, T. A. (2020). A survey of bidding games on graphs.
In 31st International Conference on Concurrency Theory (Vol. 171). Virtual:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2020.2'
chicago: Avni, Guy, and Thomas A Henzinger. “A Survey of Bidding Games on Graphs.”
In 31st International Conference on Concurrency Theory, Vol. 171. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CONCUR.2020.2.
ieee: G. Avni and T. A. Henzinger, “A survey of bidding games on graphs,” in 31st
International Conference on Concurrency Theory, Virtual, 2020, vol. 171.
ista: 'Avni G, Henzinger TA. 2020. A survey of bidding games on graphs. 31st International
Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs,
vol. 171, 2.'
mla: Avni, Guy, and Thomas A. Henzinger. “A Survey of Bidding Games on Graphs.”
31st International Conference on Concurrency Theory, vol. 171, 2, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.CONCUR.2020.2.
short: G. Avni, T.A. Henzinger, in:, 31st International Conference on Concurrency
Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
conference:
end_date: 2020-09-04
location: Virtual
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2020-09-01
date_created: 2020-10-04T22:01:36Z
date_published: 2020-08-06T00:00:00Z
date_updated: 2021-01-12T08:20:13Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2020.2
file:
- access_level: open_access
checksum: 8f33b098e73724e0ac817f764d8e1a2d
content_type: application/pdf
creator: dernst
date_created: 2020-10-05T14:13:19Z
date_updated: 2020-10-05T14:13:19Z
file_id: '8611'
file_name: 2020_LIPIcsCONCUR_Avni.pdf
file_size: 868510
relation: main_file
success: 1
file_date_updated: 2020-10-05T14:13:19Z
has_accepted_license: '1'
intvolume: ' 171'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 31st International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959771603'
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: A survey of bidding games on graphs
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 171
year: '2020'
...
---
_id: '8600'
abstract:
- lang: eng
text: 'A vector addition system with states (VASS) consists of a finite set of states
and counters. A transition changes the current state to the next state, and every
counter is either incremented, or decremented, or left unchanged. A state and
value for each counter is a configuration; and a computation is an infinite sequence
of configurations with transitions between successive configurations. A probabilistic
VASS consists of a VASS along with a probability distribution over the transitions
for each state. Qualitative properties such as state and configuration reachability
have been widely studied for VASS. In this work we consider multi-dimensional
long-run average objectives for VASS and probabilistic VASS. For a counter, the
cost of a configuration is the value of the counter; and the long-run average
value of a computation for the counter is the long-run average of the costs of
the configurations in the computation. The multi-dimensional long-run average
problem given a VASS and a threshold value for each counter, asks whether there
is a computation such that for each counter the long-run average value for the
counter does not exceed the respective threshold. For probabilistic VASS, instead
of the existence of a computation, we consider whether the expected long-run average
value for each counter does not exceed the respective threshold. Our main results
are as follows: we show that the multi-dimensional long-run average problem (a)
is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued
VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for
probabilistic integer-valued VASS, and probabilistic natural-valued VASS when
all computations are non-terminating.'
alternative_title:
- LIPIcs
article_number: '23'
article_processing_charge: No
arxiv: 1
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Chatterjee K, Henzinger TA, Otop J. Multi-dimensional long-run average problems
for vector addition systems with states. In: 31st International Conference
on Concurrency Theory. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2020. doi:10.4230/LIPIcs.CONCUR.2020.23'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2020). Multi-dimensional
long-run average problems for vector addition systems with states. In 31st
International Conference on Concurrency Theory (Vol. 171). Virtual: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2020.23'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Multi-Dimensional
Long-Run Average Problems for Vector Addition Systems with States.” In 31st
International Conference on Concurrency Theory, Vol. 171. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CONCUR.2020.23.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Multi-dimensional long-run average
problems for vector addition systems with states,” in 31st International Conference
on Concurrency Theory, Virtual, 2020, vol. 171.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2020. Multi-dimensional long-run average
problems for vector addition systems with states. 31st International Conference
on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol.
171, 23.'
mla: Chatterjee, Krishnendu, et al. “Multi-Dimensional Long-Run Average Problems
for Vector Addition Systems with States.” 31st International Conference on
Concurrency Theory, vol. 171, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2020, doi:10.4230/LIPIcs.CONCUR.2020.23.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, 31st International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
conference:
end_date: 2020-09-04
location: Virtual
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2020-09-01
date_created: 2020-10-04T22:01:36Z
date_published: 2020-08-06T00:00:00Z
date_updated: 2021-01-12T08:20:15Z
day: '06'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2020.23
external_id:
arxiv:
- '2007.08917'
file:
- access_level: open_access
checksum: 5039752f644c4b72b9361d21a5e31baf
content_type: application/pdf
creator: dernst
date_created: 2020-10-05T14:04:25Z
date_updated: 2020-10-05T14:04:25Z
file_id: '8610'
file_name: 2020_LIPIcsCONCUR_Chatterjee.pdf
file_size: 601231
relation: main_file
success: 1
file_date_updated: 2020-10-05T14:04:25Z
has_accepted_license: '1'
intvolume: ' 171'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 31st International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959771603'
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Multi-dimensional long-run average problems for vector addition systems with
states
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 171
year: '2020'
...
---
_id: '8623'
abstract:
- lang: eng
text: We introduce the monitoring of trace properties under assumptions. An assumption
limits the space of possible traces that the monitor may encounter. An assumption
may result from knowledge about the system that is being monitored, about the
environment, or about another, connected monitor. We define monitorability under
assumptions and study its theoretical properties. In particular, we show that
for every assumption A, the boolean combinations of properties that are safe or
co-safe relative to A are monitorable under A. We give several examples and constructions
on how an assumption can make a non-monitorable property monitorable, and how
an assumption can make a monitorable property monitorable with fewer resources,
such as integer registers.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award).
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: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Sarac NE. Monitorability under assumptions. In: Runtime Verification.
Vol 12399. Springer Nature; 2020:3-18. doi:10.1007/978-3-030-60508-7_1'
apa: 'Henzinger, T. A., & Sarac, N. E. (2020). Monitorability under assumptions.
In Runtime Verification (Vol. 12399, pp. 3–18). Los Angeles, CA, United
States: Springer Nature. https://doi.org/10.1007/978-3-030-60508-7_1'
chicago: Henzinger, Thomas A, and Naci E Sarac. “Monitorability under Assumptions.”
In Runtime Verification, 12399:3–18. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-60508-7_1.
ieee: T. A. Henzinger and N. E. Sarac, “Monitorability under assumptions,” in Runtime
Verification, Los Angeles, CA, United States, 2020, vol. 12399, pp. 3–18.
ista: 'Henzinger TA, Sarac NE. 2020. Monitorability under assumptions. Runtime Verification.
RV: Runtime Verification, LNCS, vol. 12399, 3–18.'
mla: Henzinger, Thomas A., and Naci E. Sarac. “Monitorability under Assumptions.”
Runtime Verification, vol. 12399, Springer Nature, 2020, pp. 3–18, doi:10.1007/978-3-030-60508-7_1.
short: T.A. Henzinger, N.E. Sarac, in:, Runtime Verification, Springer Nature, 2020,
pp. 3–18.
conference:
end_date: 2020-10-09
location: Los Angeles, CA, United States
name: 'RV: Runtime Verification'
start_date: 2020-10-06
date_created: 2020-10-07T15:05:37Z
date_published: 2020-10-02T00:00:00Z
date_updated: 2023-09-05T15:08:26Z
day: '02'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-60508-7_1
external_id:
isi:
- '000728160600001'
file:
- access_level: open_access
checksum: 00661f9b7034f52e18bf24fa552b8194
content_type: application/pdf
creator: esarac
date_created: 2020-10-15T14:28:06Z
date_updated: 2020-10-15T14:28:06Z
file_id: '8665'
file_name: monitorability.pdf
file_size: 478148
relation: main_file
success: 1
file_date_updated: 2020-10-15T14:28:06Z
has_accepted_license: '1'
intvolume: ' 12399'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 3-18
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030605070'
- '9783030605087'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitorability under assumptions
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12399
year: '2020'
...
---
_id: '8679'
abstract:
- lang: eng
text: A central goal of artificial intelligence in high-stakes decision-making applications
is to design a single algorithm that simultaneously expresses generalizability
by learning coherent representations of their world and interpretable explanations
of its dynamics. Here, we combine brain-inspired neural computation principles
and scalable deep learning architectures to design compact neural controllers
for task-specific compartments of a full-stack autonomous vehicle control system.
We discover that a single algorithm with 19 control neurons, connecting 32 encapsulated
input features to outputs by 253 synapses, learns to map high-dimensional inputs
into steering commands. This system shows superior generalizability, interpretability
and robustness compared with orders-of-magnitude larger black-box learning systems.
The obtained neural agents enable high-fidelity autonomy for task-specific parts
of a complex autonomous system.
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: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- 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
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: Lechner M, Hasani R, Amini A, Henzinger TA, Rus D, Grosu R. Neural circuit
policies enabling auditable autonomy. Nature Machine Intelligence. 2020;2:642-652.
doi:10.1038/s42256-020-00237-3
apa: Lechner, M., Hasani, R., Amini, A., Henzinger, T. A., Rus, D., & Grosu,
R. (2020). Neural circuit policies enabling auditable autonomy. Nature Machine
Intelligence. Springer Nature. https://doi.org/10.1038/s42256-020-00237-3
chicago: Lechner, Mathias, Ramin Hasani, Alexander Amini, Thomas A Henzinger, Daniela
Rus, and Radu Grosu. “Neural Circuit Policies Enabling Auditable Autonomy.” Nature
Machine Intelligence. Springer Nature, 2020. https://doi.org/10.1038/s42256-020-00237-3.
ieee: M. Lechner, R. Hasani, A. Amini, T. A. Henzinger, D. Rus, and R. Grosu, “Neural
circuit policies enabling auditable autonomy,” Nature Machine Intelligence,
vol. 2. Springer Nature, pp. 642–652, 2020.
ista: Lechner M, Hasani R, Amini A, Henzinger TA, Rus D, Grosu R. 2020. Neural circuit
policies enabling auditable autonomy. Nature Machine Intelligence. 2, 642–652.
mla: Lechner, Mathias, et al. “Neural Circuit Policies Enabling Auditable Autonomy.”
Nature Machine Intelligence, vol. 2, Springer Nature, 2020, pp. 642–52,
doi:10.1038/s42256-020-00237-3.
short: M. Lechner, R. Hasani, A. Amini, T.A. Henzinger, D. Rus, R. Grosu, Nature
Machine Intelligence 2 (2020) 642–652.
date_created: 2020-10-19T13:46:06Z
date_published: 2020-10-01T00:00:00Z
date_updated: 2023-08-22T10:36:06Z
day: '01'
department:
- _id: ToHe
doi: 10.1038/s42256-020-00237-3
external_id:
isi:
- '000583337200011'
intvolume: ' 2'
isi: 1
language:
- iso: eng
month: '10'
oa_version: None
page: 642-652
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Nature Machine Intelligence
publication_identifier:
eissn:
- 2522-5839
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
link:
- description: News on IST Homepage
relation: press_release
url: https://ist.ac.at/en/news/new-deep-learning-models/
scopus_import: '1'
status: public
title: Neural circuit policies enabling auditable autonomy
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 2
year: '2020'
...
---
_id: '8704'
abstract:
- lang: eng
text: Traditional robotic control suits require profound task-specific knowledge
for designing, building and testing control software. The rise of Deep Learning
has enabled end-to-end solutions to be learned entirely from data, requiring minimal
knowledge about the application area. We design a learning scheme to train end-to-end
linear dynamical systems (LDS)s by gradient descent in imitation learning robotic
domains. We introduce a new regularization loss component together with a learning
algorithm that improves the stability of the learned autonomous system, by forcing
the eigenvalues of the internal state updates of an LDS to be negative reals.
We evaluate our approach on a series of real-life and simulated robotic experiments,
in comparison to linear and nonlinear Recurrent Neural Network (RNN) architectures.
Our results show that our stabilizing method significantly improves test performance
of LDS, enabling such linear models to match the performance of contemporary nonlinear
RNN architectures. A video of the obstacle avoidance performance of our method
on a mobile robot, in unseen environments, compared to other methods can be viewed
at https://youtu.be/mhEsCoNao5E.
acknowledgement: M.L. is supported in parts by the Austrian Science Fund (FWF) under
grant Z211-N23 (Wittgenstein Award). R.H., and R.G. are partially supported by the
Horizon-2020 ECSELProject grant No. 783163 (iDev40), and the Austrian Research Promotion
Agency (FFG), Project No. 860424. R.H. and D.R. is partially supported by the Boeing
Company.
alternative_title:
- ICRA
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Lechner M, Hasani R, Rus D, Grosu R. Gershgorin loss stabilizes the recurrent
neural network compartment of an end-to-end robot learning scheme. In: Proceedings
- IEEE International Conference on Robotics and Automation. IEEE; 2020:5446-5452.
doi:10.1109/ICRA40945.2020.9196608'
apa: 'Lechner, M., Hasani, R., Rus, D., & Grosu, R. (2020). Gershgorin loss
stabilizes the recurrent neural network compartment of an end-to-end robot learning
scheme. In Proceedings - IEEE International Conference on Robotics and Automation
(pp. 5446–5452). Paris, France: IEEE. https://doi.org/10.1109/ICRA40945.2020.9196608'
chicago: Lechner, Mathias, Ramin Hasani, Daniela Rus, and Radu Grosu. “Gershgorin
Loss Stabilizes the Recurrent Neural Network Compartment of an End-to-End Robot
Learning Scheme.” In Proceedings - IEEE International Conference on Robotics
and Automation, 5446–52. IEEE, 2020. https://doi.org/10.1109/ICRA40945.2020.9196608.
ieee: M. Lechner, R. Hasani, D. Rus, and R. Grosu, “Gershgorin loss stabilizes the
recurrent neural network compartment of an end-to-end robot learning scheme,”
in Proceedings - IEEE International Conference on Robotics and Automation,
Paris, France, 2020, pp. 5446–5452.
ista: 'Lechner M, Hasani R, Rus D, Grosu R. 2020. Gershgorin loss stabilizes the
recurrent neural network compartment of an end-to-end robot learning scheme. Proceedings
- IEEE International Conference on Robotics and Automation. ICRA: International
Conference on Robotics and Automation, ICRA, , 5446–5452.'
mla: Lechner, Mathias, et al. “Gershgorin Loss Stabilizes the Recurrent Neural Network
Compartment of an End-to-End Robot Learning Scheme.” Proceedings - IEEE International
Conference on Robotics and Automation, IEEE, 2020, pp. 5446–52, doi:10.1109/ICRA40945.2020.9196608.
short: M. Lechner, R. Hasani, D. Rus, R. Grosu, in:, Proceedings - IEEE International
Conference on Robotics and Automation, IEEE, 2020, pp. 5446–5452.
conference:
end_date: 2020-08-31
location: Paris, France
name: 'ICRA: International Conference on Robotics and Automation'
start_date: 2020-05-31
date_created: 2020-10-25T23:01:19Z
date_published: 2020-05-01T00:00:00Z
date_updated: 2023-08-22T10:40:15Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/ICRA40945.2020.9196608
external_id:
isi:
- '000712319503110'
file:
- access_level: open_access
checksum: fccf7b986ac78046918a298cc6849a50
content_type: application/pdf
creator: dernst
date_created: 2020-11-06T10:58:49Z
date_updated: 2020-11-06T10:58:49Z
file_id: '8733'
file_name: 2020_ICRA_Lechner.pdf
file_size: 1070010
relation: main_file
success: 1
file_date_updated: 2020-11-06T10:58:49Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
page: 5446-5452
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings - IEEE International Conference on Robotics and Automation
publication_identifier:
isbn:
- '9781728173955'
issn:
- '10504729'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Gershgorin loss stabilizes the recurrent neural network compartment of an end-to-end
robot learning scheme
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2020'
...
---
_id: '8750'
abstract:
- lang: eng
text: "Efficiently handling time-triggered and possibly nondeterministic switches\r\nfor
hybrid systems reachability is a challenging task. In this paper we present\r\nan
approach based on conservative set-based enclosure of the dynamics that can\r\nhandle
systems with uncertain parameters and inputs, where the uncertainties\r\nare bound
to given intervals. The method is evaluated on the plant model of an\r\nexperimental
electro-mechanical braking system with periodic controller. In\r\nthis model,
the fast-switching controller dynamics requires simulation time\r\nscales of the
order of nanoseconds. Accurate set-based computations for\r\nrelatively large
time horizons are known to be expensive. However, by\r\nappropriately decoupling
the time variable with respect to the spatial\r\nvariables, and enclosing the
uncertain parameters using interval matrix maps\r\nacting on zonotopes, we show
that the computation time can be lowered to 5000\r\ntimes faster with respect
to previous works. This is a step forward in formal\r\nverification of hybrid
systems because reduced run-times allow engineers to\r\nintroduce more expressiveness
in their models with a relatively inexpensive\r\ncomputational cost."
article_number: '9314994'
article_processing_charge: No
arxiv: 1
author:
- first_name: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Daniel
full_name: Freire, Daniel
last_name: Freire
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Forets M, Freire D, Schilling C. Efficient reachability analysis of parametric
linear hybrid systems with time-triggered transitions. In: 18th ACM-IEEE International
Conference on Formal Methods and Models for System Design. IEEE; 2020. doi:10.1109/MEMOCODE51338.2020.9314994'
apa: 'Forets, M., Freire, D., & Schilling, C. (2020). Efficient reachability
analysis of parametric linear hybrid systems with time-triggered transitions.
In 18th ACM-IEEE International Conference on Formal Methods and Models for
System Design. Virtual Conference: IEEE. https://doi.org/10.1109/MEMOCODE51338.2020.9314994'
chicago: Forets, Marcelo, Daniel Freire, and Christian Schilling. “Efficient Reachability
Analysis of Parametric Linear Hybrid Systems with Time-Triggered Transitions.”
In 18th ACM-IEEE International Conference on Formal Methods and Models for
System Design. IEEE, 2020. https://doi.org/10.1109/MEMOCODE51338.2020.9314994.
ieee: M. Forets, D. Freire, and C. Schilling, “Efficient reachability analysis of
parametric linear hybrid systems with time-triggered transitions,” in 18th
ACM-IEEE International Conference on Formal Methods and Models for System Design,
Virtual Conference, 2020.
ista: 'Forets M, Freire D, Schilling C. 2020. Efficient reachability analysis of
parametric linear hybrid systems with time-triggered transitions. 18th ACM-IEEE
International Conference on Formal Methods and Models for System Design. MEMOCODE:
Conference on Formal Methods and Models for System Design, 9314994.'
mla: Forets, Marcelo, et al. “Efficient Reachability Analysis of Parametric Linear
Hybrid Systems with Time-Triggered Transitions.” 18th ACM-IEEE International
Conference on Formal Methods and Models for System Design, 9314994, IEEE,
2020, doi:10.1109/MEMOCODE51338.2020.9314994.
short: M. Forets, D. Freire, C. Schilling, in:, 18th ACM-IEEE International Conference
on Formal Methods and Models for System Design, IEEE, 2020.
conference:
end_date: 2020-12-04
location: Virtual Conference
name: 'MEMOCODE: Conference on Formal Methods and Models for System Design'
start_date: 2020-12-02
date_created: 2020-11-10T07:04:57Z
date_published: 2020-12-04T00:00:00Z
date_updated: 2023-08-22T12:48:18Z
day: '04'
department:
- _id: ToHe
doi: 10.1109/MEMOCODE51338.2020.9314994
ec_funded: 1
external_id:
arxiv:
- '2006.12325'
isi:
- '000661920400013'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2006.12325
month: '12'
oa: 1
oa_version: Preprint
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: 18th ACM-IEEE International Conference on Formal Methods and Models for
System Design
publication_identifier:
isbn:
- '9781728191485'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Efficient reachability analysis of parametric linear hybrid systems with time-triggered
transitions
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2020'
...
---
_id: '8790'
abstract:
- lang: eng
text: Reachability analysis aims at identifying states reachable by a system within
a given time horizon. This task is known to be computationally expensive for linear
hybrid systems. Reachability analysis works by iteratively applying continuous
and discrete post operators to compute states reachable according to continuous
and discrete dynamics, respectively. In this article, we enhance both of these
operators and make sure that most of the involved computations are performed in
low-dimensional state space. In particular, we improve the continuous-post operator
by performing computations in high-dimensional state space only for time intervals
relevant for the subsequent application of the discrete-post operator. Furthermore,
the new discrete-post operator performs low-dimensional computations by leveraging
the structure of the guard and assignment of a considered transition. We illustrate
the potential of our approach on a number of challenging benchmarks.
acknowledgement: 'This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), the
European Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie grant agreement No. 754411, and the Air Force Office of Scientific
Research under award number FA2386-17-1-4065. Any opinions, findings, and conclusions
or recommendations expressed in this material are those of the authors and do not
necessarily reflect the views of the United States Air Force. '
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Kostiantyn
full_name: Potomkin, Kostiantyn
last_name: Potomkin
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis
of linear hybrid systems via block decomposition. IEEE Transactions on Computer-Aided
Design of Integrated Circuits and Systems. 2020;39(11):4018-4029. doi:10.1109/TCAD.2020.3012859
apa: Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2020).
Reachability analysis of linear hybrid systems via block decomposition. IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems.
IEEE. https://doi.org/10.1109/TCAD.2020.3012859
chicago: Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and
Christian Schilling. “Reachability Analysis of Linear Hybrid Systems via Block
Decomposition.” IEEE Transactions on Computer-Aided Design of Integrated Circuits
and Systems. IEEE, 2020. https://doi.org/10.1109/TCAD.2020.3012859.
ieee: S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “Reachability
analysis of linear hybrid systems via block decomposition,” IEEE Transactions
on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, no.
11. IEEE, pp. 4018–4029, 2020.
ista: Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2020. Reachability
analysis of linear hybrid systems via block decomposition. IEEE Transactions on
Computer-Aided Design of Integrated Circuits and Systems. 39(11), 4018–4029.
mla: Bogomolov, Sergiy, et al. “Reachability Analysis of Linear Hybrid Systems via
Block Decomposition.” IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems, vol. 39, no. 11, IEEE, 2020, pp. 4018–29, doi:10.1109/TCAD.2020.3012859.
short: S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, IEEE Transactions
on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 4018–4029.
date_created: 2020-11-22T23:01:25Z
date_published: 2020-11-01T00:00:00Z
date_updated: 2023-08-22T13:27:33Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/TCAD.2020.3012859
ec_funded: 1
external_id:
arxiv:
- '1905.02458'
isi:
- '000587712700072'
intvolume: ' 39'
isi: 1
issue: '11'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1905.02458
month: '11'
oa: 1
oa_version: Preprint
page: 4018-4029
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: IEEE Transactions on Computer-Aided Design of Integrated Circuits and
Systems
publication_identifier:
eissn:
- '19374151'
issn:
- '02780070'
publication_status: published
publisher: IEEE
quality_controlled: '1'
related_material:
record:
- id: '8287'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Reachability analysis of linear hybrid systems via block decomposition
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 39
year: '2020'
...
---
_id: '9040'
abstract:
- lang: eng
text: Machine learning and formal methods have complimentary benefits and drawbacks.
In this work, we address the controller-design problem with a combination of techniques
from both fields. The use of black-box neural networks in deep reinforcement learning
(deep RL) poses a challenge for such a combination. Instead of reasoning formally
about the output of deep RL, which we call the wizard, we extract from it a decision-tree
based model, which we refer to as the magic book. Using the extracted model as
an intermediary, we are able to handle problems that are infeasible for either
deep RL or formal methods by themselves. First, we suggest, for the first time,
a synthesis procedure that is based on a magic book. We synthesize a stand-alone
correct-by-design controller that enjoys the favorable performance of RL. Second,
we incorporate a magic book in a bounded model checking (BMC) procedure. BMC allows
us to find numerous traces of the plant under the control of the wizard, which
a user can use to increase the trustworthiness of the wizard and direct further
training.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award).
article_processing_charge: No
author:
- first_name: Par Alizadeh
full_name: Alamdari, Par Alizadeh
last_name: Alamdari
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Anna
full_name: Lukina, Anna
id: CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425
last_name: Lukina
citation:
ama: 'Alamdari PA, Avni G, Henzinger TA, Lukina A. Formal methods with a touch of
magic. In: Proceedings of the 20th Conference on Formal Methods in Computer-Aided
Design. TU Wien Academic Press; 2020:138-147. doi:10.34727/2020/isbn.978-3-85448-042-6_21'
apa: 'Alamdari, P. A., Avni, G., Henzinger, T. A., & Lukina, A. (2020). Formal
methods with a touch of magic. In Proceedings of the 20th Conference on Formal
Methods in Computer-Aided Design (pp. 138–147). Online Conference: TU Wien
Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21'
chicago: Alamdari, Par Alizadeh, Guy Avni, Thomas A Henzinger, and Anna Lukina.
“Formal Methods with a Touch of Magic.” In Proceedings of the 20th Conference
on Formal Methods in Computer-Aided Design, 138–47. TU Wien Academic Press,
2020. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21.
ieee: P. A. Alamdari, G. Avni, T. A. Henzinger, and A. Lukina, “Formal methods with
a touch of magic,” in Proceedings of the 20th Conference on Formal Methods
in Computer-Aided Design, Online Conference, 2020, pp. 138–147.
ista: 'Alamdari PA, Avni G, Henzinger TA, Lukina A. 2020. Formal methods with a
touch of magic. Proceedings of the 20th Conference on Formal Methods in Computer-Aided
Design. FMCAD: Formal Methods in Computer-Aided Design, 138–147.'
mla: Alamdari, Par Alizadeh, et al. “Formal Methods with a Touch of Magic.” Proceedings
of the 20th Conference on Formal Methods in Computer-Aided Design, TU Wien
Academic Press, 2020, pp. 138–47, doi:10.34727/2020/isbn.978-3-85448-042-6_21.
short: P.A. Alamdari, G. Avni, T.A. Henzinger, A. Lukina, in:, Proceedings of the
20th Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press,
2020, pp. 138–147.
conference:
end_date: 2020-09-24
location: Online Conference
name: ' FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2020-09-21
date_created: 2021-01-24T23:01:10Z
date_published: 2020-09-21T00:00:00Z
date_updated: 2021-02-09T09:39:59Z
day: '21'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.34727/2020/isbn.978-3-85448-042-6_21
file:
- access_level: open_access
checksum: d616d549a0ade78606b16f8a9540820f
content_type: application/pdf
creator: dernst
date_created: 2021-02-09T09:39:02Z
date_updated: 2021-02-09T09:39:02Z
file_id: '9109'
file_name: 2020_FMCAD_Alamdari.pdf
file_size: 990999
relation: main_file
success: 1
file_date_updated: 2021-02-09T09:39:02Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 138-147
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 20th Conference on Formal Methods in Computer-Aided
Design
publication_identifier:
eissn:
- 2708-7824
isbn:
- '9783854480426'
publication_status: published
publisher: TU Wien Academic Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Formal methods with a touch of magic
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: '2020'
...
---
_id: '9103'
abstract:
- lang: eng
text: 'We introduce LRT-NG, a set of techniques and an associated toolset that computes
a reachtube (an over-approximation of the set of reachable states over a given
time horizon) of a nonlinear dynamical system. LRT-NG significantly advances the
state-of-the-art Langrangian Reachability and its associated tool LRT. From a
theoretical perspective, LRT-NG is superior to LRT in three ways. First, it uses
for the first time an analytically computed metric for the propagated ball which
is proven to minimize the ball’s volume. We emphasize that the metric computation
is the centerpiece of all bloating-based techniques. Secondly, it computes the
next reachset as the intersection of two balls: one based on the Cartesian metric
and the other on the new metric. While the two metrics were previously considered
opposing approaches, their joint use considerably tightens the reachtubes. Thirdly,
it avoids the "wrapping effect" associated with the validated integration of the
center of the reachset, by optimally absorbing the interval approximation in the
radius of the next ball. From a tool-development perspective, LRT-NG is superior
to LRT in two ways. First, it is a standalone tool that no longer relies on CAPD.
This required the implementation of the Lohner method and a Runge-Kutta time-propagation
method. Secondly, it has an improved interface, allowing the input model and initial
conditions to be provided as external input files. Our experiments on a comprehensive
set of benchmarks, including two Neural ODEs, demonstrates LRT-NG’s superior performance
compared to LRT, CAPD, and Flow*.'
acknowledgement: "The authors would like to thank Ramin Hasani and Guillaume Berger
for intellectual discussions about the research which lead to the generation of
new ideas. ML was supported in part by the Austrian Science Fund (FWF) under grant
Z211-N23 (Wittgenstein Award). Smolka’s research was supported by NSF grants CPS-1446832
and CCF-1918225. Gruenbacher is funded by FWF project W1255-N23. JC was partially
supported by NAWA Polish Returns grant\r\nPPN/PPO/2018/1/00029.\r\n"
article_processing_charge: No
arxiv: 1
author:
- first_name: Sophie
full_name: Gruenbacher, Sophie
last_name: Gruenbacher
- first_name: Jacek
full_name: Cyranka, Jacek
last_name: Cyranka
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Md Ariful
full_name: Islam, Md Ariful
last_name: Islam
- 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 S, Cyranka J, Lechner M, Islam MA, Smolka SA, Grosu R. Lagrangian
reachtubes: The next generation. In: Proceedings of the 59th IEEE Conference
on Decision and Control. Vol 2020. IEEE; 2020:1556-1563. doi:10.1109/CDC42340.2020.9304042'
apa: 'Gruenbacher, S., Cyranka, J., Lechner, M., Islam, M. A., Smolka, S. A., &
Grosu, R. (2020). Lagrangian reachtubes: The next generation. In Proceedings
of the 59th IEEE Conference on Decision and Control (Vol. 2020, pp. 1556–1563).
Jeju Islang, Korea (South): IEEE. https://doi.org/10.1109/CDC42340.2020.9304042'
chicago: 'Gruenbacher, Sophie, Jacek Cyranka, Mathias Lechner, Md Ariful Islam,
Scott A. Smolka, and Radu Grosu. “Lagrangian Reachtubes: The next Generation.”
In Proceedings of the 59th IEEE Conference on Decision and Control, 2020:1556–63.
IEEE, 2020. https://doi.org/10.1109/CDC42340.2020.9304042.'
ieee: 'S. Gruenbacher, J. Cyranka, M. Lechner, M. A. Islam, S. A. Smolka, and R.
Grosu, “Lagrangian reachtubes: The next generation,” in Proceedings of the
59th IEEE Conference on Decision and Control, Jeju Islang, Korea (South),
2020, vol. 2020, pp. 1556–1563.'
ista: 'Gruenbacher S, Cyranka J, Lechner M, Islam MA, Smolka SA, Grosu R. 2020.
Lagrangian reachtubes: The next generation. Proceedings of the 59th IEEE Conference
on Decision and Control. CDC: Conference on Decision and Control vol. 2020, 1556–1563.'
mla: 'Gruenbacher, Sophie, et al. “Lagrangian Reachtubes: The next Generation.”
Proceedings of the 59th IEEE Conference on Decision and Control, vol. 2020,
IEEE, 2020, pp. 1556–63, doi:10.1109/CDC42340.2020.9304042.'
short: S. Gruenbacher, J. Cyranka, M. Lechner, M.A. Islam, S.A. Smolka, R. Grosu,
in:, Proceedings of the 59th IEEE Conference on Decision and Control, IEEE, 2020,
pp. 1556–1563.
conference:
end_date: 2020-12-18
location: Jeju Islang, Korea (South)
name: 'CDC: Conference on Decision and Control'
start_date: 2020-12-14
date_created: 2021-02-07T23:01:14Z
date_published: 2020-12-14T00:00:00Z
date_updated: 2021-02-09T09:20:58Z
day: '14'
department:
- _id: ToHe
doi: 10.1109/CDC42340.2020.9304042
external_id:
arxiv:
- '2012.07458'
intvolume: ' 2020'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2012.07458
month: '12'
oa: 1
oa_version: Preprint
page: 1556-1563
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 59th IEEE Conference on Decision and Control
publication_identifier:
isbn:
- '9781728174471'
issn:
- '07431546'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Lagrangian reachtubes: The next generation'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2020
year: '2020'
...