Logical Signal Processing: a Fourier Analysis of Temporal Logic

TL;DR

This paper explores the frequency characteristics of temporal logic formulas by modeling robustness monitors with Volterra series, enabling their analysis in the frequency domain for improved signal processing and monitoring.

Contribution

It introduces a novel Fourier analysis framework for temporal logic robustness monitors, bridging logic monitoring with signal processing techniques.

Findings

Robustness monitors can be modeled using Volterra series.

Fourier transforms of temporal logic formulas can be derived.

The approach enables integration of logic monitoring into signal processing workflows.

Abstract

What is the frequency content of temporal logic formulas? That is, when we monitor a signal against a formula, which frequency bands of the signal are relevant to the logic and should be preserved, and which can be safely discarded? This question is relevant whenever signals are filtered or compressed before being monitored, which is almost always the case for analog signals. To answer this question, we focus on monitors that measure the robustness of a signal relative to a specification in Signal Temporal Logic. We prove that robustness monitors can be modeled using Volterra series. We then study the Fourier transforms of these Volterra representations, and provide a method to derive the Fourier transforms of entire formulas. We also make explicit the measurement process in temporal logic and re-define it on the basis of distributions to make it compatible with measurements in signal processing. Experiments illustrate these results. Beyond compression, this work enables the integration of temporal logic monitoring into common signal processing toolchains as just another signal processing operation, and enables a common formalism to study both logical and non-logical operations in the frequency domain, which we refer to as Logical Signal Processing.