Source-linked AI summary
On the Time and Frequency Domain Representations of Signals for CPS Specification
Claudio Mandrioli, Drishti Yadav, Domenico Bianculli
TL;DR
CPS specification languages largely use time-domain signals, which limits their treatment of signal shapes and dynamic behaviours. This paper develops S2TL and monitoring support for time-frequency requirements, finding broader applicability to linearly interpolated traces and greater tolerance to offset and high-frequency noise, with comparable fidelity and white-noise tolerance.
Problem
Time-domain CPS specification languages provide limited support for reasoning about signal shape independently of specific signal values.
Method
The paper analyses CPS requirement classes, derives time-frequency specification desiderata, proposes S2TL, defines templates, and implements an offline monitor.
Results
Time-frequency specifications broaden applicability to linearly interpolated traces, improve tolerance to offset and high-frequency noise, and retain comparable fidelity and white-noise tolerance.
Takeaways & Limitations
Time-frequency representations extend CPS specification beyond step-like or constant-interpolated traces while remaining comparable in capturing intended requirements.
Takeaways & Limitations
The evaluation considers only non-negative signal values, because the time-domain templates assume non-negative signals.
Abstract
from arXiv · showhide
Specification languages are instrumental to the Verification \& Validation of Cyber-Physical Systems (CPSs). Most state-of-the-art specification languages use the time-domain representation of signals, which is not always suitable for describing signal shapes and dynamic behaviours. Instead, fields like control and robotics use the frequency-domain representation to characterise these behaviours. Time-frequency representations combine the capabilities of both domains. We investigate the use of time-frequency representations to specify CPS requirements. We analyse existing taxonomies of CPS requirements to identify which requirement classes can benefit from time-frequency representations. We derive the desiderata for a specification language that uses time-frequency representations and propose Signal-Spectrum Temporal Logic (S2TL), a language enabling assertions over frequency intervals and relations between frequency components. We operationalise the S2TL semantics for monitoring CPS traces, and implement a monitor. We define specification templates for the identified requirement classes and compare time- and time-frequency-domain formulations in terms of applicability, expression fidelity, and noise tolerance of monitoring. We observe that, while time-domain specifications are applicable only to input traces containing step-like changes or using constant interpolation, time-frequency specifications extend their evaluation to traces generated through linear interpolation, and improve tolerance to offset and high-frequency noise, while achieving comparable fidelity to the intended system properties.
1 INTRODUCTION
The paper argues that time-domain CPS specifications are limited for describing signal shapes and dynamic behaviours, motivating time-frequency reasoning. It proposes S2TL and evaluates it against time-domain formulations for applicability, fidelity, and noise tolerance.
- Time-domain specification languages suit direct value constraints but provide limited support for reasoning about signal shape independently of specific values.
- Time-frequency representations combine frequency-domain shape analysis with time localisation, potentially broadening specification applicability and improving noise tolerance.
- The paper identifies signal-feature and step-response requirements as classes that can naturally benefit from frequency-domain properties.
- S2TL supports predicates over frequency intervals and logical relations between frequency components of multiple signals, addressing limitations observed in TFL.
- The authors operationalise S2TL semantics, implement an offline monitor, and compare S2TL and STL templates on realistic and synthetic CPS traces.
- Time-frequency specifications apply to linearly interpolated traces, show comparable requirement-capture ability, and better tolerate offset and high-frequency noise than time-domain specifications.
2 BACKGROUND
The background surveys CPS requirement classes and signal representations across time, frequency, and time-frequency domains. It presents time-frequency representations as a way to retain frequency-based shape information while localising features in time.
- Signal-Based CPS Requirements: The paper harmonises requirement taxonomies from automotive and aerospace applications into a unified classification.
- Signal-Based CPS Requirements: The taxonomy includes value constraints, functional and timed relations, spikes, oscillations, steady-state error, rise/fall time, overshoot, and settling time.
- Signal Representations: In the time domain, a signal is represented as a sequence of values over time, whereas the frequency domain represents it as sinusoidal components with amplitudes and phases.
- Signal Representations: Frequency-domain amplitudes capture how strongly a signal resembles corresponding sinusoids, but frequency-only representations hide when signal features occur.
- Signal Representations: Time-frequency representations encode evolving frequency components, combining frequency-based shape information with temporal localisation.
- Signal Representations: Time-frequency transforms face an inherent trade-off between time and frequency resolution, and high-resolution methods may introduce cross-terms.
3 CPS REQUIREMENTS IN THE FREQUENCY DOMAIN
The paper classifies which CPS requirements can benefit from frequency-domain reasoning and explains how their signal-shape properties can be expressed spectrally. This analysis yields language desiderata for frequency intervals and cross-signal component relations.
- Spike, oscillation, steady-state, rise/fall, overshoot, and settling-time requirements can benefit from frequency-domain representations because they concern signal shapes.
- Untimed and timed data assertions generally remain better suited to the time domain because they constrain signal values over time.
- Functional relations are naturally expressed in the time domain because they compare signal values directly, although selected frequency ranges may help filter high-frequency noise in specific cases.
- Timed relations remain primarily temporal even when frequency-domain representations help define their atomic predicates.
- Spike absence or presence can be expressed as upper or lower bounds on high-frequency amplitudes, while oscillations correspond to sharp spectral peaks.
- Rise/fall and settling-time requirements can be translated into bandwidth constraints, with settling time sometimes also requiring a maximum-amplification constraint.
- A suitable language must support assertions over frequency intervals and logical predicates relating corresponding frequency components across signals.
4 THE S2TL SPECIFICATION LANGUAGE
S2TL extends STL with frequency-domain predicates, enabling relations between spectra and quantification over frequency intervals. Its semantics and monitor support time-frequency assertions over CPS traces, while restricting monitored frequencies can reduce added costs.
- Language design: S2TL extends STL with frequency-domain predicates for relations between spectra and quantification over specified frequency intervals.The language combines time- and frequency-domain predicates with Boolean and until operators.
- Syntax: Frequency-domain terms include constants, signal transforms, and pointwise operator applications over complex-valued spectra.The transform W maps time-domain signals to functions over time and frequency.
- Frequency predicates: S2TL compares complex spectral values by amplitude or phase, using abs(·) and arg(·), respectively.Amplitude comparison is the implicit default when a predicate omits its subscript.
- Qualitative semantics: Frequency-interval semantics universally quantify predicates across every frequency in the specified interval, while negation expresses existential requirements through logical duality.This implements a logical conjunction along the frequency axis.
- Monitoring: The monitor extends RTAMT with discrete-time, offline qualitative S2TL monitoring because time-frequency transforms depend on future signal values.Frequency predicates are parsed and evaluated before the remaining formula is handled as standard STL.
- Monitoring complexity: Frequency predicates add computational and memory costs, but static frequency intervals reduce the monitored representation from |T| · |F| to |T| · |[f1,f2]|.The overall cost also depends on the selected time-frequency transform.
5 EXPRESSING SIGNAL-BASED CPS REQUIREMENTS IN S2TL
The paper uses S2TL to template CPS requirements whose signal features are naturally expressed in the frequency domain. These templates cover spikes, oscillations, steady state, overshoot, tracking, and settling-time behaviours using frequency-, time-, or mixed-domain predicates.
- Notation: S2TL templates use x for the output, r for the input, e = abs(r − x) for control error, and fb for expected system bandwidth.These conventions recur across the requirement templates.
- SP requirements: Spike requirements detect large high-frequency components above the system bandwidth, with thresholds and minimum-duration parameters controlling detection.The lower frequency bound fmin exceeds fb and depends on the longest spike duration considered.
- OS requirements: Oscillation requirements detect a sufficiently large component near fo while constraining neighbouring frequency components to remain low amplitude.δ identifies the oscillation interval, while α defines the wider neighbourhood subject to the low-amplitude threshold ν.
- SS requirements: Steady-state requirements use small high-frequency input components as a precondition and bound the desired–actual state error by emax.The threshold ssth determines when the signal is not considered steady state.
- OV requirements: Overshoot requirements constrain amplification by relating relevant input frequency components to an upper bound on corresponding output amplification.ovamp expresses the maximum allowable amplification, such as 1.1 for 10% overshoot.
- RT requirements: Rise-time requirements combine low-frequency tracking and high-frequency attenuation around the system bandwidth.The excluded interval around fb has width controlled by δ, and low-frequency tracking error is bounded by elf.
- ST requirements: Settling-time requirements combine bandwidth and overshoot constraints with time- and frequency-domain predicates to bound reaching steady state.The high-frequency steady-state threshold may differ between input and output because of measurement noise.
6 EVALUATION
The evaluation compares STL* and S2TL on applicability, expression fidelity, and noise tolerance. S2TL broadens applicability and improves robustness to offset and high-frequency noise, while fidelity advantages depend on the requirement class.
- Applicability: Nearly all linear and alternated-interpolation traces satisfy S2TL preconditions, compared with only 0%–17% for corresponding STL* preconditions.For the tested subjects, S2TL preconditions were satisfied by at least 99% of traces.
- Expression fidelity: S2TL achieves higher overall precision and soundness than STL*, at 82.12% and 86.47% versus 71.19% and 70%, respectively.The aggregate comparison spans spike, oscillation, and step-response requirement classes.
- Expression fidelity: For spikes and oscillations, S2TL outperforms STL* in both soundness and precision, especially for oscillation soundness at 94% versus 48.67%.For spikes, S2TL precision is 81.48% versus 67.84% for STL*, while soundness is 97.78% versus 100%.
- Expression fidelity: Step-response fidelity is mixed: STL* is stronger for RT, while ST, SS, and OV show differing precision–soundness trade-offs between the languages.Neither language clearly outperforms the other across all step-response classes.
- Noise tolerance: S2TL is more tolerant of offset and high-frequency noise than STL*, with exceptions for spike and oscillation classes under offset noise.The advantage is attributed to isolating frequency components carrying relevant system behaviour.
- Noise tolerance: White noise degrades both approaches because it affects the whole spectrum, although S2TL remains more tolerant for SP, ST, and SS.For RT, STL* has fewer flipped verdicts than S2TL: 29.23% versus 67.69%.
7 OUTLOOK ON SOFTWARE ENGINEERING FOR CPS WITH TIME-FREQUENCY SPECIFICATIONS
The paper discusses how time-frequency signal representations could affect software-engineering activities for CPS, especially through broader monitoring applicability and improved noise tolerance.
- Time-frequency representations may support requirements mining, falsification testing, and fault localisation by improving specification-based monitoring.The paper identifies these as potential developments across software-engineering activities that use specification languages and runtime verification.
- The outlook connects time-frequency specifications to software-engineering activities that rely on specification languages and runtime verification.
- Broader trace applicability and greater noise tolerance could make specification development and maintenance more cost-effective for practitioners.Specifications could serve as oracles on a larger number of traces.
8 RELATED WORK
The related-work review traces CPS specification languages from LTL, MTL, and STL extensions to approaches using convolution, patterns, and frequency-domain representations. The paper positions S2TL as a time-frequency logic with stronger frequency-domain expressiveness than TFL.
- Time-Based Specification Languages: STL extends temporal logics to dense-timed, real-valued signals through atomic propositions expressing inequalities over signal values.STL is also used in prior work to define templates for CPS requirement classes.
- SCL specifies predicates holding for a percentage of an interval while using convolution to filter noise.
- Other approaches represent signal requirements as sequences of basic patterns such as linear increase, exponential growth, or sinusoidal oscillations.These sequences can be written with a grammar similar to regular expressions.
- The paper addresses signal-shape specification through time-frequency representations rather than solely comparing signal values at different times.
- Compared with TFL, S2TL supports predicates over frequency intervals and more expressive relations among frequency components of one or more signals.The paper identifies these features as essential for specifying CPS requirements.
9 CONCLUSIONS
The paper proposes S2TL after analysing CPS requirement taxonomies and evaluating time-frequency formulations against time-domain formulations. The results show broader applicability and improved noise tolerance while preserving comparable fidelity.
- The study identifies CPS requirement classes that can benefit from time-frequency representations and derives desiderata for a corresponding specification language.
- S2TL enables predicates over frequency intervals and logical relations between frequency components.
- Time-frequency formulations broaden step-response applicability by removing dependence on step-like inputs and supporting traces generated through linear interpolation.
- Time-frequency requirements tolerate signal offsets and high-frequency noise better while maintaining comparable fidelity to intended signal properties.
- Future work will study practitioner understandability and develop GUI-based tools for using S2TL.
A.1 RQ1
The RQ1 precondition specifications use empirically selected parameter values, including bandwidth estimates and frequency intervals for the frequency predicates.
- The estimated bandwidths are approximately 1 Hz for the drone and 0.2 Hz for the aircraft.These values correspond intuitively to reaction times of seconds for the drone and tens of seconds for the aircraft.
- Table 8 reports the parameter values and selected frequency intervals used in the RQ1 precondition formulas.
A.2 RQ2
The templates evaluate formulas over the entire trace, with trace duration depending on the requirement. They set f_max to 4 Hz to exclude high-frequency components that carry little useful information.
- Formulas use a global time interval spanning the entire trace.The traces last 20 s for SP and OS, and 100 s for RT, ST, OV, and SS.
- The templates denote the maximum frequency of the time-frequency representation by f_max.
- f_max is set to 4 Hz because most high-frequency components have very small amplitude and little or no useful information.Relevant components typically lie below 3 Hz, with f_b around 1 Hz.
A.2.1 SP.
The SP templates calibrate time- and time-frequency-domain thresholds to expected spike amplitude and duration. The S2TL formulation uses frequency components above 0.5 Hz to represent spikes up to 2 s long.
- The STL derivative uses 0.01, corresponding to the sampling time.
- The STL spike template bounds spike width by 2 s and uses an amplitude threshold of 5.The threshold is adopted from the original work, which assumes an expected spike amplitude of 10.
- The S2TL spike template uses a 1 s lower bound on spike width.
- S2TL uses a threshold of 1 and the frequency interval [0.5, 4] Hz to capture components associated with spikes up to 2 s long.The threshold is reduced by one order of magnitude because the component is higher-frequency; duration is inverse to frequency.
A.2.2 OS.
The OS templates encode expected oscillation amplitude and period differently in STL and S2TL. S2TL targets the 1 Hz component and adjacent low-amplitude frequency ranges.
- STL evaluates around half the expected oscillation period, using [0.48, 0.52] s and a 0.25 s time shift.
- S2TL uses amplitude thresholds of 4.5 and 10 to account for time-frequency representation scaling.
- S2TL targets [0.85, 1.15] Hz for the expected 1 s oscillation and adjacent intervals [0.4, 0.85] Hz and [1.15, 1.6] Hz.
A.2.3 RT.
The RT templates translate rise-time, settling-time, bandwidth, overshoot, and tracking-error requirements between time-domain and time-frequency formulations. S2TL uses frequency ranges and adjusted time bounds to represent these behaviours.
- The RT templates consider input step changes with minimum magnitude 1.
- STL encodes the prescribed 0%–75% rise time with the interval [0, 0.75] s.
- S2TL maps the 0.75 s rise time to approximately 0.3 Hz, using [0, 0.3] Hz for low frequencies and frequencies above 0.6 Hz for high frequencies.
- STL evaluates settling from [4.5, 6] s using coefficient 0.02, based on a 4.5 s settling time and its 2%-range definition.
- S2TL uses [0, 2.25] in the until operator and [0.15, 4] Hz to represent a 4.5 s settling requirement.The time bound is halved because the time-frequency transform reduces time-axis resolution and requires slack.
- For overshoot, S2TL evaluates [1, 3] Hz with threshold 0.05 and coefficient 1.15, implementing a 15% allowable amplification.
- For steady-state tracking, S2TL uses [0.5, 4] Hz for input behaviour and [0, 0.2] Hz for tracking error bounded by 0.1.The high-frequency input threshold is 0.01, reduced because the predicate operates on high-frequency components.