Formal Semantics of Hybrid Automata

Manasvi Saxena and Nishant Rodrigues and Xiaohong Chen and Grigore Rosu
Technical Report April 2020
PDF BIB Matching Logic

Abstract. Hybrid Automata (HA) form the backbone of modeling systems with both discrete and continuous components. However, the semantics of HA are usually described loosely using Labeled Transition Systems (LTS), and reasoning about HA involves informal proofs over LTS. In this paper, we propose a formally rigorous, concise, and semantically correct definition of HA in Matching Logic (ML), which is a uniform logic for programming languages design and verification. We show how our definition allows formal reasoning about HA using ML's proof system. Our approach exposes HA to a rich set of tools that operate over ML and provide a sound logical basis for various techniques like Deductive Verification, Monitoring and Runtime Verification.