On the Time and Frequency Domain Representations of Signals for CPS Specification

1 INTRODUCTION

• Time-domain languages such as STL constrain values over time, making signal shapes and dynamic relations harder to specify without assumptions tied to particular signal realizations.Frequency representations describe shape-related features, while time-frequency representations retain their temporal locations.Source: §1 · pp. 2–3
• CPS specification languages offer limited support for reasoning about signal shape; TFL is the identified exception, but remains largely time-oriented and has seen little CPS application.The paper frames which requirements benefit from time-frequency representations, what language constructs they need, and whether they provide practical assessment advantages as open questions.Source: §1 · p. 3
• Signal-feature and step-response requirements can be reformulated as frequency-domain properties, motivating desiderata for predicates over frequency intervals and relations between components.The authors analyse existing taxonomies of signal-based CPS requirements to identify classes that benefit from time-frequency representations.Source: §1 · p. 3
• S2TL supports predicates over frequency intervals and logical relations between frequency components of multiple signals, addressing limitations in TFL.The paper operationalises S2TL semantics and implements a discrete-time offline monitor as an extension of RTAMT.Source: §1 · p. 3
• The evaluation compares S2TL and STL templates on drone and aircraft traces, including realistic CPS traces and synthetic traces with known requirement satisfaction.It examines applicability, expression fidelity, and monitoring noise tolerance.Source: §1 · pp. 3–4
• Time-frequency specifications also apply to linearly interpolated traces, match time-domain fidelity where both apply, and better tolerate offset and high-frequency noise while matching white-noise tolerance.Time-domain specifications apply only to traces with step-like input changes or constant interpolation; the comparison assesses applicability, expression fidelity, and noise tolerance.Source: §1 · p. 4

2.1 Signal-Based CPS Requirements

• Automotive and aerospace taxonomies identify similar signal-based CPS requirement classes, which the paper harmonizes in Table 1.The proposed nomenclature is intended to unify the prior taxonomies.Source: §2.1 · p. 4, Table 1 · p. 5
• The harmonized classes cover data constraints, relations, spikes, oscillations, steady-state error, rise/fall time, overshoot, and settling time.Data assertions may be untimed or time-bounded; relations may be functional or express temporal precedence or response. Rise/fall time, overshoot, and settling time describe responses after step-like changes.Source: §2.1 · pp. 5–6

2.2 Time-, Frequency-, and Time-Frequency-Domain Representation of Signals

• Time-domain signals map equally spaced samples over a finite time domain to real values.The sampling interval is dt; the representation associates a value with each time point.Source: §2.2.1 · p. 6

2.2.2 Frequency-Domain Representation of Signals.

• The frequency domain represents a signal as sinusoidal components with amplitudes and phases, highlighting shape-related frequencies but hiding when they occur [30].The spectrum is obtained using the Fourier transform; the paper focuses on component amplitudes unless otherwise stated.Source: §2.2.2 · pp. 6–7

2.2.3 Time-Frequency-Domain Representation of Signals.

• Time-frequency representations combine frequency-based shape information with temporal localization, but resolution trade-offs and cross-terms make transform choice application-specific.The paper uses STFT because it produces no cross-terms and is comparatively straightforward to interpret; window length and shape affect resolution and interference.Source: §2.2.3 · pp. 7–8

2.3.1 STL (Signal Temporal Logic).

• STL extends MITL with predicates over signal values, enabling signal requirements to be monitored through time-bounded temporal logic.Signal predicates translate values into Boolean predicates so STL formulas can be interpreted as MITL formulas over time.Source: §2.3.1 · pp. 8–9

2.3.2 TFL (Time-Frequency Logic).

• TFL extends STL with predicates on STFT-derived frequency amplitudes, turning each selected component into a time-domain signal for STL monitoring.Prior work applied TFL to melody identification; a wavelet-based variant was used for abnormal-data classification in a hydrogen fuel cell and an electrocardiogram.Source: §2.3.2 · p. 9

3.1 Requirements Classes that Can Benefit from Using the Frequency-Domain

• SP and OS are signal-feature classes, while SS, RT, OV, and ST describe step-response shapes and can benefit from frequency-domain representations.The step-response classes express implications from a step-like set-point change to the actual physical quantity’s response.Source: §3.1 · p. 9
• UA and TA constrain time-domain signal values, while TR concerns temporal relationships and FR is excluded because its frequency-domain usefulness is application-dependent.For TR, a frequency representation may help define atomic predicates, but not the temporal relations between them.Source: §3.1 · pp. 9–10

