Temporal Logic Resilience for Dynamical Systems

TL;DR

This work introduces a quantitative resilience metric for cyber-physical systems by embedding discrete-time dynamics within finite LTL$_F$ specifications. It develops exact, scalable methods for linear systems via LPs and LMIs and extends to nonlinear dynamics with linearization-based bounds and SMT-based approaches, including novel closed and convex LTL$_F$ specification fragments. The paper derives structural properties of resilience, provides exact-time reachability and finite-horizon safety/reachability computations, and offers scenario-optimization and SMT-based techniques for nonlinear cases, validated through case studies on temperature regulation, adaptive cruise control, and DC motors. The framework enables rigorous assessment of how large disturbances can be while preserving desired temporal behaviors, supporting robust design and verification of CPS under uncertainties.

Abstract

We consider the notion of resilience for cyber-physical systems, that is, the ability of the system to withstand adverse events while maintaining acceptable functionality. We use finite temporal logic to express the requirements on the acceptable functionality and define the resilience metric as the maximum disturbance under which the system satisfies the temporal requirements. We fix a parameterized template for the set of disturbances and form a robust optimization problem under the system dynamics and the temporal specifications to find the maximum value of the parameter. Additionally, we introduce two novel classes of specifications: closed and convex finite temporal logics specifications, offering a comprehensive analysis of the resilience metric within these specific frameworks. From a computational standpoint, we present an exact solution for linear systems and exact-time reachability and finite-horizon safety, complemented by an approximate solution for finite-horizon reachability. Extending our findings to nonlinear systems, we leverage linear approximations and SMT-based approaches to offer viable computational methodologies. The theoretical results are demonstrated on the temperature regulation of buildings, adaptive cruise control and DC motors.

Figures (3)

• Figure 1: Function $g_{\psi}(x)$ for Example \ref{['examp:1']}.
• Figure 2: Evolution of the temperatures in the nine rooms with a disturbance $\delta T_e=0$ (top) and with a disturbance $\delta T_e$ randomly chosen in the set $\Delta_{T_e}=[-3.12, 3.12] ^\circ C$ (bottom). The red boundaries represent the safe set $X_S$. The green region represents the set $X_{T_1}$. The black region represents the set $X_{T_2}$ and the blue region represents the set $X_{T_3}$.
• Figure 3: Evolution of $1000$ perturbed trajectory starting from the initial condition $x_0=(0.4,0.5)$. The green boundaries represent the target set $X_T$.

Theorems & Definitions (41)

• Definition 2.1
• Remark 1
• Definition 3.1
• Remark 2
• Proposition 3.1
• proof
• Example 3.1
• Definition 3.2: Closed specification
• Lemma 3.2
• proof