Towards Physical Hybrid Systems
For researchers in cyber-physical systems verification, this work provides a method to reconcile mathematical models with physical reality by ignoring measure zero distinctions, though it is an incremental extension of existing logic.
The paper introduces 'physical hybrid systems' (PHS) to address unsafe classifications in hybrid systems due to measure zero sets, modifying differential temporal dynamic logic with an operator to ignore such sets, enabling verification of physically realistic models that would otherwise be deemed mathematically unsafe.
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.