3.2 Frequency-Domain Formulation of CPS Requirements

• SP maps rapid changes to high-frequency energy, while OS maps periodic patterns to sharp spectral peaks.Frequency-domain assertions can bound high-frequency amplitudes to express spike presence or absence; periodicity can be detected through peaks rather than comparing signal segments over time.Source: §3.2 · pp. 10–11, Figure 2 · p. 10
• SS can compare low-frequency desired- and actual-state components, while OV can constrain amplification between their spectra.This lets SS disregard higher-frequency transient oscillations and characterizes OV through amplification of corresponding components, typically at higher frequencies during transients.Source: Figure 2 · p. 10, §3.2 · p. 11
• RT and ST can be expressed as constraints on bandwidth f_b, with ST sometimes also requiring a bound on maximum amplification.A larger bandwidth indicates faster tracking; overshoot can induce oscillations that increase settling time.Source: Figure 2 · p. 10, §3.2 · pp. 11–12

3.3 Desiderata for a Frequency-Extended Logic

• A frequency-extended specification language should support assertions over frequency intervals and logical relations between corresponding components of different signals.Intervals accommodate requirements such as high-frequency SP bounds, low-frequency SS checks, and RT/ST bandwidth; native relations avoid tedious, error-prone per-component predicates for cases such as OV.Source: §3.3 · p. 12

4.1 Syntax

• S2TL formulas combine time- and frequency-domain predicates using Boolean and until operators, with each frequency predicate scoped to a specified frequency interval.Frequency-domain terms can include transformed signals and operators, and predicates support amplitude- or phase-based inequalities.Source: §4.1 · p. 13

4.2 Qualitative Semantics

• S2TL frequency predicates universally quantify over specified frequency intervals and express logical relations between corresponding components in one or more signal spectra.Existential requirements can be expressed by negating the corresponding predicate; comparisons may be based on amplitude or phase.Source: §4.1 · p. 13, §4.2 · p. 15

4.3 S2TL Implementation and Monitoring Complexity

• The authors extended RTAMT with a discrete-time offline qualitative monitor that computes spectra, checks frequency predicates, and then evaluates the remaining STL formula.Offline monitoring accommodates the time-frequency transform’s dependence on future signal values; online monitoring would incur transform-dependent delay and is left for future work.Source: §4.3 · pp. 15–16
• Frequency predicates add computational and memory costs, but restricting monitoring to the statically specified frequency interval reduces the effective representation from |T| · |F| to |T| · |[f1, f2]|.The authors report that this overhead did not significantly affect their experiments, whose cost was dominated by the number of traces and formulas.Source: §4.3 · p. 16

5 EXPRESSING SIGNAL-BASED CPS REQUIREMENTS IN S2TL

• The templates target requirement classes identified as benefiting from time-frequency representations of signals.For step-response requirements, x denotes the output, r the input, e = abs(r − x) the control error, and fb the expected system bandwidth.Source: §5 · p. 16

5.1.1 Spike.

• A spike is detected when a sufficiently large component occurs above system bandwidth, with frequency bounds tied to the spike durations of interest.The template uses τ for minimum duration, sp for the amplitude threshold, and fmin > fb, chosen in relation to the maximum spike duration considered.Source: §5.1.1 · p. 16

5.1.2 Oscillation.

• An oscillation at fo is detected by a sufficiently strong spectral component near fo while neighboring components remain low.The template uses os as the minimum amplitude, δ for the detection interval, and ν and α to bound neighboring components; an upper amplitude bound can also be added.Source: §5.1.2 · p. 17, §5.2.2 · p. 17

5.2 Step-Response Requirements

• Step-response templates use the expected system bandwidth fb to distinguish low- and high-frequency signal components.The recurring signals are x for output, r for input, and e = abs(r − x) for control error.Source: §5 · p. 16, §5.2.1 · p. 17

5.2.1 Steady-State Error.

• Steady-state error is expressed as an implication: small high-frequency input components indicate steady state, while low-frequency error components must remain small.Components are divided at fb; ssth marks when input high-frequency amplitudes preclude steady state, and emax is the maximum acceptable steady-state error. Using the full ranges around fb can be restrictive; a small band may be excluded.Source: §5.2.1 · p. 17, §5.2.2 · p. 17

5.2.2 Overshoot.

• Overshoot is constrained by requiring that input frequency components above a relevance threshold are amplified by no more than a specified amount near fb.The template bounds amplification around the system bandwidth; ovth identifies relevant input components, ovamp sets maximum amplification, and δ defines the interval width.Source: §5.2.2 · pp. 17–18

