---
_id: '8790'
abstract:
- lang: eng
text: Reachability analysis aims at identifying states reachable by a system within
a given time horizon. This task is known to be computationally expensive for linear
hybrid systems. Reachability analysis works by iteratively applying continuous
and discrete post operators to compute states reachable according to continuous
and discrete dynamics, respectively. In this article, we enhance both of these
operators and make sure that most of the involved computations are performed in
low-dimensional state space. In particular, we improve the continuous-post operator
by performing computations in high-dimensional state space only for time intervals
relevant for the subsequent application of the discrete-post operator. Furthermore,
the new discrete-post operator performs low-dimensional computations by leveraging
the structure of the guard and assignment of a considered transition. We illustrate
the potential of our approach on a number of challenging benchmarks.
acknowledgement: 'This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), the
European Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie grant agreement No. 754411, and the Air Force Office of Scientific
Research under award number FA2386-17-1-4065. Any opinions, findings, and conclusions
or recommendations expressed in this material are those of the authors and do not
necessarily reflect the views of the United States Air Force. '
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Kostiantyn
full_name: Potomkin, Kostiantyn
last_name: Potomkin
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis
of linear hybrid systems via block decomposition. IEEE Transactions on Computer-Aided
Design of Integrated Circuits and Systems. 2020;39(11):4018-4029. doi:10.1109/TCAD.2020.3012859
apa: Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2020).
Reachability analysis of linear hybrid systems via block decomposition. IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems.
IEEE. https://doi.org/10.1109/TCAD.2020.3012859
chicago: Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and
Christian Schilling. “Reachability Analysis of Linear Hybrid Systems via Block
Decomposition.” IEEE Transactions on Computer-Aided Design of Integrated Circuits
and Systems. IEEE, 2020. https://doi.org/10.1109/TCAD.2020.3012859.
ieee: S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “Reachability
analysis of linear hybrid systems via block decomposition,” IEEE Transactions
on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, no.
11. IEEE, pp. 4018–4029, 2020.
ista: Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2020. Reachability
analysis of linear hybrid systems via block decomposition. IEEE Transactions on
Computer-Aided Design of Integrated Circuits and Systems. 39(11), 4018–4029.
mla: Bogomolov, Sergiy, et al. “Reachability Analysis of Linear Hybrid Systems via
Block Decomposition.” IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems, vol. 39, no. 11, IEEE, 2020, pp. 4018–29, doi:10.1109/TCAD.2020.3012859.
short: S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, IEEE Transactions
on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 4018–4029.
date_created: 2020-11-22T23:01:25Z
date_published: 2020-11-01T00:00:00Z
date_updated: 2023-08-22T13:27:33Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/TCAD.2020.3012859
ec_funded: 1
external_id:
arxiv:
- '1905.02458'
isi:
- '000587712700072'
intvolume: ' 39'
isi: 1
issue: '11'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1905.02458
month: '11'
oa: 1
oa_version: Preprint
page: 4018-4029
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 260C2330-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '754411'
name: ISTplus - Postdoctoral Fellowships
publication: IEEE Transactions on Computer-Aided Design of Integrated Circuits and
Systems
publication_identifier:
eissn:
- '19374151'
issn:
- '02780070'
publication_status: published
publisher: IEEE
quality_controlled: '1'
related_material:
record:
- id: '8287'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Reachability analysis of linear hybrid systems via block decomposition
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 39
year: '2020'
...
---
_id: '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
arxiv: 1
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Marcelo
full_name: Forets, Marcelo
last_name: Forets
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Kostiantyn
full_name: Potomkin, Kostiantyn
last_name: Potomkin
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 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: '631'
abstract:
- lang: eng
text: Template polyhedra generalize intervals and octagons to polyhedra whose facets
are orthogonal to a given set of arbitrary directions. They have been employed
in the abstract interpretation of programs and, with particular success, in the
reachability analysis of hybrid automata. While previously, the choice of directions
has been left to the user or a heuristic, we present a method for the automatic
discovery of directions that generalize and eliminate spurious counterexamples.
We show that for the class of convex hybrid automata, i.e., hybrid automata with
(possibly nonlinear) convex constraints on derivatives, such directions always
exist and can be found using convex optimization. We embed our method inside a
CEGAR loop, thus enabling the time-unbounded reachability analysis of an important
and richer class of hybrid automata than was previously possible. We evaluate
our method on several benchmarks, demonstrating also its superior efficiency for
the special case of linear hybrid automata.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by
the European Commission under grant 643921 (UnCoVerCPS), and by the ARC project
DP140104219 (Robust AI Planning for Hybrid Systems).
alternative_title:
- LNCS
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- 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
citation:
ama: 'Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement
of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:10.1007/978-3-662-54577-5_34'
apa: 'Bogomolov, S., Frehse, G., Giacobbe, M., & Henzinger, T. A. (2017). Counterexample
guided refinement of template polyhedra (Vol. 10205, pp. 589–606). Presented at
the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_34'
chicago: Bogomolov, Sergiy, Goran Frehse, Mirco Giacobbe, and Thomas A Henzinger.
“Counterexample Guided Refinement of Template Polyhedra,” 10205:589–606. Springer,
2017. https://doi.org/10.1007/978-3-662-54577-5_34.
ieee: 'S. Bogomolov, G. Frehse, M. Giacobbe, and T. A. Henzinger, “Counterexample
guided refinement of template polyhedra,” presented at the TACAS: Tools and Algorithms
for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205,
pp. 589–606.'
ista: 'Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. 2017. Counterexample guided
refinement of template polyhedra. TACAS: Tools and Algorithms for the Construction
and Analysis of Systems, LNCS, vol. 10205, 589–606.'
mla: Bogomolov, Sergiy, et al. Counterexample Guided Refinement of Template Polyhedra.
Vol. 10205, Springer, 2017, pp. 589–606, doi:10.1007/978-3-662-54577-5_34.
short: S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017,
pp. 589–606.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2017-04-22
date_created: 2018-12-11T11:47:36Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-09-07T12:53:00Z
day: '31'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-662-54577-5_34
file:
- access_level: open_access
checksum: f395d0d20102b89aeaad8b4ef4f18f4f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:41Z
date_updated: 2020-07-14T12:47:27Z
file_id: '4897'
file_name: IST-2017-741-v1+1_main.pdf
file_size: 569863
relation: main_file
- access_level: open_access
checksum: f416ee1ae4497b23ecdf28b1f18bb8df
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:42Z
date_updated: 2020-07-14T12:47:27Z
file_id: '4898'
file_name: IST-2018-741-v2+2_main.pdf
file_size: 563276
relation: main_file
file_date_updated: 2020-07-14T12:47:27Z
has_accepted_license: '1'
intvolume: ' 10205'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 589 - 606
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
isbn:
- 978-366254576-8
publication_status: published
publisher: Springer
publist_id: '7162'
pubrep_id: '966'
quality_controlled: '1'
related_material:
record:
- id: '6894'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Counterexample guided refinement of template polyhedra
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10205
year: '2017'
...
---
_id: '633'
abstract:
- lang: eng
text: A Rapidly-exploring Random Tree (RRT) is an algorithm which can search a non-convex
region of space by incrementally building a space-filling tree. The tree is constructed
from random points drawn from system’s state space and is biased to grow towards
large unexplored areas in the system. RRT can provide better coverage of a system’s
possible behaviors compared with random simulations, but is more lightweight than
full reachability analysis. In this paper, we explore some of the design decisions
encountered while implementing a hybrid extension of the RRT algorithm, which
have not been elaborated on before. In particular, we focus on handling non-determinism,
which arises due to discrete transitions. We introduce the notion of important
points to account for this phenomena. We showcase our ideas using heater and navigation
benchmarks.
alternative_title:
- LNCS
author:
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- 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: Aviral
full_name: Kumar, Aviral
last_name: Kumar
citation:
ama: 'Bak S, Bogomolov S, Henzinger TA, Kumar A. Challenges and tool implementation
of hybrid rapidly exploring random trees. In: Abate A, Bodo S, eds. Vol 10381.
Springer; 2017:83-89. doi:10.1007/978-3-319-63501-9_6'
apa: 'Bak, S., Bogomolov, S., Henzinger, T. A., & Kumar, A. (2017). Challenges
and tool implementation of hybrid rapidly exploring random trees. In A. Abate
& S. Bodo (Eds.) (Vol. 10381, pp. 83–89). Presented at the NSV: Numerical
Software Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63501-9_6'
chicago: Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, and Aviral Kumar. “Challenges
and Tool Implementation of Hybrid Rapidly Exploring Random Trees.” edited by Alessandro
Abate and Sylvie Bodo, 10381:83–89. Springer, 2017. https://doi.org/10.1007/978-3-319-63501-9_6.
ieee: 'S. Bak, S. Bogomolov, T. A. Henzinger, and A. Kumar, “Challenges and tool
implementation of hybrid rapidly exploring random trees,” presented at the NSV:
Numerical Software Verification, Heidelberg, Germany, 2017, vol. 10381, pp. 83–89.'
ista: 'Bak S, Bogomolov S, Henzinger TA, Kumar A. 2017. Challenges and tool implementation
of hybrid rapidly exploring random trees. NSV: Numerical Software Verification,
LNCS, vol. 10381, 83–89.'
mla: Bak, Stanley, et al. Challenges and Tool Implementation of Hybrid Rapidly
Exploring Random Trees. Edited by Alessandro Abate and Sylvie Bodo, vol. 10381,
Springer, 2017, pp. 83–89, doi:10.1007/978-3-319-63501-9_6.
short: S. Bak, S. Bogomolov, T.A. Henzinger, A. Kumar, in:, A. Abate, S. Bodo (Eds.),
Springer, 2017, pp. 83–89.
conference:
end_date: 2017-07-23
location: Heidelberg, Germany
name: 'NSV: Numerical Software Verification'
start_date: 2017-07-22
date_created: 2018-12-11T11:47:37Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2021-01-12T08:07:06Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-319-63501-9_6
editor:
- first_name: Alessandro
full_name: Abate, Alessandro
last_name: Abate
- first_name: Sylvie
full_name: Bodo, Sylvie
last_name: Bodo
intvolume: ' 10381'
language:
- iso: eng
month: '01'
oa_version: None
page: 83 - 89
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
isbn:
- 978-331963500-2
publication_status: published
publisher: Springer
publist_id: '7159'
quality_controlled: '1'
scopus_import: 1
status: public
title: Challenges and tool implementation of hybrid rapidly exploring random trees
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10381
year: '2017'
...
---
_id: '638'
abstract:
- lang: eng
text: "This book constitutes the refereed proceedings of the 9th InternationalWorkshop
on Numerical Software Verification, NSV 2016, held in Toronto, ON, Canada in July
2011 - colocated with CAV 2016, the 28th International Conference on Computer
Aided Verification.\r\nThe NSV workshop is dedicated to the development of logical
and mathematical techniques for the reasoning about programmability and reliability."
article_processing_charge: No
citation:
ama: Bogomolov S, Martel M, Prabhakar P, eds. Numerical Software Verification.
Vol 10152. Springer; 2017. doi:10.1007/978-3-319-54292-8
apa: 'Bogomolov, S., Martel, M., & Prabhakar, P. (Eds.). (2017). Numerical
Software Verification (Vol. 10152). Presented at the NSV: Numerical Software
Verification, Toronto, ON, Canada: Springer. https://doi.org/10.1007/978-3-319-54292-8'
chicago: Bogomolov, Sergiy, Matthieu Martel, and Pavithra Prabhakar, eds. Numerical
Software Verification. Vol. 10152. LNCS. Springer, 2017. https://doi.org/10.1007/978-3-319-54292-8.
ieee: S. Bogomolov, M. Martel, and P. Prabhakar, Eds., Numerical Software Verification,
vol. 10152. Springer, 2017.
ista: Bogomolov S, Martel M, Prabhakar P eds. 2017. Numerical Software Verification,
Springer,p.
mla: Bogomolov, Sergiy, et al., editors. Numerical Software Verification.
Vol. 10152, Springer, 2017, doi:10.1007/978-3-319-54292-8.
short: S. Bogomolov, M. Martel, P. Prabhakar, eds., Numerical Software Verification,
Springer, 2017.
conference:
end_date: 2016-07-18
location: Toronto, ON, Canada
name: 'NSV: Numerical Software Verification'
start_date: 2016-07-17
date_created: 2018-12-11T11:47:38Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2022-05-24T07:09:52Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-319-54292-8
editor:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Matthieu
full_name: Martel, Matthieu
last_name: Martel
- first_name: Pavithra
full_name: Prabhakar, Pavithra
last_name: Prabhakar
intvolume: ' 10152'
language:
- iso: eng
month: '01'
oa_version: None
publication_identifier:
eisbn:
- 978-3-319-54292-8
issn:
- 0302-9743
publication_status: published
publisher: Springer
publist_id: '7150'
quality_controlled: '1'
series_title: LNCS
status: public
title: Numerical Software Verification
type: conference_editor
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10152
year: '2017'
...
---
_id: '647'
abstract:
- lang: eng
text: Despite researchers’ efforts in the last couple of decades, reachability analysis
is still a challenging problem even for linear hybrid systems. Among the existing
approaches, the most practical ones are mainly based on bounded-time reachable
set over-approximations. For the purpose of unbounded-time analysis, one important
strategy is to abstract the original system and find an invariant for the abstraction.
In this paper, we propose an approach to constructing a new kind of abstraction
called conic abstraction for affine hybrid systems, and to computing reachable
sets based on this abstraction. The essential feature of a conic abstraction is
that it partitions the state space of a system into a set of convex polyhedral
cones which is derived from a uniform conic partition of the derivative space.
Such a set of polyhedral cones is able to cut all trajectories of the system into
almost straight segments so that every segment of a reach pipe in a polyhedral
cone tends to be straight as well, and hence can be over-approximated tightly
by polyhedra using similar techniques as HyTech or PHAVer. In particular, for
diagonalizable affine systems, our approach can guarantee to find an invariant
for unbounded reachable sets, which is beyond the capability of bounded-time reachability
analysis tools. We implemented the approach in a tool and experiments on benchmarks
show that our approach is more powerful than SpaceEx and PHAVer in dealing with
diagonalizable systems.
alternative_title:
- LNCS
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- 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: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
citation:
ama: 'Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid
systems. In: Vol 10419. Springer; 2017:116-132. doi:10.1007/978-3-319-65765-3_7'
apa: 'Bogomolov, S., Giacobbe, M., Henzinger, T. A., & Kong, H. (2017). Conic
abstractions for hybrid systems (Vol. 10419, pp. 116–132). Presented at the FORMATS:
Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. https://doi.org/10.1007/978-3-319-65765-3_7'
chicago: Bogomolov, Sergiy, Mirco Giacobbe, Thomas A Henzinger, and Hui Kong. “Conic
Abstractions for Hybrid Systems,” 10419:116–32. Springer, 2017. https://doi.org/10.1007/978-3-319-65765-3_7.
ieee: 'S. Bogomolov, M. Giacobbe, T. A. Henzinger, and H. Kong, “Conic abstractions
for hybrid systems,” presented at the FORMATS: Formal Modelling and Analysis of
Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 116–132.'
ista: 'Bogomolov S, Giacobbe M, Henzinger TA, Kong H. 2017. Conic abstractions for
hybrid systems. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS,
vol. 10419, 116–132.'
mla: Bogomolov, Sergiy, et al. Conic Abstractions for Hybrid Systems. Vol.
10419, Springer, 2017, pp. 116–32, doi:10.1007/978-3-319-65765-3_7.
short: S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, Springer, 2017,
pp. 116–132.
conference:
end_date: 2017-09-07
location: Berlin, Germany
name: 'FORMATS: Formal Modelling and Analysis of Timed Systems'
start_date: 2017-09-05
date_created: 2018-12-11T11:47:41Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-09-07T12:53:00Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-65765-3_7
file:
- access_level: open_access
checksum: faf546914ba29bcf9974ee36b6b16750
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:38Z
date_updated: 2020-07-14T12:47:31Z
file_id: '4956'
file_name: IST-2017-831-v1+1_main.pdf
file_size: 3806864
relation: main_file
file_date_updated: 2020-07-14T12:47:31Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 116 - 132
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
isbn:
- 978-331965764-6
publication_status: published
publisher: Springer
publist_id: '7129'
pubrep_id: '831'
quality_controlled: '1'
related_material:
record:
- id: '6894'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Conic abstractions for hybrid systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: '10419 '
year: '2017'
...
---
_id: '1103'
abstract:
- lang: eng
text: We propose two parallel state-space-exploration algorithms for hybrid automaton
(HA), with the goal of enhancing performance on multi-core shared-memory systems.
The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN
model checker, when traversing the discrete modes of the HA, and enhances it with
a parallel exploration of the continuous states within each mode. We show that
this simple-minded extension of PBFS does not provide the desired load balancing
in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS),
which uses a cheap precomputation of the cost associated with the post operations
(both continuous and discrete) in order to improve load balancing. We illustrate
the TP-BFS and the cost precomputation of the post operators on a support-function-based
algorithm for state-space exploration. The performance comparison of the two algorithms
shows that, in general, TP-BFS provides a better utilization/load-balancing of
the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments
show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect
to SpaceEx LGG scenario. In order to make the comparison fair, we employed an
equal number of post operations in both tools. To the best of our knowledge, this
paper represents the first attempt to provide parallel, reachability-analysis
algorithms for HA.
acknowledgement: This work was supported in part by DST-SERB, GoI under Project No.
YSS/2014/000623 and by the European Research Council (ERC) under grant 267989 (QUAREM)
and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23
(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
article_number: '7797741'
author:
- first_name: Amit
full_name: Gurung, Amit
last_name: Gurung
- first_name: Arup
full_name: Deka, Arup
last_name: Deka
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- first_name: Rajarshi
full_name: Ray, Rajarshi
last_name: Ray
citation:
ama: 'Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability
analysis for hybrid systems. In: IEEE; 2016. doi:10.1109/MEMCOD.2016.7797741'
apa: 'Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., & Ray, R.
(2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE:
International Conference on Formal Methods and Models for System Design, Kanpur,
India : IEEE. https://doi.org/10.1109/MEMCOD.2016.7797741'
chicago: Gurung, Amit, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and
Rajarshi Ray. “Parallel Reachability Analysis for Hybrid Systems.” IEEE, 2016.
https://doi.org/10.1109/MEMCOD.2016.7797741.
ieee: 'A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, and R. Ray, “Parallel
reachability analysis for hybrid systems,” presented at the MEMOCODE: International
Conference on Formal Methods and Models for System Design, Kanpur, India , 2016.'
ista: 'Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. 2016. Parallel
reachability analysis for hybrid systems. MEMOCODE: International Conference on
Formal Methods and Models for System Design, 7797741.'
mla: Gurung, Amit, et al. Parallel Reachability Analysis for Hybrid Systems.
7797741, IEEE, 2016, doi:10.1109/MEMCOD.2016.7797741.
short: A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, R. Ray, in:, IEEE,
2016.
conference:
end_date: 2016-11-20
location: 'Kanpur, India '
name: 'MEMOCODE: International Conference on Formal Methods and Models for System
Design'
start_date: 2016-11-18
date_created: 2018-12-11T11:50:09Z
date_published: 2016-12-27T00:00:00Z
date_updated: 2021-01-12T06:48:18Z
day: '27'
department:
- _id: ToHe
doi: 10.1109/MEMCOD.2016.7797741
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1606.05473
month: '12'
oa: 1
oa_version: Preprint
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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_status: published
publisher: IEEE
publist_id: '6272'
quality_controlled: '1'
scopus_import: 1
status: public
title: Parallel reachability analysis for hybrid systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1134'
abstract:
- lang: eng
text: 'Hybrid systems have both continuous and discrete dynamics and are useful
for modeling a variety of control systems, from air traffic control protocols
to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools
for analyzing hybrid systems have emerged. Several of these tools implement automated
formal methods for mathematically proving a system meets a specification. This
tutorial session will present three recent hybrid systems tools: C2E2, HyST, and
TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses
validated numerical solvers and bloating of simulation traces to verify systems
meet specifications. HyST is a hybrid systems model transformation and translation
tool, and uses a canonical intermediate representation to support most of the
recent verification tools, as well as automated sound abstractions that simplify
verification of a given hybrid system. TuLiP is a controller synthesis tool for
hybrid systems, where given a temporal logic specification to be satisfied for
a system (plant) model, TuLiP will find a controller that meets a given specification.
© 2016 IEEE.'
article_number: '7587948'
author:
- first_name: Parasara
full_name: Duggirala, Parasara
last_name: Duggirala
- first_name: Chuchu
full_name: Fan, Chuchu
last_name: Fan
- first_name: Matthew
full_name: Potok, Matthew
last_name: Potok
- first_name: Bolun
full_name: Qi, Bolun
last_name: Qi
- first_name: Sayan
full_name: Mitra, Sayan
last_name: Mitra
- first_name: Mahesh
full_name: Viswanathan, Mahesh
last_name: Viswanathan
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
- first_name: Luan
full_name: Nguyen, Luan
last_name: Nguyen
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Andrew
full_name: Sogokon, Andrew
last_name: Sogokon
- first_name: Hoang
full_name: Tran, Hoang
last_name: Tran
- first_name: Weiming
full_name: Xiang, Weiming
last_name: Xiang
citation:
ama: 'Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems
verification transformation and synthesis C2E2 HyST and TuLiP. In: 2016 IEEE
Conference on Control Applications. IEEE; 2016. doi:10.1109/CCA.2016.7587948'
apa: 'Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang,
W. (2016). Tutorial: Software tools for hybrid systems verification transformation
and synthesis C2E2 HyST and TuLiP. In 2016 IEEE Conference on Control Applications.
Buenos Aires, Argentina : IEEE. https://doi.org/10.1109/CCA.2016.7587948'
chicago: 'Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra,
Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems
Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In 2016 IEEE
Conference on Control Applications. IEEE, 2016. https://doi.org/10.1109/CCA.2016.7587948.'
ieee: 'P. Duggirala et al., “Tutorial: Software tools for hybrid systems
verification transformation and synthesis C2E2 HyST and TuLiP,” in 2016 IEEE
Conference on Control Applications, Buenos Aires, Argentina , 2016.'
ista: 'Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov
S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial:
Software tools for hybrid systems verification transformation and synthesis C2E2
HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications
, 7587948.'
mla: 'Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification
Transformation and Synthesis C2E2 HyST and TuLiP.” 2016 IEEE Conference on
Control Applications, 7587948, IEEE, 2016, doi:10.1109/CCA.2016.7587948.'
short: P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak,
S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang,
in:, 2016 IEEE Conference on Control Applications, IEEE, 2016.
conference:
end_date: 2016-09-22
location: 'Buenos Aires, Argentina '
name: 'CCA: Control Applications '
start_date: 2016-09-19
date_created: 2018-12-11T11:50:20Z
date_published: 2016-10-10T00:00:00Z
date_updated: 2021-01-12T06:48:32Z
day: '10'
department:
- _id: ToHe
doi: 10.1109/CCA.2016.7587948
language:
- iso: eng
month: '10'
oa_version: None
publication: 2016 IEEE Conference on Control Applications
publication_status: published
publisher: IEEE
publist_id: '6224'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Tutorial: Software tools for hybrid systems verification transformation and
synthesis C2E2 HyST and TuLiP'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1148'
abstract:
- lang: eng
text: Continuous-time Markov chain (CTMC) models have become a central tool for
understanding the dynamics of complex reaction networks and the importance of
stochasticity in the underlying biochemical processes. When such models are employed
to answer questions in applications, in order to ensure that the model provides
a sufficiently accurate representation of the real system, it is of vital importance
that the model parameters are inferred from real measured data. This, however,
is often a formidable task and all of the existing methods fail in one case or
the other, usually because the underlying CTMC model is high-dimensional and computationally
difficult to analyze. The parameter inference methods that tend to scale best
in the dimension of the CTMC are based on so-called moment closure approximations.
However, there exists a large number of different moment closure approximations
and it is typically hard to say a priori which of the approximations is the most
suitable for the inference procedure. Here, we propose a moment-based parameter
inference method that automatically chooses the most appropriate moment closure
method. Accordingly, contrary to existing methods, the user is not required to
be experienced in moment closure techniques. In addition to that, our method adaptively
changes the approximation during the parameter inference to ensure that always
the best approximation is used, even in cases where different approximations are
best in different regions of the parameter space. © 2016 Elsevier Ireland Ltd
acknowledgement: This work is based on the CMSB 2015 paper “Adaptive moment closure
for parameter inference of biochemical reaction networks” (Bogomolov et al., 2015).
The work was partly supported by the German Research Foundation (DFG) as part of
the Transregional Collaborative Research Center “Automatic Verification and Analysis
of Complex Systems” (SFB/TR 14 AVACS1), by the European Research Council (ERC) under
grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23
(RiSE) and Z211-N23 (Wittgenstein Award). J.R. acknowledges support from the People
Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme
(FP7/2007-2013) under REA grant agreement no. 291734.
author:
- first_name: Christian
full_name: Schilling, Christian
last_name: Schilling
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- 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: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Jakob
full_name: Ruess, Jakob
id: 4A245D00-F248-11E8-B48F-1D18A9856A87
last_name: Ruess
orcid: 0000-0003-1615-3282
citation:
ama: Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. Adaptive moment
closure for parameter inference of biochemical reaction networks. Biosystems.
2016;149:15-25. doi:10.1016/j.biosystems.2016.07.005
apa: Schilling, C., Bogomolov, S., Henzinger, T. A., Podelski, A., & Ruess,
J. (2016). Adaptive moment closure for parameter inference of biochemical reaction
networks. Biosystems. Elsevier. https://doi.org/10.1016/j.biosystems.2016.07.005
chicago: Schilling, Christian, Sergiy Bogomolov, Thomas A Henzinger, Andreas Podelski,
and Jakob Ruess. “Adaptive Moment Closure for Parameter Inference of Biochemical
Reaction Networks.” Biosystems. Elsevier, 2016. https://doi.org/10.1016/j.biosystems.2016.07.005.
ieee: C. Schilling, S. Bogomolov, T. A. Henzinger, A. Podelski, and J. Ruess, “Adaptive
moment closure for parameter inference of biochemical reaction networks,” Biosystems,
vol. 149. Elsevier, pp. 15–25, 2016.
ista: Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. 2016. Adaptive
moment closure for parameter inference of biochemical reaction networks. Biosystems.
149, 15–25.
mla: Schilling, Christian, et al. “Adaptive Moment Closure for Parameter Inference
of Biochemical Reaction Networks.” Biosystems, vol. 149, Elsevier, 2016,
pp. 15–25, doi:10.1016/j.biosystems.2016.07.005.
short: C. Schilling, S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, Biosystems
149 (2016) 15–25.
date_created: 2018-12-11T11:50:24Z
date_published: 2016-11-01T00:00:00Z
date_updated: 2023-02-23T10:08:46Z
day: '01'
department:
- _id: ToHe
- _id: GaTk
doi: 10.1016/j.biosystems.2016.07.005
ec_funded: 1
intvolume: ' 149'
language:
- iso: eng
month: '11'
oa_version: None
page: 15 - 25
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: Biosystems
publication_status: published
publisher: Elsevier
publist_id: '6210'
quality_controlled: '1'
related_material:
record:
- id: '1658'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Adaptive moment closure for parameter inference of biochemical reaction networks
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 149
year: '2016'
...
---
_id: '1705'
abstract:
- lang: eng
text: Hybrid systems represent an important and powerful formalism for modeling
real-world applications such as embedded systems. A verification tool like SpaceEx
is based on the exploration of a symbolic search space (the region space). As
a verification tool, it is typically optimized towards proving the absence of
errors. In some settings, e.g., when the verification tool is employed in a feedback-directed
design cycle, one would like to have the option to call a version that is optimized
towards finding an error trajectory in the region space. A recent approach in
this direction is based on guided search. Guided search relies on a cost function
that indicates which states are promising to be explored, and preferably explores
more promising states first. In this paper, we propose an abstraction-based cost
function based on coarse-grained space abstractions for guiding the reachability
analysis. For this purpose, a suitable abstraction technique that exploits the
flexible granularity of modern reachability analysis algorithms is introduced.
The new cost function is an effective extension of pattern database approaches
that have been successfully applied in other areas. The approach has been implemented
in the SpaceEx model checker. The evaluation shows its practical potential.
article_processing_charge: Yes (via OA deal)
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Alexandre
full_name: Donzé, Alexandre
last_name: Donzé
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
- first_name: Hamed
full_name: Ladan, Hamed
last_name: Ladan
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Martin
full_name: Wehrle, Martin
last_name: Wehrle
citation:
ama: Bogomolov S, Donzé A, Frehse G, et al. Guided search for hybrid systems based
on coarse-grained space abstractions. International Journal on Software Tools
for Technology Transfer. 2016;18(4):449-467. doi:10.1007/s10009-015-0393-y
apa: Bogomolov, S., Donzé, A., Frehse, G., Grosu, R., Johnson, T., Ladan, H., …
Wehrle, M. (2016). Guided search for hybrid systems based on coarse-grained space
abstractions. International Journal on Software Tools for Technology Transfer.
Springer. https://doi.org/10.1007/s10009-015-0393-y
chicago: Bogomolov, Sergiy, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor Johnson,
Hamed Ladan, Andreas Podelski, and Martin Wehrle. “Guided Search for Hybrid Systems
Based on Coarse-Grained Space Abstractions.” International Journal on Software
Tools for Technology Transfer. Springer, 2016. https://doi.org/10.1007/s10009-015-0393-y.
ieee: S. Bogomolov et al., “Guided search for hybrid systems based on coarse-grained
space abstractions,” International Journal on Software Tools for Technology
Transfer, vol. 18, no. 4. Springer, pp. 449–467, 2016.
ista: Bogomolov S, Donzé A, Frehse G, Grosu R, Johnson T, Ladan H, Podelski A, Wehrle
M. 2016. Guided search for hybrid systems based on coarse-grained space abstractions.
International Journal on Software Tools for Technology Transfer. 18(4), 449–467.
mla: Bogomolov, Sergiy, et al. “Guided Search for Hybrid Systems Based on Coarse-Grained
Space Abstractions.” International Journal on Software Tools for Technology
Transfer, vol. 18, no. 4, Springer, 2016, pp. 449–67, doi:10.1007/s10009-015-0393-y.
short: S. Bogomolov, A. Donzé, G. Frehse, R. Grosu, T. Johnson, H. Ladan, A. Podelski,
M. Wehrle, International Journal on Software Tools for Technology Transfer 18
(2016) 449–467.
date_created: 2018-12-11T11:53:34Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:52:38Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s10009-015-0393-y
ec_funded: 1
file:
- access_level: open_access
checksum: 31561d7705599a9bd4ea816accc0752e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:26Z
date_updated: 2020-07-14T12:45:13Z
file_id: '5146'
file_name: IST-2016-457-v1+1_s10009-015-0393-y.pdf
file_size: 2296522
relation: main_file
file_date_updated: 2020-07-14T12:45:13Z
has_accepted_license: '1'
intvolume: ' 18'
issue: '4'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 449 - 467
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '5431'
pubrep_id: '457'
quality_controlled: '1'
scopus_import: 1
status: public
title: Guided search for hybrid systems based on coarse-grained space abstractions
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2016'
...
---
_id: '1421'
abstract:
- lang: eng
text: 'Hybridization methods enable the analysis of hybrid automata with complex,
nonlinear dynamics through a sound abstraction process. Complex dynamics are converted
to simpler ones with added noise, and then analysis is done using a reachability
method for the simpler dynamics. Several such recent approaches advocate that
only "dynamic" hybridization techniquesi.e., those where the dynamics
are abstracted on-The-fly during a reachability computation are effective. In
this paper, we demonstrate this is not the case, and create static hybridization
methods that are more scalable than earlier approaches. The main insight in our
approach is that quick, numeric simulations can be used to guide the process,
eliminating the need for an exponential number of hybridization domains. Transitions
between domains are generally timetriggered, avoiding accumulated error from geometric
intersections. We enhance our static technique by combining time-Triggered transitions
with occasional space-Triggered transitions, and demonstrate the benefits of the
combined approach in what we call mixed-Triggered hybridization. Finally, error
modes are inserted to confirm that the reachable states stay within the hybridized
regions. The developed techniques can scale to higher dimensions than previous
static approaches, while enabling the parallelization of the main performance
bottleneck for many dynamic hybridization approaches: The nonlinear optimization
required for sound dynamics abstraction. We implement our method as a model transformation
pass in the HYST tool, and perform reachability analysis and evaluation using
an unmodified version of SpaceEx on nonlinear models with up to six dimensions.'
author:
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- 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: Taylor
full_name: Johnson, Taylor
last_name: Johnson
- first_name: Pradyot
full_name: Prakash, Pradyot
last_name: Prakash
citation:
ama: 'Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. Scalable static hybridization
methods for analysis of nonlinear systems. In: Springer; 2016:155-164. doi:10.1145/2883817.2883837'
apa: 'Bak, S., Bogomolov, S., Henzinger, T. A., Johnson, T., & Prakash, P. (2016).
Scalable static hybridization methods for analysis of nonlinear systems (pp. 155–164).
Presented at the HSCC 2016: International Conference on Hybrid Systems: Computation
and Control, Vienna, Austria: Springer. https://doi.org/10.1145/2883817.2883837'
chicago: Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, Taylor Johnson, and
Pradyot Prakash. “Scalable Static Hybridization Methods for Analysis of Nonlinear
Systems,” 155–64. Springer, 2016. https://doi.org/10.1145/2883817.2883837.
ieee: 'S. Bak, S. Bogomolov, T. A. Henzinger, T. Johnson, and P. Prakash, “Scalable
static hybridization methods for analysis of nonlinear systems,” presented at
the HSCC 2016: International Conference on Hybrid Systems: Computation and Control,
Vienna, Austria, 2016, pp. 155–164.'
ista: 'Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. 2016. Scalable static
hybridization methods for analysis of nonlinear systems. HSCC 2016: International
Conference on Hybrid Systems: Computation and Control, 155–164.'
mla: Bak, Stanley, et al. Scalable Static Hybridization Methods for Analysis
of Nonlinear Systems. Springer, 2016, pp. 155–64, doi:10.1145/2883817.2883837.
short: S. Bak, S. Bogomolov, T.A. Henzinger, T. Johnson, P. Prakash, in:, Springer,
2016, pp. 155–164.
conference:
end_date: 2016-04-14
location: Vienna, Austria
name: 'HSCC 2016: International Conference on Hybrid Systems: Computation and Control'
start_date: 2016-04-12
date_created: 2018-12-11T11:51:55Z
date_published: 2016-04-11T00:00:00Z
date_updated: 2021-01-12T06:50:37Z
day: '11'
department:
- _id: ToHe
doi: 10.1145/2883817.2883837
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 155 - 164
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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_status: published
publisher: Springer
publist_id: '5786'
quality_controlled: '1'
scopus_import: 1
status: public
title: Scalable static hybridization methods for analysis of nonlinear systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1227'
abstract:
- lang: eng
text: Many biological systems can be modeled as multiaffine hybrid systems. Due
to the nonlinearity of multiaffine systems, it is difficult to verify their properties
of interest directly. A common strategy to tackle this problem is to construct
and analyze a discrete overapproximation of the original system. However, the
conservativeness of a discrete abstraction significantly determines the level
of confidence we can have in the properties of the original system. In this paper,
in order to reduce the conservativeness of a discrete abstraction, we propose
a new method based on a sufficient and necessary decision condition for computing
discrete transitions between states in the abstract system. We assume the state
space partition of a multiaffine system to be based on a set of multivariate polynomials.
Hence, a rectangular partition defined in terms of polynomials of the form (xi
− c) is just a simple case of multivariate polynomial partition, and the new decision
condition applies naturally. We analyze and demonstrate the improvement of our
method over the existing methods using some examples.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23
(Wittgenstein Award).
alternative_title:
- LNCS
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: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- 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: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine
systems. In: Vol 9957. Springer; 2016:128-144. doi:10.1007/978-3-319-47151-8_9'
apa: 'Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang,
Y., & Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol.
9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France:
Springer. https://doi.org/10.1007/978-3-319-47151-8_9'
chicago: Kong, Hui, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Thomas A Henzinger,
Yu Jiang, and Christian Schilling. “Discrete Abstraction of Multiaffine Systems,”
9957:128–44. Springer, 2016. https://doi.org/10.1007/978-3-319-47151-8_9.
ieee: 'H. Kong et al., “Discrete abstraction of multiaffine systems,” presented
at the HSB: Hybrid Systems Biology, Grenoble, France, 2016, vol. 9957, pp. 128–144.'
ista: 'Kong H, Bartocci E, Bogomolov S, Grosu R, Henzinger TA, Jiang Y, Schilling
C. 2016. Discrete abstraction of multiaffine systems. HSB: Hybrid Systems Biology,
LNCS, vol. 9957, 128–144.'
mla: Kong, Hui, et al. Discrete Abstraction of Multiaffine Systems. Vol.
9957, Springer, 2016, pp. 128–44, doi:10.1007/978-3-319-47151-8_9.
short: H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C.
Schilling, in:, Springer, 2016, pp. 128–144.
conference:
end_date: 2016-10-21
location: Grenoble, France
name: 'HSB: Hybrid Systems Biology'
start_date: 2016-10-20
date_created: 2018-12-11T11:50:49Z
date_published: 2016-09-25T00:00:00Z
date_updated: 2021-01-12T06:49:13Z
day: '25'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-47151-8_9
file:
- access_level: open_access
checksum: 994e164b558c47bacf8dc066dd27c8fc
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:49Z
date_updated: 2020-07-14T12:44:39Z
file_id: '4840'
file_name: IST-2017-781-v1+1_main.pdf
file_size: 683955
relation: main_file
file_date_updated: 2020-07-14T12:44:39Z
has_accepted_license: '1'
intvolume: ' 9957'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 128 - 144
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
publication_status: published
publisher: Springer
publist_id: '6107'
pubrep_id: '781'
quality_controlled: '1'
scopus_import: 1
status: public
title: Discrete abstraction of multiaffine systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9957
year: '2016'
...
---
_id: '1658'
abstract:
- lang: eng
text: Continuous-time Markov chain (CTMC) models have become a central tool for
understanding the dynamics of complex reaction networks and the importance of
stochasticity in the underlying biochemical processes. When such models are employed
to answer questions in applications, in order to ensure that the model provides
a sufficiently accurate representation of the real system, it is of vital importance
that the model parameters are inferred from real measured data. This, however,
is often a formidable task and all of the existing methods fail in one case or
the other, usually because the underlying CTMC model is high-dimensional and computationally
difficult to analyze. The parameter inference methods that tend to scale best
in the dimension of the CTMC are based on so-called moment closure approximations.
However, there exists a large number of different moment closure approximations
and it is typically hard to say a priori which of the approximations is the most
suitable for the inference procedure. Here, we propose a moment-based parameter
inference method that automatically chooses the most appropriate moment closure
method. Accordingly, contrary to existing methods, the user is not required to
be experienced in moment closure techniques. In addition to that, our method adaptively
changes the approximation during the parameter inference to ensure that always
the best approximation is used, even in cases where different approximations are
best in different regions of the parameter space.
alternative_title:
- LNCS
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- 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: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Jakob
full_name: Ruess, Jakob
id: 4A245D00-F248-11E8-B48F-1D18A9856A87
last_name: Ruess
orcid: 0000-0003-1615-3282
- first_name: Christian
full_name: Schilling, Christian
last_name: Schilling
citation:
ama: Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. Adaptive moment
closure for parameter inference of biochemical reaction networks. 2015;9308:77-89.
doi:10.1007/978-3-319-23401-4_8
apa: 'Bogomolov, S., Henzinger, T. A., Podelski, A., Ruess, J., & Schilling,
C. (2015). Adaptive moment closure for parameter inference of biochemical reaction
networks. Presented at the CMSB: Computational Methods in Systems Biology, Nantes,
France: Springer. https://doi.org/10.1007/978-3-319-23401-4_8'
chicago: Bogomolov, Sergiy, Thomas A Henzinger, Andreas Podelski, Jakob Ruess, and
Christian Schilling. “Adaptive Moment Closure for Parameter Inference of Biochemical
Reaction Networks.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-319-23401-4_8.
ieee: S. Bogomolov, T. A. Henzinger, A. Podelski, J. Ruess, and C. Schilling, “Adaptive
moment closure for parameter inference of biochemical reaction networks,” vol.
9308. Springer, pp. 77–89, 2015.
ista: Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. 2015. Adaptive
moment closure for parameter inference of biochemical reaction networks. 9308,
77–89.
mla: Bogomolov, Sergiy, et al. Adaptive Moment Closure for Parameter Inference
of Biochemical Reaction Networks. Vol. 9308, Springer, 2015, pp. 77–89, doi:10.1007/978-3-319-23401-4_8.
short: S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, C. Schilling, 9308 (2015)
77–89.
conference:
end_date: 2015-09-18
location: Nantes, France
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2015-09-16
date_created: 2018-12-11T11:53:18Z
date_published: 2015-09-01T00:00:00Z
date_updated: 2023-02-21T16:17:24Z
day: '01'
department:
- _id: ToHe
- _id: GaTk
doi: 10.1007/978-3-319-23401-4_8
ec_funded: 1
intvolume: ' 9308'
language:
- iso: eng
month: '09'
oa_version: None
page: 77 - 89
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5492'
quality_controlled: '1'
related_material:
record:
- id: '1148'
relation: later_version
status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Adaptive moment closure for parameter inference of biochemical reaction networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9308
year: '2015'
...
---
_id: '1670'
abstract:
- lang: eng
text: Planning in hybrid domains poses a special challenge due to the involved mixed
discrete-continuous dynamics. A recent solving approach for such domains is based
on applying model checking techniques on a translation of PDDL+ planning problems
to hybrid automata. However, the proposed translation is limited because must
behavior is only overapproximated, and hence, processes and events are not reflected
exactly. In this paper, we present the theoretical foundation of an exact PDDL+
translation. We propose a schema to convert a hybrid automaton with must transitions
into an equivalent hybrid automaton featuring only may transitions.
acknowledgement: This work was partly supported by the German Research Foundation
(DFG) as part of the Transregional Collaborative Research Center “Automatic Verification
and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/), by the
European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science
Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and
by the Swiss National Science Foundation (SNSF) as part of the project “Automated
Reformulation and Pruning in Factored State Spaces (ARAP)”.
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Daniele
full_name: Magazzeni, Daniele
last_name: Magazzeni
- first_name: Stefano
full_name: Minopoli, Stefano
last_name: Minopoli
- first_name: Martin
full_name: Wehrle, Martin
last_name: Wehrle
citation:
ama: 'Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. PDDL+ planning with hybrid
automata: Foundations of translating must behavior. In: AAAI Press; 2015:42-46.'
apa: 'Bogomolov, S., Magazzeni, D., Minopoli, S., & Wehrle, M. (2015). PDDL+
planning with hybrid automata: Foundations of translating must behavior (pp. 42–46).
Presented at the ICAPS: International Conference on Automated Planning and Scheduling,
Jerusalem, Israel: AAAI Press.'
chicago: 'Bogomolov, Sergiy, Daniele Magazzeni, Stefano Minopoli, and Martin Wehrle.
“PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior,”
42–46. AAAI Press, 2015.'
ieee: 'S. Bogomolov, D. Magazzeni, S. Minopoli, and M. Wehrle, “PDDL+ planning with
hybrid automata: Foundations of translating must behavior,” presented at the ICAPS:
International Conference on Automated Planning and Scheduling, Jerusalem, Israel,
2015, pp. 42–46.'
ista: 'Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. 2015. PDDL+ planning with
hybrid automata: Foundations of translating must behavior. ICAPS: International
Conference on Automated Planning and Scheduling, 42–46.'
mla: 'Bogomolov, Sergiy, et al. PDDL+ Planning with Hybrid Automata: Foundations
of Translating Must Behavior. AAAI Press, 2015, pp. 42–46.'
short: S. Bogomolov, D. Magazzeni, S. Minopoli, M. Wehrle, in:, AAAI Press, 2015,
pp. 42–46.
conference:
end_date: 2015-06-11
location: Jerusalem, Israel
name: 'ICAPS: International Conference on Automated Planning and Scheduling'
start_date: 2015-06-07
date_created: 2018-12-11T11:53:23Z
date_published: 2015-06-01T00:00:00Z
date_updated: 2021-01-12T06:52:25Z
day: '01'
department:
- _id: ToHe
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: https://www.aaai.org/ocs/index.php/ICAPS/ICAPS15/paper/view/10606/10394
month: '06'
oa_version: None
page: 42 - 46
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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_status: published
publisher: AAAI Press
publist_id: '5479'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'PDDL+ planning with hybrid automata: Foundations of translating must behavior'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1690'
abstract:
- lang: eng
text: A number of powerful and scalable hybrid systems model checkers have recently
emerged. Although all of them honor roughly the same hybrid systems semantics,
they have drastically different model description languages. This situation (a)
makes it difficult to quickly evaluate a specific hybrid automaton model using
the different tools, (b) obstructs comparisons of reachability approaches, and
(c) impedes the widespread application of research results that perform model
modification and could benefit many of the tools. In this paper, we present Hyst,
a Hybrid Source Transformer. Hyst is a source-to-source translation tool, currently
taking input in the SpaceEx model format, and translating to the formats of HyCreate,
Flow∗, or dReach. Internally, the tool supports generic model-to-model transformation
passes that serve to both ease the translation and potentially improve reachability
results for the supported tools. Although these model transformation passes could
be implemented within each tool, the Hyst approach provides a single place for
model modification, generating modified input sources for the unmodified target
tools. Our evaluation demonstrates Hyst is capable of automatically translating
benchmarks in several classes (including affine and nonlinear hybrid automata)
to the input formats of several tools. Additionally, we illustrate a general model
transformation pass based on pseudo-invariants implemented in Hyst that illustrates
the reachability improvement.
acknowledgement: The material presented in this paper is based upon work sup-ported
by the Air Force Research Laboratory’s Information Directorate (AFRL/RI) through
the Visiting Faculty Research Program (VFRP) under contract number FA8750-13-2-0115
and the Air Force Office of Scientific Research (AFOSR). Any opinions,findings,
and conclusions or recommendations expressed in this publication are those of the
authors and do not necessarily reflect the views of the AFRL/RI or AFOSR. This work
was also partly supported in part by the German Research Foundation (DFG) as part
of the Transregional Collaborative Research Center “Automatic Verification and Analysis
of Complex Systems” (SFB/TR14 AVACS, http://www.avacs.org/), by the European Research
Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF)
under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).
author:
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
citation:
ama: 'Bak S, Bogomolov S, Johnson T. HYST: A source transformation and translation
tool for hybrid automaton models. In: Springer; 2015:128-133. doi:10.1145/2728606.2728630'
apa: 'Bak, S., Bogomolov, S., & Johnson, T. (2015). HYST: A source transformation
and translation tool for hybrid automaton models (pp. 128–133). Presented at the
HSCC: Hybrid Systems - Computation and Control, Seattle, WA, United States: Springer.
https://doi.org/10.1145/2728606.2728630'
chicago: 'Bak, Stanley, Sergiy Bogomolov, and Taylor Johnson. “HYST: A Source Transformation
and Translation Tool for Hybrid Automaton Models,” 128–33. Springer, 2015. https://doi.org/10.1145/2728606.2728630.'
ieee: 'S. Bak, S. Bogomolov, and T. Johnson, “HYST: A source transformation and
translation tool for hybrid automaton models,” presented at the HSCC: Hybrid Systems
- Computation and Control, Seattle, WA, United States, 2015, pp. 128–133.'
ista: 'Bak S, Bogomolov S, Johnson T. 2015. HYST: A source transformation and translation
tool for hybrid automaton models. HSCC: Hybrid Systems - Computation and Control,
128–133.'
mla: 'Bak, Stanley, et al. HYST: A Source Transformation and Translation Tool
for Hybrid Automaton Models. Springer, 2015, pp. 128–33, doi:10.1145/2728606.2728630.'
short: S. Bak, S. Bogomolov, T. Johnson, in:, Springer, 2015, pp. 128–133.
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2728606.2728630
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 128 - 133
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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_status: published
publisher: Springer
publist_id: '5454'
quality_controlled: '1'
status: public
title: 'HYST: A source transformation and translation tool for hybrid automaton models'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1692'
abstract:
- lang: eng
text: Computing an approximation of the reachable states of a hybrid system is a
challenge, mainly because overapproximating the solutions of ODEs with a finite
number of sets does not scale well. Using template polyhedra can greatly reduce
the computational complexity, since it replaces complex operations on sets with
a small number of optimization problems. However, the use of templates may make
the over-approximation too conservative. Spurious transitions, which are falsely
considered reachable, are particularly detrimental to performance and accuracy,
and may exacerbate the state explosion problem. In this paper, we examine how
spurious transitions can be avoided with minimal computational effort. To this
end, detecting spurious transitions is reduced to the well-known problem of showing
that two convex sets are disjoint by finding a hyperplane that separates them.
We generalize this to owpipes by considering hyperplanes that evolve with time
in correspondence to the dynamics of the system. The approach is implemented in
the model checker SpaceEx and demonstrated on examples.
author:
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Marius
full_name: Greitschus, Marius
last_name: Greitschus
- first_name: Thomas
full_name: Strump, Thomas
last_name: Strump
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
citation:
ama: 'Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. Eliminating spurious
transitions in reachability with support functions. In: Proceedings of the
18th International Conference on Hybrid Systems: Computation and Control.
ACM; 2015:149-158. doi:10.1145/2728606.2728622'
apa: 'Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., & Podelski, A.
(2015). Eliminating spurious transitions in reachability with support functions.
In Proceedings of the 18th International Conference on Hybrid Systems: Computation
and Control (pp. 149–158). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728622'
chicago: 'Frehse, Goran, Sergiy Bogomolov, Marius Greitschus, Thomas Strump, and
Andreas Podelski. “Eliminating Spurious Transitions in Reachability with Support
Functions.” In Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control, 149–58. ACM, 2015. https://doi.org/10.1145/2728606.2728622.'
ieee: 'G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, and A. Podelski, “Eliminating
spurious transitions in reachability with support functions,” in Proceedings
of the 18th International Conference on Hybrid Systems: Computation and Control,
Seattle, WA, United States, 2015, pp. 149–158.'
ista: 'Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. 2015. Eliminating
spurious transitions in reachability with support functions. Proceedings of the
18th International Conference on Hybrid Systems: Computation and Control. HSCC:
Hybrid Systems - Computation and Control, 149–158.'
mla: 'Frehse, Goran, et al. “Eliminating Spurious Transitions in Reachability with
Support Functions.” Proceedings of the 18th International Conference on Hybrid
Systems: Computation and Control, ACM, 2015, pp. 149–58, doi:10.1145/2728606.2728622.'
short: 'G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, A. Podelski, in:, Proceedings
of the 18th International Conference on Hybrid Systems: Computation and Control,
ACM, 2015, pp. 149–158.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:30Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2728606.2728622
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 149 - 158
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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 18th International Conference on Hybrid Systems:
Computation and Control'
publication_identifier:
isbn:
- 978-1-4503-3433-4
publication_status: published
publisher: ACM
publist_id: '5452'
quality_controlled: '1'
scopus_import: 1
status: public
title: Eliminating spurious transitions in reachability with support functions
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1500'
abstract:
- lang: eng
text: In this poster, we present methods for randomly generating hybrid automata
with affine differential equations, invariants, guards, and assignments. Selecting
an arbitrary affine function from the set of all affine functions results in a
low likelihood of generating hybrid automata with diverse and interesting behaviors,
as there are an uncountable number of elements in the set of all affine functions.
Instead, we partition the set of all affine functions into potentially interesting
classes and randomly select elements from these classes. For example, we partition
the set of all affine differential equations by using restrictions on eigenvalues
such as those that yield stable, unstable, etc. equilibrium points. We partition
the components describing discrete behavior (guards, assignments, and invariants)
to allow either time-dependent or state-dependent switching, and in particular
provide the ability to generate subclasses of piecewise-affine hybrid automata.
Our preliminary experimental results with a prototype tool called HyRG (Hybrid
Random Generator) illustrate the feasibility of this generation method to automatically
create standard hybrid automaton examples like the bouncing ball and thermostat.
alternative_title:
- '18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC
2015'
author:
- first_name: Luan
full_name: Nguyen, Luan V
last_name: Nguyen
- first_name: Christian
full_name: Christian Schilling
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Sergiy
full_name: Sergiy Bogomolov
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Taylor
full_name: Johnson, Taylor T
last_name: Johnson
citation:
ama: 'Nguyen L, Schilling C, Bogomolov S, Johnson T. Poster: HyRG: A Random Generation
Tool for Affine Hybrid Automata. Springer; 2015:289-290. doi:10.1145/2728606.2728650'
apa: 'Nguyen, L., Schilling, C., Bogomolov, S., & Johnson, T. (2015). Poster:
HyRG: A random generation tool for affine hybrid automata. HSCC: Hybrid
Systems - Computation and Control (pp. 289–290). Springer. https://doi.org/10.1145/2728606.2728650'
chicago: 'Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson.
Poster: HyRG: A Random Generation Tool for Affine Hybrid Automata. HSCC:
Hybrid Systems - Computation and Control. Springer, 2015. https://doi.org/10.1145/2728606.2728650.'
ieee: 'L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, Poster: HyRG: A
random generation tool for affine hybrid automata. Springer, 2015, pp. 289–290.'
ista: 'Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Poster: HyRG: A random
generation tool for affine hybrid automata, Springer,p.'
mla: 'Nguyen, Luan, et al. “Poster: HyRG: A Random Generation Tool for Affine Hybrid
Automata.” HSCC: Hybrid Systems - Computation and Control, Springer, 2015,
pp. 289–90, doi:10.1145/2728606.2728650.'
short: 'L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, Poster: HyRG: A Random
Generation Tool for Affine Hybrid Automata, Springer, 2015.'
date_created: 2018-12-11T11:52:23Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2019-04-26T07:22:03Z
day: '14'
doi: 10.1145/2728606.2728650
extern: 1
month: '04'
page: 289 - 290
publication: 'HSCC: Hybrid Systems - Computation and Control'
publication_status: published
publisher: Springer
publist_id: '5678'
quality_controlled: 0
status: public
title: 'Poster: HyRG: A random generation tool for affine hybrid automata'
type: conference_poster
year: '2015'
...
---
_id: '1541'
abstract:
- lang: eng
text: We present XSpeed a parallel state-space exploration algorithm for continuous
systems with linear dynamics and nondeterministic inputs. The motivation of having
parallel algorithms is to exploit the computational power of multi-core processors
to speed-up performance. The parallelization is achieved on two fronts. First,
we propose a parallel implementation of the support function algorithm by sampling
functions in parallel. Second, we propose a parallel state-space exploration by
slicing the time horizon and computing the reachable states in the time slices
in parallel. The second method can be however applied only to a class of linear
systems with invertible dynamics and fixed input. A GP-GPU implementation is also
presented following a lazy evaluation strategy on support functions. The parallel
algorithms are implemented in the tool XSpeed. We evaluated the performance on
two benchmarks including an 28 dimension Helicopter model. Comparison with the
sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread
Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up
of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario),
the state of the art tool for reachability analysis of linear hybrid systems.
Experiments illustrate that our parallel algorithm with time slicing not only
speeds-up performance but also improves precision.
acknowledgement: This work was supported in part by the European Research Council
(ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants
S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
alternative_title:
- LNCS
author:
- first_name: Rajarshi
full_name: Ray, Rajarshi
last_name: Ray
- first_name: Amit
full_name: Gurung, Amit
last_name: Gurung
- first_name: Binayak
full_name: Das, Binayak
last_name: Das
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. XSpeed: Accelerating
reachability analysis on multi-core processors. 2015;9434:3-18. doi:10.1007/978-3-319-26287-1_1'
apa: 'Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., & Grosu, R.
(2015). XSpeed: Accelerating reachability analysis on multi-core processors. Presented
at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. https://doi.org/10.1007/978-3-319-26287-1_1'
chicago: 'Ray, Rajarshi, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov,
and Radu Grosu. “XSpeed: Accelerating Reachability Analysis on Multi-Core Processors.”
Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-319-26287-1_1.'
ieee: 'R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, and R. Grosu, “XSpeed:
Accelerating reachability analysis on multi-core processors,” vol. 9434. Springer,
pp. 3–18, 2015.'
ista: 'Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. 2015. XSpeed: Accelerating
reachability analysis on multi-core processors. 9434, 3–18.'
mla: 'Ray, Rajarshi, et al. XSpeed: Accelerating Reachability Analysis on Multi-Core
Processors. Vol. 9434, Springer, 2015, pp. 3–18, doi:10.1007/978-3-319-26287-1_1.'
short: R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, R. Grosu, 9434 (2015)
3–18.
conference:
end_date: 2015-11-19
location: Haifa, Israel
name: 'HVC: Haifa Verification Conference'
start_date: 2015-11-17
date_created: 2018-12-11T11:52:37Z
date_published: 2015-11-28T00:00:00Z
date_updated: 2020-08-11T10:09:17Z
day: '28'
department:
- _id: ToHe
doi: 10.1007/978-3-319-26287-1_1
ec_funded: 1
intvolume: ' 9434'
language:
- iso: eng
month: '11'
oa_version: None
page: 3 - 18
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _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_status: published
publisher: Springer
publist_id: '5630'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: 'XSpeed: Accelerating reachability analysis on multi-core processors'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9434
year: '2015'
...
---
_id: '1605'
abstract:
- lang: eng
text: Multiaffine hybrid automata (MHA) represent a powerful formalism to model
complex dynamical systems. This formalism is particularly suited for the representation
of biological systems which often exhibit highly non-linear behavior. In this
paper, we consider the problem of parameter identification for MHA. We present
an abstraction of MHA based on linear hybrid automata, which can be analyzed by
the SpaceEx model checker. This abstraction enables a precise handling of time-dependent
properties. We demonstrate the potential of our approach on a model of a genetic
regulatory network and a myocyte model.
acknowledgement: This work was partly supported by the European Research Council (ERC)
under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23,
S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by
the German Research Foundation (DFG) as part of the Transregional Collaborative
Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR
14 AVACS, http://www.avacs.org/).
alternative_title:
- LNCS
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: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Grégory
full_name: Batt, Grégory
last_name: Batt
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: 'Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based
parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35.
doi:10.1007/978-3-319-26287-1_2'
apa: 'Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., & Grosu,
R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol.
9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa,
Israel: Springer. https://doi.org/10.1007/978-3-319-26287-1_2'
chicago: Bogomolov, Sergiy, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui
Kong, and Radu Grosu. “Abstraction-Based Parameter Synthesis for Multiaffine Systems,”
9434:19–35. Springer, 2015. https://doi.org/10.1007/978-3-319-26287-1_2.
ieee: 'S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, and R. Grosu,
“Abstraction-based parameter synthesis for multiaffine systems,” presented at
the HVC: Haifa Verification Conference, Haifa, Israel, 2015, vol. 9434, pp. 19–35.'
ista: 'Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. 2015. Abstraction-based
parameter synthesis for multiaffine systems. HVC: Haifa Verification Conference,
LNCS, vol. 9434, 19–35.'
mla: Bogomolov, Sergiy, et al. Abstraction-Based Parameter Synthesis for Multiaffine
Systems. Vol. 9434, Springer, 2015, pp. 19–35, doi:10.1007/978-3-319-26287-1_2.
short: S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:,
Springer, 2015, pp. 19–35.
conference:
end_date: 2015-11-19
location: Haifa, Israel
name: 'HVC: Haifa Verification Conference'
start_date: 2015-11-17
date_created: 2018-12-11T11:52:59Z
date_published: 2015-11-28T00:00:00Z
date_updated: 2021-01-12T06:51:56Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-26287-1_2
ec_funded: 1
file:
- access_level: open_access
checksum: 3aab260f3f34641d622030ba22645b3e
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T08:43:19Z
date_updated: 2020-07-14T12:45:05Z
file_id: '7851'
file_name: 2015_LNCS_Bogomolov.pdf
file_size: 1053207
relation: main_file
file_date_updated: 2020-07-14T12:45:05Z
has_accepted_license: '1'
intvolume: ' 9434'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 19 - 35
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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_status: published
publisher: Springer
publist_id: '5561'
quality_controlled: '1'
scopus_import: 1
status: public
title: Abstraction-based parameter synthesis for multiaffine systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9434
year: '2015'
...
---
_id: '1606'
abstract:
- lang: eng
text: 'In this paper, we present the first steps toward a runtime verification framework
for monitoring hybrid and cyber-physical systems (CPS) development tools based
on randomized differential testing. The development tools include hybrid systems
reachability analysis tools, model-based development environments like Simulink/Stateflow
(SLSF), etc. First, hybrid automaton models are randomly generated. Next, these
hybrid automaton models are translated to a number of different tools (currently,
SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using
the HyST source transformation and translation tool. Then, the hybrid automaton
models are executed in the different tools and their outputs are parsed. The final
step is the differential comparison: the outputs of the different tools are compared.
If the results do not agree (in the sense that an analysis or verification result
from one tool does not match that of another tool, ignoring timeouts, etc.), a
candidate bug is flagged and the model is saved for future analysis by the user.
The process then repeats and the monitoring continues until the user terminates
the process. We present preliminary results that have been useful in identifying
a few bugs in the analysis methods of different development tools, and in an earlier
version of HyST.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luan
full_name: Nguyen, Luan
last_name: Nguyen
- first_name: Christian
full_name: Schilling, Christian
last_name: Schilling
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
citation:
ama: 'Nguyen L, Schilling C, Bogomolov S, Johnson T. Runtime verification for hybrid
analysis tools. In: 6th International Conference. Vol 9333. Springer Nature;
2015:281-286. doi:10.1007/978-3-319-23820-3_19'
apa: 'Nguyen, L., Schilling, C., Bogomolov, S., & Johnson, T. (2015). Runtime
verification for hybrid analysis tools. In 6th International Conference
(Vol. 9333, pp. 281–286). Vienna, Austria: Springer Nature. https://doi.org/10.1007/978-3-319-23820-3_19'
chicago: Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson.
“Runtime Verification for Hybrid Analysis Tools.” In 6th International Conference,
9333:281–86. Springer Nature, 2015. https://doi.org/10.1007/978-3-319-23820-3_19.
ieee: L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, “Runtime verification
for hybrid analysis tools,” in 6th International Conference, Vienna, Austria,
2015, vol. 9333, pp. 281–286.
ista: 'Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Runtime verification
for hybrid analysis tools. 6th International Conference. RV: Runtime Verification,
LNCS, vol. 9333, 281–286.'
mla: Nguyen, Luan, et al. “Runtime Verification for Hybrid Analysis Tools.” 6th
International Conference, vol. 9333, Springer Nature, 2015, pp. 281–86, doi:10.1007/978-3-319-23820-3_19.
short: L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, in:, 6th International
Conference, Springer Nature, 2015, pp. 281–286.
conference:
end_date: 2015-09-25
location: Vienna, Austria
name: 'RV: Runtime Verification'
start_date: 2015-09-22
date_created: 2018-12-11T11:52:59Z
date_published: 2015-11-15T00:00:00Z
date_updated: 2022-02-01T14:52:59Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-319-23820-3_19
ec_funded: 1
intvolume: ' 9333'
language:
- iso: eng
month: '11'
oa_version: None
page: 281 - 286
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _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: 6th International Conference
publication_identifier:
isbn:
- 978-3-319-23819-7
publication_status: published
publisher: Springer Nature
publist_id: '5562'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Runtime verification for hybrid analysis tools
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9333
year: '2015'
...