2020/12/31 by Nikolaos Kekatos, Kekatos, Nikolaos
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Modeling and Simulation Systems
paper · pdf · doi:10.48550/arxiv.2101.00012
openalex publication_date 2020/12/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.