Frequency Automata: A novel formal model of hybrid systems in combined time and frequency domains

Hybrid systems are mostly modelled, simulated, and verified in the time domain by computer scientists. Engineers, however, use both frequency and time domain modelling due to their distinct advantages. For example, frequency domain modelling is better suited for control systems, using features such as spectra of the signal. Considering this, we introduce, for the first time, a formal model called frequency automata for hybrid systems modelling and simulation, which are represented in combined time and frequency domains. We propose a sound translation from Hybrid Automata (HA) to Frequency Automata (FA). We also develop a numerical simulator for FA and compare it with the performance of HA. Our approach provides precise level crossing detection and efficient simulation of hybrid systems. We provide empirical results comparing simulation of HA via its translation to FA and its simulation via Matlab Simulink/Stateflow. The results show clear superiority of the proposed technique with the execution times of the proposed technique 118x to 1129x faster compared to Simulink/Stateflow. Moreover, we also observe that the proposed technique is able to detect level crossing with complex guards (including equality), which Simulink/Stateflow fail.