Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A contract negotiation scheme for safety verification of interconnected systems

Xiao Tan, Antonis Papachristodoulou, Dimos V. Dimarogonas

TL;DR

This paper proposes a (control) barrier function synthesis and safety verification scheme for interconnected nonlinear systems based on assume-guarantee contracts (AGC) and sum-of-squares techniques and shows that compositional methods like AGC can mitigate this problem.

Abstract

This paper proposes a (control) barrier function synthesis and safety verification scheme for interconnected nonlinear systems based on assume-guarantee contracts (AGC) and sum-of-squares (SOS) techniques. It is well-known that the SOS approach does not scale well for barrier function synthesis for high-dimensional systems. In this paper, we show that compositional methods like AGC can mitigate this problem. We formulate the synthesis problem into a set of small-size problems, which constructs local contracts for subsystems, and propose a negotiation scheme among the subsystems at the contract level. The proposed scheme is then implemented numerically on two examples: vehicle platooning and room temperature regulation.

A contract negotiation scheme for safety verification of interconnected systems

TL;DR

This paper proposes a (control) barrier function synthesis and safety verification scheme for interconnected nonlinear systems based on assume-guarantee contracts (AGC) and sum-of-squares techniques and shows that compositional methods like AGC can mitigate this problem.

Abstract

This paper proposes a (control) barrier function synthesis and safety verification scheme for interconnected nonlinear systems based on assume-guarantee contracts (AGC) and sum-of-squares (SOS) techniques. It is well-known that the SOS approach does not scale well for barrier function synthesis for high-dimensional systems. In this paper, we show that compositional methods like AGC can mitigate this problem. We formulate the synthesis problem into a set of small-size problems, which constructs local contracts for subsystems, and propose a negotiation scheme among the subsystems at the contract level. The proposed scheme is then implemented numerically on two examples: vehicle platooning and room temperature regulation.
Paper Structure (19 sections, 8 theorems, 21 equations, 4 figures, 5 algorithms)

This paper contains 19 sections, 8 theorems, 21 equations, 4 figures, 5 algorithms.

Table of Contents

  1. Introduction
  2. Notation and Preliminaries
  3. Systems and Interconnections
  4. Assume-guarantee contracts for invariance
  5. System safety and barrier functions
  6. Sum-of-squares programs
  7. Problem formulation
  8. Proposed solutions
  9. Local barrier function and AGC construction
  10. Maximal internal input set
  11. Minimal safe region
  12. Contract composition and negotiation
  13. Acyclic connectivity graph
  14. Homogeneous interconnected system
  15. General case
  16. ...and 4 more sections

Key Result

Lemma 1

Consider an interconnected system $\langle (G_i)_{i\in \mathcal{I}}, \mathcal{E}\rangle = (U,\{0\}, X, Y, X^0, \mathcal{T})$ composed of $N$ subsystems with a compatible binary connectivity relation $\mathcal{E}$. If for each subsystem $G_i = ( U_i, W_i, X_i, Y_i, X_i^0, \mathcal{T}_i)$, there exist

Figures (4)

  • Figure 1: Platooning scenario
  • Figure 2: Results for the platooning example.
  • Figure 3: Room temperature scenario.
  • Figure 4: Assume/guarantee sets for the room temperature example. Left: iteration 1, right: iteration 2.

Theorems & Definitions (21)

  • Definition 1: Continuous-time system
  • Definition 2
  • Definition 3
  • Lemma 1: Compositional reasoning
  • Definition 4
  • Definition 5
  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • ...and 11 more