Files in this item



application/pdfsaxena-rodrigues-chen-rosu-2020-tr.pdf (369kB)
(no description provided)PDF


Title:Formal semantics of hybrid automata
Author(s):Saxena, Manasvi; Chen, Xiaohong; Rodrigues, Nishant; Rosu, Grigore
Subject(s):Hybrid Systems
Cyber Physical Systems
Matching Logic
Formal Methods
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.
Issue Date:2020
Genre:Technical Report
Date Available in IDEALS:2020-04-14

This item appears in the following Collection(s)

Item Statistics