# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1905.09520