Encoding sinusoidal functions in hybrid automata formalism

TL;DR

This paper introduces a method to encode sinusoidal functions directly within hybrid automata, enhancing the capabilities of existing tools like SpaceEx for more expressive modeling of physical systems.

Contribution

It presents a novel approach to incorporate sinusoidal functions into hybrid automata, enabling more natural modeling of systems with oscillatory behavior.

Findings

Supported sinusoidal functions in SpaceEx.

Translated Simulink blocks into hybrid automata.

Enhanced expressiveness of hybrid automata models.

Abstract

Hybrid systems can express a plethora of physical phenomena and systems as they can combine continuous and discrete dynamics. There exist several tools that enable the reachability analysis of hybrid systems modeled as hybrid automata. However, these tools exhibit certain limitations in the type of mathematical operations that they natively support. For example, SpaceEx, a well-established tool in the hybrid verification community, supports the use of linear ODEs in the flow of each discrete location. Mathematical functions like algebraic equations or trigonometric functions have to be encoded as the solutions of a set of ODEs. In this article, we provide a mechanism to define sinusoidal functions that are supported by SpaceEx. We also show how certain Simulink blocks can be translated into hybrid automata.