Model Predictive Monitoring of Dynamical Systems for Signal Temporal Logic Specifications

TL;DR

This paper introduces a model predictive monitoring approach for dynamical systems that evaluates Signal Temporal Logic specifications by leveraging system models to predict future states, enabling earlier falsification or certification.

Contribution

It proposes a novel online monitoring method that uses known system models to improve prediction accuracy and early detection of specification satisfaction or violation.

Findings

The approach can falsify or certify specifications earlier than existing methods.

Effective computation of feasible sets for STL formulae is demonstrated.

Real-world case studies validate the method's effectiveness.

Abstract

Online monitoring aims to evaluate or to predict, at runtime, whether or not the behaviors of a system satisfy some desired specification. It plays a key role in safety-critical cyber-physical systems. In this work, we propose a new monitoring approach, called model predictive monitoring, for specifications described by Signal Temporal Logic (STL) formulae. Specifically, we assume that the observed state traces are generated by an underlying dynamical system whose model is known but the control law is unknown. The main idea is to use the dynamic of the system to predict future states when evaluating the satisfaction of the STL formulae. To this end, effective approaches for the computation of feasible sets of STL formulae are provided. We show that, by explicitly utilizing the model information of the dynamical system, the proposed online monitoring algorithm can falsify or certify of the specification in advance compared with existing algorithms, where no model information is used. We also demonstrate the proposed monitoring algorithm by several real world case studies.