Temporal logic as filtering

DOI10.1145/2883817.2883839MaRDI QIDQ2988956zbMATH OpenOpenAlexWikidataFDO

Authors Alena Rodionova, Ezio Bartocci, Dejan Ničković, Radu Grosu

Publication date 19 May 2017

Published in Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1510.08079

zbMATH Keywords

correspondenceLTI filteringmeasureMTLqualitative semanticsquantitative semanticstemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Signal theory (characterization, reconstruction, filtering, etc.) (94A12)

Abstract: We show that metric temporal logic can be viewed as linear time-invariant filtering, by interpreting addition, multiplication, and their neutral elements, over the (max,min,0,1) idempotent dioid. Moreover, by interpreting these operators over the field of reals (+,*,0,1), one can associate various quantitative semantics to a metric-temporal-logic formula, depending on the filter's kernel used: square, rounded-square, Gaussian, low-pass, band-pass, or high-pass. This remarkable connection between filtering and metric temporal logic allows us to freely navigate between the two, and to regard signal-feature detection as logical inference. To the best of our knowledge, this connection has not been established before. We prove that our qualitative, filtering semantics is identical to the classical MTL semantics. We also provide a quantitative semantics for MTL, which measures the normalized, maximum number of times a formula is satisfied within its associated kernel, by a given signal. We show that this semantics is sound, in the sense that, if its measure is 0, then the formula is not satisfied, and it is satisfied otherwise. We have implemented both of our semantics in Matlab, and illustrate their properties on various formulas and signals, by plotting their computed measures.

Recommendations

• A sampling approach to the analysis of metric temporal logic
• scientific article; zbMATH DE number 7056237
• Some Recent Results in Metric Temporal Logic
• A theory of sampling for continuous-time metric temporal logic
• Metric temporal logic with durations

Cited in

(7)

• Robust control for signal temporal logic specifications using discrete average space robustness
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Robust online monitoring of signal temporal logic
• On temporal logic and signal processing
• Introduction to the special issue on runtime verification
• From LTL to rLTL monitoring: improved monitorability through robust semantics
• A Multiresolution Analysis of Temporal Logic

Describes a project that uses

Uses Software

• Matlab

This page was built for publication: Temporal logic as filtering

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988956)