5.2.3 Rise Time.

• Rise-time requirements combine low-frequency tracking with high-frequency attenuation, excluding a band around fb where amplification may occur.The low-frequency predicate allows a larger tracking error than steady-state error; the high-frequency predicate requires corresponding output components to be smaller than input components.Source: §5.2.3 · p. 18

5.2.4 Settling Time.

• Settling time is formulated so that once the input remains steady for the prescribed interval, the output must reach steady state unless the input leaves steady state first.Steady state is characterized by bounded high-frequency components; input and output may use different thresholds to account for output measurement noise.Source: §5.2.4 · p. 18

6 EVALUATION

• The evaluation asks whether time and time-frequency formulations broaden applicability, faithfully express signal properties, and yield consistent monitoring verdicts under signal noise.Fidelity is assessed by whether specifications distinguish systems that intrinsically satisfy or violate requirements, using precision and soundness.Source: §6 · p. 19, §6.3.1 · p. 24

6.1 Setup

• Experiments use simulated longitudinal drone motion and aircraft altitude traces, with test inputs comprising single steps or randomly sampled control points interpolated linearly, constantly, or alternately.For fidelity testing, control-theory formulas are used to construct systems that satisfy or violate step-response requirements independently of the input signal.Source: §6.1.1 · pp. 19–20, §6.1.2 · p. 20

6.1.3 Specification Languages and Templates

• The comparison uses STL* templates adapted from Kapinski et al. and S2TL templates from Section 5, monitored with the same extended RTAMT framework.S2TL experiments use the STFT; window shapes and lengths are selected according to the requirement and application.Source: §6.1.3 · pp. 20, 22, §6.1.4 · p. 22

6.2.1 Methodology and Parameters Settings.

• S2TL preconditions differ by requirement: they check steady state for SS and ST, a bandwidth-region input component for OV, and a high-frequency component for RT.Applicability was tested on 200 traces per input type, with rectangular STFT windows of 15 s for the aircraft and 4 s for the drone.Source: §6.2.1 · p. 23

6.2.2 Results.

• For linear and alternated inputs, only 0%–17% of traces met the STL* preconditions, versus ≥99% for S2TL; S2TL also preserves applicability to step and constant-interpolation inputs.The result is particularly relevant because linear interpolation is commonly used for CPS testing.Source: §6.2.2 · pp. 23–24, Table 2 · p. 24

6.3.1 Methodology and Parameters Settings.

• For fidelity testing, only traces applicable to both languages are included: step and constant-interpolation inputs for ST, RT, and OV, and also linear and alternated inputs for SS.Signal-feature tests synthesize valid and invalid spikes or oscillations; step-response tests simulate systems constructed to satisfy or violate the selected thresholds.Source: §6.3.1 · p. 25
• The evaluation measures fidelity using precision—the share of flagged traces that are actual violations—and soundness—the share of violations detected.Table 5 reports these metrics for spikes, oscillations, and step-response requirements, with a total across traces.Source: §6.3.1 · p. 26, §6.3.2 · p. 26

6.3.2 Results.

• S2TL achieves 82.12% precision and 86.47% soundness overall, versus 71.19% and 70% for STL*.Table 5 summarizes fidelity across all traces.Source: Table 5 · p. 27, §6.3.2 · p. 27
• For spikes and oscillations, S2TL outperforms STL* on precision, and on both precision and soundness for oscillations; step-response classes show mixed trade-offs.For RT, STL* leads in precision and soundness; for ST and SS, S2TL has higher precision but lower soundness, while OV reverses that pattern. With linear or alternate interpolation, S2TL retains high precision but low soundness for ST, RT, and OV; OV detects only 5% of violations because such inputs provide less excitation.Source: §6.3.2 · pp. 27–28, Table 6 · p. 27

6.4.1 Methodology.

• Noise-tolerance analysis retained only traces on which both specifications initially gave the correct verdict and tested offset, Gaussian white, and Gaussian high-frequency noise at four levels from 5% to 30% of signal range.The retained sets contained 379 SP, 538 OS, 65 RT, 87 ST, 82 OV, and 110 SS traces; noise was applied only to outputs for step-response requirements, with cases where noise changed the ground truth excluded.Source: §6.4.1 · pp. 28–29

6.4.2 Results.

• S2TL is more noise-tolerant than STL* for offsets and high-frequency noise, while white-noise results vary by requirement class.For white noise, S2TL performs better for SP, ST, and SS, the languages are comparable for OS and OV, and STL* is better for RT (29.23% versus 67.69% of traces flipped). S2TL’s spectral selectivity helps isolate offset and high-frequency noise, but white noise affects relevant frequencies too.Source: §6.4.2 · pp. 29–30

