PaperlayerView exact revision on arXiv

Source-linked AI summary

Logical Signal Processing: a Fourier Analysis of Temporal Logic

Niraj Basnet, Houssam Abbas

arXiv:2009.08090v1eess.SYcs.SY

TL;DR

Because measurement, filtering, and compression can affect temporal-logic monitor verdicts, the paper develops a Fourier-domain analysis of robustness monitors using Volterra series. Its frequency responses identify relevant signal bands, and the paper reformulates measurement to account for finite bandwidth. In an example, filtering above a derived cutoff leaves robustness outputs almost unchanged.

  • Problem

    The paper addresses the lack of a systematic Fourier representation for temporal-logic monitoring, needed to analyze how measurement, filtering, and compression affect monitor verdicts.

    Source: §1 · p. 1

  • Method

    The authors model robustness monitors with Volterra series, derive generalized frequency responses for formulas, and redefine atomic propositions using distributions to represent finite-bandwidth measurements.

    Source: §1 · p. 2, §4 · p. 8, §4.2 · p. 11

  • Results

    3π rad/s: for “Once p,” the GFRFs are negligible above this cutoff, and filtering there leaves the original and compressed signals’ robustness outputs almost indistinguishable.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The frequency analysis can guide monitoring-safe filtering and compression and treat temporal-logic monitors as operations in signal-processing chains.

    Source: §1 · p. 2, §6 · p. 15

    The analysis retains a compact-support requirement for signals; relaxing it is identified as future work.

    Source: §6 · p. 15

Abstract

from arXiv · show

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.

1 Introduction: The Place of Runtime Verification in the Signal Processing Chain

The paper asks how measurement and signal-processing operations affect temporal-logic monitor verdicts, and develops a Fourier-domain account of robustness monitoring to identify relevant signal frequencies. It also reformulates temporal-logic measurement to reflect finite-bandwidth physical measurements.

1 Introduction: The Place of Runtime Verification in the Signal Processing Chain

  • The work addresses the lack of a systematic frequency-domain account for assessing how filtering and compression affect runtime-monitor verdicts.The introduction contrasts this gap with time-domain analyses relying on ad hoc assumptions such as Lipschitz constants.Source: §1 · p. 1
  • Volterra series provide generalized Fourier representations for nonlinear robustness monitors, enabling analysis of which input frequencies contribute to their outputs.The paper derives responses for complete formulas by composing the representations of logical operations.Source: §1 · pp. 1, 3
  • Because instantaneous measurements require infinite bandwidth, the paper redefines atomic propositions using distributions and demonstrates sound robust semantics that still yield robustness tubes for falsification.The reformulation makes the measurement model compatible with finite-resolution measurements of analog signals.Source: §1 · pp. 1–3
  • 3π rad/s: for “Once p,” the GFRFs are negligible above this cutoff, and filtering there leaves robustness signals almost indistinguishable despite marked input differences.The example supports suppressing frequencies above the cutoff before transmission while preserving monitoring robustness.Source: §1 · p. 2, Figure 2 · p. 2
  • Unlike Time-Frequency Logic, which specifies spectral properties, this approach starts from standard STL formulas and analyzes which signal frequencies affect their verdicts.The authors state that their methods can also extract hidden frequency aspects of TFL formulas.Source: §1 · p. 3

2 Preliminaries: Signal Temporal Logic and Volterra Series

The section introduces past-time STL robustness as an operator on signals, then develops Fourier and Volterra tools for analyzing how input frequencies contribute to monitor outputs.

2.1 Signal Temporal Logic (STL)

  • Past-bounded STL uses compact time intervals and past operators, with Boolean semantics defined for disjunction, temporal operators, and Since.The section also treats Once and Historically as base operations for its analysis.Source: §2.1 · p. 4

2.2 Robust Semantics

  • Robustness maps an input signal to a real-valued robustness signal, and its sign indicates satisfaction or violation while its magnitude supports a robustness margin.A signal perturbation smaller than the robustness value preserves the satisfaction status.Source: §2.2 · p. 4

