Quasi-Dependent Variables in Hybrid Automata

The concept of hybrid automata provides a powerful framework to model and analyze real-world problem domains. Due to the structural complexity of hybrid systems it is important to ensure the scalability of analysis algorithms. We approach this problem by providing an eective extension of the recently introduced notion of quasi-equal clocks to hybrid systems. For this purpose, we introduce the concept of quasi-dependent variables. Our contribution is twofold: we demonstrate how such variables can be automatically detected, and we present a transformation leading to an abstraction with a smaller state space which, however, still retains the same properties as an original system. We demonstrate the practical applicability of our methods on a range of industrial benchmarks.