Towards Physical Hybrid Systems

TL;DR

This paper introduces 'physical hybrid systems' (PHS), a new modeling approach that adjusts hybrid systems logic to better align mathematical models with physical reality, especially regarding measure zero sets.

Contribution

It develops the concept of PHS and extends differential temporal dynamic logic with an operator to ignore measure zero distinctions, enabling more physically realistic modeling and verification.

Findings

Allows verification of models previously considered unsafe due to measure zero issues

Extends hybrid systems logic with a new operator for measure zero elision

Provides a proof calculus for verifying physical hybrid systems

Abstract

Some hybrid systems models are unsafe for mathematically correct but physically unrealistic reasons. For example, mathematical models can classify a system as being unsafe on a set that is too small to have physical importance. In particular, differences in measure zero sets in models of cyber-physical systems (CPS) have significant mathematical impact on the mathematical safety of these models even though differences on measure zero sets have no tangible physical effect in a real system. We develop the concept of "physical hybrid systems" (PHS) to help reunite mathematical models with physical reality. We modify a hybrid systems logic (differential temporal dynamic logic) by adding a first-class operator to elide distinctions on measure zero sets of time within CPS models. This approach facilitates modeling since it admits the verification of a wider class of models, including some physically realistic models that would otherwise be classified as mathematically unsafe. We also develop a proof calculus to help with the verification of PHS.