2.3 Fourier Analysis

  • Fourier analysis decomposes signals by frequency, and for linear time-invariant systems converts convolution into multiplication of Fourier transforms.This supports filter design to pass or block selected frequency components.Source: §2.3 · p. 5

2.4 Volterra Series Approximation of Non-Linear Operators

  • A Volterra series extends convolution to nonlinear time-invariant operators; its kernels’ Fourier transforms, the GFRFs, describe output spectra through products of input spectra.The series approximation is used because robustness operators are nonlinear and GFRFs enable analysis of their output spectra.Source: §2.4 · pp. 5–6
  • A frequency with sufficiently small GFRF contributions across the relevant kernel arguments contributes little to robustness and can be discarded.The paper’s criterion checks the frequency across each argument position of the GFRFs against a user-set threshold.Source: §2.4 · p. 6
  • Volterra approximation applies to time-invariant operators with fading memory; the stated theorem guarantees a finite-series approximation on a bounded, smooth input class.For inputs in K_M1,M2, the approximation error can be made less than ε.Source: §2.4 · p. 6

2.5 Measurement Devices and the spaces D(E) and D′

  • The paper models measurement with a smooth compactly supported kernel, producing a signal through an inner product that acts as a filtered, weighted measurement.The kernel’s width determines measurement resolution: narrower kernels provide higher resolution.Source: §2.5 · p. 6

1. Note that Dirac’s δ is not in D′

The passage states that narrow integrable functions can provide arbitrarily close approximations.

1. Note that Dirac’s δ is not in D′

  • Narrow integrable functions can provide arbitrarily close approximations.The passage fragment does not identify the object being approximated.Source: §1 · p. 6

3 Bounded-Bandwidth STL

Instantaneous measurements are physically unrealizable and make frequency analysis uninformative; BB-STL replaces punctual atomic measurements while preserving the logic’s robust semantics.

3 Bounded-Bandwidth STL

  • Instantaneous measurement is physically impossible because it requires the unrealizable Dirac delta, whose infinite bandwidth would make every frequency band relevant.The paper notes that this would yield a trivial and useless frequency analysis.Source: §3 · p. 7
  • BB-STL removes punctual measurements by changing atomic propositions, while retaining the other STLpast syntax and its Boolean semantics.Its atomic propositions correspond to filters rather than instantaneous signal values.Source: §3 · p. 7
  • BB-STL preserves the logical relations and soundness of robust semantics while replacing instantaneous measurements.Source: §3 · p. 7

Its robust semantics are identical to those of STLpast

The section establishes soundness for BB-STL robust semantics and describes the conditions and measurement choices underlying that result.

Its robust semantics are identical to those of STLpast

4 Volterra Approximations and Frequency Response of BB-STL Formulas

The section establishes finite Volterra-series approximability for BB-STL robustness operators, then uses approximations of basic operators and a composition theorem to derive frequency responses for whole formulas. The general strategy does not yet provide a practical generic approximation for formulas using Since.

4.1 Approximability by Volterra Series

  • Every BB-STL formula that does not explicitly include ⊤ has a robustness operator that can be approximated by a finite Volterra series.The paper often refers directly to the Volterra kernels of the formula, although strictly they belong to the series approximating its robustness operator.Source: §4.1 · pp. 9–10
  • The proof establishes time invariance and fading memory, then applies a Volterra approximation result by decomposing the signal domain into bounded classes.The argument assumes the formula does not explicitly include ⊤.Source: §4.1 · pp. 9–10

4 Volterra Approximations and Frequency Response of BB-STL Formulas

  • To derive a formula’s frequency response, the method approximates basic operators and composes their generalized frequency response functions (GFRFs).The section excludes Since because the authors lack tools to compute its approximation, despite its approximability.Source: §4 · p. 8, §4.2 · p. 11