6.5 Discussion.

• The discussion finds broader trace applicability and greater tolerance to noise with a known spectral profile for time-frequency specifications, while time-domain formulas can attain higher fidelity through stronger signal-shape assumptions.Time-domain specifications remain effective when signal-shape assumptions are strong and noise is low.Source: §6.5 · pp. 30–31

6.6.1 Internal Validity.

• Internal validity is limited by choices in STL* and S2TL formulas and parameters, random noise sampling, and the RT time-domain formula’s assumption that step inputs start at zero.The authors ground the templates in requirement definitions or control theory and parameters in engineering considerations; both specifications were evaluated on identical noisy traces across 1,252 traces. The RT assumption may reduce soundness for some inputs, but the authors say correcting it would not change their conclusion that the time-domain representation outperforms S2TL for RT.Source: §6.6.1 · p. 31

6.6.2 External Validity.

• External validity depends on whether the modeled systems and generated inputs represent real CPS tests; the study used synthetic second-order systems and non-negative inputs.The authors regard the inputs as representative of common testing approaches and the second-order model as a good closed-loop approximation; they argue that negative signals would further reduce time-domain applicability, fidelity, and noise tolerance while leaving S2TL templates unchanged.Source: §6.6.2 · pp. 31–32

• Requirements-mining research should investigate synthesising specification transforms to capture relevant signal properties, alongside learning specification parameters.Source: §7 · p. 32
• Falsification testing should explore behaviours with different frequency content [46], while fault localisation could track fault-induced changes in signals’ spectral properties.Source: §7 · p. 32
• Broader applicability and noise tolerance can make specification development and maintenance more cost-effective by enabling specifications to serve as oracles on more traces.Source: §7 · p. 32
• A formalism expressing time- and frequency-domain properties can foster collaboration among software, systems, and control engineers [32], making industrial adoption of formal specifications and runtime verification more likely.Source: §7 · p. 32

8.1 Time-Based Specification Languages

• Time-domain specification languages develop from LTL and MTL to STL, whose extensions address comparisons across time and combined source-code and signal properties.STL* [15] adds a signal-value-freeze operator for comparisons across time; HLS [35] adds timestamp and time-index quantification, and SCSL combines HLS with iCFTL. RTAMT supports STL and STL*, while HLS and SCSL authors provide monitor replication packages; these tools have permissive open-source licenses.Source: §8.1 · pp. 33–34
• Other time-based approaches include SCL for interval-percentage predicates and noise filtering, SFO for value and time quantification, and Shape Expressions for signal patterns.Shape Expressions describe patterns such as linear increase, exponential growth, or sinusoidal oscillation as sequences in a grammar similar to regular expressions.Source: §8.1 · pp. 33–34

8.2 Use of the Frequency Domain for Signal-Based CPS Specifications

• S2TL takes a different approach from time-domain languages by using time-frequency representations, with expressive predicates over spectra and frequency intervals rather than only individual frequency components.The paper identifies both capabilities as important for specifying CPS requirements.Source: §8.1 · p. 34, §8.2 · p. 34
• Prior frequency-domain specification work ranges from Fourier constraints for periodic signals to TFL and PTFL for time-varying spectra and anomaly detection.The paper notes that discards temporal information, while TFL uses STFT and PTFL replaces it with wavelets and supports parameters learned from traces; neither TFL nor PTFL has a known implementation.Source: §8.2 · p. 34
• Other frequency-domain CPS V&V work uses LTI filters for MTL semantics, analyzes STL monitors [8], or applies frequency analysis to test generation [32], rather than specifying requirements directly.These works nevertheless underscore the relevance and potential of frequency-domain methods for CPS V&V.Source: §8.2 · p. 34

9 CONCLUSIONS

• The study identifies CPS requirement classes suited to time-frequency representations, derives language desiderata, proposes S2TL predicates over frequency intervals and component relations, and supplies specification templates.The templates cover the identified requirement classes and support empirical comparison of time- and time-frequency-domain formulations.Source: §9 · pp. 34–35
• Time-frequency specifications extend step-response requirements to linearly interpolated traces without step-like inputs and improve tolerance to offsets and high-frequency noise while retaining comparable fidelity.The reported fidelity remains comparable in capturing the intended signal properties.Source: §9 · p. 35
• Future work includes a practitioner user study on S2TL understandability, GUI-based tools for formula visualization alongside signals, and investigation of online monitors.The planned user study will examine S2TL’s potential adoption by CPS software engineering practitioners.Source: §9 · p. 35

