---
_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'
...