4.2 Calculating the Volterra Approximations and their GFRFs

  • Basic operators are approximated on representative signals by delayed inputs followed by a read-out polynomial, a structure represented exactly by Volterra series.The numerical procedure is presented as a practical, simple option; the first two operators can be represented exactly as Volterra series.Source: §4.2 · p. 11
  • For the pointwise min of two signals, separate polynomial approximations avoid cross-products that would lose the Volterra kernels’ convenient GFRF representation.The polynomials are fitted by least squares and use only each signal’s present value.Source: §4.2 · p. 12
  • A composition theorem combines the GFRFs of component operators to calculate the GFRF of a whole formula.The section illustrates this by deriving the GFRF for an interval-temporal operator applied to an atomic proposition.Source: §4.2 · p. 12

4.3 Why is Approximating φ1 SI φ2 Different?

  • For Since, the needed component operators change signal dimensions, and available approximation tools do not handle all of them.A formula-specific fit is possible, but changing atoms or formula structure requires a new fit and does not yield a generic composable approximation.Source: §4.3 · pp. 12–13

5 Experiments: Fourier Analysis of Temporal Logic

The experiments use Volterra approximations to examine how temporal intervals and atomic-proposition measurements shape formula spectra, and how frequency-aware compression affects monitoring.

5 Experiments: Fourier Analysis of Temporal Logic

  • The experiments approximate GFRFs with degree-4 polynomials on random combinations of sinusoids, with approximation error on the order of 10^-12.The authors state that efficiency and generality of the approximation scheme are left for future work.Source: §5 · p. 13

5.1 GFRFs of BB-STL formulas

  • Increasing T2 spreads H1 energy more uniformly over 0–2.5 Hz and suppresses high frequencies less, while H2’s increase is less marked when both frequencies are high.The spectra shown are for Historically[1,T2] p with g = G(0, 0.04).Source: §5.1 · p. 13, Figure 3 · p. 14
  • As T increases for [0,T] p, H1 becomes more low-pass while H2 becomes more high-pass.This contrast motivates examining response orders beyond the first-order spectrum.Source: §5.1 · p. 13, Figure 3 · p. 14
  • Increasing the Gaussian measurement width s makes the formula more low-pass, so high-frequency noise is ignored by the formula and does not affect its verdict.The experiments also show second-order spectra for increasing s, without stating a corresponding trend.Source: §5.1 · p. 13, Figure 4 · p. 15
  • For a composite formula, the block diagram tracks how the overall first-order spectrum changes as monitoring components are added.The formula’s sub-monitor responses and their interactions or cancellations are not apparent from the formula alone.Source: §5.1 · pp. 13–14

5.2 Compression’s effect on monitoring

  • Monitoring-safe compression keeps monitoring results almost identical even when the compressed signal differs markedly from the original.By contrast, low-pass filtering without regard to the formula significantly changes robustness and can change the truth value.Source: §5.2 · p. 15

6 Conclusions

The paper presents Fourier analysis of temporal logic using Volterra approximations and bounded-bandwidth atomic propositions. It identifies constraints for future work and the prospect of monitoring-safe filter design.

6 Conclusions

  • The paper presents Fourier analysis of temporal logic using Volterra approximations of robustness operators and redefines atomic propositions with bounded-bandwidth filters.This enables temporal logic monitors to be incorporated into signal-processing chains as signal-processing boxes.Source: §6 · p. 15
  • The current analysis constrains the signal space, and removing its compact-support requirement remains a conjecture.Future work also seeks more general operator approximations and an extension to Since.Source: §6 · p. 15
  • The figure indicates a safe cutoff near 1.5 Hz, while a 0.5 Hz upstream low-pass filter significantly changes robustness and truth values.The figure illustrates that filtering without accounting for the downstream monitor can produce incorrect monitoring results.Source: Figure 6 · p. 16
  • A monitoring-safe optimal filter would preserve signal content relevant to the output robustness signal.The paper identifies this as a direction for future work.Source: §6 · p. 16
Loading 2009.08090v1…