---
_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
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: 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: '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: '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
arxiv: 1
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: '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
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
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: '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
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: 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: '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: '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: '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: '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: '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: '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
license: https://creativecommons.org/licenses/by-nc-nd/3.0/
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: '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: '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
arxiv: 1
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: '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: '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: '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'
arxiv: 1
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: '7109'
abstract:
- lang: eng
text: We show how to construct temporal testers for the logic MITL, a prominent
linear-time logic for real-time systems. A temporal tester is a transducer that
inputs a signal holding the Boolean value of atomic propositions and outputs the
truth value of a formula along time. Here we consider testers over continuous-time
Boolean signals that use clock variables to enforce duration constraints, as in
timed automata. We first rewrite the MITL formula into a “simple” formula using
a limited set of temporal modalities. We then build testers for these specific
modalities and show how to compose testers for simple formulae into complex ones.
Temporal testers can be turned into acceptors, yielding a compositional translation
from MITL to timed automata. This construction is much simpler than previously
known and remains asymptotically optimal. It supports both past and future operators
and can easily be extended.
article_number: '19'
article_processing_charge: No
article_type: original
author:
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Ničković, Dejan
last_name: Ničković
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: Ferrere T, Maler O, Ničković D, Pnueli A. From real-time logic to timed automata.
Journal of the ACM. 2019;66(3). doi:10.1145/3286976
apa: Ferrere, T., Maler, O., Ničković, D., & Pnueli, A. (2019). From real-time
logic to timed automata. Journal of the ACM. ACM. https://doi.org/10.1145/3286976
chicago: Ferrere, Thomas, Oded Maler, Dejan Ničković, and Amir Pnueli. “From Real-Time
Logic to Timed Automata.” Journal of the ACM. ACM, 2019. https://doi.org/10.1145/3286976.
ieee: T. Ferrere, O. Maler, D. Ničković, and A. Pnueli, “From real-time logic to
timed automata,” Journal of the ACM, vol. 66, no. 3. ACM, 2019.
ista: Ferrere T, Maler O, Ničković D, Pnueli A. 2019. From real-time logic to timed
automata. Journal of the ACM. 66(3), 19.
mla: Ferrere, Thomas, et al. “From Real-Time Logic to Timed Automata.” Journal
of the ACM, vol. 66, no. 3, 19, ACM, 2019, doi:10.1145/3286976.
short: T. Ferrere, O. Maler, D. Ničković, A. Pnueli, Journal of the ACM 66 (2019).
date_created: 2019-11-26T10:22:32Z
date_published: 2019-05-01T00:00:00Z
date_updated: 2023-09-06T11:11:56Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3286976
external_id:
isi:
- '000495406300005'
intvolume: ' 66'
isi: 1
issue: '3'
language:
- iso: eng
month: '05'
oa_version: None
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: Journal of the ACM
publication_identifier:
issn:
- 0004-5411
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: From real-time logic to timed automata
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 66
year: '2019'
...
---
_id: '7147'
abstract:
- lang: eng
text: "The expression of a gene is characterised by its transcription factors and
the function processing them. If the transcription factors are not affected by
gene products, the regulating function is often represented as a combinational
logic circuit, where the outputs (product) are determined by current input values
(transcription factors) only, and are hence independent on their relative arrival
times. However, the simultaneous arrival of transcription factors (TFs) in genetic
circuits is a strong assumption, given that the processes of transcription and
translation of a gene into a protein introduce intrinsic time delays and that
there is no global synchronisation among the arrival times of different molecular
species at molecular targets.\r\n\r\nIn this paper, we construct an experimentally
implementable genetic circuit with two inputs and a single output, such that,
in presence of small delays in input arrival, the circuit exhibits qualitatively
distinct observable phenotypes. In particular, these phenotypes are long lived
transients: they all converge to a single value, but so slowly, that they seem
stable for an extended time period, longer than typical experiment duration. We
used rule-based language to prototype our circuit, and we implemented a search
for finding the parameter combinations raising the phenotypes of interest.\r\n\r\nThe
behaviour of our prototype circuit has wide implications. First, it suggests that
GRNs can exploit event timing to create phenotypes. Second, it opens the possibility
that GRNs are using event timing to react to stimuli and memorise events, without
explicit feedback in regulation. From the modelling perspective, our prototype
circuit demonstrates the critical importance of analysing the transient dynamics
at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Calin C
full_name: Guet, Calin C
id: 47F8433E-F248-11E8-B48F-1D18A9856A87
last_name: Guet
orcid: 0000-0001-6220-2052
- 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: Claudia
full_name: Igler, Claudia
id: 46613666-F248-11E8-B48F-1D18A9856A87
last_name: Igler
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: 'Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. Transient memory in gene
regulation. In: 17th International Conference on Computational Methods in Systems
Biology. Vol 11773. Springer Nature; 2019:155-187. doi:10.1007/978-3-030-31304-3_9'
apa: 'Guet, C. C., Henzinger, T. A., Igler, C., Petrov, T., & Sezgin, A. (2019).
Transient memory in gene regulation. In 17th International Conference on Computational
Methods in Systems Biology (Vol. 11773, pp. 155–187). Trieste, Italy: Springer
Nature. https://doi.org/10.1007/978-3-030-31304-3_9'
chicago: Guet, Calin C, Thomas A Henzinger, Claudia Igler, Tatjana Petrov, and Ali
Sezgin. “Transient Memory in Gene Regulation.” In 17th International Conference
on Computational Methods in Systems Biology, 11773:155–87. Springer Nature,
2019. https://doi.org/10.1007/978-3-030-31304-3_9.
ieee: C. C. Guet, T. A. Henzinger, C. Igler, T. Petrov, and A. Sezgin, “Transient
memory in gene regulation,” in 17th International Conference on Computational
Methods in Systems Biology, Trieste, Italy, 2019, vol. 11773, pp. 155–187.
ista: 'Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. 2019. Transient memory
in gene regulation. 17th International Conference on Computational Methods in
Systems Biology. CMSB: Computational Methods in Systems Biology, LNCS, vol. 11773,
155–187.'
mla: Guet, Calin C., et al. “Transient Memory in Gene Regulation.” 17th International
Conference on Computational Methods in Systems Biology, vol. 11773, Springer
Nature, 2019, pp. 155–87, doi:10.1007/978-3-030-31304-3_9.
short: C.C. Guet, T.A. Henzinger, C. Igler, T. Petrov, A. Sezgin, in:, 17th International
Conference on Computational Methods in Systems Biology, Springer Nature, 2019,
pp. 155–187.
conference:
end_date: 2019-09-20
location: Trieste, Italy
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2019-09-18
date_created: 2019-12-04T16:07:50Z
date_published: 2019-09-17T00:00:00Z
date_updated: 2023-09-06T11:18:08Z
day: '17'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/978-3-030-31304-3_9
external_id:
isi:
- '000557875100009'
intvolume: ' 11773'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 155-187
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 251EE76E-B435-11E9-9278-68D0E5697425
grant_number: '24573'
name: Design principles underlying genetic switch architecture
publication: 17th International Conference on Computational Methods in Systems Biology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783030313036'
- '9783030313043'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Transient memory in gene regulation
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11773
year: '2019'
...
---
_id: '7159'
abstract:
- lang: eng
text: 'Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a
tremendous amount of generated, measured and recorded time-series data. Extracting
temporal segments that encode patterns with useful information out of these huge
amounts of data is an extremely difficult problem. We propose shape expressions
as a declarative formalism for specifying, querying and extracting sophisticated
temporal patterns from possibly noisy data. Shape expressions are regular expressions
with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters
as atomic predicates and additional constraints on these parameters. We equip
shape expressions with a novel noisy semantics that combines regular expression
matching semantics with statistical regression. We characterize essential properties
of the formalism and propose an efficient approximate shape expression matching
procedure. We demonstrate the wide applicability of this technique on two case
studies. '
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Dejan
full_name: Ničković, Dejan
last_name: Ničković
- first_name: Xin
full_name: Qin, Xin
last_name: Qin
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Cristinel
full_name: Mateis, Cristinel
last_name: Mateis
- first_name: Jyotirmoy
full_name: Deshmukh, Jyotirmoy
last_name: Deshmukh
citation:
ama: 'Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. Shape expressions for
specifying and extracting signal features. In: 19th International Conference
on Runtime Verification. Vol 11757. Springer Nature; 2019:292-309. doi:10.1007/978-3-030-32079-9_17'
apa: 'Ničković, D., Qin, X., Ferrere, T., Mateis, C., & Deshmukh, J. (2019).
Shape expressions for specifying and extracting signal features. In 19th International
Conference on Runtime Verification (Vol. 11757, pp. 292–309). Porto, Portugal:
Springer Nature. https://doi.org/10.1007/978-3-030-32079-9_17'
chicago: Ničković, Dejan, Xin Qin, Thomas Ferrere, Cristinel Mateis, and Jyotirmoy
Deshmukh. “Shape Expressions for Specifying and Extracting Signal Features.” In
19th International Conference on Runtime Verification, 11757:292–309. Springer
Nature, 2019. https://doi.org/10.1007/978-3-030-32079-9_17.
ieee: D. Ničković, X. Qin, T. Ferrere, C. Mateis, and J. Deshmukh, “Shape expressions
for specifying and extracting signal features,” in 19th International Conference
on Runtime Verification, Porto, Portugal, 2019, vol. 11757, pp. 292–309.
ista: 'Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. 2019. Shape expressions
for specifying and extracting signal features. 19th International Conference on
Runtime Verification. RV: Runtime Verification, LNCS, vol. 11757, 292–309.'
mla: Ničković, Dejan, et al. “Shape Expressions for Specifying and Extracting Signal
Features.” 19th International Conference on Runtime Verification, vol.
11757, Springer Nature, 2019, pp. 292–309, doi:10.1007/978-3-030-32079-9_17.
short: D. Ničković, X. Qin, T. Ferrere, C. Mateis, J. Deshmukh, in:, 19th International
Conference on Runtime Verification, Springer Nature, 2019, pp. 292–309.
conference:
end_date: 2019-10-11
location: Porto, Portugal
name: 'RV: Runtime Verification'
start_date: 2019-10-08
date_created: 2019-12-09T08:47:55Z
date_published: 2019-10-01T00:00:00Z
date_updated: 2023-09-06T11:24:10Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-030-32079-9_17
external_id:
isi:
- '000570006300017'
intvolume: ' 11757'
isi: 1
language:
- iso: eng
month: '10'
oa_version: None
page: 292-309
project:
- _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: 19th International Conference on Runtime Verification
publication_identifier:
isbn:
- '9783030320782'
- '9783030320799'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Shape expressions for specifying and extracting signal features
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11757
year: '2019'
...
---
_id: '7231'
abstract:
- lang: eng
text: Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation
for nonlinear systems with polynomial dynamics, which leverages a combination
of barrier certificates. PBT has advantages over traditional time-step based methods
in dealing with those nonlinear dynamical systems in which there is a large difference
in speed between trajectories, producing an overapproximation that is time independent.
However, the existing approach for PBT is not efficient due to the application
of interval methods for enclosure-box computation, and it can only deal with continuous
dynamical systems without uncertainty. In this paper, we extend the approach with
the ability to handle both continuous and hybrid dynamical systems with uncertainty
that can reside in parameters and/or noise. We also improve the efficiency of
the method significantly, by avoiding the use of interval-based methods for the
enclosure-box computation without loosing soundness. We have developed a C++ prototype
implementing the proposed approach and we evaluate it on several benchmarks. The
experiments show that our approach is more efficient and precise than other methods
in the literature.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- 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: 'Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes
for nonlinear hybrid systems with uncertainty. In: 17th International Conference
on Formal Modeling and Analysis of Timed Systems. Vol 11750. Springer Nature;
2019:123-141. doi:10.1007/978-3-030-29662-9_8'
apa: 'Kong, H., Bartocci, E., Jiang, Y., & Henzinger, T. A. (2019). Piecewise
robust barrier tubes for nonlinear hybrid systems with uncertainty. In 17th
International Conference on Formal Modeling and Analysis of Timed Systems
(Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. https://doi.org/10.1007/978-3-030-29662-9_8'
chicago: Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise
Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In 17th
International Conference on Formal Modeling and Analysis of Timed Systems,
11750:123–41. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_8.
ieee: H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier
tubes for nonlinear hybrid systems with uncertainty,” in 17th International
Conference on Formal Modeling and Analysis of Timed Systems, Amsterdam, The
Netherlands, 2019, vol. 11750, pp. 123–141.
ista: 'Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier
tubes for nonlinear hybrid systems with uncertainty. 17th International Conference
on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and
Analysis of Timed Systems, LNCS, vol. 11750, 123–141.'
mla: Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems
with Uncertainty.” 17th International Conference on Formal Modeling and Analysis
of Timed Systems, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:10.1007/978-3-030-29662-9_8.
short: H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference
on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.
conference:
end_date: 2019-08-29
location: Amsterdam, The Netherlands
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2019-08-27
date_created: 2020-01-05T23:00:47Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2023-09-06T14:55:15Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-030-29662-9_8
external_id:
arxiv:
- '1907.11514'
isi:
- '000611677700008'
intvolume: ' 11750'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1907.11514
month: '08'
oa: 1
oa_version: Preprint
page: 123-141
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _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: 17th International Conference on Formal Modeling and Analysis of Timed
Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- 978-3-0302-9661-2
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11750
year: '2019'
...