Learning What to Monitor: Using Machine Learning to Improve past STL Monitoring

Monitoring is a runtime verification technique that can be used to check whether an execution of a system (trace) satisfies or not a given set of properties. Compared to other formal verification techniques, eg, model checking, one needs to specify the properties to be monitored, but a complete model of the system is no longer necessary. First, we introduce the pure past fragment of Signal Temporal Logic (ppSTL), and we use it to define the monitorable safety (G (ppSTL)) and cosafety (F (ppSTL)) fragments of STL, which properly extend the commonly-used bounded-future fragment. Then, we devise a multi-objective genetic programming algorithm to automatically extend the set of properties to monitor on the basis of the history of failure traces collected over time. The framework resulting from the integration of the monitor and the learning algorithm is then experimentally validated on various public datasets. The outcomes of the experimentation confirm the effectiveness of the proposed solution.