A.1 RQ1

• The observed bandwidth is approximately 1 Hz for the drone and 0.2 Hz for the aircraft, corresponding to reaction times on the order of seconds and tens of seconds, respectively.Source: §A.1 · p. 38
• Table 8 reports the parameter values and selection rationale for the RQ1 precondition formulas, with “f.int.” rows marking frequency intervals for frequency predicates.Source: §A.1 · p. 38, Table 8 · p. 38

A.2 RQ2

• Formulas span each full trace (20 s for SP and OS; 100 s for RT, ST, OV, and SS) and set fmax to 4 Hz.The frequency cap avoids evaluating high-frequency components that typically have little useful information; fb is typically around 1 Hz, with relevant components below 3 Hz.Source: §A.2 · p. 38

A.2.1 SP.

• STL’s 0.01 discrete-derivative value corresponds to the sampling time.Source: §A.2.1 · p. 38
• STL uses a 2 s upper spike-width bound and amplitude threshold 5 from, calibrated so spike amplitude times derivative threshold stays proportional to expected amplitude 10.Source: §A.2.1 · pp. 38–39
• S2TL uses a 1 s lower spike-width bound and transform threshold 1, derived from expected amplitude 10 but reduced by one order of magnitude as a higher-frequency component.Source: §A.2.1 · p. 39
• S2TL’s [0.5, 4] Hz interval includes components above 0.5 Hz to cover the expected longest 2 s spike, whose duration is inverse to frequency.Source: §A.2.1 · p. 39

A.2.2 OS.

• STL uses amplitude thresholds of 20 and 40, a [0.48, 0.52]s interval for ^, and a 0.25s shift for *, following.The thresholds are based on the expected peak-to-peak amplitude; the ^ interval allows a margin around half the expected oscillation period.Source: §A.2.2 · p. 39
• S2TL uses amplitude thresholds of 4.5 and 10 and frequency intervals [0.85, 1.15]Hz, [0.4, 0.85]Hz, and [1.15, 1.6]Hz.The central interval captures the expected 1 Hz oscillation, while the flanking intervals characterize low-amplitude frequency regions; the thresholds account for time-frequency scaling.Source: §A.2.2 · p. 39

A.2.3 RT.

• For rise time, STL uses a minimum input step of 1 and a [0, 0.75]s interval for the prescribed 0%-to-75% rise time.The interval reflects the 0.75 s rise-time requirement.Source: §A.2.3 · p. 39
• S2TL checks rise-time behavior over [0, 0.3]Hz and frequencies above 0.6Hz, using thresholds of 0.25 for low-frequency error and 0.1 for high-frequency components.The low-frequency threshold allows for transient tracking error; the high-frequency threshold excludes components too small for reliable assessment.Source: §A.2.3 · p. 39

A.2.4 ST.

• For settling time, STL considers input steps of at least 1, evaluates error over [4.5, 6]s, and uses a 0.02 coefficient for the 2%-range definition.The 1.5 s evaluation window extends beyond the prescribed 4.5 s settling time.Source: §A.2.4 · p. 39
• S2TL uses an until interval of [0, 2.25]s and checks steady state over [0.15, 4]Hz with a threshold of 0.1.The time bound is halved to account for reduced time-axis resolution, while the frequency range reflects the approximate 0.15 Hz bandwidth.Source: §A.2.4 · pp. 39–40

A.2.5 OV.

• For overshoot, STL considers input steps of at least 1, captures the transient over [0, 2]s, and uses a 0.15 coefficient for the allowable overshoot.The coefficient is based on the maximum allowable overshoot in Table 3.Source: §A.2.5 · p. 40
• S2TL evaluates overshoot over [1, 3]Hz, uses 0.05 to disregard insignificant output variations, and permits amplification up to 1.15, implementing 15% overshoot.The frequency range corresponds to a system bandwidth of 2 Hz.Source: §A.2.5 · p. 40

A.2.6 SS.

• For steady state, STL uses a 0.01 discrete-derivative threshold, evaluates tracking error over [2, 2.02]s after the 2 s settling time, and allows static error of 0.1.The derivative threshold corresponds to a rate of change of 1 unit per second.Source: §A.2.6 · p. 40
• S2TL checks steady-state input over [0.5, 4]Hz, limits its high-frequency components to 0.01, and bounds tracking-error spectrum by 0.1 over [0, 0.2]Hz.The thresholds are based on the allowable static error, with the input threshold reduced for high-frequency components.Source: §A.2.6 · p. 40