Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Vertical Contracts for Safety Control

Armin Pirastehzad, Bart Besselink

Abstract

We propose a methodology that exploits the contract formalism to characterize the continuous-time safety control problem, which is often difficult to address, in terms of a discrete-time one, for which numerous efficient solution scheme exist. We construct contracts as pairs of assumptions and guarantees which are set-valued mappings that describe the safe boundaries within which the system must operate. By formalizing safety control as contract implementation, we develop a vertical hierarchy according to which we translate implementation from continuous to discrete time. We accomplish this by constructing a discrete-time system and a contract such that a solution to the continuous-time implementation problem can be characterized in terms of a solution to its discrete-time counterpart. We then use this characterization to construct a control input that establishes implementation in continuous time on the basis of the control sequence that achieves implementation in discrete time.

Vertical Contracts for Safety Control

Abstract

We propose a methodology that exploits the contract formalism to characterize the continuous-time safety control problem, which is often difficult to address, in terms of a discrete-time one, for which numerous efficient solution scheme exist. We construct contracts as pairs of assumptions and guarantees which are set-valued mappings that describe the safe boundaries within which the system must operate. By formalizing safety control as contract implementation, we develop a vertical hierarchy according to which we translate implementation from continuous to discrete time. We accomplish this by constructing a discrete-time system and a contract such that a solution to the continuous-time implementation problem can be characterized in terms of a solution to its discrete-time counterpart. We then use this characterization to construct a control input that establishes implementation in continuous time on the basis of the control sequence that achieves implementation in discrete time.

Paper Structure

This paper contains 11 sections, 5 theorems, 39 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Safety Contracts
  3. Vertical Contract implementation
  4. Discretization
  5. Contract Discretization
  6. System Discretization
  7. From Continuous-Time to Discrete-Time Implementation
  8. Numerical Example
  9. Conclusion
  10. Technical Lemma
  11. Proof of Theorem \ref{['Th_Implication']}

Key Result

Proposition 1

For a sampling time $\tau>0$ and an integer $N\geq 1$, $\bm{\Sigma}_c$ is an $N$-th order interpolator of $\bm{\Sigma}_d$ with respect to the sampling time $\tau$ if and only if

Figures (1)

  • Figure 1: The continuous-time control input obtained as in \ref{['MidU']} satisfies the assumptions $\mathcal{A}_c$ and enforces the robot to operate in accordance with the guarantees $\mathcal{G}_c$.

Theorems & Definitions (11)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Proposition 1
  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Remark 1
  • Lemma 1
  • ...and 1 more