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

TL;DR

This paper presents a novel online monitoring approach for cyber-physical systems with nested STL specifications, leveraging model predictive techniques and syntax tree structures to improve accuracy and handle complex temporal operators.

Contribution

It introduces a new model-predictive monitoring algorithm capable of handling nested temporal operators in STL specifications, addressing limitations of previous methods.

Findings

The proposed method is sound and complete, avoiding false and missed alarms.

Case studies demonstrate improved monitoring accuracy for complex STL formulas.

The approach efficiently updates satisfaction vectors online using offline pre-computation.

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.