conference paper published yes Marcelo Forets author Daniel Freire author Christian Schilling author 3A2F4DCE-F248-11E8-B48F-1D18A9856A870000-0003-3658-1065 ToHe department MEMOCODE: Conference on Formal Methods and Models for System Design Formal methods for the design and analysis of complex systems project ISTplus - Postdoctoral Fellowships project Efficiently handling time-triggered and possibly nondeterministic switches for hybrid systems reachability is a challenging task. In this paper we present an approach based on conservative set-based enclosure of the dynamics that can handle systems with uncertain parameters and inputs, where the uncertainties are bound to given intervals. The method is evaluated on the plant model of an experimental electro-mechanical braking system with periodic controller. In this model, the fast-switching controller dynamics requires simulation time scales of the order of nanoseconds. Accurate set-based computations for relatively large time horizons are known to be expensive. However, by appropriately decoupling the time variable with respect to the spatial variables, and enclosing the uncertain parameters using interval matrix maps acting on zonotopes, we show that the computation time can be lowered to 5000 times faster with respect to previous works. This is a step forward in formal verification of hybrid systems because reduced run-times allow engineers to introduce more expressiveness in their models with a relatively inexpensive computational cost. IEEE2020Virtual Conference eng 9781728191485 2006.12325 00066192040001310.1109/MEMOCODE51338.2020.9314994 M. Forets, D. Freire, and C. Schilling, “Efficient reachability analysis of parametric linear hybrid systems with  time-triggered transitions,” in <i>18th ACM-IEEE International Conference on Formal Methods and Models for System Design</i>, Virtual Conference, 2020. Forets M, Freire D, Schilling C. Efficient reachability analysis of parametric linear hybrid systems with  time-triggered transitions. In: <i>18th ACM-IEEE International Conference on Formal Methods and Models for System Design</i>. IEEE; 2020. doi:<a href="https://doi.org/10.1109/MEMOCODE51338.2020.9314994">10.1109/MEMOCODE51338.2020.9314994</a> Forets, M., Freire, D., &#38; Schilling, C. (2020). Efficient reachability analysis of parametric linear hybrid systems with  time-triggered transitions. In <i>18th ACM-IEEE International Conference on Formal Methods and Models for System Design</i>. Virtual Conference: IEEE. <a href="https://doi.org/10.1109/MEMOCODE51338.2020.9314994">https://doi.org/10.1109/MEMOCODE51338.2020.9314994</a> Forets, Marcelo, Daniel Freire, and Christian Schilling. “Efficient Reachability Analysis of Parametric Linear Hybrid Systems with  Time-Triggered Transitions.” In <i>18th ACM-IEEE International Conference on Formal Methods and Models for System Design</i>. IEEE, 2020. <a href="https://doi.org/10.1109/MEMOCODE51338.2020.9314994">https://doi.org/10.1109/MEMOCODE51338.2020.9314994</a>. Forets, Marcelo, et al. “Efficient Reachability Analysis of Parametric Linear Hybrid Systems with  Time-Triggered Transitions.” <i>18th ACM-IEEE International Conference on Formal Methods and Models for System Design</i>, 9314994, IEEE, 2020, doi:<a href="https://doi.org/10.1109/MEMOCODE51338.2020.9314994">10.1109/MEMOCODE51338.2020.9314994</a>. M. Forets, D. Freire, C. Schilling, in:, 18th ACM-IEEE International Conference on Formal Methods and Models for System Design, IEEE, 2020. Forets M, Freire D, Schilling C. 2020. Efficient reachability analysis of parametric linear hybrid systems with  time-triggered transitions. 18th ACM-IEEE International Conference on Formal Methods and Models for System Design. MEMOCODE: Conference on Formal Methods and Models for System Design, 9314994. 87502020-11-10T07:04:57Z2025-04-15T06:26:12Z