Online Monitoring of Dynamic Systems for Signal Temporal Logic Specifications with Model Information

TL;DR

This paper introduces a model-based online monitoring approach for dynamic systems with known models, enabling earlier detection of STL specification satisfaction or violation during runtime.

Contribution

It presents a novel model-aware online monitoring algorithm for STL specifications that improves detection speed over existing model-free methods.

Findings

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

Effective computation of feasible sets for STL formulae is achieved.

Case studies demonstrate the practical effectiveness of the method.

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 model-based approach for online monitoring for specifications described by Signal Temporal Logic (STL) formulae. Specifically, we assume that the observed state traces are generated by an underlying dynamic system whose model is known. The main idea is to consider the dynamic of the system when evaluating the satisfaction of the STL formulae. To this end, effective approaches for the computation of feasible sets for STL formulae are provided. We show that, by explicitly utilizing the model information of the dynamic 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 case studies.