Time-Robust Control for STL Specifications

TL;DR

This paper introduces a control framework that optimizes the time robustness of STL specifications in real-time systems, ensuring safety despite timing uncertainties through a MILP encoding.

Contribution

It formulates a control problem maximizing STL time robustness and provides a MILP encoding with correctness guarantees and complexity analysis.

Findings

Maximizing STL time robustness improves system safety under timing uncertainties.

The MILP encoding effectively solves the control problem with formal correctness guarantees.

Case studies demonstrate practical benefits of the proposed approach.

Abstract

We present a robust control framework for time-critical systems in which satisfying real-time constraints robustly is of utmost importance for the safety of the system. Signal Temporal Logic (STL) provides a formal means to express a large variety of real-time constraints over signals and is suited for planning and control purposes as it allows us to reason about the time robustness of such constraints. The time robustness of STL particularly quantifies the extent to which timing uncertainties can be tolerated without violating real-time specifications. In this paper, we first pose a control problem in which we aim to find an optimal input sequence to a control system that maximizes the time robustness of an STL constraint. We then propose a Mixed Integer Linear Program (MILP) encoding and provide correctness guarantees along with a complexity analysis of the encoding. We also show in two case studies that maximizing STL time robustness allows to account for timing uncertainties of the underlying control system.