Reachability analysis of linear hybrid systems via block decomposition

S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings of the International Conference on Embedded Software, n.d.

Download
OA 2020EMSOFT.pdf 696.38 KB
Conference Paper | In Press | English
Author
Bogomolov, Sergiy; Forets, Marcelo; Frehse, Goran; Potomkin, Kostiantyn; Schilling, ChristianIST Austria
Department
Abstract
Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this paper, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.
Publishing Year
Date Published
2020-01-01
Proceedings Title
Proceedings of the International Conference on Embedded Software
Conference
EMSOFT: International Conference on Embedded Software
Conference Location
Virtual
Conference Date
2020-09-20 – 2020-09-25
IST-REx-ID

Cite this

Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis of linear hybrid systems via block decomposition. In: Proceedings of the International Conference on Embedded Software.
Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (n.d.). Reachability analysis of linear hybrid systems via block decomposition. In Proceedings of the International Conference on Embedded Software. Virtual .
Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” In Proceedings of the International Conference on Embedded Software, n.d.
S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “Reachability analysis of linear hybrid systems via block decomposition,” in Proceedings of the International Conference on Embedded Software, Virtual .
Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis of linear hybrid systems via block decomposition. Proceedings of the International Conference on Embedded Software. EMSOFT: International Conference on Embedded Software
Bogomolov, Sergiy, et al. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” Proceedings of the International Conference on Embedded Software.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2020-08-24
MD5 Checksum
d19e97d0f8a3a441dc078ec812297d75


Export

Marked Publications

Open Data IST Research Explorer

Sources

arXiv 1905.02458

Search this title in

Google Scholar