Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Model Predictive Online Monitoring of Dynamical Systems for Nested Signal Temporal Logic Specifications

Tao Han, Shaoyuan Li, Xiang Yin

TL;DR

This work tackles online monitoring of discrete-time dynamical systems against nested Signal Temporal Logic specifications by embedding STL progress into a syntax-tree structure and maintaining basic satisfaction vectors. It combines online updates with offline precomputation of feasible state sets to decide, at each step, whether a prefix is still feasible or already violated, yielding a sound and complete monitor. The approach extends model-predictive monitoring to general STL fragments with nested operators, validated through case studies on building temperature regulation and autonomous robot patrol tasks. By leveraging an explicit system model and offline reachability-like analysis, the method achieves accurate, real-time monitoring with bounded computational overhead for the online phase.

Abstract

This paper investigates the online monitoring problem for cyber-physical systems under signal temporal logic (STL) specifications. The objective is to design an online monitor that evaluates system correctness at runtime based on partial signal observations up to the current time so that alarms can be issued whenever the specification is violated or will inevitably be violated in the future. We consider a model-predictive setting where the system's dynamic model is available and can be leveraged to enhance monitoring accuracy. However, existing approaches are limited to a restricted class of STL formulae, permitting only a single application of temporal operators. This work addresses the challenge of nested temporal operators in the design of model-predictive monitors. Our method utilizes syntax tree structures to resolve dependencies between temporal operators and introduces the concept of basic satisfaction vectors. A new model-predictive monitoring algorithm is proposed by recursively updating these vectors online while incorporating pre-computed satisfaction regions derived from offline model analysis. We prove that the proposed approach is both sound and complete, ensuring no false alarms or missed alarms. Case studies are provided to demonstrate the effectiveness of our method.

Model Predictive Online Monitoring of Dynamical Systems for Nested Signal Temporal Logic Specifications

TL;DR

This work tackles online monitoring of discrete-time dynamical systems against nested Signal Temporal Logic specifications by embedding STL progress into a syntax-tree structure and maintaining basic satisfaction vectors. It combines online updates with offline precomputation of feasible state sets to decide, at each step, whether a prefix is still feasible or already violated, yielding a sound and complete monitor. The approach extends model-predictive monitoring to general STL fragments with nested operators, validated through case studies on building temperature regulation and autonomous robot patrol tasks. By leveraging an explicit system model and offline reachability-like analysis, the method achieves accurate, real-time monitoring with bounded computational overhead for the online phase.

Abstract

This paper investigates the online monitoring problem for cyber-physical systems under signal temporal logic (STL) specifications. The objective is to design an online monitor that evaluates system correctness at runtime based on partial signal observations up to the current time so that alarms can be issued whenever the specification is violated or will inevitably be violated in the future. We consider a model-predictive setting where the system's dynamic model is available and can be leveraged to enhance monitoring accuracy. However, existing approaches are limited to a restricted class of STL formulae, permitting only a single application of temporal operators. This work addresses the challenge of nested temporal operators in the design of model-predictive monitors. Our method utilizes syntax tree structures to resolve dependencies between temporal operators and introduces the concept of basic satisfaction vectors. A new model-predictive monitoring algorithm is proposed by recursively updating these vectors online while incorporating pre-computed satisfaction regions derived from offline model analysis. We prove that the proposed approach is both sound and complete, ensuring no false alarms or missed alarms. Case studies are provided to demonstrate the effectiveness of our method.

Paper Structure

This paper contains 18 sections, 4 theorems, 33 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminary
  3. System Model
  4. Signal Temporal Logic
  5. Problem Formulation
  6. Fragment of STL Formulae
  7. Online Monitoring of STL
  8. Tree of Nested STL Formulae
  9. Syntax Trees for STL formulae
  10. Satisfaction Vector
  11. Online Monitoring Algorithms
  12. Evolution of Basic Vectors
  13. Model-Predictive Monitor
  14. Offline Computation of Feasible Sets
  15. Case Studies for Online Monitoring
  16. ...and 3 more sections

Key Result

Proposition 1

Let $I$ be a basic set and $k$ be a time instant. For any two sequences $\mathbf{x}_{0:k-1}',\mathbf{x}_{0:k-1}"\in \mathbf{x}_{0:k-1}^I$ consistent with $I$, and any future sequence $\mathbf{x}_{k:T}=x_{k}x_{k+1}\cdots x_T$, we have

Figures (3)

  • Figure 1: Syntax Tree of STL formula \ref{['example']}
  • Figure 2: Two trajectories temperature control system.
  • Figure 3: Two trajectories that violate at different instants.

Theorems & Definitions (16)

  • Definition 1: Syntax Trees
  • Definition 2: Evaluation Horizons
  • Definition 3: Satisfaction Vectors
  • Definition 4: Basic Vectors
  • Definition 5: Induced Vectors
  • Proposition 1
  • proof
  • Proposition 2
  • Definition 6: $I$-Determined Feasible Sets
  • Theorem 1
  • ...and 6 more