Approximated Symbolic Computations over Hybrid Automata

TL;DR

This paper introduces a flexible framework for hybrid automata that incorporates approximated semantics, enabling better handling of noise, partial information, and finite precision in modeling complex systems.

Contribution

It develops a unified approach combining over and under-approximation techniques for hybrid automata to improve reachability analysis under realistic conditions.

Findings

Framework supports mixing and comparing approximation techniques

Enables more realistic modeling of noisy and imprecise systems

Facilitates development of diverse approximated reachability algorithms

Abstract

Hybrid automata are a natural framework for modeling and analyzing systems which exhibit a mixed discrete continuous behaviour. However, the standard operational semantics defined over such models implicitly assume perfect knowledge of the real systems and infinite precision measurements. Such assumptions are not only unrealistic, but often lead to the construction of misleading models. For these reasons we believe that it is necessary to introduce more flexible semantics able to manage with noise, partial information, and finite precision instruments. In particular, in this paper we integrate in a single framework based on approximated semantics different over and under-approximation techniques for hybrid automata. Our framework allows to both compare, mix, and generalize such techniques obtaining different approximated reachability algorithms.