Contract-Based Design for Hybrid Dynamical Systems and Invariance Properties

TL;DR

The paper develops a contract-based framework for interconnected hybrid dynamical systems, addressing how contract satisfaction can evolve over hybrid time domains such as $E \subset \mathbb{R}_{\ge 0}\times \mathbb{N}$. It defines assume-guarantee contracts for hybrids and introduces weak and strong satisfaction notions, analyzing cascade and feedback interconnections and establishing a link to forward invariance notions with forward (pre-)invariance as a tool for reasoning about feedback. Key results show that both semantics are compatible with cascade composition, while strong semantics are required for feedback composition, and provide a pathway to upgrade weak to strong satisfaction under bounded output variation with a parameter $\beta$ and an expansion $\varepsilon>\beta$. The work further introduces forward (pre-)invariant concepts relative to a contract and demonstrates their compatibility with feedback, supported by simple numerical illustrations, contributing to a scalable, compositional approach to verifying hybrid cyber-physical systems.

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.

Figures (4)

• Figure 1: Cascade and feedback compositions of hybrid systems.
• Figure 2: Graphical representation of $E_{1}$ and $E_{2}$ and their shared hybrid time domain $E_{12}$.
• Figure 3: An illustration of weak and strong satisfaction of an AG contract. Top: Weak satisfaction; Middle: Strong satisfaction with jump; Bottom: Strong satisfaction with flow. Continuous curves: flow mode; Circles: jump mode.
• Figure 4: Overview of Key Findings