@inproceedings{77a736ce3e5a41ec896907efee950133,
title = "Time-triggered conversion of guards for reachability analysis of hybrid automata",
abstract = "A promising technique for the formal verification of embedded and cyber-physical systems is flow-pipe construction, which creates a sequence of regions covering all reachable states over time. Flow-pipe construction methods can check whether specifications are met for all states, rather than just testing using a finite and incomplete set of simulation traces. A fundamental challenge when using flow-pipe construction on high-dimensional systems is the cost of geometric operations, such as intersection and convex hull. We address this challenge by showing that it is often possible to remove the need to perform high-dimensional geometric operations by combining two model transformations, direct time-triggered conversion and dynamics scaling. Further, we prove the overapproximation error in the conversion can be made arbitrarily small. Finally, we show that our transformation-based approach enables the analysis of a drivetrain system with up to 51 dimensions.",
author = "Stanley Bak and Sergiy Bogomolov and Matthias Althoff",
note = "Publisher Copyright: {\textcopyright} 2017, Springer International Publishing AG.; 15th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2017 ; Conference date: 05-09-2017 Through 07-09-2017",
year = "2017",
doi = "10.1007/978-3-319-65765-3\_8",
language = "English",
isbn = "9783319657646",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "133--150",
editor = "Alessandro Abate and Gilles Geeraerts",
booktitle = "Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Proceedings",
address = "Germany",
}