Formal Semantics of Hybrid Automata

From FSL
Jump to: navigation, search

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.
PDF, Matching Logic, DOI, BIB

Personal tools
Namespaces

Variants
Actions
Navigation