Trajectory-based Safety of Monotone Systems: Verification and Control Synthesis

TL;DR

This paper introduces a data-driven method for verifying safety and synthesizing safe controls for unknown monotone systems, using dominance functions derived from trajectory data to provide formal guarantees.

Contribution

It develops a new framework leveraging system monotonicity to reduce data needs and construct safety certificates directly from trajectories.

Findings

Successfully derived safety certificates from few trajectories

Validated approach on two monotone systems

Ensured formal safety guarantees with limited data

Abstract

This paper presents a novel data-driven framework for the robust safety verification and safe control synthesis of unknown monotone discrete-time systems. While existing data-driven safety analysis approaches are often either heuristic in nature or require large amounts of data to provide rigorous guarantees, we leverage the structural property of monotonicity to significantly reduce data requirements while still ensuring formal safety guarantees. Our approach is built upon a new class of certificates called dominance functions, constructed directly from collected system trajectories, which themselves need not be safe. By exploiting the monotone structure of the dynamics, we show that dominance functions are (i) dissipative, meaning that they decrease monotonically along system trajectories, and (ii) sufficiently \expressive to characterize safety certificates for monotone systems. Together, these properties establish dominance functions as principled building blocks for the systematic construction of formal safety certificates directly from trajectory data. For both robust safety verification and safe control synthesis, we develop an efficient sampling-based optimization framework that searches for safety certificates represented as linear combinations of dominance functions constructed from collected trajectories. We validate our data-driven framework on two monotone systems by successfully deriving safety certificates from a small number of trajectories.