---
_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'
...
---
_id: '6042'
abstract:
- lang: eng
text: Static program analyzers are increasingly effective in checking correctness
properties of programs and reporting any errors found, often in the form of error
traces. However, developers still spend a significant amount of time on debugging.
This involves processing long error traces in an effort to localize a bug to a
relatively small part of the program and to identify its cause. In this paper,
we present a technique for automated fault localization that, given a program
and an error trace, efficiently narrows down the cause of the error to a few statements.
These statements are then ranked in terms of their suspiciousness. Our technique
relies only on the semantics of the given program and does not require any test
cases or user guidance. In experiments on a set of C benchmarks, we show that
our technique is effective in quickly isolating the cause of error while out-performing
other state-of-the-art fault-localization techniques.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Maria
full_name: Christakis, Maria
last_name: Christakis
- first_name: Matthias
full_name: Heizmann, Matthias
last_name: Heizmann
- first_name: Muhammad Numair
full_name: Mansur, Muhammad Numair
last_name: Mansur
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Valentin
full_name: Wüstholz, Valentin
last_name: Wüstholz
citation:
ama: 'Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. Semantic fault
localization and suspiciousness ranking. In: 25th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems . Vol
11427. Springer Nature; 2019:226-243. doi:10.1007/978-3-030-17462-0_13'
apa: 'Christakis, M., Heizmann, M., Mansur, M. N., Schilling, C., & Wüstholz,
V. (2019). Semantic fault localization and suspiciousness ranking. In 25th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 11427, pp. 226–243). Prague, Czech Republic: Springer Nature.
https://doi.org/10.1007/978-3-030-17462-0_13'
chicago: Christakis, Maria, Matthias Heizmann, Muhammad Numair Mansur, Christian
Schilling, and Valentin Wüstholz. “Semantic Fault Localization and Suspiciousness
Ranking.” In 25th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems , 11427:226–43. Springer Nature, 2019.
https://doi.org/10.1007/978-3-030-17462-0_13.
ieee: M. Christakis, M. Heizmann, M. N. Mansur, C. Schilling, and V. Wüstholz, “Semantic
fault localization and suspiciousness ranking,” in 25th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems , Prague,
Czech Republic, 2019, vol. 11427, pp. 226–243.
ista: 'Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. 2019. Semantic
fault localization and suspiciousness ranking. 25th 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. 11427,
226–243.'
mla: Christakis, Maria, et al. “Semantic Fault Localization and Suspiciousness Ranking.”
25th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems , vol. 11427, Springer Nature, 2019, pp. 226–43, doi:10.1007/978-3-030-17462-0_13.
short: M. Christakis, M. Heizmann, M.N. Mansur, C. Schilling, V. Wüstholz, in:,
25th International Conference on Tools and Algorithms for the Construction and
Analysis of Systems , Springer Nature, 2019, pp. 226–243.
conference:
end_date: 2019-04-11
location: Prague, Czech Republic
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2019-04-06
date_created: 2019-02-18T16:44:06Z
date_published: 2019-04-04T00:00:00Z
date_updated: 2023-08-24T14:47:45Z
day: '04'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-17462-0_13
ec_funded: 1
external_id:
isi:
- '000681166500013'
file:
- access_level: open_access
checksum: 9998496f6fe202c0a19124b4209154c6
content_type: application/pdf
creator: dernst
date_created: 2019-05-10T14:16:05Z
date_updated: 2020-07-14T12:47:17Z
file_id: '6408'
file_name: 2019_LNCS_Christakis.pdf
file_size: 773083
relation: main_file
file_date_updated: 2020-07-14T12:47:17Z
has_accepted_license: '1'
intvolume: ' 11427'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 226-243
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
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: '25th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems '
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Semantic fault localization and suspiciousness ranking
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 11427
year: '2019'
...
---
_id: '6035'
abstract:
- lang: eng
text: 'We present JuliaReach, a toolbox for set-based reachability analysis of dynamical
systems. JuliaReach consists of two main packages: Reachability, containing implementations
of reachability algorithms for continuous and hybrid systems, and LazySets, a
standalone library that implements state-of-the-art algorithms for calculus with
convex sets. The library offers both concrete and lazy set representations, where
the latter stands for the ability to delay set computations until they are needed.
The choice of the programming language Julia and the accompanying documentation
of our toolbox allow researchers to easily translate set-based algorithms from
mathematics to software in a platform-independent way, while achieving runtime
performance that is comparable to statically compiled languages. Combining lazy
operations in high dimensions and explicit computations in low dimensions, JuliaReach
can be applied to solve complex, large-scale problems.'
article_processing_charge: No
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. JuliaReach: A toolbox
for set-based reachability. In: Proceedings of the 22nd International Conference
on Hybrid Systems: Computation and Control. Vol 22. ACM; 2019:39-44. doi:10.1145/3302504.3311804'
apa: 'Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2019).
JuliaReach: A toolbox for set-based reachability. In Proceedings of the 22nd
International Conference on Hybrid Systems: Computation and Control (Vol.
22, pp. 39–44). Montreal, QC, Canada: ACM. https://doi.org/10.1145/3302504.3311804'
chicago: 'Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin,
and Christian Schilling. “JuliaReach: A Toolbox for Set-Based Reachability.” In
Proceedings of the 22nd International Conference on Hybrid Systems: Computation
and Control, 22:39–44. ACM, 2019. https://doi.org/10.1145/3302504.3311804.'
ieee: 'S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “JuliaReach:
A toolbox for set-based reachability,” in Proceedings of the 22nd International
Conference on Hybrid Systems: Computation and Control, Montreal, QC, Canada,
2019, vol. 22, pp. 39–44.'
ista: 'Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2019. JuliaReach:
A toolbox for set-based reachability. Proceedings of the 22nd International Conference
on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and
Control vol. 22, 39–44.'
mla: 'Bogomolov, Sergiy, et al. “JuliaReach: A Toolbox for Set-Based Reachability.”
Proceedings of the 22nd International Conference on Hybrid Systems: Computation
and Control, vol. 22, ACM, 2019, pp. 39–44, doi:10.1145/3302504.3311804.'
short: 'S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings
of the 22nd International Conference on Hybrid Systems: Computation and Control,
ACM, 2019, pp. 39–44.'
conference:
end_date: 2019-04-18
location: Montreal, QC, Canada
name: 'HSCC: Hybrid Systems Computation and Control'
start_date: 2019-04-16
date_created: 2019-02-18T14:43:28Z
date_published: 2019-04-16T00:00:00Z
date_updated: 2023-08-24T14:47:21Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3302504.3311804
ec_funded: 1
external_id:
arxiv:
- '1901.10736'
isi:
- '000516713900005'
file:
- access_level: open_access
checksum: 28ed56439aea5991c3122d4730fd828f
content_type: application/pdf
creator: cschilli
date_created: 2019-03-05T09:27:18Z
date_updated: 2020-07-14T12:47:17Z
file_id: '6067'
file_name: hscc19.pdf
file_size: 3784414
relation: main_file
file_date_updated: 2020-07-14T12:47:17Z
has_accepted_license: '1'
intvolume: ' 22'
isi: 1
keyword:
- reachability analysis
- hybrid systems
- lazy computation
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 39-44
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: 'Proceedings of the 22nd International Conference on Hybrid Systems:
Computation and Control'
publication_identifier:
isbn:
- '9781450362825'
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'JuliaReach: A toolbox for set-based reachability'
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 22
year: '2019'
...
---
_id: '6428'
abstract:
- lang: eng
text: 'Safety and security are major concerns in the development of Cyber-Physical
Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify
and monitor the correctness of CPS relativeto formalized requirements. Incorporating
STL into a developmentprocess enables designers to automatically monitor and diagnosetraces,
compute robustness estimates based on requirements, andperform requirement falsification,
leading to productivity gains inverification and validation activities; however,
in its current formSTL is agnostic to the input/output classification of signals,
andthis negatively impacts the relevance of the analysis results.In this paper
we propose to make the interface explicit in theSTL language by introducing input/output
signal declarations. Wethen define new measures of input vacuity and output robustnessthat
better reflect the nature of the system and the specification in-tent. The resulting
framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification
and validation activities.We demonstrate the benefits of IA-STL on several CPS
analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand
(3) fault localization. We describe an implementation of our en-hancement to STL
and associated notions of robustness and vacuityin a prototype extension of Breach,
a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these
methodologi-cal improvements and evaluate our results on two examples fromthe
automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell
system.'
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: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Alexandre
full_name: Donzé, Alexandre
last_name: Donzé
- first_name: Hisahiro
full_name: Ito, Hisahiro
last_name: Ito
- first_name: James
full_name: Kapinski, James
last_name: Kapinski
citation:
ama: 'Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. Interface-aware signal
temporal logic. In: Proceedings of the 2019 22nd ACM International Conference
on Hybrid Systems: Computation and Control. ACM; 2019:57-66. doi:10.1145/3302504.3311800'
apa: 'Ferrere, T., Nickovic, D., Donzé, A., Ito, H., & Kapinski, J. (2019).
Interface-aware signal temporal logic. In Proceedings of the 2019 22nd ACM
International Conference on Hybrid Systems: Computation and Control (pp. 57–66).
Montreal, Canada: ACM. https://doi.org/10.1145/3302504.3311800'
chicago: 'Ferrere, Thomas, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James
Kapinski. “Interface-Aware Signal Temporal Logic.” In Proceedings of the 2019
22nd ACM International Conference on Hybrid Systems: Computation and Control,
57–66. ACM, 2019. https://doi.org/10.1145/3302504.3311800.'
ieee: 'T. Ferrere, D. Nickovic, A. Donzé, H. Ito, and J. Kapinski, “Interface-aware
signal temporal logic,” in Proceedings of the 2019 22nd ACM International Conference
on Hybrid Systems: Computation and Control, Montreal, Canada, 2019, pp. 57–66.'
ista: 'Ferrere T, Nickovic D, Donzé A, Ito H, Kapinski J. 2019. Interface-aware
signal temporal logic. Proceedings of the 2019 22nd ACM International Conference
on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and
Control, 57–66.'
mla: 'Ferrere, Thomas, et al. “Interface-Aware Signal Temporal Logic.” Proceedings
of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and
Control, ACM, 2019, pp. 57–66, doi:10.1145/3302504.3311800.'
short: 'T. Ferrere, D. Nickovic, A. Donzé, H. Ito, J. Kapinski, in:, Proceedings
of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and
Control, ACM, 2019, pp. 57–66.'
conference:
end_date: 2019-04-18
location: Montreal, Canada
name: 'HSCC: Hybrid Systems Computation and Control'
start_date: 2019-04-16
date_created: 2019-05-13T08:13:46Z
date_published: 2019-04-16T00:00:00Z
date_updated: 2023-08-25T10:19:23Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3302504.3311800
external_id:
isi:
- '000516713900007'
file:
- access_level: open_access
checksum: b8e967081e051d1c55ca5d18fb187890
content_type: application/pdf
creator: dernst
date_created: 2020-10-08T17:25:45Z
date_updated: 2020-10-08T17:25:45Z
file_id: '8633'
file_name: 2019_ACM_Ferrere.pdf
file_size: 1055421
relation: main_file
success: 1
file_date_updated: 2020-10-08T17:25:45Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 57-66
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: 'Proceedings of the 2019 22nd ACM International Conference on Hybrid
Systems: Computation and Control'
publication_identifier:
isbn:
- '9781450362825'
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interface-aware signal temporal logic
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2019'
...
---
_id: '6462'
abstract:
- lang: eng
text: A controller is a device that interacts with a plant. At each time point,it
reads the plant’s state and issues commands with the goal that the plant oper-ates
optimally. Constructing optimal controllers is a fundamental and challengingproblem.
Machine learning techniques have recently been successfully applied totrain controllers,
yet they have limitations. Learned controllers are monolithic andhard to reason
about. In particular, it is difficult to add features without retraining,to guarantee
any level of performance, and to achieve acceptable performancewhen encountering
untrained scenarios. These limitations can be addressed bydeploying quantitative
run-timeshieldsthat serve as a proxy for the controller.At each time point, the
shield reads the command issued by the controller andmay choose to alter it before
passing it on to the plant. We show how optimalshields that interfere as little
as possible while guaranteeing a desired level ofcontroller performance, can be
generated systematically and automatically usingreactive synthesis. First, we abstract the plant by building a stochastic model.Second,
we consider the learned controller to be a black box. Third, we mea-surecontroller
performanceandshield interferenceby two quantitative run-timemeasures that are
formally defined using weighted automata. Then, the problemof constructing a shield
that guarantees maximal performance with minimal inter-ference is the problem
of finding an optimal strategy in a stochastic2-player game“controller versus
shield” played on the abstract state space of the plant with aquantitative objective
obtained from combining the performance and interferencemeasures. We illustrate
the effectiveness of our approach by automatically con-structing lightweight shields
for learned traffic-light controllers in various roadnetworks. The shields we
generate avoid liveness bugs, improve controller per-formance in untrained and
changing traffic situations, and add features to learnedcontrollers, such as giving
priority to emergency vehicles.
alternative_title:
- LNCS
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: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- 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: Bettina
full_name: Konighofer, Bettina
last_name: Konighofer
- first_name: Stefan
full_name: Pranger, Stefan
last_name: Pranger
citation:
ama: 'Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. Run-time
optimization for learned controllers through quantitative games. In: 31st International
Conference on Computer-Aided Verification. Vol 11561. Springer; 2019:630-649.
doi:10.1007/978-3-030-25540-4_36'
apa: 'Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., &
Pranger, S. (2019). Run-time optimization for learned controllers through quantitative
games. In 31st International Conference on Computer-Aided Verification
(Vol. 11561, pp. 630–649). New York, NY, United States: Springer. https://doi.org/10.1007/978-3-030-25540-4_36'
chicago: Avni, Guy, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina
Konighofer, and Stefan Pranger. “Run-Time Optimization for Learned Controllers
through Quantitative Games.” In 31st International Conference on Computer-Aided
Verification, 11561:630–49. Springer, 2019. https://doi.org/10.1007/978-3-030-25540-4_36.
ieee: G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Konighofer, and S. Pranger,
“Run-time optimization for learned controllers through quantitative games,” in
31st International Conference on Computer-Aided Verification, New York,
NY, United States, 2019, vol. 11561, pp. 630–649.
ista: 'Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. 2019.
Run-time optimization for learned controllers through quantitative games. 31st
International Conference on Computer-Aided Verification. CAV: Computer Aided Verification,
LNCS, vol. 11561, 630–649.'
mla: Avni, Guy, et al. “Run-Time Optimization for Learned Controllers through Quantitative
Games.” 31st International Conference on Computer-Aided Verification, vol.
11561, Springer, 2019, pp. 630–49, doi:10.1007/978-3-030-25540-4_36.
short: G. Avni, R. Bloem, K. Chatterjee, T.A. Henzinger, B. Konighofer, S. Pranger,
in:, 31st International Conference on Computer-Aided Verification, Springer, 2019,
pp. 630–649.
conference:
end_date: 2019-07-18
location: New York, NY, United States
name: 'CAV: Computer Aided Verification'
start_date: 2019-07-13
date_created: 2019-05-16T11:22:30Z
date_published: 2019-07-12T00:00:00Z
date_updated: 2023-08-25T10:33:27Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-030-25540-4_36
external_id:
isi:
- '000491468000036'
file:
- access_level: open_access
checksum: c231579f2485c6fd4df17c9443a4d80b
content_type: application/pdf
creator: dernst
date_created: 2019-08-14T09:35:24Z
date_updated: 2020-07-14T12:47:31Z
file_id: '6816'
file_name: 2019_CAV_Avni.pdf
file_size: 659766
relation: main_file
file_date_updated: 2020-07-14T12:47:31Z
has_accepted_license: '1'
intvolume: ' 11561'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 630-649
project:
- _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: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: 31st International Conference on Computer-Aided Verification
publication_identifier:
isbn:
- '9783030255398'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Run-time optimization for learned controllers through quantitative 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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 11561
year: '2019'
...
---
_id: '6493'
abstract:
- lang: eng
text: We present two algorithmic approaches for synthesizing linear hybrid automata
from experimental data. Unlike previous approaches, our algorithms work without
a template and generate an automaton with nondeterministic guards and invariants,
and with an arbitrary number and topology of modes. They thus construct a succinct
model from the data and provide formal guarantees. In particular, (1) the generated
automaton can reproduce the data up to a specified tolerance and (2) the automaton
is tight, given the first guarantee. Our first approach encodes the synthesis
problem as a logical formula in the theory of linear arithmetic, which can then
be solved by an SMT solver. This approach minimizes the number of modes in the
resulting model but is only feasible for limited data sets. To address scalability,
we propose a second approach that does not enforce to find a minimal model. The
algorithm constructs an initial automaton and then iteratively extends the automaton
based on processing new data. Therefore the algorithm is well-suited for online
and synthesis-in-the-loop applications. The core of the algorithm is a membership
query that checks whether, within the specified tolerance, a given data set can
result from the execution of a given automaton. We solve this membership problem
for linear hybrid automata by repeated reachability computations. We demonstrate
the effectiveness of the algorithm on synthetic data sets and on cardiac-cell
measurements.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Miriam
full_name: Garcia Soto, Miriam
id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
last_name: Garcia Soto
orcid: 0000−0003−2936−5719
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Luka
full_name: Zeleznik, Luka
id: 3ADCA2E4-F248-11E8-B48F-1D18A9856A87
last_name: Zeleznik
citation:
ama: 'Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis
of linear hybrid automata. In: 31st International Conference on Computer-Aided
Verification. Vol 11561. Springer; 2019:297-314. doi:10.1007/978-3-030-25540-4_16'
apa: 'Garcia Soto, M., Henzinger, T. A., Schilling, C., & Zeleznik, L. (2019).
Membership-based synthesis of linear hybrid automata. In 31st International
Conference on Computer-Aided Verification (Vol. 11561, pp. 297–314). New York
City, NY, USA: Springer. https://doi.org/10.1007/978-3-030-25540-4_16'
chicago: Garcia Soto, Miriam, Thomas A Henzinger, Christian Schilling, and Luka
Zeleznik. “Membership-Based Synthesis of Linear Hybrid Automata.” In 31st International
Conference on Computer-Aided Verification, 11561:297–314. Springer, 2019.
https://doi.org/10.1007/978-3-030-25540-4_16.
ieee: M. Garcia Soto, T. A. Henzinger, C. Schilling, and L. Zeleznik, “Membership-based
synthesis of linear hybrid automata,” in 31st International Conference on Computer-Aided
Verification, New York City, NY, USA, 2019, vol. 11561, pp. 297–314.
ista: 'Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. 2019. Membership-based
synthesis of linear hybrid automata. 31st International Conference on Computer-Aided
Verification. CAV: Computer-Aided Verification, LNCS, vol. 11561, 297–314.'
mla: Garcia Soto, Miriam, et al. “Membership-Based Synthesis of Linear Hybrid Automata.”
31st International Conference on Computer-Aided Verification, vol. 11561,
Springer, 2019, pp. 297–314, doi:10.1007/978-3-030-25540-4_16.
short: M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International
Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314.
conference:
end_date: 2019-07-18
location: New York City, NY, USA
name: 'CAV: Computer-Aided Verification'
start_date: 2019-07-15
date_created: 2019-05-27T07:09:53Z
date_published: 2019-07-12T00:00:00Z
date_updated: 2023-08-25T10:40:41Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-25540-4_16
ec_funded: 1
external_id:
isi:
- '000491468000016'
file:
- access_level: open_access
checksum: 1f1d61b83a151031745ef70a501da3d6
content_type: application/pdf
creator: dernst
date_created: 2019-08-14T11:05:30Z
date_updated: 2020-07-14T12:47:32Z
file_id: '6817'
file_name: 2019_CAV_GarciaSoto.pdf
file_size: 674795
relation: main_file
file_date_updated: 2020-07-14T12:47:32Z
has_accepted_license: '1'
intvolume: ' 11561'
isi: 1
keyword:
- Synthesis
- Linear hybrid automaton
- Membership
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 297-314
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: 31st International Conference on Computer-Aided Verification
publication_identifier:
isbn:
- '9783030255398'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Membership-based synthesis of linear hybrid automata
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 11561
year: '2019'
...
---
_id: '6752'
abstract:
- lang: eng
text: 'Two-player games on graphs are widely studied in formal methods, as they
model the interaction between a system and its environment. The game is played
by moving a token throughout a graph to produce an infinite path. There are several
common modes to determine how the players move the token through the graph; e.g.,
in turn-based games the players alternate turns in moving the token. We study
the bidding mode of moving the token, which, to the best of our knowledge, has
never been studied in infinite-duration games. The following bidding rule was
previously defined and called Richman bidding. Both players have separate budgets,
which sum up to 1. In each turn, a bidding takes place: Both players submit bids
simultaneously, where a bid is legal if it does not exceed the available budget,
and the higher bidder pays his bid to the other player and moves the token. The
central question studied in bidding games is a necessary and sufficient initial
budget for winning the game: a threshold budget in a vertex is a value t ∈ [0,
1] such that if Player 1’s budget exceeds t, he can win the game; and if Player
2’s budget exceeds 1 − t, he can win the game. Threshold budgets were previously
shown to exist in every vertex of a reachability game, which have an interesting
connection with random-turn games—a sub-class of simple stochastic games in which
the player who moves is chosen randomly. We show the existence of threshold budgets
for a qualitative class of infinite-duration games, namely parity games, and a
quantitative class, namely mean-payoff games. The key component of the proof is
a quantitative solution to strongly connected mean-payoff bidding games in which
we extend the connection with random-turn games to these games, and construct
explicit optimal strategies for both players.'
article_number: '31'
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
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
citation:
ama: Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. Journal
of the ACM. 2019;66(4). doi:10.1145/3340295
apa: Avni, G., Henzinger, T. A., & Chonev, V. K. (2019). Infinite-duration bidding
games. Journal of the ACM. ACM. https://doi.org/10.1145/3340295
chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
Bidding Games.” Journal of the ACM. ACM, 2019. https://doi.org/10.1145/3340295.
ieee: G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
Journal of the ACM, vol. 66, no. 4. ACM, 2019.
ista: Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal
of the ACM. 66(4), 31.
mla: Avni, Guy, et al. “Infinite-Duration Bidding Games.” Journal of the ACM,
vol. 66, no. 4, 31, ACM, 2019, doi:10.1145/3340295.
short: G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).
date_created: 2019-08-04T21:59:16Z
date_published: 2019-07-16T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '16'
department:
- _id: ToHe
doi: 10.1145/3340295
external_id:
arxiv:
- '1705.01433'
isi:
- '000487714900008'
intvolume: ' 66'
isi: 1
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.01433
month: '07'
oa: 1
oa_version: Preprint
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
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
publication: Journal of the ACM
publication_identifier:
eissn:
- 1557735X
issn:
- '00045411'
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
record:
- id: '950'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Infinite-duration bidding games
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 66
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
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'
...
---
_id: '7232'
abstract:
- lang: eng
text: 'We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism
which extends STL by capturing the discrete/ continuous time duality found in
many cyber-physical systems (CPS), as well as mixed-signal electronic designs.
In STL−MX, properties of components with continuous dynamics are expressed in
STL, while specifications of components with discrete dynamics are written in
LTL. To combine the two layers, we evaluate formulas on two traces, discrete-
and continuous-time, and introduce two interface operators that map signals, properties
and their satisfaction signals across the two time domains. We show that STL-mx
has the expressive power of STL supplemented with an implicit T-periodic clock
signal. We develop and implement an algorithm for monitoring STL-mx formulas and
illustrate the approach using a mixed-signal example. '
alternative_title:
- LNCS
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: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: 17th
International Conference on Formal Modeling and Analysis of Timed Systems.
Vol 11750. Springer Nature; 2019:59-75. doi:10.1007/978-3-030-29662-9_4'
apa: 'Ferrere, T., Maler, O., & Nickovic, D. (2019). Mixed-time signal temporal
logic. In 17th International Conference on Formal Modeling and Analysis of
Timed Systems (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer
Nature. https://doi.org/10.1007/978-3-030-29662-9_4'
chicago: Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal
Logic.” In 17th International Conference on Formal Modeling and Analysis of
Timed Systems, 11750:59–75. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-29662-9_4.
ieee: T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,”
in 17th International Conference on Formal Modeling and Analysis of Timed Systems,
Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.
ista: 'Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th
International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS:
Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.'
mla: Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” 17th International
Conference on Formal Modeling and Analysis of Timed Systems, vol. 11750, Springer
Nature, 2019, pp. 59–75, doi:10.1007/978-3-030-29662-9_4.
short: T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on
Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75.
conference:
end_date: 2019-08-29
location: Amsterdam, The Netherlands
name: 'FORMATS: Formal Modeling and Anaysis of Timed Systems'
start_date: 2019-08-27
date_created: 2020-01-05T23:00:48Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2023-09-06T14:57:17Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-030-29662-9_4
external_id:
isi:
- '000611677700004'
intvolume: ' 11750'
isi: 1
language:
- iso: eng
month: '08'
oa_version: None
page: 59-75
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: 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: Mixed-time signal temporal logic
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11750
year: '2019'
...
---
_id: '6894'
abstract:
- lang: eng
text: "Hybrid automata combine finite automata and dynamical systems, and model
the interaction of digital with physical systems. Formal analysis that can guarantee
the safety of all behaviors or rigorously witness failures, while unsolvable in
general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking,
assisted theorem proving.\r\nNevertheless, very few methods have addressed the
time-unbounded reachability analysis of hybrid automata and, for current sound
and automatic tools, scalability remains critical. We develop methods for the
polyhedral abstraction of hybrid automata, which construct coarse overapproximations
and tightens them incrementally, in a CEGAR fashion. We use template polyhedra,
i.e., polyhedra whose facets are normal to a given set of directions.\r\nWhile,
previously, directions were given by the user, we introduce (1) the first method\r\nfor
computing template directions from spurious counterexamples, so as to generalize
and\r\neliminate them. The method applies naturally to convex hybrid automata,
i.e., hybrid\r\nautomata with (possibly non-linear) convex constraints on derivatives
only, while for linear\r\nODE requires further abstraction. Specifically, we introduce
(2) the conic abstractions,\r\nwhich, partitioning the state space into appropriate
(possibly non-uniform) cones, divide\r\ncurvy trajectories into relatively straight
sections, suitable for polyhedral abstractions.\r\nFinally, we introduce (3) space-time
interpolation, which, combining interval arithmetic\r\nand template refinement,
computes appropriate (possibly non-uniform) time partitioning\r\nand template
directions along spurious trajectories, so as to eliminate them.\r\nWe obtain
sound and automatic methods for the reachability analysis over dense\r\nand unbounded
time of convex hybrid automata and hybrid automata with linear ODE.\r\nWe build
prototype tools and compare—favorably—our methods against the respective\r\nstate-of-the-art
tools, on several benchmarks."
alternative_title:
- ISTA Thesis
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
citation:
ama: Giacobbe M. Automatic time-unbounded reachability analysis of hybrid systems.
2019. doi:10.15479/AT:ISTA:6894
apa: Giacobbe, M. (2019). Automatic time-unbounded reachability analysis of hybrid
systems. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:6894
chicago: Giacobbe, Mirco. “Automatic Time-Unbounded Reachability Analysis of Hybrid
Systems.” Institute of Science and Technology Austria, 2019. https://doi.org/10.15479/AT:ISTA:6894.
ieee: M. Giacobbe, “Automatic time-unbounded reachability analysis of hybrid systems,”
Institute of Science and Technology Austria, 2019.
ista: Giacobbe M. 2019. Automatic time-unbounded reachability analysis of hybrid
systems. Institute of Science and Technology Austria.
mla: Giacobbe, Mirco. Automatic Time-Unbounded Reachability Analysis of Hybrid
Systems. Institute of Science and Technology Austria, 2019, doi:10.15479/AT:ISTA:6894.
short: M. Giacobbe, Automatic Time-Unbounded Reachability Analysis of Hybrid Systems,
Institute of Science and Technology Austria, 2019.
date_created: 2019-09-22T14:08:44Z
date_published: 2019-09-30T00:00:00Z
date_updated: 2023-09-19T09:30:43Z
day: '30'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:6894
file:
- access_level: open_access
checksum: 773beaf4a85dc2acc2c12b578fbe1965
content_type: application/pdf
creator: mgiacobbe
date_created: 2019-09-27T14:15:05Z
date_updated: 2020-07-14T12:47:43Z
file_id: '6916'
file_name: giacobbe_thesis.pdf
file_size: 4100685
relation: main_file
- access_level: closed
checksum: 97f1c3da71feefd27e6e625d32b4c75b
content_type: application/gzip
creator: mgiacobbe
date_created: 2019-09-27T14:22:04Z
date_updated: 2020-07-14T12:47:43Z
file_id: '6917'
file_name: giacobbe_thesis_src.tar.gz
file_size: 7959732
relation: source_file
file_date_updated: 2020-07-14T12:47:43Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '132'
publication_identifier:
eissn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '631'
relation: part_of_dissertation
status: public
- id: '647'
relation: part_of_dissertation
status: public
- id: '140'
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: Automatic time-unbounded reachability analysis of hybrid systems
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2019'
...
---
_id: '3300'
abstract:
- lang: eng
text: "This book first explores the origins of this idea, grounded in theoretical
work on temporal logic and automata. The editors and authors are among the world's
leading researchers in this domain, and they contributed 32 chapters representing
a thorough view of the development and application of the technique. Topics covered
include binary decision diagrams, symbolic model checking, satisfiability modulo
theories, partial-order reduction, abstraction, interpolation, concurrency, security
protocols, games, probabilistic model checking, and process algebra, and chapters
on the transfer of theory to industrial practice, property specification languages
for hardware, and verification of real-time systems and hybrid systems.\r\n\r\nThe
book will be valuable for researchers and graduate students engaged with the development
of formal methods and verification tools."
article_processing_charge: No
author:
- first_name: Edmund M.
full_name: Clarke, Edmund M.
last_name: Clarke
- 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: Helmut
full_name: Veith, Helmut
last_name: Veith
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
citation:
ama: 'Clarke EM, Henzinger TA, Veith H, Bloem R. Handbook of Model Checking.
1st ed. Cham: Springer Nature; 2018. doi:10.1007/978-3-319-10575-8'
apa: 'Clarke, E. M., Henzinger, T. A., Veith, H., & Bloem, R. (2018). Handbook
of Model Checking (1st ed.). Cham: Springer Nature. https://doi.org/10.1007/978-3-319-10575-8'
chicago: 'Clarke, Edmund M., Thomas A Henzinger, Helmut Veith, and Roderick Bloem.
Handbook of Model Checking. 1st ed. Cham: Springer Nature, 2018. https://doi.org/10.1007/978-3-319-10575-8.'
ieee: 'E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model
Checking, 1st ed. Cham: Springer Nature, 2018.'
ista: 'Clarke EM, Henzinger TA, Veith H, Bloem R. 2018. Handbook of Model Checking
1st ed., Cham: Springer Nature, XLVIII, 1212p.'
mla: Clarke, Edmund M., et al. Handbook of Model Checking. 1st ed., Springer
Nature, 2018, doi:10.1007/978-3-319-10575-8.
short: E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking,
1st ed., Springer Nature, Cham, 2018.
date_created: 2018-12-11T12:02:32Z
date_published: 2018-06-08T00:00:00Z
date_updated: 2021-12-21T10:49:36Z
day: '08'
department:
- _id: ToHe
doi: 10.1007/978-3-319-10575-8
edition: '1'
language:
- iso: eng
month: '06'
oa_version: None
page: XLVIII, 1212
place: Cham
publication_identifier:
eisbn:
- 978-3-319-10575-8
isbn:
- 978-3-319-10574-1
publication_status: published
publisher: Springer Nature
publist_id: '3340'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Handbook of Model Checking
type: book
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2018'
...
---
_id: '60'
abstract:
- lang: eng
text: Model checking is a computer-assisted method for the analysis of dynamical
systems that can be modeled by state-transition systems. Drawing from research
traditions in mathematical logic, programming languages, hardware design, and
theoretical computer science, model checking is now widely used for the verification
of hardware and software in industry. This chapter is an introduction and short
survey of model checking. The chapter aims to motivate and link the individual
chapters of the handbook, and to provide context for readers who are not familiar
with model checking.
author:
- first_name: Edmund
full_name: Clarke, Edmund
last_name: Clarke
- 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: Helmut
full_name: Veith, Helmut
last_name: Veith
citation:
ama: 'Clarke E, Henzinger TA, Veith H. Introduction to model checking. In: Henzinger
TA, ed. Handbook of Model Checking. Handbook of Model Checking. Springer;
2018:1-26. doi:10.1007/978-3-319-10575-8_1'
apa: Clarke, E., Henzinger, T. A., & Veith, H. (2018). Introduction to model
checking. In T. A. Henzinger (Ed.), Handbook of Model Checking (pp. 1–26).
Springer. https://doi.org/10.1007/978-3-319-10575-8_1
chicago: Clarke, Edmund, Thomas A Henzinger, and Helmut Veith. “Introduction to
Model Checking.” In Handbook of Model Checking, edited by Thomas A Henzinger,
1–26. Handbook of Model Checking. Springer, 2018. https://doi.org/10.1007/978-3-319-10575-8_1.
ieee: E. Clarke, T. A. Henzinger, and H. Veith, “Introduction to model checking,”
in Handbook of Model Checking, T. A. Henzinger, Ed. Springer, 2018, pp.
1–26.
ista: 'Clarke E, Henzinger TA, Veith H. 2018.Introduction to model checking. In:
Handbook of Model Checking. , 1–26.'
mla: Clarke, Edmund, et al. “Introduction to Model Checking.” Handbook of Model
Checking, edited by Thomas A Henzinger, Springer, 2018, pp. 1–26, doi:10.1007/978-3-319-10575-8_1.
short: E. Clarke, T.A. Henzinger, H. Veith, in:, T.A. Henzinger (Ed.), Handbook
of Model Checking, Springer, 2018, pp. 1–26.
date_created: 2018-12-11T11:44:25Z
date_published: 2018-05-19T00:00:00Z
date_updated: 2021-01-12T08:05:35Z
day: '19'
department:
- _id: ToHe
doi: 10.1007/978-3-319-10575-8_1
editor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
last_name: Henzinger
language:
- iso: eng
month: '05'
oa_version: None
page: 1 - 26
publication: Handbook of Model Checking
publication_status: published
publisher: Springer
publist_id: '7994'
quality_controlled: '1'
scopus_import: 1
series_title: Handbook of Model Checking
status: public
title: Introduction to model checking
type: book_chapter
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2018'
...
---
_id: '86'
abstract:
- lang: eng
text: Responsiveness—the requirement that every request to a system be eventually
handled—is one of the fundamental liveness properties of a reactive system. Average
response time is a quantitative measure for the responsiveness requirement used
commonly in performance evaluation. We show how average response time can be computed
on state-transition graphs, on Markov chains, and on game graphs. In all three
cases, we give polynomial-time algorithms.
acknowledgement: 'This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23, S11407-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein
Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund
(WWTF) through project ICT15-003 and by the National Science Centre (NCN), Poland
under grant 2014/15/D/ST6/04543.'
alternative_title:
- LNCS
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. Computing average response time. In: Lohstroh
M, Derler P, Sirjani M, eds. Principles of Modeling. Vol 10760. Springer;
2018:143-161. doi:10.1007/978-3-319-95246-8_9'
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2018). Computing average
response time. In M. Lohstroh, P. Derler, & M. Sirjani (Eds.), Principles
of Modeling (Vol. 10760, pp. 143–161). Springer. https://doi.org/10.1007/978-3-319-95246-8_9
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Computing Average
Response Time.” In Principles of Modeling, edited by Marten Lohstroh, Patricia
Derler, and Marjan Sirjani, 10760:143–61. Springer, 2018. https://doi.org/10.1007/978-3-319-95246-8_9.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Computing average response time,”
in Principles of Modeling, vol. 10760, M. Lohstroh, P. Derler, and M. Sirjani,
Eds. Springer, 2018, pp. 143–161.
ista: 'Chatterjee K, Henzinger TA, Otop J. 2018.Computing average response time.
In: Principles of Modeling. LNCS, vol. 10760, 143–161.'
mla: Chatterjee, Krishnendu, et al. “Computing Average Response Time.” Principles
of Modeling, edited by Marten Lohstroh et al., vol. 10760, Springer, 2018,
pp. 143–61, doi:10.1007/978-3-319-95246-8_9.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani
(Eds.), Principles of Modeling, Springer, 2018, pp. 143–161.
date_created: 2018-12-11T11:44:33Z
date_published: 2018-07-20T00:00:00Z
date_updated: 2021-01-12T08:20:14Z
day: '20'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-95246-8_9
ec_funded: 1
editor:
- first_name: Marten
full_name: Lohstroh, Marten
last_name: Lohstroh
- first_name: Patricia
full_name: Derler, Patricia
last_name: Derler
- first_name: Marjan
full_name: Sirjani, Marjan
last_name: Sirjani
file:
- access_level: open_access
checksum: 9995c6ce6957333baf616fc4f20be597
content_type: application/pdf
creator: dernst
date_created: 2019-11-19T08:22:18Z
date_updated: 2020-07-14T12:48:14Z
file_id: '7053'
file_name: 2018_PrinciplesModeling_Chatterjee.pdf
file_size: 516307
relation: main_file
file_date_updated: 2020-07-14T12:48:14Z
has_accepted_license: '1'
intvolume: ' 10760'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 143 - 161
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
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Principles of Modeling
publication_status: published
publisher: Springer
publist_id: '7968'
quality_controlled: '1'
scopus_import: 1
status: public
title: Computing average response time
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10760
year: '2018'
...