Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fully Automated Verification of Linear Time-Invariant Systems against Signal Temporal Logic Specifications via Reachability Analysis

Niklas Kochdumper, Stanley Bak

TL;DR

The paper addresses the challenge of formally verifying linear time-invariant systems against signal temporal logic specifications when initial states and inputs are uncertain. It introduces a fully automated verifier that refines reachability parameters and employs dependency-preserving reachability combined with model checking in a factor-space representation to avoid RTL conservatism and spurious traces. The method guarantees finite-time convergence for decidable instances, returns falsifying trajectories when violations exist, and scales to high-dimensional systems with complex STL formulas. This framework enables robust verification and set-based prediction in engineering domains such as mobile robotics and traffic planning, reducing manual tuning and enabling automated safety guarantees. The results demonstrate substantial speedups over SMT-based approaches and effective handling of benchmarks with up to 1000 states.

Abstract

While reachability analysis is one of the most promising approaches for formal verification of dynamic systems, a major disadvantage preventing a more widespread application is the requirement to manually tune algorithm parameters such as the time step size. Manual tuning is especially problematic if one aims to verify that the system satisfies complicated specifications described by signal temporal logic formulas since the effect the tightness of the reachable set has on the satisfaction of the specification is often non-trivial to see for humans. We address this problem with a fully-automated verifier for linear systems, which automatically refines all parameters for reachability analysis until it can either prove or disprove that the system satisfies a signal temporal logic formula for all initial states and all uncertain inputs. Our verifier combines reachset temporal logic with dependency preservation to obtain a model checking approach whose over-approximation error converges to zero for adequately tuned parameters. While we in this work focus on linear systems for simplicity, the general concept we present can equivalently be applied for nonlinear and hybrid systems.

Fully Automated Verification of Linear Time-Invariant Systems against Signal Temporal Logic Specifications via Reachability Analysis

TL;DR

The paper addresses the challenge of formally verifying linear time-invariant systems against signal temporal logic specifications when initial states and inputs are uncertain. It introduces a fully automated verifier that refines reachability parameters and employs dependency-preserving reachability combined with model checking in a factor-space representation to avoid RTL conservatism and spurious traces. The method guarantees finite-time convergence for decidable instances, returns falsifying trajectories when violations exist, and scales to high-dimensional systems with complex STL formulas. This framework enables robust verification and set-based prediction in engineering domains such as mobile robotics and traffic planning, reducing manual tuning and enabling automated safety guarantees. The results demonstrate substantial speedups over SMT-based approaches and effective handling of benchmarks with up to 1000 states.

Abstract

While reachability analysis is one of the most promising approaches for formal verification of dynamic systems, a major disadvantage preventing a more widespread application is the requirement to manually tune algorithm parameters such as the time step size. Manual tuning is especially problematic if one aims to verify that the system satisfies complicated specifications described by signal temporal logic formulas since the effect the tightness of the reachable set has on the satisfaction of the specification is often non-trivial to see for humans. We address this problem with a fully-automated verifier for linear systems, which automatically refines all parameters for reachability analysis until it can either prove or disprove that the system satisfies a signal temporal logic formula for all initial states and all uncertain inputs. Our verifier combines reachset temporal logic with dependency preservation to obtain a model checking approach whose over-approximation error converges to zero for adequately tuned parameters. While we in this work focus on linear systems for simplicity, the general concept we present can equivalently be applied for nonlinear and hybrid systems.
Paper Structure (20 sections, 6 theorems, 58 equations, 6 figures, 1 table, 3 algorithms)

This paper contains 20 sections, 6 theorems, 58 equations, 6 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. State of the Art
  3. Contribution
  4. Overview
  5. Preliminaries
  6. Notation
  7. Set Representations and Operations
  8. Reachability Analysis
  9. Temporal Logic
  10. Problem Formulation
  11. Reachability Analysis
  12. Model Checking
  13. Automated Verification
  14. Numerical Examples
  15. Comparison with Other Approaches
  16. ...and 5 more sections

Key Result

Proposition 1

We consider the initial set $\mathcal{X}_0 = \langle c_x,G_x \rangle_Z \subset \mathbb{R}^n$ with $\gamma_x$ generators, the input set $\mathcal{U} = \langle c_u,G_u \rangle_Z \subset \mathbb{R}^m$ with $\gamma_u$ generators, and the corresponding enclosure of the reachable set $\mathcal{R}(t)$ comp with $j = 1,\dots,t_{\text{\normalfont end}}/\Delta t$, the approximate solution $\mu(t,x_0,u(\cdot

Figures (6)

  • Figure 1: Exemplary verification problem, where the initial set is shown in white with a black border, the reachable set is depicted in gray, the unsafe sets defined by the STL formula $\varphi$ are visualized in red, and exemplary trajectories of the system are shown in black. Even though the system satisfies the temporal logic formula $\varphi$, the reachset temporal logic approach Roehm2016b classifies the system as unsafe since it checks if the whole reachable set satisfies the predicates $x_2 < 0.5$ and $x_2 > -0.5$. This procedure produces so-called spurious traces (orange), which are not consistent with the system dynamics.
  • Figure 2: Schematic visualization of the model checking approach presented in Sec. \ref{['sec:modelChecking']}, where the reachable sets $\widetilde{\mathcal{R}}(j \, \Delta t/2)$ are visualized in blue and the polytopes $\mathcal{P}_{hjkl}$ as well as the corresponding sets of unsafe factors $\mathcal{K}$ are depicted in red. Moreover, the green arrows represent the mapping from the state space to the space of zonotope factors $\widetilde{\alpha} \in [-\mathbf{1},\mathbf{1}]$.
  • Figure 3: Reachable set for the mobile robot, where the initial set is shown in white with a black border and the sets $\mathcal{S}_1$, $\mathcal{S}_2$, $\mathcal{S}_3$ are visualized in green and red.
  • Figure 4: Reachable set (left) and falsifying trajectory (right) for the safe and the unsafe specification of the HEAT02 benchmark, where the dashed red line visualizes the boundary of the safe region and the dashed blue lines mark the points in time relevant for the temporal logic specification.
  • Figure 5: Computation time for our automated verifier on the ARCH benchmarks from Tab. \ref{['tab:ARCH']} partitioned into the time required for reachablity analysis (see Alg. \ref{['alg:reach']}), for verification (see Line \ref{['line:safeStart']}-\ref{['line:safeEnd']} of Alg. \ref{['alg:verify']}), and for falsification (see Line \ref{['line:unsafe1']}-\ref{['line:unsafe2']} of Alg. \ref{['alg:verify']}).
  • ...and 1 more figures

Theorems & Definitions (18)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • ...and 8 more