Monitoring Temporal Properties of Continuous Signals

Abstract. In this paper we introduce a variant of temporal logic tailored for specifying desired properties of continuous signals. The logic is based on a bounded subset of the real-time logic MITL, augmented with a static mapping from continuous domains into propositions. From formulae in this logic we create automatically property monitors that can check whether a given signal of bounded length and finite variability satisfies the property. A prototype implementation of this procedure was used to check properties of simulation traces generated by Matlab/Simulink.

• Type: Conference
• Year: 2004
• Where: FORMATS
• Authors: Oded Maler, Dejan Nickovic
• Keywords: FORMATS 2004, Logic, Real-time Logic Mitl, Temporal Logic