---
_id: '10667'
abstract:
- lang: eng
text: Bayesian neural networks (BNNs) place distributions over the weights of a
neural network to model uncertainty in the data and the network's prediction.
We consider the problem of verifying safety when running a Bayesian neural network
policy in a feedback loop with infinite time horizon systems. Compared to the
existing sampling-based approaches, which are inapplicable to the infinite time
horizon setting, we train a separate deterministic neural network that serves
as an infinite time horizon safety certificate. In particular, we show that the
certificate network guarantees the safety of the system over a subset of the BNN
weight posterior's support. Our method first computes a safe weight set and then
alters the BNN's weight posterior to reject samples outside this set. Moreover,
we show how to extend our approach to a safe-exploration reinforcement learning
setting, in order to avoid unsafe trajectories during the training of the policy.
We evaluate our approach on a series of reinforcement learning benchmarks, including
non-Lyapunovian safety specifications.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and
the European Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- ' Advances in Neural Information Processing Systems'
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Ðorđe
full_name: Žikelić, Ðorđe
last_name: Žikelić
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. Infinite time horizon safety
of Bayesian neural networks. In: 35th Conference on Neural Information Processing
Systems. ; 2021. doi:10.48550/arXiv.2111.03165'
apa: Lechner, M., Žikelić, Ð., Chatterjee, K., & Henzinger, T. A. (2021). Infinite
time horizon safety of Bayesian neural networks. In 35th Conference on Neural
Information Processing Systems. Virtual. https://doi.org/10.48550/arXiv.2111.03165
chicago: Lechner, Mathias, Ðorđe Žikelić, Krishnendu Chatterjee, and Thomas A Henzinger.
“Infinite Time Horizon Safety of Bayesian Neural Networks.” In 35th Conference
on Neural Information Processing Systems, 2021. https://doi.org/10.48550/arXiv.2111.03165.
ieee: M. Lechner, Ð. Žikelić, K. Chatterjee, and T. A. Henzinger, “Infinite time
horizon safety of Bayesian neural networks,” in 35th Conference on Neural Information
Processing Systems, Virtual, 2021.
ista: 'Lechner M, Žikelić Ð, Chatterjee K, Henzinger TA. 2021. Infinite time horizon
safety of Bayesian neural networks. 35th Conference on Neural Information Processing
Systems. NeurIPS: Neural Information Processing Systems, Advances in Neural Information
Processing Systems, .'
mla: Lechner, Mathias, et al. “Infinite Time Horizon Safety of Bayesian Neural Networks.”
35th Conference on Neural Information Processing Systems, 2021, doi:10.48550/arXiv.2111.03165.
short: M. Lechner, Ð. Žikelić, K. Chatterjee, T.A. Henzinger, in:, 35th Conference
on Neural Information Processing Systems, 2021.
conference:
end_date: 2021-12-10
location: Virtual
name: 'NeurIPS: Neural Information Processing Systems'
start_date: 2021-12-06
date_created: 2022-01-25T15:45:58Z
date_published: 2021-12-01T00:00:00Z
date_updated: 2023-06-23T07:01:11Z
day: '01'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
- _id: KrCh
doi: 10.48550/arXiv.2111.03165
ec_funded: 1
external_id:
arxiv:
- '2111.03165'
file:
- access_level: open_access
checksum: 0fc0f852525c10dda9cc9ffea07fb4e4
content_type: application/pdf
creator: mlechner
date_created: 2022-01-26T07:39:59Z
date_updated: 2022-01-26T07:39:59Z
file_id: '10682'
file_name: infinite_time_horizon_safety_o.pdf
file_size: 452492
relation: main_file
success: 1
file_date_updated: 2022-01-26T07:39:59Z
has_accepted_license: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/3.0/
main_file_link:
- open_access: '1'
url: https://proceedings.neurips.cc/paper/2021/hash/544defa9fddff50c53b71c43e0da72be-Abstract.html
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 35th Conference on Neural Information Processing Systems
publication_status: published
quality_controlled: '1'
related_material:
record:
- id: '11362'
relation: dissertation_contains
status: public
status: public
title: Infinite time horizon safety of Bayesian neural networks
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND
3.0)
short: CC BY-NC-ND (3.0)
type: conference
user_id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
year: '2021'
...
---
_id: '8912'
abstract:
- lang: eng
text: "For automata, synchronization, the problem of bringing an automaton to a
particular state regardless of its initial state, is important. It has several
applications in practice and is related to a fifty-year-old conjecture on the
length of the shortest synchronizing word. Although using shorter words increases
the effectiveness in practice, finding a shortest one (which is not necessarily
unique) is NP-hard. For this reason, there exist various heuristics in the literature.
However, high-quality heuristics such as SynchroP producing relatively shorter
sequences are very expensive and can take hours when the automaton has tens of
thousands of states. The SynchroP heuristic has been frequently used as a benchmark
to evaluate the performance of the new heuristics. In this work, we first improve
the runtime of SynchroP and its variants by using algorithmic techniques. We then
focus on adapting SynchroP for many-core architectures,\r\nand overall, we obtain
more than 1000× speedup on GPUs compared to naive sequential implementation that
has been frequently used as a benchmark to evaluate new heuristics in the literature.
We also propose two SynchroP variants and evaluate their performance."
acknowledgement: This work was supported by The Scientific and Technological Research
Council of Turkey (TUBITAK) [grant number 114E569]. This research was supported
in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).
We would like to thank the authors of (Roman & Szykula, 2015) for providing their
heuristics implementations, which we used to compare our SynchroP implementation
as given in Table 11.
article_number: '114203'
article_processing_charge: No
article_type: original
author:
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
- first_name: Ömer Faruk
full_name: Altun, Ömer Faruk
last_name: Altun
- first_name: Kamil Tolga
full_name: Atam, Kamil Tolga
last_name: Atam
- first_name: Sertac
full_name: Karahoda, Sertac
last_name: Karahoda
- first_name: Kamer
full_name: Kaya, Kamer
last_name: Kaya
- first_name: Hüsnü
full_name: Yenigün, Hüsnü
last_name: Yenigün
citation:
ama: Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. Boosting expensive
synchronizing heuristics. Expert Systems with Applications. 2021;167(4).
doi:10.1016/j.eswa.2020.114203
apa: Sarac, N. E., Altun, Ö. F., Atam, K. T., Karahoda, S., Kaya, K., & Yenigün,
H. (2021). Boosting expensive synchronizing heuristics. Expert Systems with
Applications. Elsevier. https://doi.org/10.1016/j.eswa.2020.114203
chicago: Sarac, Naci E, Ömer Faruk Altun, Kamil Tolga Atam, Sertac Karahoda, Kamer
Kaya, and Hüsnü Yenigün. “Boosting Expensive Synchronizing Heuristics.” Expert
Systems with Applications. Elsevier, 2021. https://doi.org/10.1016/j.eswa.2020.114203.
ieee: N. E. Sarac, Ö. F. Altun, K. T. Atam, S. Karahoda, K. Kaya, and H. Yenigün,
“Boosting expensive synchronizing heuristics,” Expert Systems with Applications,
vol. 167, no. 4. Elsevier, 2021.
ista: Sarac NE, Altun ÖF, Atam KT, Karahoda S, Kaya K, Yenigün H. 2021. Boosting
expensive synchronizing heuristics. Expert Systems with Applications. 167(4),
114203.
mla: Sarac, Naci E., et al. “Boosting Expensive Synchronizing Heuristics.” Expert
Systems with Applications, vol. 167, no. 4, 114203, Elsevier, 2021, doi:10.1016/j.eswa.2020.114203.
short: N.E. Sarac, Ö.F. Altun, K.T. Atam, S. Karahoda, K. Kaya, H. Yenigün, Expert
Systems with Applications 167 (2021).
date_created: 2020-12-02T13:34:25Z
date_published: 2021-04-01T00:00:00Z
date_updated: 2023-08-04T11:19:00Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.eswa.2020.114203
external_id:
isi:
- '000640531100038'
file:
- access_level: open_access
checksum: 600c2f81bc898a725bcfa7cf26ff4fed
content_type: application/pdf
creator: esarac
date_created: 2020-12-02T13:33:51Z
date_updated: 2020-12-02T13:33:51Z
file_id: '8913'
file_name: synchroPaperRevised.pdf
file_size: 634967
relation: main_file
file_date_updated: 2020-12-02T13:33:51Z
has_accepted_license: '1'
intvolume: ' 167'
isi: 1
issue: '4'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Expert Systems with Applications
publication_identifier:
issn:
- '09574174'
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Boosting expensive synchronizing heuristics
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 167
year: '2021'
...
---
_id: '9200'
abstract:
- lang: eng
text: Formal design of embedded and cyber-physical systems relies on mathematical
modeling. In this paper, we consider the model class of hybrid automata whose
dynamics are defined by affine differential equations. Given a set of time-series
data, we present an algorithmic approach to synthesize a hybrid automaton exhibiting
behavior that is close to the data, up to a specified precision, and changes in
synchrony with the data. A fundamental problem in our synthesis algorithm is to
check membership of a time series in a hybrid automaton. Our solution integrates
reachability and optimization techniques for affine dynamical systems to obtain
both a sufficient and a necessary condition for membership, combined in a refinement
framework. The algorithm processes one time series at a time and hence can be
interrupted, provide an intermediate result, and be resumed. We report experimental
results demonstrating the applicability of our synthesis approach.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award) and the European Union’s Horizon
2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement
No. 754411.
article_processing_charge: No
author:
- first_name: Miriam
full_name: Garcia Soto, Miriam
id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
last_name: Garcia Soto
orcid: 0000-0003-2936-5719
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Garcia Soto M, Henzinger TA, Schilling C. Synthesis of hybrid automata with
affine dynamics from time-series data. In: HSCC ’21: Proceedings of the 24th
International Conference on Hybrid Systems: Computation and Control. Association
for Computing Machinery; 2021:2102.12734. doi:10.1145/3447928.3456704'
apa: 'Garcia Soto, M., Henzinger, T. A., & Schilling, C. (2021). Synthesis of
hybrid automata with affine dynamics from time-series data. In HSCC ’21: Proceedings
of the 24th International Conference on Hybrid Systems: Computation and Control
(p. 2102.12734). Nashville, TN, United States: Association for Computing Machinery.
https://doi.org/10.1145/3447928.3456704'
chicago: 'Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis
of Hybrid Automata with Affine Dynamics from Time-Series Data.” In HSCC ’21:
Proceedings of the 24th International Conference on Hybrid Systems: Computation
and Control, 2102.12734. Association for Computing Machinery, 2021. https://doi.org/10.1145/3447928.3456704.'
ieee: 'M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of hybrid automata
with affine dynamics from time-series data,” in HSCC ’21: Proceedings of the
24th International Conference on Hybrid Systems: Computation and Control,
Nashville, TN, United States, 2021, p. 2102.12734.'
ista: 'Garcia Soto M, Henzinger TA, Schilling C. 2021. Synthesis of hybrid automata
with affine dynamics from time-series data. HSCC ’21: Proceedings of the 24th
International Conference on Hybrid Systems: Computation and Control. HSCC: International
Conference on Hybrid Systems Computation and Control, 2102.12734.'
mla: 'Garcia Soto, Miriam, et al. “Synthesis of Hybrid Automata with Affine Dynamics
from Time-Series Data.” HSCC ’21: Proceedings of the 24th International Conference
on Hybrid Systems: Computation and Control, Association for Computing Machinery,
2021, p. 2102.12734, doi:10.1145/3447928.3456704.'
short: 'M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, HSCC ’21: Proceedings
of the 24th International Conference on Hybrid Systems: Computation and Control,
Association for Computing Machinery, 2021, p. 2102.12734.'
conference:
end_date: 2021-05-21
location: Nashville, TN, United States
name: 'HSCC: International Conference on Hybrid Systems Computation and Control'
start_date: 2021-05-19
date_created: 2021-02-26T16:30:39Z
date_published: 2021-05-01T00:00:00Z
date_updated: 2023-08-07T13:49:33Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3447928.3456704
ec_funded: 1
external_id:
arxiv:
- '2102.12734'
isi:
- '000932821700028'
file:
- access_level: open_access
checksum: 4c1202c1abf71384c3ee6fea88c2f80e
content_type: application/pdf
creator: kschuh
date_created: 2021-05-25T13:53:22Z
date_updated: 2021-05-25T13:53:22Z
file_id: '9424'
file_name: 2021_HSCC_Soto.pdf
file_size: 1474786
relation: main_file
success: 1
file_date_updated: 2021-05-25T13:53:22Z
has_accepted_license: '1'
isi: 1
keyword:
- hybrid automaton
- membership
- system identification
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: '2102.12734'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: 'HSCC ''21: Proceedings of the 24th International Conference on Hybrid
Systems: Computation and Control'
publication_identifier:
isbn:
- '9781450383394'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of hybrid automata with affine dynamics from time-series data
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '9239'
abstract:
- lang: eng
text: 'A graph game proceeds as follows: two players move a token through a graph
to produce a finite or infinite path, which determines the payoff of the game.
We study bidding games in which in each turn, an auction determines which player
moves the token. Bidding games were largely studied in combination with two variants
of first-price auctions called “Richman” and “poorman” bidding. We study taxman
bidding, which span the spectrum between the two. The game is parameterized by
a constant : portion τ of the winning bid is paid to the other player, and portion to
the bank. While finite-duration (reachability) taxman games have been studied
before, we present, for the first time, results on infinite-duration taxman games:
we unify, generalize, and simplify previous equivalences between bidding games
and a class of stochastic games called random-turn games.'
article_processing_charge: No
article_type: original
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Đorđe
full_name: Žikelić, Đorđe
last_name: Žikelić
citation:
ama: Avni G, Henzinger TA, Žikelić Đ. Bidding mechanisms in graph games. Journal
of Computer and System Sciences. 2021;119(8):133-144. doi:10.1016/j.jcss.2021.02.008
apa: Avni, G., Henzinger, T. A., & Žikelić, Đ. (2021). Bidding mechanisms in
graph games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2021.02.008
chicago: Avni, Guy, Thomas A Henzinger, and Đorđe Žikelić. “Bidding Mechanisms in
Graph Games.” Journal of Computer and System Sciences. Elsevier, 2021.
https://doi.org/10.1016/j.jcss.2021.02.008.
ieee: G. Avni, T. A. Henzinger, and Đ. Žikelić, “Bidding mechanisms in graph games,”
Journal of Computer and System Sciences, vol. 119, no. 8. Elsevier, pp.
133–144, 2021.
ista: Avni G, Henzinger TA, Žikelić Đ. 2021. Bidding mechanisms in graph games.
Journal of Computer and System Sciences. 119(8), 133–144.
mla: Avni, Guy, et al. “Bidding Mechanisms in Graph Games.” Journal of Computer
and System Sciences, vol. 119, no. 8, Elsevier, 2021, pp. 133–44, doi:10.1016/j.jcss.2021.02.008.
short: G. Avni, T.A. Henzinger, Đ. Žikelić, Journal of Computer and System Sciences
119 (2021) 133–144.
date_created: 2021-03-14T23:01:32Z
date_published: 2021-03-03T00:00:00Z
date_updated: 2023-08-07T14:08:34Z
day: '03'
department:
- _id: ToHe
doi: 10.1016/j.jcss.2021.02.008
external_id:
arxiv:
- '1905.03835'
isi:
- '000634149800009'
intvolume: ' 119'
isi: 1
issue: '8'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.1905.03835
month: '03'
oa: 1
oa_version: Preprint
page: 133-144
publication: Journal of Computer and System Sciences
publication_identifier:
eissn:
- 1090-2724
issn:
- 0022-0000
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '6884'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Bidding mechanisms in graph games
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 119
year: '2021'
...
---
_id: '9356'
abstract:
- lang: eng
text: 'In runtime verification, a monitor watches a trace of a system and, if possible,
decides after observing each finite prefix whether or not the unknown infinite
trace satisfies a given specification. We generalize the theory of runtime verification
to monitors that attempt to estimate numerical values of quantitative trace properties
(instead of attempting to conclude boolean values of trace specifications), such
as maximal or average response time along a trace. Quantitative monitors are approximate:
with every finite prefix, they can improve their estimate of the infinite trace''s
unknown property value. Consequently, quantitative monitors can be compared with
regard to a precision-cost trade-off: better approximations of the property value
require more monitor resources, such as states (in the case of finite-state monitors)
or registers, and additional resources yield better approximations. We introduce
a formal framework for quantitative and approximate monitoring, show how it conservatively
generalizes the classical boolean setting for monitoring, and give several precision-cost
trade-offs for monitors. For example, we prove that there are quantitative properties
for which every additional register improves monitoring precision.'
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23
(Wittgenstein Award).
article_number: '9470547'
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Sarac NE. Quantitative and approximate monitoring. In: Proceedings
of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. Institute
of Electrical and Electronics Engineers; 2021. doi:10.1109/LICS52264.2021.9470547'
apa: 'Henzinger, T. A., & Sarac, N. E. (2021). Quantitative and approximate
monitoring. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in
Computer Science. Online: Institute of Electrical and Electronics Engineers.
https://doi.org/10.1109/LICS52264.2021.9470547'
chicago: Henzinger, Thomas A, and Naci E Sarac. “Quantitative and Approximate Monitoring.”
In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science.
Institute of Electrical and Electronics Engineers, 2021. https://doi.org/10.1109/LICS52264.2021.9470547.
ieee: T. A. Henzinger and N. E. Sarac, “Quantitative and approximate monitoring,”
in Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science,
Online, 2021.
ista: 'Henzinger TA, Sarac NE. 2021. Quantitative and approximate monitoring. Proceedings
of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium
on Logic in Computer Science, 9470547.'
mla: Henzinger, Thomas A., and Naci E. Sarac. “Quantitative and Approximate Monitoring.”
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science,
9470547, Institute of Electrical and Electronics Engineers, 2021, doi:10.1109/LICS52264.2021.9470547.
short: T.A. Henzinger, N.E. Sarac, in:, Proceedings of the 36th Annual ACM/IEEE
Symposium on Logic in Computer Science, Institute of Electrical and Electronics
Engineers, 2021.
conference:
end_date: 2021-07-02
location: Online
name: 'LICS: Symposium on Logic in Computer Science'
start_date: 2021-06-29
date_created: 2021-04-30T17:30:47Z
date_published: 2021-06-29T00:00:00Z
date_updated: 2023-08-08T13:52:56Z
day: '29'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1109/LICS52264.2021.9470547
external_id:
arxiv:
- '2105.08353'
isi:
- '000947350400021'
file:
- access_level: open_access
checksum: 6e4cba3f72775f479c5b1b75d1a4a0c4
content_type: application/pdf
creator: esarac
date_created: 2021-06-16T08:23:54Z
date_updated: 2021-06-16T08:23:54Z
file_id: '9557'
file_name: qam.pdf
file_size: 641990
relation: main_file
success: 1
file_date_updated: 2021-06-16T08:23:54Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
Science
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative and approximate monitoring
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '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
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
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: '10108'
abstract:
- lang: eng
text: We argue that the time is ripe to investigate differential monitoring, in
which the specification of a program's behavior is implicitly given by a second
program implementing the same informal specification. Similar ideas have been
proposed before, and are currently implemented in restricted form for testing
and specialized run-time analyses, aspects of which we combine. We discuss the
challenges of implementing differential monitoring as a general-purpose, black-box
run-time monitoring framework, and present promising results of a preliminary
implementation, showing low monitoring overheads for diverse programs.
acknowledgement: The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer,
Adrian Francalanza, Owolabi Legunsen, Mae Milano, Manuel Rigger, Cesar Sanchez,
and the members of the IST Verification Seminar for their helpful comments and insights
on various stages of this work, as well as the reviewers of RV’21 for their helpful
suggestions on the actual paper.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Mühlböck F, Henzinger TA. Differential monitoring. In: International Conference
on Runtime Verification. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:10.1007/978-3-030-88494-9_12'
apa: 'Mühlböck, F., & Henzinger, T. A. (2021). Differential monitoring. In International
Conference on Runtime Verification (Vol. 12974, pp. 231–243). Cham: Springer
Nature. https://doi.org/10.1007/978-3-030-88494-9_12'
chicago: 'Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In
International Conference on Runtime Verification, 12974:231–43. Cham: Springer
Nature, 2021. https://doi.org/10.1007/978-3-030-88494-9_12.'
ieee: F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in International
Conference on Runtime Verification, Virtual, 2021, vol. 12974, pp. 231–243.
ista: 'Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference
on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 231–243.'
mla: Mühlböck, Fabian, and Thomas A. Henzinger. “Differential Monitoring.” International
Conference on Runtime Verification, vol. 12974, Springer Nature, 2021, pp.
231–43, doi:10.1007/978-3-030-88494-9_12.
short: F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification,
Springer Nature, Cham, 2021, pp. 231–243.
conference:
end_date: 2021-10-14
location: Virtual
name: 'RV: Runtime Verification'
start_date: 2021-10-11
date_created: 2021-10-07T23:30:10Z
date_published: 2021-10-06T00:00:00Z
date_updated: 2023-08-14T07:20:30Z
day: '06'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-030-88494-9_12
external_id:
isi:
- '000719383800012'
file:
- access_level: open_access
checksum: 554c7fdb259eda703a8b6328a6dad55a
content_type: application/pdf
creator: fmuehlbo
date_created: 2021-10-07T23:32:18Z
date_updated: 2021-10-07T23:32:18Z
file_id: '10109'
file_name: differentialmonitoring-cameraready-openaccess.pdf
file_size: 350632
relation: main_file
success: 1
file_date_updated: 2021-10-07T23:32:18Z
has_accepted_license: '1'
intvolume: ' 12974'
isi: 1
keyword:
- run-time verification
- software engineering
- implicit specification
language:
- iso: eng
month: '10'
oa: 1
oa_version: Preprint
page: 231-243
place: Cham
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: International Conference on Runtime Verification
publication_identifier:
eisbn:
- 978-3-030-88494-9
eissn:
- 1611-3349
isbn:
- 978-3-030-88493-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '9946'
relation: extended_version
status: public
scopus_import: '1'
status: public
title: Differential monitoring
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 12974
year: '2021'
...
---
_id: '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: '10404'
abstract:
- lang: eng
text: While convolutional neural networks (CNNs) have found wide adoption as state-of-the-art
models for image-related tasks, their predictions are often highly sensitive to
small input perturbations, which the human vision is robust against. This paper
presents Perturber, a web-based application that allows users to instantaneously
explore how CNN activations and predictions evolve when a 3D input scene is interactively
perturbed. Perturber offers a large variety of scene modifications, such as camera
controls, lighting and shading effects, background modifications, object morphing,
as well as adversarial attacks, to facilitate the discovery of potential vulnerabilities.
Fine-tuned model versions can be directly compared for qualitative evaluation
of their robustness. Case studies with machine learning experts have shown that
Perturber helps users to quickly generate hypotheses about model vulnerabilities
and to qualitatively compare model behavior. Using quantitative analyses, we could
replicate users’ insights with other CNN architectures and input images, yielding
new insights about the vulnerability of adversarially trained models.
acknowledgement: "We thank Robert Geirhos and Roland Zimmermann for their participation
in the case study and valuable feedback, Chris Olah and Nick Cammarata for valuable
discussions in the early phase of the project, as well as the Distill Slack workspace
as a platform for discussions. M.L. is supported in part by the Austrian Science
Fund (FWF) under grant Z211-N23 (Wittgenstein Award). J.B. is supported by the German
Federal Ministry of Education and Research\r\n(BMBF) through the Competence Center
for Machine Learning (TUE.AI, FKZ 01IS18039A) and the International Max Planck Research
School for Intelligent Systems (IMPRS-IS). R.H. is partially supported by Boeing
and Horizon-2020 ECSEL (grant 783163, iDev40).\r\n"
article_processing_charge: No
article_type: original
author:
- first_name: Stefan
full_name: Sietzen, Stefan
last_name: Sietzen
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Judy
full_name: Borowski, Judy
last_name: Borowski
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Manuela
full_name: Waldner, Manuela
last_name: Waldner
citation:
ama: Sietzen S, Lechner M, Borowski J, Hasani R, Waldner M. Interactive analysis
of CNN robustness. Computer Graphics Forum. 2021;40(7):253-264. doi:10.1111/cgf.14418
apa: Sietzen, S., Lechner, M., Borowski, J., Hasani, R., & Waldner, M. (2021).
Interactive analysis of CNN robustness. Computer Graphics Forum. Wiley.
https://doi.org/10.1111/cgf.14418
chicago: Sietzen, Stefan, Mathias Lechner, Judy Borowski, Ramin Hasani, and Manuela
Waldner. “Interactive Analysis of CNN Robustness.” Computer Graphics Forum.
Wiley, 2021. https://doi.org/10.1111/cgf.14418.
ieee: S. Sietzen, M. Lechner, J. Borowski, R. Hasani, and M. Waldner, “Interactive
analysis of CNN robustness,” Computer Graphics Forum, vol. 40, no. 7. Wiley,
pp. 253–264, 2021.
ista: Sietzen S, Lechner M, Borowski J, Hasani R, Waldner M. 2021. Interactive analysis
of CNN robustness. Computer Graphics Forum. 40(7), 253–264.
mla: Sietzen, Stefan, et al. “Interactive Analysis of CNN Robustness.” Computer
Graphics Forum, vol. 40, no. 7, Wiley, 2021, pp. 253–64, doi:10.1111/cgf.14418.
short: S. Sietzen, M. Lechner, J. Borowski, R. Hasani, M. Waldner, Computer Graphics
Forum 40 (2021) 253–264.
date_created: 2021-12-05T23:01:40Z
date_published: 2021-11-27T00:00:00Z
date_updated: 2023-08-14T13:11:42Z
day: '27'
department:
- _id: ToHe
doi: 10.1111/cgf.14418
external_id:
arxiv:
- '2110.07667'
isi:
- '000722952000024'
intvolume: ' 40'
isi: 1
issue: '7'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2110.07667
month: '11'
oa: 1
oa_version: Preprint
page: 253-264
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Computer Graphics Forum
publication_identifier:
eissn:
- 1467-8659
issn:
- 0167-7055
publication_status: published
publisher: Wiley
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interactive analysis of CNN robustness
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 40
year: '2021'
...
---
_id: '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
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: '10666'
abstract:
- lang: eng
text: Adversarial training is an effective method to train deep learning models
that are resilient to norm-bounded perturbations, with the cost of nominal performance
drop. While adversarial training appears to enhance the robustness and safety
of a deep model deployed in open-world decision-critical applications, counterintuitively,
it induces undesired behaviors in robot learning settings. In this paper, we show
theoretically and experimentally that neural controllers obtained via adversarial
training are subjected to three types of defects, namely transient, systematic,
and conditional errors. We first generalize adversarial training to a safety-domain
optimization scheme allowing for more generic specifications. We then prove that
such a learning process tends to cause certain error profiles. We support our
theoretical results by a thorough experimental safety analysis in a robot-learning
task. Our results suggest that adversarial training is not yet ready for robot
learning.
acknowledgement: M.L. and T.A.H. are supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23 (Wittgenstein Award). R.H. and D.R. are supported by
Boeing and R.G. by Horizon-2020 ECSEL Project grant no. 783163 (iDev40).
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Lechner M, Hasani R, Grosu R, Rus D, Henzinger TA. Adversarial training is
not ready for robot learning. In: 2021 IEEE International Conference on Robotics
and Automation. ICRA. ; 2021:4140-4147. doi:10.1109/ICRA48506.2021.9561036'
apa: Lechner, M., Hasani, R., Grosu, R., Rus, D., & Henzinger, T. A. (2021).
Adversarial training is not ready for robot learning. In 2021 IEEE International
Conference on Robotics and Automation (pp. 4140–4147). Xi’an, China. https://doi.org/10.1109/ICRA48506.2021.9561036
chicago: Lechner, Mathias, Ramin Hasani, Radu Grosu, Daniela Rus, and Thomas A Henzinger.
“Adversarial Training Is Not Ready for Robot Learning.” In 2021 IEEE International
Conference on Robotics and Automation, 4140–47. ICRA, 2021. https://doi.org/10.1109/ICRA48506.2021.9561036.
ieee: M. Lechner, R. Hasani, R. Grosu, D. Rus, and T. A. Henzinger, “Adversarial
training is not ready for robot learning,” in 2021 IEEE International Conference
on Robotics and Automation, Xi’an, China, 2021, pp. 4140–4147.
ista: 'Lechner M, Hasani R, Grosu R, Rus D, Henzinger TA. 2021. Adversarial training
is not ready for robot learning. 2021 IEEE International Conference on Robotics
and Automation. ICRA: International Conference on Robotics and AutomationICRA,
4140–4147.'
mla: Lechner, Mathias, et al. “Adversarial Training Is Not Ready for Robot Learning.”
2021 IEEE International Conference on Robotics and Automation, 2021, pp.
4140–47, doi:10.1109/ICRA48506.2021.9561036.
short: M. Lechner, R. Hasani, R. Grosu, D. Rus, T.A. Henzinger, in:, 2021 IEEE International
Conference on Robotics and Automation, 2021, pp. 4140–4147.
conference:
end_date: 2021-06-05
location: Xi'an, China
name: 'ICRA: International Conference on Robotics and Automation'
start_date: 2021-05-30
date_created: 2022-01-25T15:44:54Z
date_published: 2021-01-01T00:00:00Z
date_updated: 2023-08-17T06:58:38Z
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1109/ICRA48506.2021.9561036
external_id:
arxiv:
- '2103.08187'
isi:
- '000765738803040'
has_accepted_license: '1'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2103.08187
oa: 1
oa_version: None
page: 4140-4147
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 2021 IEEE International Conference on Robotics and Automation
publication_identifier:
eisbn:
- 978-1-7281-9077-8
eissn:
- 2577-087X
isbn:
- 978-1-7281-9078-5
issn:
- 1050-4729
publication_status: published
quality_controlled: '1'
related_material:
record:
- id: '11362'
relation: dissertation_contains
status: public
series_title: ICRA
status: public
title: Adversarial training is not ready for robot learning
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND
3.0)
short: CC BY-NC-ND (3.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '10206'
abstract:
- lang: eng
text: Neural-network classifiers achieve high accuracy when predicting the class
of an input that they were trained to identify. Maintaining this accuracy in dynamic
environments, where inputs frequently fall outside the fixed set of initially
known classes, remains a challenge. The typical approach is to detect inputs from
novel classes and retrain the classifier on an augmented dataset. However, not
only the classifier but also the detection mechanism needs to adapt in order to
distinguish between newly learned and yet unknown input classes. To address this
challenge, we introduce an algorithmic framework for active monitoring of a neural
network. A monitor wrapped in our framework operates in parallel with the neural
network and interacts with a human user via a series of interpretable labeling
queries for incremental adaptation. In addition, we propose an adaptive quantitative
monitor to improve precision. An experimental evaluation on a diverse set of benchmarks
with varying numbers of classes confirms the benefits of our active monitoring
framework in dynamic scenarios.
acknowledgement: We thank Christoph Lampert and Alex Greengold for fruitful discussions.
This research was supported in part by the Simons Institute for the Theory of Computing,
the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), and the
European Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie grant agreement No. 754411.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Anna
full_name: Lukina, Anna
id: CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425
last_name: Lukina
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Lukina A, Schilling C, Henzinger TA. Into the unknown: active monitoring of neural
networks. In: 21st International Conference on Runtime Verification. Vol
12974. Cham: Springer Nature; 2021:42-61. doi:10.1007/978-3-030-88494-9_3'
apa: 'Lukina, A., Schilling, C., & Henzinger, T. A. (2021). Into the unknown:
active monitoring of neural networks. In 21st International Conference on Runtime
Verification (Vol. 12974, pp. 42–61). Cham: Springer Nature. https://doi.org/10.1007/978-3-030-88494-9_3'
chicago: 'Lukina, Anna, Christian Schilling, and Thomas A Henzinger. “Into the Unknown:
Active Monitoring of Neural Networks.” In 21st International Conference on
Runtime Verification, 12974:42–61. Cham: Springer Nature, 2021. https://doi.org/10.1007/978-3-030-88494-9_3.'
ieee: 'A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: active monitoring
of neural networks,” in 21st International Conference on Runtime Verification,
Virtual, 2021, vol. 12974, pp. 42–61.'
ista: 'Lukina A, Schilling C, Henzinger TA. 2021. Into the unknown: active monitoring
of neural networks. 21st International Conference on Runtime Verification. RV:
Runtime Verification, LNCS, vol. 12974, 42–61.'
mla: 'Lukina, Anna, et al. “Into the Unknown: Active Monitoring of Neural Networks.”
21st International Conference on Runtime Verification, vol. 12974, Springer
Nature, 2021, pp. 42–61, doi:10.1007/978-3-030-88494-9_3.'
short: A. Lukina, C. Schilling, T.A. Henzinger, in:, 21st International Conference
on Runtime Verification, Springer Nature, Cham, 2021, pp. 42–61.
conference:
end_date: 2021-10-14
location: Virtual
name: 'RV: Runtime Verification'
start_date: 2021-10-11
date_created: 2021-10-31T23:01:31Z
date_published: 2021-10-06T00:00:00Z
date_updated: 2024-01-30T12:06:56Z
day: '06'
department:
- _id: ToHe
doi: 10.1007/978-3-030-88494-9_3
ec_funded: 1
external_id:
arxiv:
- '2009.06429'
isi:
- '000719383800003'
isi: 1
keyword:
- monitoring
- neural networks
- novelty detection
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2009.06429
month: '10'
oa: 1
oa_version: Preprint
page: 42-61
place: Cham
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 21st International Conference on Runtime Verification
publication_identifier:
eisbn:
- 978-3-030-88494-9
eissn:
- 1611-3349
isbn:
- 9-783-0308-8493-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '13234'
relation: extended_version
status: public
scopus_import: '1'
status: public
title: 'Into the unknown: active monitoring of neural networks'
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: '12974 '
year: '2021'
...
---
_id: '10673'
abstract:
- lang: eng
text: We propose a neural information processing system obtained by re-purposing
the function of a biological neural circuit model to govern simulated and real-world
control tasks. Inspired by the structure of the nervous system of the soil-worm,
C. elegans, we introduce ordinary neural circuits (ONCs), defined as the model
of biological neural circuits reparameterized for the control of alternative tasks.
We first demonstrate that ONCs realize networks with higher maximum flow compared
to arbitrary wired networks. We then learn instances of ONCs to control a series
of robotic tasks, including the autonomous parking of a real-world rover robot.
For reconfiguration of the purpose of the neural circuit, we adopt a search-based
optimization algorithm. Ordinary neural circuits perform on par and, in some cases,
significantly surpass the performance of contemporary deep learning models. ONC
networks are compact, 77% sparser than their counterpart neural controllers, and
their neural dynamics are fully interpretable at the cell-level.
acknowledgement: "RH and RG are partially supported by Horizon-2020 ECSEL Project
grant No. 783163 (iDev40), Productive 4.0, and ATBMBFW CPS-IoT Ecosystem. ML was
supported in part by the Austrian Science Fund (FWF) under grant Z211-N23\r\n(Wittgenstein
Award). AA is supported by the National Science Foundation (NSF) Graduate Research
Fellowship\r\nProgram. RH and DR are partially supported by The Boeing Company and
JP Morgan Chase. This research work is\r\npartially drawn from the PhD dissertation
of RH.\r\n"
alternative_title:
- PMLR
article_processing_charge: No
author:
- first_name: Ramin
full_name: Hasani, Ramin
last_name: Hasani
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Alexander
full_name: Amini, Alexander
last_name: Amini
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Hasani R, Lechner M, Amini A, Rus D, Grosu R. A natural lottery ticket winner:
Reinforcement learning with ordinary neural circuits. In: Proceedings of the
37th International Conference on Machine Learning. PMLR. ; 2020:4082-4093.'
apa: 'Hasani, R., Lechner, M., Amini, A., Rus, D., & Grosu, R. (2020). A natural
lottery ticket winner: Reinforcement learning with ordinary neural circuits. In
Proceedings of the 37th International Conference on Machine Learning (pp.
4082–4093). Virtual.'
chicago: 'Hasani, Ramin, Mathias Lechner, Alexander Amini, Daniela Rus, and Radu
Grosu. “A Natural Lottery Ticket Winner: Reinforcement Learning with Ordinary
Neural Circuits.” In Proceedings of the 37th International Conference on Machine
Learning, 4082–93. PMLR, 2020.'
ieee: 'R. Hasani, M. Lechner, A. Amini, D. Rus, and R. Grosu, “A natural lottery
ticket winner: Reinforcement learning with ordinary neural circuits,” in Proceedings
of the 37th International Conference on Machine Learning, Virtual, 2020, pp.
4082–4093.'
ista: 'Hasani R, Lechner M, Amini A, Rus D, Grosu R. 2020. A natural lottery ticket
winner: Reinforcement learning with ordinary neural circuits. Proceedings of the
37th International Conference on Machine Learning. ML: Machine LearningPMLR, PMLR,
, 4082–4093.'
mla: 'Hasani, Ramin, et al. “A Natural Lottery Ticket Winner: Reinforcement Learning
with Ordinary Neural Circuits.” Proceedings of the 37th International Conference
on Machine Learning, 2020, pp. 4082–93.'
short: R. Hasani, M. Lechner, A. Amini, D. Rus, R. Grosu, in:, Proceedings of the
37th International Conference on Machine Learning, 2020, pp. 4082–4093.
conference:
end_date: 2020-07-18
location: Virtual
name: 'ML: Machine Learning'
start_date: 2020-07-12
date_created: 2022-01-25T15:50:34Z
date_published: 2020-01-01T00:00:00Z
date_updated: 2022-01-26T11:14:27Z
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
file:
- access_level: open_access
checksum: c9a4a29161777fc1a89ef451c040e3b1
content_type: application/pdf
creator: cchlebak
date_created: 2022-01-26T11:08:51Z
date_updated: 2022-01-26T11:08:51Z
file_id: '10691'
file_name: 2020_PMLR_Hasani.pdf
file_size: 2329798
relation: main_file
success: 1
file_date_updated: 2022-01-26T11:08:51Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://proceedings.mlr.press/v119/hasani20a.html
oa: 1
oa_version: Published Version
page: 4082-4093
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 37th International Conference on Machine Learning
publication_identifier:
issn:
- 2640-3498
publication_status: published
quality_controlled: '1'
scopus_import: '1'
series_title: PMLR
status: public
title: 'A natural lottery ticket winner: Reinforcement learning with ordinary neural
circuits'
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: '2020'
...
---
_id: '7348'
abstract:
- lang: eng
text: 'The monitoring of event frequencies can be used to recognize behavioral anomalies,
to identify trends, and to deduce or discard hypotheses about the underlying system.
For example, the performance of a web server may be monitored based on the ratio
of the total count of requests from the least and most active clients. Exact frequency
monitoring, however, can be prohibitively expensive; in the above example it would
require as many counters as there are clients. In this paper, we propose the efficient
probabilistic monitoring of common frequency properties, including the mode (i.e.,
the most common event) and the median of an event sequence. We define a logic
to express composite frequency properties as a combination of atomic frequency
properties. Our main contribution is an algorithm that, under suitable probabilistic
assumptions, can be used to monitor these important frequency properties with
four counters, independent of the number of different events. Our algorithm samples
longer and longer subwords of an infinite event sequence. We prove the almost-sure
convergence of our algorithm by generalizing ergodic theory from increasing-length
prefixes to increasing-length subwords of an infinite sequence. A similar algorithm
could be used to learn a connected Markov chain of a given structure from observing
its outputs, to arbitrary precision, for a given confidence. '
alternative_title:
- LIPIcs
article_number: '20'
article_processing_charge: No
author:
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
citation:
ama: 'Ferrere T, Henzinger TA, Kragl B. Monitoring event frequencies. In: 28th
EACSL Annual Conference on Computer Science Logic. Vol 152. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.CSL.2020.20'
apa: 'Ferrere, T., Henzinger, T. A., & Kragl, B. (2020). Monitoring event frequencies.
In 28th EACSL Annual Conference on Computer Science Logic (Vol. 152). Barcelona,
Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2020.20'
chicago: Ferrere, Thomas, Thomas A Henzinger, and Bernhard Kragl. “Monitoring Event
Frequencies.” In 28th EACSL Annual Conference on Computer Science Logic,
Vol. 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CSL.2020.20.
ieee: T. Ferrere, T. A. Henzinger, and B. Kragl, “Monitoring event frequencies,”
in 28th EACSL Annual Conference on Computer Science Logic, Barcelona, Spain,
2020, vol. 152.
ista: 'Ferrere T, Henzinger TA, Kragl B. 2020. Monitoring event frequencies. 28th
EACSL Annual Conference on Computer Science Logic. CSL: Computer Science Logic,
LIPIcs, vol. 152, 20.'
mla: Ferrere, Thomas, et al. “Monitoring Event Frequencies.” 28th EACSL Annual
Conference on Computer Science Logic, vol. 152, 20, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2020, doi:10.4230/LIPIcs.CSL.2020.20.
short: T. Ferrere, T.A. Henzinger, B. Kragl, in:, 28th EACSL Annual Conference on
Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
conference:
end_date: 2020-01-16
location: Barcelona, Spain
name: 'CSL: Computer Science Logic'
start_date: 2020-01-13
date_created: 2020-01-21T11:22:21Z
date_published: 2020-01-15T00:00:00Z
date_updated: 2021-01-12T08:13:12Z
day: '15'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CSL.2020.20
external_id:
arxiv:
- '1910.06097'
file:
- access_level: open_access
checksum: b9a691d658d075c6369d3304d17fb818
content_type: application/pdf
creator: bkragl
date_created: 2020-01-21T11:21:04Z
date_updated: 2020-07-14T12:47:56Z
file_id: '7349'
file_name: main.pdf
file_size: 617206
relation: main_file
file_date_updated: 2020-07-14T12:47:56Z
has_accepted_license: '1'
intvolume: ' 152'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _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: 28th EACSL Annual Conference on Computer Science Logic
publication_identifier:
isbn:
- '9783959771320'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: 1
status: public
title: Monitoring event frequencies
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 152
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: '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: '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
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
license: https://creativecommons.org/licenses/by/3.0/
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: '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: '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: '9632'
abstract:
- lang: eng
text: "Second-order information, in the form of Hessian- or Inverse-Hessian-vector
products, is a fundamental tool for solving optimization problems. Recently, there
has been significant interest in utilizing this information in the context of
deep\r\nneural networks; however, relatively little is known about the quality
of existing approximations in this context. Our work examines this question, identifies
issues with existing approaches, and proposes a method called WoodFisher to compute
a faithful and efficient estimate of the inverse Hessian. Our main application
is to neural network compression, where we build on the classic Optimal Brain
Damage/Surgeon framework. We demonstrate that WoodFisher significantly outperforms
popular state-of-the-art methods for oneshot pruning. Further, even when iterative,
gradual pruning is allowed, our method results in a gain in test accuracy over
the state-of-the-art approaches, for standard image classification datasets such
as ImageNet ILSVRC. We examine how our method can be extended to take into account
first-order information, as well as\r\nillustrate its ability to automatically
set layer-wise pruning thresholds and perform compression in the limited-data
regime. The code is available at the following link, https://github.com/IST-DASLab/WoodFisher."
acknowledgement: This project has received funding from the European Research Council
(ERC) under the European Union’s Horizon 2020 research and innovation programme
(grant agreement No 805223 ScaleML). Also, we would like to thank Alexander Shevchenko,
Alexandra Peste, and other members of the group for fruitful discussions.
article_processing_charge: No
author:
- first_name: Sidak Pal
full_name: Singh, Sidak Pal
id: DD138E24-D89D-11E9-9DC0-DEF6E5697425
last_name: Singh
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
citation:
ama: 'Singh SP, Alistarh D-A. WoodFisher: Efficient second-order approximation for
neural network compression. In: Advances in Neural Information Processing Systems.
Vol 33. Curran Associates; 2020:18098-18109.'
apa: 'Singh, S. P., & Alistarh, D.-A. (2020). WoodFisher: Efficient second-order
approximation for neural network compression. In Advances in Neural Information
Processing Systems (Vol. 33, pp. 18098–18109). Vancouver, Canada: Curran Associates.'
chicago: 'Singh, Sidak Pal, and Dan-Adrian Alistarh. “WoodFisher: Efficient Second-Order
Approximation for Neural Network Compression.” In Advances in Neural Information
Processing Systems, 33:18098–109. Curran Associates, 2020.'
ieee: 'S. P. Singh and D.-A. Alistarh, “WoodFisher: Efficient second-order approximation
for neural network compression,” in Advances in Neural Information Processing
Systems, Vancouver, Canada, 2020, vol. 33, pp. 18098–18109.'
ista: 'Singh SP, Alistarh D-A. 2020. WoodFisher: Efficient second-order approximation
for neural network compression. Advances in Neural Information Processing Systems.
NeurIPS: Conference on Neural Information Processing Systems vol. 33, 18098–18109.'
mla: 'Singh, Sidak Pal, and Dan-Adrian Alistarh. “WoodFisher: Efficient Second-Order
Approximation for Neural Network Compression.” Advances in Neural Information
Processing Systems, vol. 33, Curran Associates, 2020, pp. 18098–109.'
short: S.P. Singh, D.-A. Alistarh, in:, Advances in Neural Information Processing
Systems, Curran Associates, 2020, pp. 18098–18109.
conference:
end_date: 2020-12-12
location: Vancouver, Canada
name: 'NeurIPS: Conference on Neural Information Processing Systems'
start_date: 2020-12-06
date_created: 2021-07-04T22:01:26Z
date_published: 2020-12-06T00:00:00Z
date_updated: 2023-02-23T14:03:06Z
day: '06'
department:
- _id: DaAl
- _id: ToHe
ec_funded: 1
external_id:
arxiv:
- '2004.14340'
intvolume: ' 33'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://proceedings.neurips.cc/paper/2020/hash/d1ff1ec86b62cd5f3903ff19c3a326b2-Abstract.html
month: '12'
oa: 1
oa_version: Published Version
page: 18098-18109
project:
- _id: 268A44D6-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '805223'
name: Elastic Coordination for Scalable Machine Learning
publication: Advances in Neural Information Processing Systems
publication_identifier:
isbn:
- '9781713829546'
issn:
- '10495258'
publication_status: published
publisher: Curran Associates
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'WoodFisher: Efficient second-order approximation for neural network compression'
type: conference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
volume: 33
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
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'
...
---
_id: '10672'
abstract:
- lang: eng
text: The family of feedback alignment (FA) algorithms aims to provide a more biologically
motivated alternative to backpropagation (BP), by substituting the computations
that are unrealistic to be implemented in physical brains. While FA algorithms
have been shown to work well in practice, there is a lack of rigorous theory proofing
their learning capabilities. Here we introduce the first feedback alignment algorithm
with provable learning guarantees. In contrast to existing work, we do not require
any assumption about the size or depth of the network except that it has a single
output neuron, i.e., such as for binary classification tasks. We show that our
FA algorithm can deliver its theoretical promises in practice, surpassing the
learning performance of existing FA methods and matching backpropagation in binary
classification tasks. Finally, we demonstrate the limits of our FA variant when
the number of output neurons grows beyond a certain quantity.
acknowledgement: "This research was supported in part by the Austrian Science Fund
(FWF) under grant Z211-N23\r\n(Wittgenstein Award).\r\n"
article_processing_charge: No
author:
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
citation:
ama: 'Lechner M. Learning representations for binary-classification without backpropagation.
In: 8th International Conference on Learning Representations. ICLR; 2020.'
apa: 'Lechner, M. (2020). Learning representations for binary-classification without
backpropagation. In 8th International Conference on Learning Representations.
Virtual ; Addis Ababa, Ethiopia: ICLR.'
chicago: Lechner, Mathias. “Learning Representations for Binary-Classification without
Backpropagation.” In 8th International Conference on Learning Representations.
ICLR, 2020.
ieee: M. Lechner, “Learning representations for binary-classification without backpropagation,”
in 8th International Conference on Learning Representations, Virtual ;
Addis Ababa, Ethiopia, 2020.
ista: 'Lechner M. 2020. Learning representations for binary-classification without
backpropagation. 8th International Conference on Learning Representations. ICLR:
International Conference on Learning Representations.'
mla: Lechner, Mathias. “Learning Representations for Binary-Classification without
Backpropagation.” 8th International Conference on Learning Representations,
ICLR, 2020.
short: M. Lechner, in:, 8th International Conference on Learning Representations,
ICLR, 2020.
conference:
end_date: 2020-05-01
location: Virtual ; Addis Ababa, Ethiopia
name: 'ICLR: International Conference on Learning Representations'
start_date: 2020-04-26
date_created: 2022-01-25T15:50:00Z
date_published: 2020-03-11T00:00:00Z
date_updated: 2023-04-03T07:33:40Z
day: '11'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
file:
- access_level: open_access
checksum: ea13d42dd4541ddb239b6a75821fd6c9
content_type: application/pdf
creator: mlechner
date_created: 2022-01-26T07:35:17Z
date_updated: 2022-01-26T07:35:17Z
file_id: '10677'
file_name: iclr_2020.pdf
file_size: 249431
relation: main_file
success: 1
file_date_updated: 2022-01-26T07:35:17Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://openreview.net/forum?id=Bke61krFvS
month: '03'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 8th International Conference on Learning Representations
publication_status: published
publisher: ICLR
quality_controlled: '1'
scopus_import: '1'
status: public
title: Learning representations for binary-classification without backpropagation
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND
3.0)
short: CC BY-NC-ND (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2020'
...
---
_id: '7808'
abstract:
- lang: eng
text: Quantization converts neural networks into low-bit fixed-point computations
which can be carried out by efficient integer-only hardware, and is standard practice
for the deployment of neural networks on real-time embedded devices. However,
like their real-numbered counterpart, quantized networks are not immune to malicious
misclassification caused by adversarial attacks. We investigate how quantization
affects a network’s robustness to adversarial attacks, which is a formal verification
question. We show that neither robustness nor non-robustness are monotonic with
changing the number of bits for the representation and, also, neither are preserved
by quantization from a real-numbered network. For this reason, we introduce a
verification method for quantized neural networks which, using SMT solving over
bit-vectors, accounts for their exact, bit-precise semantics. We built a tool
and analyzed the effect of quantization on a classifier for the MNIST dataset.
We demonstrate that, compared to our method, existing methods for the analysis
of real-numbered networks often derive false conclusions about their quantizations,
both when determining robustness and when detecting attacks, and that existing
methods for quantized networks often miss attacks. Furthermore, we applied our
method beyond robustness, showing how the number of bits in quantization enlarges
the gender bias of a predictor for students’ grades.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Mirco
full_name: Giacobbe, Mirco
id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
last_name: Giacobbe
orcid: 0000-0001-8180-0904
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
citation:
ama: 'Giacobbe M, Henzinger TA, Lechner M. How many bits does it take to quantize
your neural network? In: International Conference on Tools and Algorithms for
the Construction and Analysis of Systems. Vol 12079. Springer Nature; 2020:79-97.
doi:10.1007/978-3-030-45237-7_5'
apa: 'Giacobbe, M., Henzinger, T. A., & Lechner, M. (2020). How many bits does
it take to quantize your neural network? In International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (Vol. 12079, pp.
79–97). Dublin, Ireland: Springer Nature. https://doi.org/10.1007/978-3-030-45237-7_5'
chicago: Giacobbe, Mirco, Thomas A Henzinger, and Mathias Lechner. “How Many Bits
Does It Take to Quantize Your Neural Network?” In International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, 12079:79–97.
Springer Nature, 2020. https://doi.org/10.1007/978-3-030-45237-7_5.
ieee: M. Giacobbe, T. A. Henzinger, and M. Lechner, “How many bits does it take
to quantize your neural network?,” in International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, Dublin, Ireland,
2020, vol. 12079, pp. 79–97.
ista: 'Giacobbe M, Henzinger TA, Lechner M. 2020. How many bits does it take to
quantize your neural network? International Conference on Tools and Algorithms
for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for
the Construction and Analysis of Systems, LNCS, vol. 12079, 79–97.'
mla: Giacobbe, Mirco, et al. “How Many Bits Does It Take to Quantize Your Neural
Network?” International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 12079, Springer Nature, 2020, pp. 79–97, doi:10.1007/978-3-030-45237-7_5.
short: M. Giacobbe, T.A. Henzinger, M. Lechner, in:, International Conference on
Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature,
2020, pp. 79–97.
conference:
end_date: 2020-04-30
location: Dublin, Ireland
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2020-04-25
date_created: 2020-05-10T22:00:49Z
date_published: 2020-04-17T00:00:00Z
date_updated: 2023-06-23T07:01:11Z
day: '17'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-45237-7_5
file:
- access_level: open_access
checksum: f19905a42891fe5ce93d69143fa3f6fb
content_type: application/pdf
creator: dernst
date_created: 2020-05-26T12:48:15Z
date_updated: 2020-07-14T12:48:03Z
file_id: '7893'
file_name: 2020_TACAS_Giacobbe.pdf
file_size: 2744030
relation: main_file
file_date_updated: 2020-07-14T12:48:03Z
has_accepted_license: '1'
intvolume: ' 12079'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 79-97
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
publication: International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783030452360'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '11362'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: How many bits does it take to quantize your neural network?
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 12079
year: '2020'
...
---
_id: '6761'
abstract:
- lang: eng
text: In resource allocation games, selfish players share resources that are needed
in order to fulfill their objectives. The cost of using a resource depends on
the load on it. In the traditional setting, the players make their choices concurrently
and in one-shot. That is, a strategy for a player is a subset of the resources.
We introduce and study dynamic resource allocation games. In this setting, the
game proceeds in phases. In each phase each player chooses one resource. A scheduler
dictates the order in which the players proceed in a phase, possibly scheduling
several players to proceed concurrently. The game ends when each player has collected
a set of resources that fulfills his objective. The cost for each player then
depends on this set as well as on the load on the resources in it – we consider
both congestion and cost-sharing games. We argue that the dynamic setting is the
suitable setting for many applications in practice. We study the stability of
dynamic resource allocation games, where the appropriate notion of stability is
that of subgame perfect equilibrium, study the inefficiency incurred due to selfish
behavior, and also study problems that are particular to the dynamic setting,
like constraints on the order in which resources can be chosen or the problem
of finding a scheduler that achieves stability.
article_processing_charge: No
article_type: original
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. Theoretical
Computer Science. 2020;807:42-55. doi:10.1016/j.tcs.2019.06.031
apa: Avni, G., Henzinger, T. A., & Kupferman, O. (2020). Dynamic resource allocation
games. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2019.06.031
chicago: Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation
Games.” Theoretical Computer Science. Elsevier, 2020. https://doi.org/10.1016/j.tcs.2019.06.031.
ieee: G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,”
Theoretical Computer Science, vol. 807. Elsevier, pp. 42–55, 2020.
ista: Avni G, Henzinger TA, Kupferman O. 2020. Dynamic resource allocation games.
Theoretical Computer Science. 807, 42–55.
mla: Avni, Guy, et al. “Dynamic Resource Allocation Games.” Theoretical Computer
Science, vol. 807, Elsevier, 2020, pp. 42–55, doi:10.1016/j.tcs.2019.06.031.
short: G. Avni, T.A. Henzinger, O. Kupferman, Theoretical Computer Science 807 (2020)
42–55.
date_created: 2019-08-04T21:59:20Z
date_published: 2020-02-06T00:00:00Z
date_updated: 2023-08-17T13:52:49Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.tcs.2019.06.031
external_id:
isi:
- '000512219400004'
file:
- access_level: open_access
checksum: e86635417f45eb2cd75778f91382f737
content_type: application/pdf
creator: dernst
date_created: 2020-10-09T06:31:22Z
date_updated: 2020-10-09T06:31:22Z
file_id: '8639'
file_name: 2020_TheoreticalCS_Avni.pdf
file_size: 1413001
relation: main_file
success: 1
file_date_updated: 2020-10-09T06:31:22Z
has_accepted_license: '1'
intvolume: ' 807'
isi: 1
language:
- iso: eng
month: '02'
oa: 1
oa_version: Submitted Version
page: 42-55
project:
- _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
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
publication: Theoretical Computer Science
publication_identifier:
issn:
- '03043975'
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '1341'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Dynamic resource allocation games
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 807
year: '2020'
...
---
_id: '7505'
abstract:
- lang: eng
text: Neural networks have demonstrated unmatched performance in a range of classification
tasks. Despite numerous efforts of the research community, novelty detection remains
one of the significant limitations of neural networks. The ability to identify
previously unseen inputs as novel is crucial for our understanding of the decisions
made by neural networks. At runtime, inputs not falling into any of the categories
learned during training cannot be classified correctly by the neural network.
Existing approaches treat the neural network as a black box and try to detect
novel inputs based on the confidence of the output predictions. However, neural
networks are not trained to reduce their confidence for novel inputs, which limits
the effectiveness of these approaches. We propose a framework to monitor a neural
network by observing the hidden layers. We employ a common abstraction from program
analysis - boxes - to identify novel behaviors in the monitored layers, i.e.,
inputs that cause behaviors outside the box. For each neuron, the boxes range
over the values seen in training. The framework is efficient and flexible to achieve
a desired trade-off between raising false warnings and detecting novel inputs.
We illustrate the performance and the robustness to variability in the unknown
classes on popular image-classification benchmarks.
acknowledgement: We thank Christoph Lampert and Nikolaus Mayer for fruitful discussions.
This research was supported in part by the Austrian Science Fund (FWF) under grants
S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award) and the European Union’s
Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie grant
agreement No. 754411.
alternative_title:
- Frontiers in Artificial Intelligence and Applications
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: Anna
full_name: Lukina, Anna
id: CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425
last_name: Lukina
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Henzinger TA, Lukina A, Schilling C. Outside the box: Abstraction-based monitoring
of neural networks. In: 24th European Conference on Artificial Intelligence.
Vol 325. IOS Press; 2020:2433-2440. doi:10.3233/FAIA200375'
apa: 'Henzinger, T. A., Lukina, A., & Schilling, C. (2020). Outside the box:
Abstraction-based monitoring of neural networks. In 24th European Conference
on Artificial Intelligence (Vol. 325, pp. 2433–2440). Santiago de Compostela,
Spain: IOS Press. https://doi.org/10.3233/FAIA200375'
chicago: 'Henzinger, Thomas A, Anna Lukina, and Christian Schilling. “Outside the
Box: Abstraction-Based Monitoring of Neural Networks.” In 24th European Conference
on Artificial Intelligence, 325:2433–40. IOS Press, 2020. https://doi.org/10.3233/FAIA200375.'
ieee: 'T. A. Henzinger, A. Lukina, and C. Schilling, “Outside the box: Abstraction-based
monitoring of neural networks,” in 24th European Conference on Artificial Intelligence,
Santiago de Compostela, Spain, 2020, vol. 325, pp. 2433–2440.'
ista: 'Henzinger TA, Lukina A, Schilling C. 2020. Outside the box: Abstraction-based
monitoring of neural networks. 24th European Conference on Artificial Intelligence.
ECAI: European Conference on Artificial Intelligence, Frontiers in Artificial
Intelligence and Applications, vol. 325, 2433–2440.'
mla: 'Henzinger, Thomas A., et al. “Outside the Box: Abstraction-Based Monitoring
of Neural Networks.” 24th European Conference on Artificial Intelligence,
vol. 325, IOS Press, 2020, pp. 2433–40, doi:10.3233/FAIA200375.'
short: T.A. Henzinger, A. Lukina, C. Schilling, in:, 24th European Conference on
Artificial Intelligence, IOS Press, 2020, pp. 2433–2440.
conference:
end_date: 2020-09-08
location: Santiago de Compostela, Spain
name: 'ECAI: European Conference on Artificial Intelligence'
start_date: 2020-08-29
date_created: 2020-02-21T16:44:03Z
date_published: 2020-02-24T00:00:00Z
date_updated: 2023-08-18T06:38:16Z
day: '24'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.3233/FAIA200375
ec_funded: 1
external_id:
arxiv:
- '1911.09032'
isi:
- '000650971303002'
file:
- access_level: open_access
checksum: 80642fa0b6cd7da95dcd87d63789ad5e
content_type: application/pdf
creator: dernst
date_created: 2020-09-21T07:12:32Z
date_updated: 2020-09-21T07:12:32Z
file_id: '8540'
file_name: 2020_ECAI_Henzinger.pdf
file_size: 1692214
relation: main_file
success: 1
file_date_updated: 2020-09-21T07:12:32Z
has_accepted_license: '1'
intvolume: ' 325'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc/4.0/
month: '02'
oa: 1
oa_version: Published Version
page: 2433-2440
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
- _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
publication: 24th European Conference on Artificial Intelligence
publication_status: published
publisher: IOS Press
quality_controlled: '1'
status: public
title: 'Outside the box: Abstraction-based monitoring of neural networks'
tmp:
image: /images/cc_by_nc.png
legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
short: CC BY-NC (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 325
year: '2020'
...
---
_id: '8194'
abstract:
- lang: eng
text: 'Fixed-point arithmetic is a popular alternative to floating-point arithmetic
on embedded systems. Existing work on the verification of fixed-point programs
relies on custom formalizations of fixed-point arithmetic, which makes it hard
to compare the described techniques or reuse the implementations. In this paper,
we address this issue by proposing and formalizing an SMT theory of fixed-point
arithmetic. We present an intuitive yet comprehensive syntax of the fixed-point
theory, and provide formal semantics for it based on rational arithmetic. We also
describe two decision procedures for this theory: one based on the theory of bit-vectors
and the other on the theory of reals. We implement the two decision procedures,
and evaluate our implementations using existing mature SMT solvers on a benchmark
suite we created. Finally, we perform a case study of using the theory we propose
to verify properties of quantized neural networks.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Baranowski, Marek
last_name: Baranowski
- first_name: Shaobo
full_name: He, Shaobo
last_name: He
- first_name: Mathias
full_name: Lechner, Mathias
id: 3DC22916-F248-11E8-B48F-1D18A9856A87
last_name: Lechner
- first_name: Thanh Son
full_name: Nguyen, Thanh Son
last_name: Nguyen
- first_name: Zvonimir
full_name: Rakamarić, Zvonimir
last_name: Rakamarić
citation:
ama: 'Baranowski M, He S, Lechner M, Nguyen TS, Rakamarić Z. An SMT theory of fixed-point
arithmetic. In: Automated Reasoning. Vol 12166. Springer Nature; 2020:13-31.
doi:10.1007/978-3-030-51074-9_2'
apa: 'Baranowski, M., He, S., Lechner, M., Nguyen, T. S., & Rakamarić, Z. (2020).
An SMT theory of fixed-point arithmetic. In Automated Reasoning (Vol. 12166,
pp. 13–31). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-030-51074-9_2'
chicago: Baranowski, Marek, Shaobo He, Mathias Lechner, Thanh Son Nguyen, and Zvonimir
Rakamarić. “An SMT Theory of Fixed-Point Arithmetic.” In Automated Reasoning,
12166:13–31. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-51074-9_2.
ieee: M. Baranowski, S. He, M. Lechner, T. S. Nguyen, and Z. Rakamarić, “An SMT
theory of fixed-point arithmetic,” in Automated Reasoning, Paris, France,
2020, vol. 12166, pp. 13–31.
ista: 'Baranowski M, He S, Lechner M, Nguyen TS, Rakamarić Z. 2020. An SMT theory
of fixed-point arithmetic. Automated Reasoning. IJCAR: International Joint Conference
on Automated Reasoning, LNCS, vol. 12166, 13–31.'
mla: Baranowski, Marek, et al. “An SMT Theory of Fixed-Point Arithmetic.” Automated
Reasoning, vol. 12166, Springer Nature, 2020, pp. 13–31, doi:10.1007/978-3-030-51074-9_2.
short: M. Baranowski, S. He, M. Lechner, T.S. Nguyen, Z. Rakamarić, in:, Automated
Reasoning, Springer Nature, 2020, pp. 13–31.
conference:
end_date: 2020-07-04
location: Paris, France
name: 'IJCAR: International Joint Conference on Automated Reasoning'
start_date: 2020-07-01
date_created: 2020-08-02T22:00:59Z
date_published: 2020-06-24T00:00:00Z
date_updated: 2023-08-22T08:27:25Z
day: '24'
department:
- _id: ToHe
doi: 10.1007/978-3-030-51074-9_2
external_id:
isi:
- '000884318000002'
intvolume: ' 12166'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1007/978-3-030-51074-9_2
month: '06'
oa: 1
oa_version: Published Version
page: 13-31
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Automated Reasoning
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783030510732'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: An SMT theory of fixed-point arithmetic
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 12166
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
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: '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
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: '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
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: '9197'
abstract:
- lang: eng
text: In this paper we introduce and study all-pay bidding games, a class of two
player, zero-sum games on graphs. The game proceeds as follows. We place a token
on some vertex in the graph and assign budgets to the two players. Each turn,
each player submits a sealed legal bid (non-negative and below their remaining
budget), which is deducted from their budget and the highest bidder moves the
token onto an adjacent vertex. The game ends once a sink is reached, and Player
1 pays Player 2 the outcome that is associated with the sink. The players attempt
to maximize their expected outcome. Our games model settings where effort (of
no inherent value) needs to be invested in an ongoing and stateful manner. On
the negative side, we show that even in simple games on DAGs, optimal strategies
may require a distribution over bids with infinite support. A central quantity
in bidding games is the ratio of the players budgets. On the positive side, we
show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation
for the optimal strategy for that ratio. We also implement it, show that it performs
well, and suggests interesting properties of these games. Then, given an outcome
c, we show an algorithm for finding the necessary and sufficient initial ratio
for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally,
while the general case has not previously been studied, solving the specific game
in which Player 1 wins iff he wins the first two auctions, has been long stated
as an open question, which we solve.
acknowledgement: This research was supported by the Austrian Science Fund (FWF) under
grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner
fellowship).
article_processing_charge: No
article_type: original
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
citation:
ama: Avni G, Ibsen-Jensen R, Tkadlec J. All-pay bidding games on graphs. Proceedings
of the AAAI Conference on Artificial Intelligence. 2020;34(02):1798-1805.
doi:10.1609/aaai.v34i02.5546
apa: 'Avni, G., Ibsen-Jensen, R., & Tkadlec, J. (2020). All-pay bidding games
on graphs. Proceedings of the AAAI Conference on Artificial Intelligence.
New York, NY, United States: Association for the Advancement of Artificial Intelligence.
https://doi.org/10.1609/aaai.v34i02.5546'
chicago: Avni, Guy, Rasmus Ibsen-Jensen, and Josef Tkadlec. “All-Pay Bidding Games
on Graphs.” Proceedings of the AAAI Conference on Artificial Intelligence.
Association for the Advancement of Artificial Intelligence, 2020. https://doi.org/10.1609/aaai.v34i02.5546.
ieee: G. Avni, R. Ibsen-Jensen, and J. Tkadlec, “All-pay bidding games on graphs,”
Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34,
no. 02. Association for the Advancement of Artificial Intelligence, pp. 1798–1805,
2020.
ista: Avni G, Ibsen-Jensen R, Tkadlec J. 2020. All-pay bidding games on graphs.
Proceedings of the AAAI Conference on Artificial Intelligence. 34(02), 1798–1805.
mla: Avni, Guy, et al. “All-Pay Bidding Games on Graphs.” Proceedings of the
AAAI Conference on Artificial Intelligence, vol. 34, no. 02, Association for
the Advancement of Artificial Intelligence, 2020, pp. 1798–805, doi:10.1609/aaai.v34i02.5546.
short: G. Avni, R. Ibsen-Jensen, J. Tkadlec, Proceedings of the AAAI Conference
on Artificial Intelligence 34 (2020) 1798–1805.
conference:
end_date: 2020-02-12
location: New York, NY, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2020-02-07
date_created: 2021-02-25T09:05:18Z
date_published: 2020-04-03T00:00:00Z
date_updated: 2023-09-05T12:40:00Z
day: '03'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v34i02.5546
external_id:
arxiv:
- '1911.08360'
intvolume: ' 34'
issue: '02'
language:
- iso: eng
month: '04'
oa_version: Preprint
page: 1798-1805
project:
- _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
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- '9781577358350'
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: All-pay bidding games on graphs
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 34
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: '8195'
abstract:
- lang: eng
text: This paper presents a foundation for refining concurrent programs with structured
control flow. The verification problem is decomposed into subproblems that aid
interactive program development, proof reuse, and automation. The formalization
in this paper is the basis of a new design and implementation of the Civl verifier.
acknowledgement: "Bernhard Kragl and Thomas A. Henzinger were supported by\r\nthe
Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award)."
alternative_title:
- LNCS
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
- 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: 'Kragl B, Qadeer S, Henzinger TA. Refinement for structured concurrent programs.
In: Computer Aided Verification. Vol 12224. Springer Nature; 2020:275-298.
doi:10.1007/978-3-030-53288-8_14'
apa: Kragl, B., Qadeer, S., & Henzinger, T. A. (2020). Refinement for structured
concurrent programs. In Computer Aided Verification (Vol. 12224, pp. 275–298).
Springer Nature. https://doi.org/10.1007/978-3-030-53288-8_14
chicago: Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Refinement for Structured
Concurrent Programs.” In Computer Aided Verification, 12224:275–98. Springer
Nature, 2020. https://doi.org/10.1007/978-3-030-53288-8_14.
ieee: B. Kragl, S. Qadeer, and T. A. Henzinger, “Refinement for structured concurrent
programs,” in Computer Aided Verification, 2020, vol. 12224, pp. 275–298.
ista: Kragl B, Qadeer S, Henzinger TA. 2020. Refinement for structured concurrent
programs. Computer Aided Verification. , LNCS, vol. 12224, 275–298.
mla: Kragl, Bernhard, et al. “Refinement for Structured Concurrent Programs.” Computer
Aided Verification, vol. 12224, Springer Nature, 2020, pp. 275–98, doi:10.1007/978-3-030-53288-8_14.
short: B. Kragl, S. Qadeer, T.A. Henzinger, in:, Computer Aided Verification, Springer
Nature, 2020, pp. 275–298.
date_created: 2020-08-03T11:45:35Z
date_published: 2020-07-14T00:00:00Z
date_updated: 2023-09-07T13:18:00Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-53288-8_14
external_id:
isi:
- '000695276000014'
file:
- access_level: open_access
content_type: application/pdf
creator: dernst
date_created: 2020-08-06T08:14:54Z
date_updated: 2020-08-06T08:14:54Z
file_id: '8201'
file_name: 2020_LNCS_Kragl.pdf
file_size: 804237
relation: main_file
success: 1
file_date_updated: 2020-08-06T08:14:54Z
has_accepted_license: '1'
intvolume: ' 12224'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 275-298
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Computer Aided Verification
publication_identifier:
eisbn:
- '9783030532888'
eissn:
- 1611-3349
isbn:
- '9783030532871'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '8332'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Refinement for structured concurrent programs
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12224
year: '2020'
...
---
_id: '8012'
abstract:
- lang: eng
text: Asynchronous programs are notoriously difficult to reason about because they
spawn computation tasks which take effect asynchronously in a nondeterministic
way. Devising inductive invariants for such programs requires understanding and
stating complex relationships between an unbounded number of computation tasks
in arbitrarily long executions. In this paper, we introduce inductive sequentialization,
a new proof rule that sidesteps this complexity via a sequential reduction, a
sequential program 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. We have implemented and integrated our proof
rule in the CIVL verifier, allowing us to provably derive fine-grained implementations
of asynchronous programs. We have successfully applied our proof rule to a diverse
set of message-passing protocols, including leader election protocols, two-phase
commit, and Paxos.
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: Constantin
full_name: Enea, Constantin
last_name: Enea
- 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: Suha Orhun
full_name: Mutluergil, Suha Orhun
last_name: Mutluergil
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: 'Kragl B, Enea C, Henzinger TA, Mutluergil SO, Qadeer S. Inductive sequentialization
of asynchronous programs. In: Proceedings of the 41st ACM SIGPLAN Conference
on Programming Language Design and Implementation. Association for Computing
Machinery; 2020:227-242. doi:10.1145/3385412.3385980'
apa: 'Kragl, B., Enea, C., Henzinger, T. A., Mutluergil, S. O., & Qadeer, S.
(2020). Inductive sequentialization of asynchronous programs. In Proceedings
of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
(pp. 227–242). London, United Kingdom: Association for Computing Machinery. https://doi.org/10.1145/3385412.3385980'
chicago: Kragl, Bernhard, Constantin Enea, Thomas A Henzinger, Suha Orhun Mutluergil,
and Shaz Qadeer. “Inductive Sequentialization of Asynchronous Programs.” In Proceedings
of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation,
227–42. Association for Computing Machinery, 2020. https://doi.org/10.1145/3385412.3385980.
ieee: B. Kragl, C. Enea, T. A. Henzinger, S. O. Mutluergil, and S. Qadeer, “Inductive
sequentialization of asynchronous programs,” in Proceedings of the 41st ACM
SIGPLAN Conference on Programming Language Design and Implementation, London,
United Kingdom, 2020, pp. 227–242.
ista: 'Kragl B, Enea C, Henzinger TA, Mutluergil SO, Qadeer S. 2020. Inductive sequentialization
of asynchronous programs. Proceedings of the 41st ACM SIGPLAN Conference on Programming
Language Design and Implementation. PLDI: Programming Language Design and Implementation,
227–242.'
mla: Kragl, Bernhard, et al. “Inductive Sequentialization of Asynchronous Programs.”
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
and Implementation, Association for Computing Machinery, 2020, pp. 227–42,
doi:10.1145/3385412.3385980.
short: B. Kragl, C. Enea, T.A. Henzinger, S.O. Mutluergil, S. Qadeer, in:, Proceedings
of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation,
Association for Computing Machinery, 2020, pp. 227–242.
conference:
end_date: 2020-06-20
location: London, United Kingdom
name: 'PLDI: Programming Language Design and Implementation'
start_date: 2020-06-15
date_created: 2020-06-25T11:40:16Z
date_published: 2020-06-01T00:00:00Z
date_updated: 2023-09-07T13:18:00Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3385412.3385980
external_id:
isi:
- '000614622300016'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3385412.3385980
month: '06'
oa: 1
oa_version: Published Version
page: 227-242
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language
Design and Implementation
publication_identifier:
isbn:
- '9781450376136'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '8332'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Inductive sequentialization of asynchronous programs
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2020'
...
---
_id: '10861'
abstract:
- lang: eng
text: We introduce in this paper AMT2.0, a tool for qualitative and quantitative
analysis of hybrid continuous and Boolean signals that combine numerical values
and discrete events. The evaluation of the signals is based on rich temporal specifications
expressed in extended signal temporal logic, which integrates timed regular expressions
within signal temporal logic. The tool features qualitative monitoring (property
satisfaction checking), trace diagnostics for explaining and justifying property
violations and specification-driven measurement of quantitative features of the
signal. We demonstrate the tool functionality on several running examples and
case studies, and evaluate its performance.
article_processing_charge: No
article_type: original
author:
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Olivier
full_name: Lebeltel, Olivier
last_name: Lebeltel
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Dogan
full_name: Ulus, Dogan
last_name: Ulus
citation:
ama: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and
quantitative trace analysis with extended signal temporal logic. International
Journal on Software Tools for Technology Transfer. 2020;22(6):741-758. doi:10.1007/s10009-020-00582-z'
apa: 'Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., & Ulus, D. (2020).
AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal
logic. International Journal on Software Tools for Technology Transfer.
Springer Nature. https://doi.org/10.1007/s10009-020-00582-z'
chicago: 'Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan
Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal
Temporal Logic.” International Journal on Software Tools for Technology Transfer.
Springer Nature, 2020. https://doi.org/10.1007/s10009-020-00582-z.'
ieee: 'D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative
and quantitative trace analysis with extended signal temporal logic,” International
Journal on Software Tools for Technology Transfer, vol. 22, no. 6. Springer
Nature, pp. 741–758, 2020.'
ista: 'Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative
and quantitative trace analysis with extended signal temporal logic. International
Journal on Software Tools for Technology Transfer. 22(6), 741–758.'
mla: 'Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis
with Extended Signal Temporal Logic.” International Journal on Software Tools
for Technology Transfer, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58,
doi:10.1007/s10009-020-00582-z.'
short: D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal
on Software Tools for Technology Transfer 22 (2020) 741–758.
date_created: 2022-03-18T10:10:53Z
date_published: 2020-08-03T00:00:00Z
date_updated: 2023-09-08T11:52:02Z
day: '03'
department:
- _id: ToHe
doi: 10.1007/s10009-020-00582-z
external_id:
isi:
- '000555398600001'
intvolume: ' 22'
isi: 1
issue: '6'
keyword:
- Information Systems
- Software
language:
- iso: eng
month: '08'
oa_version: None
page: 741-758
publication: International Journal on Software Tools for Technology Transfer
publication_identifier:
eissn:
- 1433-2787
issn:
- 1433-2779
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '299'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'AMT 2.0: Qualitative and quantitative trace analysis with extended signal
temporal logic'
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 22
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: '9202'
abstract:
- lang: eng
text: We propose a novel hybridization method for stability analysis that over-approximates
nonlinear dynamical systems by switched systems with linear inclusion dynamics.
We observe that existing hybridization techniques for safety analysis that over-approximate
nonlinear dynamical systems by switched affine inclusion dynamics and provide
fixed approximation error, do not suffice for stability analysis. Hence, we propose
a hybridization method that provides a state-dependent error which converges to
zero as the state tends to the equilibrium point. The crux of our hybridization
computation is an elegant recursive algorithm that uses partial derivatives of
a given function to obtain upper and lower bound matrices for the over-approximating
linear inclusion. We illustrate our method on some examples to demonstrate the
application of the theory for stability analysis. In particular, our method is
able to establish stability of a nonlinear system which does not admit a polynomial
Lyapunov function.
acknowledgement: Miriam Garc´ıa Soto was partially supported by the Austrian Science
Fund (FWF) under grant Z211-N23 (Wittgenstein Award). Pavithra Prabhakar was partially
supported by NSF CAREER Award No. 1552668, NSF Award No. 2008957 and ONR YIP Award
No. N000141712577.
article_processing_charge: No
author:
- first_name: Miriam
full_name: Garcia Soto, Miriam
id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
last_name: Garcia Soto
orcid: 0000-0003-2936-5719
- first_name: Pavithra
full_name: Prabhakar, Pavithra
last_name: Prabhakar
citation:
ama: 'Garcia Soto M, Prabhakar P. Hybridization for stability verification of nonlinear
switched systems. In: 2020 IEEE Real-Time Systems Symposium. IEEE; 2020:244-256.
doi:10.1109/RTSS49844.2020.00031'
apa: 'Garcia Soto, M., & Prabhakar, P. (2020). Hybridization for stability verification
of nonlinear switched systems. In 2020 IEEE Real-Time Systems Symposium
(pp. 244–256). Houston, TX, USA : IEEE. https://doi.org/10.1109/RTSS49844.2020.00031'
chicago: Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability
Verification of Nonlinear Switched Systems.” In 2020 IEEE Real-Time Systems
Symposium, 244–56. IEEE, 2020. https://doi.org/10.1109/RTSS49844.2020.00031.
ieee: M. Garcia Soto and P. Prabhakar, “Hybridization for stability verification
of nonlinear switched systems,” in 2020 IEEE Real-Time Systems Symposium,
Houston, TX, USA , 2020, pp. 244–256.
ista: 'Garcia Soto M, Prabhakar P. 2020. Hybridization for stability verification
of nonlinear switched systems. 2020 IEEE Real-Time Systems Symposium. RTTS: Real-Time
Systems Symposium, 244–256.'
mla: Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability Verification
of Nonlinear Switched Systems.” 2020 IEEE Real-Time Systems Symposium,
IEEE, 2020, pp. 244–56, doi:10.1109/RTSS49844.2020.00031.
short: M. Garcia Soto, P. Prabhakar, in:, 2020 IEEE Real-Time Systems Symposium,
IEEE, 2020, pp. 244–256.
conference:
end_date: 2020-12-04
location: 'Houston, TX, USA '
name: 'RTTS: Real-Time Systems Symposium'
start_date: 2020-12-01
date_created: 2021-02-26T16:38:24Z
date_published: 2020-12-01T00:00:00Z
date_updated: 2024-02-22T13:25:19Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/RTSS49844.2020.00031
external_id:
isi:
- '000680435100021'
file:
- access_level: open_access
checksum: 8f97f229316c3b3a6f0cf99297aa0941
content_type: application/pdf
creator: mgarcias
date_created: 2021-02-26T16:38:14Z
date_updated: 2021-02-26T16:38:14Z
file_id: '9203'
file_name: main.pdf
file_size: 1125794
relation: main_file
file_date_updated: 2021-02-26T16:38:14Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '12'
oa: 1
oa_version: Submitted Version
page: 244-256
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 2020 IEEE Real-Time Systems Symposium
publication_identifier:
eisbn:
- '9781728183244'
eissn:
- 2576-3172
publication_status: published
publisher: IEEE
quality_controlled: '1'
status: public
title: Hybridization for stability verification of nonlinear switched systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2020'
...
---
_id: '7426'
abstract:
- lang: eng
text: This paper presents a novel abstraction technique for analyzing Lyapunov and
asymptotic stability of polyhedral switched systems. A polyhedral switched system
is a hybrid system in which the continuous dynamics is specified by polyhedral
differential inclusions, the invariants and guards are specified by polyhedral
sets and the switching between the modes do not involve reset of variables. A
finite state weighted graph abstracting the polyhedral switched system is constructed
from a finite partition of the state–space, such that the satisfaction of certain
graph conditions, such as the absence of cycles with product of weights on the
edges greater than (or equal) to 1, implies the stability of the system. However,
the graph is in general conservative and hence, the violation of the graph conditions
does not imply instability. If the analysis fails to establish stability due to
the conservativeness in the approximation, a counterexample (cycle with product
of edge weights greater than or equal to 1) indicating a potential reason for
the failure is returned. Further, a more precise approximation of the switched
system can be constructed by considering a finer partition of the state–space
in the construction of the finite weighted graph. We present experimental results
on analyzing stability of switched systems using the above method.
article_number: '100856'
article_processing_charge: No
article_type: original
author:
- first_name: Miriam
full_name: Garcia Soto, Miriam
id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
last_name: Garcia Soto
orcid: 0000−0003−2936−5719
- first_name: Pavithra
full_name: Prabhakar, Pavithra
last_name: Prabhakar
citation:
ama: 'Garcia Soto M, Prabhakar P. Abstraction based verification of stability of
polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 2020;36(5).
doi:10.1016/j.nahs.2020.100856'
apa: 'Garcia Soto, M., & Prabhakar, P. (2020). Abstraction based verification
of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems.
Elsevier. https://doi.org/10.1016/j.nahs.2020.100856'
chicago: 'Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification
of Stability of Polyhedral Switched Systems.” Nonlinear Analysis: Hybrid Systems.
Elsevier, 2020. https://doi.org/10.1016/j.nahs.2020.100856.'
ieee: 'M. Garcia Soto and P. Prabhakar, “Abstraction based verification of stability
of polyhedral switched systems,” Nonlinear Analysis: Hybrid Systems, vol.
36, no. 5. Elsevier, 2020.'
ista: 'Garcia Soto M, Prabhakar P. 2020. Abstraction based verification of stability
of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 36(5), 100856.'
mla: 'Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification
of Stability of Polyhedral Switched Systems.” Nonlinear Analysis: Hybrid Systems,
vol. 36, no. 5, 100856, Elsevier, 2020, doi:10.1016/j.nahs.2020.100856.'
short: 'M. Garcia Soto, P. Prabhakar, Nonlinear Analysis: Hybrid Systems 36 (2020).'
date_created: 2020-02-02T23:00:59Z
date_published: 2020-05-01T00:00:00Z
date_updated: 2023-08-17T14:32:54Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2020.100856
external_id:
isi:
- '000528828600003'
file:
- access_level: open_access
checksum: 560abfddb53f9fe921b6744f59f2cfaa
content_type: application/pdf
creator: dernst
date_created: 2020-10-21T13:16:45Z
date_updated: 2022-05-16T22:30:04Z
embargo: 2022-05-15
file_id: '8688'
file_name: 2020_NAHS_GarciaSoto.pdf
file_size: 818774
relation: main_file
file_date_updated: 2022-05-16T22:30:04Z
has_accepted_license: '1'
intvolume: ' 36'
isi: 1
issue: '5'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_identifier:
issn:
- 1751-570X
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstraction based verification of stability of polyhedral switched systems
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: 36
year: '2020'
...
---
_id: '10877'
abstract:
- lang: eng
text: 'This report presents the results of a friendly competition for formal verification
of continuous and hybrid systems with piecewise constant dynamics. The friendly
competition took place as part of the workshop Applied Verification for Continuous
and Hybrid Systems (ARCH) in 2019. In this third edition, six tools have been
applied to solve five different benchmark problems in the category for piecewise
constant dynamics: BACH, Lyse, Hy- COMP, PHAVer/SX, PHAVerLite, and VeriSiMPL.
Compared to last year, a new tool has participated (HyCOMP) and PHAVerLite has
replaced PHAVer-lite. The result is a snap- shot 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 probably provide
the most complete assessment of tools for the safety verification of continuous
and hybrid systems with piecewise constant dynamics up to this date.'
acknowledgement: "The authors gratefully acknowledge \fnancial support by the European
Commission project\r\nUnCoVerCPS under grant number 643921. Lei Bu is supported
by the National Natural Science\r\nFoundation of China (No.61572249)."
alternative_title:
- EPiC Series in Computing
article_processing_charge: No
author:
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Alessandro
full_name: Abate, Alessandro
last_name: Abate
- first_name: Dieky
full_name: Adzkiya, Dieky
last_name: Adzkiya
- first_name: Anna
full_name: Becchi, Anna
last_name: Becchi
- first_name: Lei
full_name: Bu, Lei
last_name: Bu
- first_name: Alessandro
full_name: Cimatti, Alessandro
last_name: Cimatti
- first_name: Mirco
full_name: Giacobbe, Mirco
id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
last_name: Giacobbe
orcid: 0000-0001-8180-0904
- first_name: Alberto
full_name: Griggio, Alberto
last_name: Griggio
- first_name: Sergio
full_name: Mover, Sergio
last_name: Mover
- first_name: Muhammad Syifa'ul
full_name: Mufid, Muhammad Syifa'ul
last_name: Mufid
- first_name: Idriss
full_name: Riouak, Idriss
last_name: Riouak
- first_name: Stefano
full_name: Tonetta, Stefano
last_name: Tonetta
- first_name: Enea
full_name: Zaffanella, Enea
last_name: Zaffanella
citation:
ama: 'Frehse G, Abate A, Adzkiya D, et al. ARCH-COMP19 Category Report: Hybrid systems
with piecewise constant dynamics. In: Frehse G, Althoff M, eds. ARCH19. 6th
International Workshop on Applied Verification of Continuous and Hybrid Systems.
Vol 61. EasyChair; 2019:1-13. doi:10.29007/rjwn'
apa: 'Frehse, G., Abate, A., Adzkiya, D., Becchi, A., Bu, L., Cimatti, A., … Zaffanella,
E. (2019). ARCH-COMP19 Category Report: Hybrid systems with piecewise constant
dynamics. In G. Frehse & M. Althoff (Eds.), ARCH19. 6th International Workshop
on Applied Verification of Continuous and Hybrid Systems (Vol. 61, pp. 1–13).
Montreal, Canada: EasyChair. https://doi.org/10.29007/rjwn'
chicago: 'Frehse, Goran, Alessandro Abate, Dieky Adzkiya, Anna Becchi, Lei Bu, Alessandro
Cimatti, Mirco Giacobbe, et al. “ARCH-COMP19 Category Report: Hybrid Systems with
Piecewise Constant Dynamics.” In ARCH19. 6th International Workshop on Applied
Verification of Continuous and Hybrid Systems, edited by Goran Frehse and
Matthias Althoff, 61:1–13. EasyChair, 2019. https://doi.org/10.29007/rjwn.'
ieee: 'G. Frehse et al., “ARCH-COMP19 Category Report: Hybrid systems with
piecewise constant dynamics,” in ARCH19. 6th International Workshop on Applied
Verification of Continuous and Hybrid Systems, Montreal, Canada, 2019, vol.
61, pp. 1–13.'
ista: 'Frehse G, Abate A, Adzkiya D, Becchi A, Bu L, Cimatti A, Giacobbe M, Griggio
A, Mover S, Mufid MS, Riouak I, Tonetta S, Zaffanella E. 2019. ARCH-COMP19 Category
Report: Hybrid systems with piecewise constant dynamics. ARCH19. 6th International
Workshop on Applied Verification of Continuous and Hybrid Systems. ARCH: International
Workshop on Applied Verification on Continuous and Hybrid Systems, EPiC Series
in Computing, vol. 61, 1–13.'
mla: 'Frehse, Goran, et al. “ARCH-COMP19 Category Report: Hybrid Systems with Piecewise
Constant Dynamics.” ARCH19. 6th International Workshop on Applied Verification
of Continuous and Hybrid Systems, edited by Goran Frehse and Matthias Althoff,
vol. 61, EasyChair, 2019, pp. 1–13, doi:10.29007/rjwn.'
short: G. Frehse, A. Abate, D. Adzkiya, A. Becchi, L. Bu, A. Cimatti, M. Giacobbe,
A. Griggio, S. Mover, M.S. Mufid, I. Riouak, S. Tonetta, E. Zaffanella, in:, G.
Frehse, M. Althoff (Eds.), ARCH19. 6th International Workshop on Applied Verification
of Continuous and Hybrid Systems, EasyChair, 2019, pp. 1–13.
conference:
end_date: 2019-04-15
location: Montreal, Canada
name: 'ARCH: International Workshop on Applied Verification on Continuous and Hybrid
Systems'
start_date: 2019-04-15
date_created: 2022-03-18T12:29:23Z
date_published: 2019-05-25T00:00:00Z
date_updated: 2022-05-17T07:09:47Z
day: '25'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.29007/rjwn
editor:
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Matthias
full_name: Althoff, Matthias
last_name: Althoff
file:
- access_level: open_access
checksum: 4b92e333db7b4e2349501a804dfede69
content_type: application/pdf
creator: dernst
date_created: 2022-05-17T06:55:49Z
date_updated: 2022-05-17T06:55:49Z
file_id: '11391'
file_name: 2019_EPiCs_Frehse.pdf
file_size: 346415
relation: main_file
success: 1
file_date_updated: 2022-05-17T06:55:49Z
has_accepted_license: '1'
intvolume: ' 61'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 1-13
publication: ARCH19. 6th International Workshop on Applied Verification of Continuous
and Hybrid Systems
publication_identifier:
issn:
- 2398-7340
publication_status: published
publisher: EasyChair
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 61
year: '2019'
...
---
_id: '6565'
abstract:
- lang: eng
text: In this paper, we address the problem of synthesizing periodic switching controllers
for stabilizing a family of linear systems. Our broad approach consists of constructing
a finite game graph based on the family of linear systems such that every winning
strategy on the game graph corresponds to a stabilizing switching controller for
the family of linear systems. The construction of a (finite) game graph, the synthesis
of a winning strategy and the extraction of a stabilizing controller are all computationally
feasible. We illustrate our method on an example.
article_number: '8715598'
article_processing_charge: No
author:
- first_name: Atreyee
full_name: Kundu, Atreyee
last_name: Kundu
- first_name: Miriam
full_name: Garcia Soto, Miriam
id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
last_name: Garcia Soto
orcid: 0000−0003−2936−5719
- first_name: Pavithra
full_name: Prabhakar, Pavithra
last_name: Prabhakar
citation:
ama: 'Kundu A, Garcia Soto M, Prabhakar P. Formal synthesis of stabilizing controllers
for periodically controlled linear switched systems. In: 5th Indian Control
Conference Proceedings. IEEE; 2019. doi:10.1109/INDIANCC.2019.8715598'
apa: 'Kundu, A., Garcia Soto, M., & Prabhakar, P. (2019). Formal synthesis of
stabilizing controllers for periodically controlled linear switched systems. In
5th Indian Control Conference Proceedings. Delhi, India: IEEE. https://doi.org/10.1109/INDIANCC.2019.8715598'
chicago: Kundu, Atreyee, Miriam Garcia Soto, and Pavithra Prabhakar. “Formal Synthesis
of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.”
In 5th Indian Control Conference Proceedings. IEEE, 2019. https://doi.org/10.1109/INDIANCC.2019.8715598.
ieee: A. Kundu, M. Garcia Soto, and P. Prabhakar, “Formal synthesis of stabilizing
controllers for periodically controlled linear switched systems,” in 5th Indian
Control Conference Proceedings, Delhi, India, 2019.
ista: Kundu A, Garcia Soto M, Prabhakar P. 2019. Formal synthesis of stabilizing
controllers for periodically controlled linear switched systems. 5th Indian Control
Conference Proceedings. ICC 2019 - Indian Control Conference, 8715598.
mla: Kundu, Atreyee, et al. “Formal Synthesis of Stabilizing Controllers for Periodically
Controlled Linear Switched Systems.” 5th Indian Control Conference Proceedings,
8715598, IEEE, 2019, doi:10.1109/INDIANCC.2019.8715598.
short: A. Kundu, M. Garcia Soto, P. Prabhakar, in:, 5th Indian Control Conference
Proceedings, IEEE, 2019.
conference:
end_date: 2019-01-11
location: Delhi, India
name: ICC 2019 - Indian Control Conference
start_date: 2019-01-09
date_created: 2019-06-17T06:57:33Z
date_published: 2019-05-16T00:00:00Z
date_updated: 2021-01-12T08:08:01Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/INDIANCC.2019.8715598
file:
- access_level: open_access
checksum: d622a91af1e427f6b1e0ba8e18a2b767
content_type: application/pdf
creator: dernst
date_created: 2020-10-21T13:13:49Z
date_updated: 2020-10-21T13:13:49Z
file_id: '8687'
file_name: 2019_ICC_Kundu.pdf
file_size: 396031
relation: main_file
success: 1
file_date_updated: 2020-10-21T13:13:49Z
has_accepted_license: '1'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
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
publication: 5th Indian Control Conference Proceedings
publication_identifier:
isbn:
- 978-153866246-5
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Formal synthesis of stabilizing controllers for periodically controlled linear
switched systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2019'
...
---
_id: '6822'
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 qualitative winner or quantitative
payoff of the game. In bidding games, in each turn, we hold an auction between
the two players to determine which player moves the token. Bidding games have
largely been studied with concrete bidding mechanisms that are variants of a first-price
auction: in each turn both players simultaneously submit bids, the higher\r\nbidder
moves the token, and pays his bid to the lower bidder in Richman bidding, to the
bank in poorman bidding, and in taxman bidding, the bid is split between the other
player and the bank according to a predefined constant factor. Bidding games are
deterministic games. They have an intriguing connection with a fragment of stochastic
games called \r\n randomturn games. We study, for the first time, a combination
of bidding games with probabilistic behavior; namely, we study bidding games that
are played on Markov decision processes, where the players bid for the right to
choose the next action, which determines the probability distribution according
to which the next vertex is chosen. We study parity and meanpayoff bidding games
on MDPs and extend results from the deterministic bidding setting to the probabilistic
one."
alternative_title:
- LNCS
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Petr
full_name: Novotny, Petr
last_name: Novotny
citation:
ama: 'Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision
processes. In: Proceedings of the 13th International Conference of Reachability
Problems. Vol 11674. Springer; 2019:1-12. doi:10.1007/978-3-030-30806-3_1'
apa: 'Avni, G., Henzinger, T. A., Ibsen-Jensen, R., & Novotny, P. (2019). Bidding
games on Markov decision processes. In Proceedings of the 13th International
Conference of Reachability Problems (Vol. 11674, pp. 1–12). Brussels, Belgium:
Springer. https://doi.org/10.1007/978-3-030-30806-3_1'
chicago: Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding
Games on Markov Decision Processes.” In Proceedings of the 13th International
Conference of Reachability Problems, 11674:1–12. Springer, 2019. https://doi.org/10.1007/978-3-030-30806-3_1.
ieee: G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games
on Markov decision processes,” in Proceedings of the 13th International Conference
of Reachability Problems, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.
ista: 'Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. 2019. Bidding games on Markov
decision processes. Proceedings of the 13th International Conference of Reachability
Problems. RP: Reachability Problems, LNCS, vol. 11674, 1–12.'
mla: Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” Proceedings
of the 13th International Conference of Reachability Problems, vol. 11674,
Springer, 2019, pp. 1–12, doi:10.1007/978-3-030-30806-3_1.
short: G. Avni, T.A. Henzinger, R. Ibsen-Jensen, P. Novotny, in:, Proceedings of
the 13th International Conference of Reachability Problems, Springer, 2019, pp.
1–12.
conference:
end_date: 2019-09-13
location: Brussels, Belgium
name: 'RP: Reachability Problems'
start_date: 2019-09-11
date_created: 2019-08-19T07:58:10Z
date_published: 2019-09-06T00:00:00Z
date_updated: 2021-01-12T08:09:12Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-30806-3_1
file:
- access_level: open_access
checksum: 45ebbc709af2b247d28c7c293c01504b
content_type: application/pdf
creator: gavni
date_created: 2019-08-19T07:56:40Z
date_updated: 2020-07-14T12:47:41Z
file_id: '6823'
file_name: prob.pdf
file_size: 436635
relation: main_file
file_date_updated: 2020-07-14T12:47:41Z
has_accepted_license: '1'
intvolume: ' 11674'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 1-12
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: ' Proceedings of the 13th International Conference of Reachability Problems'
publication_identifier:
isbn:
- 978-303030805-6
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: 1
status: public
title: Bidding games on Markov decision processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 11674
year: '2019'
...
---
_id: '6888'
abstract:
- lang: eng
text: In this paper, we design novel liquid time-constant recurrent neural networks
for robotic control, inspired by the brain of the nematode, C. elegans. In the
worm's nervous system, neurons communicate through nonlinear time-varying synaptic
links established amongst them by their particular wiring structure. This property
enables neurons to express liquid time-constants dynamics and therefore allows
the network to originate complex behaviors with a small number of neurons. We
identify neuron-pair communication motifs as design operators and use them to
configure compact neuronal network structures to govern sequential robotic tasks.
The networks are systematically designed to map the environmental observations
to motor actions, by their hierarchical topology from sensory neurons, through
recurrently-wired interneurons, to motor neurons. The networks are then parametrized
in a supervised-learning scheme by a search-based algorithm. We demonstrate that
obtained networks realize interpretable dynamics. We evaluate their performance
in controlling mobile and arm robots, and compare their attributes to other artificial
neural network-based control agents. Finally, we experimentally show their superior
resilience to environmental noise, compared to the existing machine learning-based
methods.
alternative_title:
- ICRA
article_number: '8793840'
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: Manuel
full_name: Zimmer, Manuel
last_name: Zimmer
- 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: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Lechner M, Hasani R, Zimmer M, Henzinger TA, Grosu R. Designing worm-inspired
neural networks for interpretable robotic control. In: Proceedings - IEEE International
Conference on Robotics and Automation. Vol 2019-May. IEEE; 2019. doi:10.1109/icra.2019.8793840'
apa: 'Lechner, M., Hasani, R., Zimmer, M., Henzinger, T. A., & Grosu, R. (2019).
Designing worm-inspired neural networks for interpretable robotic control. In
Proceedings - IEEE International Conference on Robotics and Automation
(Vol. 2019–May). Montreal, QC, Canada: IEEE. https://doi.org/10.1109/icra.2019.8793840'
chicago: Lechner, Mathias, Ramin Hasani, Manuel Zimmer, Thomas A Henzinger, and
Radu Grosu. “Designing Worm-Inspired Neural Networks for Interpretable Robotic
Control.” In Proceedings - IEEE International Conference on Robotics and Automation,
Vol. 2019–May. IEEE, 2019. https://doi.org/10.1109/icra.2019.8793840.
ieee: M. Lechner, R. Hasani, M. Zimmer, T. A. Henzinger, and R. Grosu, “Designing
worm-inspired neural networks for interpretable robotic control,” in Proceedings
- IEEE International Conference on Robotics and Automation, Montreal, QC,
Canada, 2019, vol. 2019–May.
ista: 'Lechner M, Hasani R, Zimmer M, Henzinger TA, Grosu R. 2019. Designing worm-inspired
neural networks for interpretable robotic control. Proceedings - IEEE International
Conference on Robotics and Automation. ICRA: International Conference on Robotics
and Automation, ICRA, vol. 2019–May, 8793840.'
mla: Lechner, Mathias, et al. “Designing Worm-Inspired Neural Networks for Interpretable
Robotic Control.” Proceedings - IEEE International Conference on Robotics and
Automation, vol. 2019–May, 8793840, IEEE, 2019, doi:10.1109/icra.2019.8793840.
short: M. Lechner, R. Hasani, M. Zimmer, T.A. Henzinger, R. Grosu, in:, Proceedings
- IEEE International Conference on Robotics and Automation, IEEE, 2019.
conference:
end_date: 2019-05-24
location: Montreal, QC, Canada
name: 'ICRA: International Conference on Robotics and Automation'
start_date: 2019-05-20
date_created: 2019-09-18T08:09:51Z
date_published: 2019-05-01T00:00:00Z
date_updated: 2021-01-12T08:09:28Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/icra.2019.8793840
file:
- access_level: open_access
checksum: f5545a6b60c3ffd01feb3613f81d03b6
content_type: application/pdf
creator: dernst
date_created: 2020-10-08T17:30:38Z
date_updated: 2020-10-08T17:30:38Z
file_id: '8636'
file_name: 2019_ICRA_Lechner.pdf
file_size: 3265107
relation: main_file
success: 1
file_date_updated: 2020-10-08T17:30:38Z
has_accepted_license: '1'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
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:
- '9781538660270'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Designing worm-inspired neural networks for interpretable robotic control
type: conference
user_id: D865714E-FA4E-11E9-B85B-F5C5E5697425
volume: 2019-May
year: '2019'
...
---
_id: '6886'
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. '
alternative_title:
- LIPIcs
article_number: '20'
article_processing_charge: No
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. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.CONCUR.2019.20'
apa: 'Aghajohari, M., Avni, G., & Henzinger, T. A. (2019). Determinacy in discrete-bidding
infinite-duration games (Vol. 140). Presented at the CONCUR: International Conference
on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPICS.CONCUR.2019.20'
chicago: Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding
Infinite-Duration Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2019. https://doi.org/10.4230/LIPICS.CONCUR.2019.20.
ieee: 'M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding
infinite-duration games,” presented at the CONCUR: International Conference on
Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.'
ista: 'Aghajohari M, Avni G, Henzinger TA. 2019. Determinacy in discrete-bidding
infinite-duration games. CONCUR: International Conference on Concurrency Theory,
LIPIcs, vol. 140, 20.'
mla: Aghajohari, Milad, et al. Determinacy in Discrete-Bidding Infinite-Duration
Games. Vol. 140, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019,
doi:10.4230/LIPICS.CONCUR.2019.20.
short: M. Aghajohari, G. Avni, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2019.
conference:
end_date: 2019-08-30
location: Amsterdam, Netherlands
name: 'CONCUR: International Conference on Concurrency Theory'
start_date: 2019-08-27
date_created: 2019-09-18T08:06:58Z
date_published: 2019-08-01T00:00:00Z
date_updated: 2022-01-26T08:27:10Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPICS.CONCUR.2019.20
external_id:
arxiv:
- '1905.03588'
file:
- access_level: open_access
checksum: 4df6d3575c506edb17215adada03cc8e
content_type: application/pdf
creator: kschuh
date_created: 2019-09-27T12:21:38Z
date_updated: 2020-07-14T12:47:43Z
file_id: '6915'
file_name: 2019_LIPIcs_Aghajohari.pdf
file_size: 741425
relation: main_file
file_date_updated: 2020-07-14T12:47:43Z
has_accepted_license: '1'
intvolume: ' 140'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
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/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 140
year: '2019'
...
---
_id: '6885'
abstract:
- lang: eng
text: 'A vector addition system with states (VASS) consists of a finite set of states
and counters. A configuration is a state and a value for each counter; a transition
changes the state and each counter is incremented, decremented, or left unchanged.
While qualitative properties such as state and configuration reachability have
been studied for VASS, we consider the long-run average cost of infinite computations
of VASS. The cost of a configuration is for each state, a linear combination of
the counter values. In the special case of uniform cost functions, the linear
combination is the same for all states. The (regular) long-run emptiness problem
is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped)
computation such that the long-run average value of the cost function does not
exceed the threshold. For uniform cost functions, we show that the regular long-run
emptiness problem is (a) decidable in polynomial time for integer-valued VASS,
and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative
counters). For general cost functions, we show that the problem is (c) NP-complete
for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most
interesting result is for (c) integer-valued VASS with general cost functions,
where we establish a connection between the regular long-run emptiness problem
and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness
problem is equally hard as the regular problem in all cases except (c), where
it remains open. '
alternative_title:
- LIPIcs
article_number: '27'
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
last_name: Otop
citation:
ama: 'Chatterjee K, Henzinger TA, Otop J. Long-run average behavior of vector addition
systems with states. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2019. doi:10.4230/LIPICS.CONCUR.2019.27'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2019). Long-run average
behavior of vector addition systems with states (Vol. 140). Presented at the CONCUR:
International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.CONCUR.2019.27'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Long-Run Average
Behavior of Vector Addition Systems with States,” Vol. 140. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2019. https://doi.org/10.4230/LIPICS.CONCUR.2019.27.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Long-run average behavior of
vector addition systems with states,” presented at the CONCUR: International Conference
on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2019. Long-run average behavior of vector
addition systems with states. CONCUR: International Conference on Concurrency
Theory, LIPIcs, vol. 140, 27.'
mla: Chatterjee, Krishnendu, et al. Long-Run Average Behavior of Vector Addition
Systems with States. Vol. 140, 27, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2019, doi:10.4230/LIPICS.CONCUR.2019.27.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2019.
conference:
end_date: 2019-08-30
location: Amsterdam, Netherlands
name: 'CONCUR: International Conference on Concurrency Theory'
start_date: 2019-08-27
date_created: 2019-09-18T08:06:14Z
date_published: 2019-08-01T00:00:00Z
date_updated: 2021-01-12T08:09:27Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPICS.CONCUR.2019.27
file:
- access_level: open_access
checksum: 4985e26e1572d1575d64d38acabd71d6
content_type: application/pdf
creator: kschuh
date_created: 2019-09-27T12:09:35Z
date_updated: 2020-07-14T12:47:43Z
file_id: '6914'
file_name: 2019_LIPIcs_Chatterjee.pdf
file_size: 538120
relation: main_file
file_date_updated: 2020-07-14T12:47:43Z
has_accepted_license: '1'
intvolume: ' 140'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: 1
status: public
title: Long-run average behavior of vector addition systems with states
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 140
year: '2019'
...
---
_id: '6985'
abstract:
- lang: eng
text: In this paper, we introduce a novel method to interpret recurrent neural networks
(RNNs), particularly long short-term memory networks (LSTMs) at the cellular level.
We propose a systematic pipeline for interpreting individual hidden state dynamics
within the network using response characterization methods. The ranked contribution
of individual cells to the network's output is computed by analyzing a set of
interpretable metrics of their decoupled step and sinusoidal responses. As a result,
our method is able to uniquely identify neurons with insightful dynamics, quantify
relationships between dynamical properties and test accuracy through ablation
analysis, and interpret the impact of network capacity on a network's dynamical
distribution. Finally, we demonstrate the generalizability and scalability of
our method by evaluating a series of different benchmark sequential datasets.
article_number: '8851954'
author:
- 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: Felix
full_name: Naser, Felix
last_name: Naser
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- first_name: Daniela
full_name: Rus, Daniela
last_name: Rus
citation:
ama: 'Hasani R, Amini A, Lechner M, Naser F, Grosu R, Rus D. Response characterization
for auditing cell dynamics in long short-term memory networks. In: Proceedings
of the International Joint Conference on Neural Networks. IEEE; 2019. doi:10.1109/ijcnn.2019.8851954'
apa: 'Hasani, R., Amini, A., Lechner, M., Naser, F., Grosu, R., & Rus, D. (2019).
Response characterization for auditing cell dynamics in long short-term memory
networks. In Proceedings of the International Joint Conference on Neural Networks.
Budapest, Hungary: IEEE. https://doi.org/10.1109/ijcnn.2019.8851954'
chicago: Hasani, Ramin, Alexander Amini, Mathias Lechner, Felix Naser, Radu Grosu,
and Daniela Rus. “Response Characterization for Auditing Cell Dynamics in Long
Short-Term Memory Networks.” In Proceedings of the International Joint Conference
on Neural Networks. IEEE, 2019. https://doi.org/10.1109/ijcnn.2019.8851954.
ieee: R. Hasani, A. Amini, M. Lechner, F. Naser, R. Grosu, and D. Rus, “Response
characterization for auditing cell dynamics in long short-term memory networks,”
in Proceedings of the International Joint Conference on Neural Networks,
Budapest, Hungary, 2019.
ista: 'Hasani R, Amini A, Lechner M, Naser F, Grosu R, Rus D. 2019. Response characterization
for auditing cell dynamics in long short-term memory networks. Proceedings of
the International Joint Conference on Neural Networks. IJCNN: International Joint
Conference on Neural Networks, 8851954.'
mla: Hasani, Ramin, et al. “Response Characterization for Auditing Cell Dynamics
in Long Short-Term Memory Networks.” Proceedings of the International Joint
Conference on Neural Networks, 8851954, IEEE, 2019, doi:10.1109/ijcnn.2019.8851954.
short: R. Hasani, A. Amini, M. Lechner, F. Naser, R. Grosu, D. Rus, in:, Proceedings
of the International Joint Conference on Neural Networks, IEEE, 2019.
conference:
end_date: 2019-07-19
location: Budapest, Hungary
name: 'IJCNN: International Joint Conference on Neural Networks'
start_date: 2019-07-14
date_created: 2019-11-04T15:59:58Z
date_published: 2019-09-30T00:00:00Z
date_updated: 2021-01-12T08:11:19Z
day: '30'
department:
- _id: ToHe
doi: 10.1109/ijcnn.2019.8851954
external_id:
arxiv:
- '1809.03864'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1809.03864
month: '09'
oa: 1
oa_version: Preprint
publication: Proceedings of the International Joint Conference on Neural Networks
publication_identifier:
isbn:
- '9781728119854'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: 1
status: public
title: Response characterization for auditing cell dynamics in long short-term memory
networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2019'
...
---
_id: '7453'
abstract:
- lang: eng
text: We illustrate the ingredients of the state-of-the-art of model-based approach
for the formal design and verification of cyber-physical systems. To capture the
interaction between a discrete controller and its continuously evolving environment,
we use the formal models of timed and hybrid automata. We explain the steps of
modeling and verification in the tools Uppaal and SpaceEx using a case study based
on a dual-chamber implantable pacemaker monitoring a human heart. We show how
to design a model as a composition of components, how to construct models at varying
levels of detail, how to establish that one model is an abstraction of another,
how to specify correctness requirements using temporal logic, and how to verify
that a model satisfies a logical requirement.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award). This
research has received funding from the Sino-Danish Basic Research Centre, IDEA4CPS,
funded by the Danish National Research Foundation and the National Science Foundation,
China, the Innovation Fund Denmark centre DiCyPS, as well as the ERC Advanced Grant
LASSO.
alternative_title:
- Lecture Notes in Computer Science
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Mirco
full_name: Giacobbe, Mirco
id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
last_name: Giacobbe
orcid: 0000-0001-8180-0904
- 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: Kim G.
full_name: Larsen, Kim G.
last_name: Larsen
- first_name: Marius
full_name: Mikučionis, Marius
last_name: Mikučionis
citation:
ama: 'Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. Continuous-time
models for system design and analysis. In: Steffen B, Woeginger G, eds. Computing
and Software Science. Vol 10000. LNCS. Springer Nature; 2019:452-477. doi:10.1007/978-3-319-91908-9_22'
apa: Alur, R., Giacobbe, M., Henzinger, T. A., Larsen, K. G., & Mikučionis,
M. (2019). Continuous-time models for system design and analysis. In B. Steffen
& G. Woeginger (Eds.), Computing and Software Science (Vol. 10000,
pp. 452–477). Springer Nature. https://doi.org/10.1007/978-3-319-91908-9_22
chicago: Alur, Rajeev, Mirco Giacobbe, Thomas A Henzinger, Kim G. Larsen, and Marius
Mikučionis. “Continuous-Time Models for System Design and Analysis.” In Computing
and Software Science, edited by Bernhard Steffen and Gerhard Woeginger, 10000:452–77.
LNCS. Springer Nature, 2019. https://doi.org/10.1007/978-3-319-91908-9_22.
ieee: R. Alur, M. Giacobbe, T. A. Henzinger, K. G. Larsen, and M. Mikučionis, “Continuous-time
models for system design and analysis,” in Computing and Software Science,
vol. 10000, B. Steffen and G. Woeginger, Eds. Springer Nature, 2019, pp. 452–477.
ista: 'Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. 2019.Continuous-time
models for system design and analysis. In: Computing and Software Science. Lecture
Notes in Computer Science, vol. 10000, 452–477.'
mla: Alur, Rajeev, et al. “Continuous-Time Models for System Design and Analysis.”
Computing and Software Science, edited by Bernhard Steffen and Gerhard
Woeginger, vol. 10000, Springer Nature, 2019, pp. 452–77, doi:10.1007/978-3-319-91908-9_22.
short: R. Alur, M. Giacobbe, T.A. Henzinger, K.G. Larsen, M. Mikučionis, in:, B.
Steffen, G. Woeginger (Eds.), Computing and Software Science, Springer Nature,
2019, pp. 452–477.
date_created: 2020-02-05T10:51:44Z
date_published: 2019-10-05T00:00:00Z
date_updated: 2022-09-06T08:25:52Z
day: '05'
department:
- _id: ToHe
doi: 10.1007/978-3-319-91908-9_22
editor:
- first_name: Bernhard
full_name: Steffen, Bernhard
last_name: Steffen
- first_name: Gerhard
full_name: Woeginger, Gerhard
last_name: Woeginger
intvolume: ' 10000'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1007/978-3-319-91908-9_22
month: '10'
oa: 1
oa_version: Published Version
page: 452-477
project:
- _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: Computing and Software Science
publication_identifier:
eisbn:
- '9783319919089'
eissn:
- 0302-9743
isbn:
- '9783319919072'
issn:
- 1611-3349
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Continuous-time models for system design and analysis
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10000
year: '2019'
...
---
_id: '7576'
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 2019. In this year, 6 tools Ariadne, CORA, DynIbex,
Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. They are
applied to solve reachability analysis problems on four benchmark problems, one
of them with 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.
article_processing_charge: No
author:
- first_name: Fabian
full_name: Immler, Fabian
last_name: Immler
- 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: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Luca
full_name: Geretti, Luca
last_name: Geretti
- first_name: Niklas
full_name: Kochdumper, Niklas
last_name: Kochdumper
- first_name: David P.
full_name: Sanders, David P.
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: 'Immler F, Althoff M, Benet L, et al. ARCH-COMP19 Category Report: Continuous
and hybrid systems with nonlinear dynamics. In: EPiC Series in Computing.
Vol 61. EasyChair Publications; 2019:41-61. doi:10.29007/m75b'
apa: 'Immler, F., Althoff, M., Benet, L., Chapoutot, A., Chen, X., Forets, M., …
Schilling, C. (2019). ARCH-COMP19 Category Report: Continuous and hybrid systems
with nonlinear dynamics. In EPiC Series in Computing (Vol. 61, pp. 41–61).
Montreal, Canada: EasyChair Publications. https://doi.org/10.29007/m75b'
chicago: 'Immler, Fabian, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin
Chen, Marcelo Forets, Luca Geretti, Niklas Kochdumper, David P. Sanders, and Christian
Schilling. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear
Dynamics.” In EPiC Series in Computing, 61:41–61. EasyChair Publications,
2019. https://doi.org/10.29007/m75b.'
ieee: 'F. Immler et al., “ARCH-COMP19 Category Report: Continuous and hybrid
systems with nonlinear dynamics,” in EPiC Series in Computing, Montreal,
Canada, 2019, vol. 61, pp. 41–61.'
ista: 'Immler F, Althoff M, Benet L, Chapoutot A, Chen X, Forets M, Geretti L, Kochdumper
N, Sanders DP, Schilling C. 2019. ARCH-COMP19 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. 61, 41–61.'
mla: 'Immler, Fabian, et al. “ARCH-COMP19 Category Report: Continuous and Hybrid
Systems with Nonlinear Dynamics.” EPiC Series in Computing, vol. 61, EasyChair
Publications, 2019, pp. 41–61, doi:10.29007/m75b.'
short: F. Immler, M. Althoff, L. Benet, A. Chapoutot, X. Chen, M. Forets, L. Geretti,
N. Kochdumper, D.P. Sanders, C. Schilling, in:, EPiC Series in Computing, EasyChair
Publications, 2019, pp. 41–61.
conference:
end_date: 2019-04-15
location: Montreal, Canada
name: 'ARCH: International Workshop on Applied Verification on Continuous and Hybrid
Systems'
start_date: 2019-04-15
date_created: 2020-03-08T23:00:49Z
date_published: 2019-05-25T00:00:00Z
date_updated: 2021-01-12T08:14:17Z
day: '25'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.29007/m75b
file:
- access_level: open_access
checksum: 9138977a06fcd6a95976eb4bca875f0c
content_type: application/pdf
creator: dernst
date_created: 2020-03-24T07:36:36Z
date_updated: 2020-07-14T12:48:00Z
file_id: '7617'
file_name: 2019_ARCH19_Immler.pdf
file_size: 1934830
relation: main_file
file_date_updated: 2020-07-14T12:48:00Z
has_accepted_license: '1'
intvolume: ' 61'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 41-61
publication: EPiC Series in Computing
publication_identifier:
eissn:
- '23987340'
publication_status: published
publisher: EasyChair Publications
quality_controlled: '1'
scopus_import: 1
status: public
title: 'ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear
dynamics'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 61
year: '2019'
...
---
_id: '8570'
abstract:
- lang: eng
text: 'This report presents the results of a friendly competition for formal verification
of continuous and hybrid systems with linear continuous dynamics. The friendly
competition took place as part of the workshop Applied Verification for Continuous
and Hybrid Systems (ARCH) in 2019. In its third edition, seven tools have been
applied to solve six different benchmark problems in the category for linear continuous
dynamics (in alphabetical order): CORA, CORA/SX, HyDRA, Hylaa, 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.'
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: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Niklas
full_name: Kochdumper, Niklas
last_name: Kochdumper
- 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
citation:
ama: 'Althoff M, Bak S, Forets M, et al. ARCH-COMP19 Category Report: Continuous
and hybrid systems with linear continuous dynamics. In: EPiC Series in Computing.
Vol 61. EasyChair; 2019:14-40. doi:10.29007/bj1w'
apa: 'Althoff, M., Bak, S., Forets, M., Frehse, G., Kochdumper, N., Ray, R., … Schupp,
S. (2019). ARCH-COMP19 Category Report: Continuous and hybrid systems with linear
continuous dynamics. In EPiC Series in Computing (Vol. 61, pp. 14–40).
Montreal, Canada: EasyChair. https://doi.org/10.29007/bj1w'
chicago: 'Althoff, Matthias, Stanley Bak, Marcelo Forets, Goran Frehse, Niklas Kochdumper,
Rajarshi Ray, Christian Schilling, and Stefan Schupp. “ARCH-COMP19 Category Report:
Continuous and Hybrid Systems with Linear Continuous Dynamics.” In EPiC Series
in Computing, 61:14–40. EasyChair, 2019. https://doi.org/10.29007/bj1w.'
ieee: 'M. Althoff et al., “ARCH-COMP19 Category Report: Continuous and hybrid
systems with linear continuous dynamics,” in EPiC Series in Computing,
Montreal, Canada, 2019, vol. 61, pp. 14–40.'
ista: 'Althoff M, Bak S, Forets M, Frehse G, Kochdumper N, Ray R, Schilling C, Schupp
S. 2019. ARCH-COMP19 Category Report: Continuous and hybrid systems with linear
continuous dynamics. EPiC Series in Computing. ARCH: International Workshop on
Applied Verification on Continuous and Hybrid Systems vol. 61, 14–40.'
mla: 'Althoff, Matthias, et al. “ARCH-COMP19 Category Report: Continuous and Hybrid
Systems with Linear Continuous Dynamics.” EPiC Series in Computing, vol.
61, EasyChair, 2019, pp. 14–40, doi:10.29007/bj1w.'
short: M. Althoff, S. Bak, M. Forets, G. Frehse, N. Kochdumper, R. Ray, C. Schilling,
S. Schupp, in:, EPiC Series in Computing, EasyChair, 2019, pp. 14–40.
conference:
end_date: 2019-04-15
location: Montreal, Canada
name: 'ARCH: International Workshop on Applied Verification on Continuous and Hybrid
Systems'
start_date: 2019-04-15
date_created: 2020-09-26T14:23:54Z
date_published: 2019-05-25T00:00:00Z
date_updated: 2021-01-12T08:20:05Z
day: '25'
department:
- _id: ToHe
doi: 10.29007/bj1w
intvolume: ' 61'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://easychair.org/publications/open/1gbP
month: '05'
oa: 1
oa_version: Published Version
page: 14-40
publication: EPiC Series in Computing
publication_identifier:
eissn:
- '23987340'
publication_status: published
publisher: EasyChair
quality_controlled: '1'
status: public
title: 'ARCH-COMP19 Category Report: Continuous and hybrid systems with linear continuous
dynamics'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 61
year: '2019'
...
---
_id: '6884'
abstract:
- lang: eng
text: 'In two-player games on graphs, the players move a token through a graph to
produce a finite or infinite path, which determines the qualitative winner or
quantitative payoff of the game. We study bidding games in which the players bid
for the right to move the token. Several bidding rules were studied previously.
In Richman bidding, in each round, the players simultaneously submit bids, and
the higher bidder moves the token and pays the other player. Poorman bidding is
similar except that the winner of the bidding pays the "bank" rather than the
other player. Taxman bidding spans the spectrum between Richman and poorman bidding.
They are parameterized by a constant tau in [0,1]: portion tau of the winning
bid is paid to the other player, and portion 1-tau to the bank. While finite-duration
(reachability) taxman games have been studied before, we present, for the first
time, results on infinite-duration taxman games. It was previously shown that
both Richman and poorman infinite-duration games with qualitative objectives reduce
to reachability games, and we show a similar result here. Our most interesting
results concern quantitative taxman games, namely mean-payoff games, where poorman
and Richman bidding differ significantly. A central quantity in these games is
the ratio between the two players'' initial budgets. While in poorman mean-payoff
games, the optimal payoff of a player depends on the initial ratio, in Richman
bidding, the payoff depends only on the structure of the game. In both games the
optimal payoffs can be found using (different) probabilistic connections with
random-turn games in which in each turn, instead of bidding, a coin is tossed
to determine which player moves. While the value with Richman bidding equals the
value of a random-turn game with an un-biased coin, with poorman bidding, the
bias in the coin is the initial ratio of the budgets. We give a complete classification
of mean-payoff taxman games that is based on a probabilistic connection: the value
of a taxman bidding game with parameter tau and initial ratio r, equals the value
of a random-turn game that uses a coin with bias F(tau, r) = (r+tau * (1-r))/(1+tau).
Thus, we show that Richman bidding is the exception; namely, for every tau <1,
the value of the game depends on the initial ratio. Our proof technique simplifies
and unifies the previous proof techniques for both Richman and poorman bidding. '
alternative_title:
- LIPIcs
article_number: '11'
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
citation:
ama: 'Avni G, Henzinger TA, Zikelic D. Bidding mechanisms in graph games. In: Vol
138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.MFCS.2019.11'
apa: 'Avni, G., Henzinger, T. A., & Zikelic, D. (2019). Bidding mechanisms in
graph games (Vol. 138). Presented at the MFCS: nternational Symposium on Mathematical
Foundations of Computer Science, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPICS.MFCS.2019.11'
chicago: Avni, Guy, Thomas A Henzinger, and Dorde Zikelic. “Bidding Mechanisms in
Graph Games,” Vol. 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
https://doi.org/10.4230/LIPICS.MFCS.2019.11.
ieee: 'G. Avni, T. A. Henzinger, and D. Zikelic, “Bidding mechanisms in graph games,”
presented at the MFCS: nternational Symposium on Mathematical Foundations of Computer
Science, Aachen, Germany, 2019, vol. 138.'
ista: 'Avni G, Henzinger TA, Zikelic D. 2019. Bidding mechanisms in graph games.
MFCS: nternational Symposium on Mathematical Foundations of Computer Science,
LIPIcs, vol. 138, 11.'
mla: Avni, Guy, et al. Bidding Mechanisms in Graph Games. Vol. 138, 11, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.MFCS.2019.11.
short: G. Avni, T.A. Henzinger, D. Zikelic, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2019.
conference:
end_date: 2019-08-30
location: Aachen, Germany
name: 'MFCS: nternational Symposium on Mathematical Foundations of Computer Science'
start_date: 2019-08-26
date_created: 2019-09-18T08:04:26Z
date_published: 2019-08-01T00:00:00Z
date_updated: 2023-08-07T14:08:34Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPICS.MFCS.2019.11
ec_funded: 1
external_id:
arxiv:
- '1905.03835'
file:
- access_level: open_access
checksum: 6346e116a4f4ed1414174d96d2c4fbd7
content_type: application/pdf
creator: kschuh
date_created: 2019-09-27T11:45:15Z
date_updated: 2020-07-14T12:47:42Z
file_id: '6913'
file_name: 2019_LIPIcs_Avni.pdf
file_size: 554457
relation: main_file
file_date_updated: 2020-07-14T12:47:42Z
has_accepted_license: '1'
intvolume: ' 138'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
record:
- id: '9239'
relation: later_version
status: public
scopus_import: 1
status: public
title: Bidding mechanisms in graph 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: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 138
year: '2019'
...