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

TL;DR

This paper introduces frequency automata, a new formal model for hybrid systems that combines time and frequency domain representations, enabling more efficient and precise simulation and analysis than traditional methods.

Contribution

The paper presents the first formal model of frequency automata for hybrid systems, along with a translation from hybrid automata and a numerical simulator demonstrating superior performance.

Findings

Simulation times 118x to 1129x faster than Simulink/Stateflow

Accurate level crossing detection including complex guards

Effective hybrid systems modeling in combined time and frequency domains

Abstract

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.