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.

This manuscript is accepted for publication in the proceedings of the 8th Workshop on Design Automation for CPS and IoT (DESTION 2026)