Online Monitoring of Spatio-Temporal Properties for Imprecise Signals

Monitoring the behavior of dynamical systems often requires reasoning about interconnected entities arranging in the spatial environment and evolving over time. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and reason about spatio-temporal properties. STREL considers each system’s entity as a node of a dynamic weighted graph representing its spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterizing the node’s behavior. While algorithms already existed for monitoring STREL specifications offline, over pre-recorded traces, we are widening the boundaries of applicability of this formal technique by extending the methodology to solve a plethora of real-world challenges, spanning from monitoring out-of-order imprecise samples, to providing partial guarantees, and to defining new operators to increase its expressivity. The co-authors of this research are Ezio Bartocci, Michele Loreti, Laura Nenzi, who contributed to a previous publication to the International Conference on Formal Methods and Models for System Design (MEMOCODE '21), and who are actively working on future developments.

Authors

• Ennio Visconti

Keywords

No keywords are indexed for this paper.