Contract-Based Design for Hybrid Dynamical Systems and Invariance Properties

TL;DR

This paper develops principles for verifying contracts in interconnected hybrid systems, focusing on temporal satisfaction and compositional reasoning, with new semantics for weak and strong satisfaction and their application to feedback and cascade compositions.

Contribution

It introduces notions of weak and strong contract satisfaction for hybrid systems, enabling compositional reasoning and analysis of feedback and cascade interconnections.

Findings

Weak and strong satisfaction semantics are compatible with cascade composition.

Strong semantics are necessary for feedback composition.

Contract satisfaction can be transitioned from weak to strong.

Abstract

This work establishes fundamental principles for verifying contract for interconnected hybrid systems. When system's hybrid arcs conform to the contract for a certain duration but subsequently violate it, the composition of hybrid dynamical systems becomes challenging. The objective of this work is to analyze the temporal satisfaction of the contract, allowing us to reason about the compositions that do not violate the contract up to a certain point in a hybrid time. Notions of weak and strong satisfaction of an assume-guarantee contract are introduced. These semantics permits the compositional reasoning on hybrid systems of varying complexity depending on the interconnection's type, feedback or cascade. The results show that both semantics are compatible with cascade composition, while strong semantic is required for feedback composition. Moreover, we have shown how one can go from weak to strong contract satisfaction. Finally, we have studied a particular class of hybrid systems and we have shown that the concept of forward (pre-)invariant relative to a contract makes it possible to deal with feedback compositions. These results are demonstrated throughout the paper with simple numerical examples.