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

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.