Monitoring Temporal Properties of Continuous Signals

Monitoring Temporal Properties of Continuous Signals

| Oded Maler and Dejan Nickovic
This paper introduces a variant of temporal logic tailored for specifying properties of continuous signals, specifically dense-time real-valued signals. The logic, called MITL$_{[a,b]}$, is based on a bounded subset of real-time logic MTL, augmented with a static mapping from continuous domains into propositions. The authors propose an automatic method to generate property monitors that can check whether a given signal of bounded length and finite variability satisfies the specified property. The paper includes a prototype implementation that has been used to check properties of simulation traces generated by Matlab/Simulink. The main contributions include the definition of the logic, the construction of property monitors, and the demonstration of the method's effectiveness through examples. The authors also discuss related work and future directions, including online monitoring, extending the logic with events, and integrating with simulators.This paper introduces a variant of temporal logic tailored for specifying properties of continuous signals, specifically dense-time real-valued signals. The logic, called MITL$_{[a,b]}$, is based on a bounded subset of real-time logic MTL, augmented with a static mapping from continuous domains into propositions. The authors propose an automatic method to generate property monitors that can check whether a given signal of bounded length and finite variability satisfies the specified property. The paper includes a prototype implementation that has been used to check properties of simulation traces generated by Matlab/Simulink. The main contributions include the definition of the logic, the construction of property monitors, and the demonstration of the method's effectiveness through examples. The authors also discuss related work and future directions, including online monitoring, extending the logic with events, and integrating with simulators.
Reach us at info@study.space
[slides and audio] Monitoring Temporal Properties of Continuous Signals