Formal Semantics of Hybrid Automata
- Formal Semantics of Hybrid Automata
- Manasvi Saxena and Nishant Rodrigues and Xiaohong Chen and Grigore Rosu
- Technical Report http://hdl.handle.net/2142/106822, April 2020
- 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.