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

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

arXiv:2608.21167v1 [cs.SE] 21 Aug 2026

CLAUDIO MANDRIOLI, University of Luxembourg, Luxembourg DRISHTI YADAV, University of Luxembourg, Luxembourg DOMENICO BIANCULLI, University of Luxembourg, Luxembourg 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. CCS Concepts: • Software and its engineering → Software verification and validation; • Computer systems organization → Embedded and cyber-physical systems. Additional Key Words and Phrases: Cyber-physical Systems, Specification Languages, Frequency Domain. ACM Reference Format: Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli. 2026. On the Time and Frequency Domain Representations of Signals for CPS Specification. 1, 1 (August 2026), 40 pages. https://doi.org/10.1145/nnnnnnn.nnnnnnn

1

INTRODUCTION

Cyber-Physical Systems (CPSs) are characterised by the tight interaction of software and physical components and are pervasive in our daily lives [45]; common examples of CPSs include robots, aircraft, drones, electric grids, smart medical devices, and satellites. Like these examples, many CPSs are safety-critical; therefore, their rigorous Verification & Validation (V&V) is of paramount importance. However, the V&V of CPSs is a time-consuming and resource-intensive process [26]. Formal specification languages support the V&V process by enabling the precise formalisation of requirements. Then, using monitors, the specified requirements can be automatically evaluated on Authors’ addresses: Claudio Mandrioli, claudio.mandrioli@uni.lu, University of Luxembourg, Luxembourg, Luxembourg; Drishti Yadav, drishti.yadav@uni.lu, University of Luxembourg, Luxembourg, Luxembourg; Domenico Bianculli, domenico. bianculli@uni.lu, University of Luxembourg, Luxembourg, Luxembourg. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. © 2026 Association for Computing Machinery. XXXX-XXXX/2026/8-ART $15.00 https://doi.org/10.1145/nnnnnnn.nnnnnnn , Vol. 1, No. 1, Article . Publication date: August 2026.

2

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

execution traces to assess whether the traces satisfy the requirements. In this way, specification languages and the associated monitor can improve both the rigour and efficiency of various V&V activities such as runtime verification, testing, and falsification [4]. Their effectiveness, however, depends on their ability to capture the properties of interest while abstracting away contingent variations of individual executions. Intuitively, making strong assumptions on the execution traces limits the applicability of a specification to diverse scenarios. Analogously, if the monitoring is easily perturbed by small variations in the signals, it provides limited support for systematic and automated V&V. At a high level, the objective of a CPS is to steer the physical component towards a desired state. For example, in a drone, the software uses accelerometer and GPS measurements to compute the propellers commands and fly the drone towards a target position, i.e., the desired state. The evolution of both the actual and desired physical states can be represented as time-varying signals. Accordingly, CPS requirements describe how the actual-state signal should evolve with respect to the desired-state (reference) signal. This concerns not only the difference in value between the two signals, but also their shape and relation over time. For example, requirements specify how close the drone should get to a target position, but also how fast it should reach it and whether it may overshoot while doing so. Common examples of specified behaviours include oscillations, overshoots, settling time, or steady-state tracking [11, 28]. Formal specification languages are languages with a formal syntax and semantics that allow for the rigorous specification of requirements. Once a requirement is specified, it can then be checked using runtime verification techniques [5] on system traces (e.g., signals recording in the case of CPSs), providing a verdict of whether the requirement specification is satisfied or not. State-of-the-art specification languages for CPSs, including Signal Temporal Logic [30] (STL) and its variants [15, 35], are based on the time-domain representation of signals. That is, they define assertions on the sequence of values that signals take over time. This representation is well suited for expressing requirements that directly constrain signal values, such as an upper bound on a signal value. However, it is less natural for expressing requirements that concern signal shapes, such as an oscillation, or the dynamic relation between multiple signals, such as an overshoot. In fact, capturing such shape-related properties in the time domain requires explicitly constraining signal values at multiple time instants, and encoding assumptions about specific signal patterns and expected signal evolution. For example, describing a sinusoidal oscillation requires constraining the signal values within one oscillation period so that they are sufficiently close to shape of the sinusoid of interest; describing an overshoot requires first encoding the shape of the reference value change (e.g., a step-like change) and then constraining the value of the actual-state signal within a time window around the reference change. In such time-domain descriptions, the resulting specifications are often tightly coupled to particular signal realisations which makes them sensitive to contingent variations. The frequency-domain representation of signals, already used in related fields such as control theory and robotics [2], can help mitigate these limitations. In the frequency domain, a signal is represented as a combination of sinusoidal components with different frequencies, amplitudes, and phases, called spectrum. Rather than describing the values assumed by the signal at individual time instants, this representation captures the rates at which the signal varies. Intuitively, slowly varying signals are dominated by low-frequency components, whereas rapidly varying signals contain more pronounced high-frequency components. As a result, the frequency domain is particularly well suited to expressing shape-related properties. For example, a sinusoidal oscillation appears as a isolated frequency component (a spike in the spectrum), or an overshoot appears as the amplitude amplification of a frequency component from the input to the output.

, Vol. 1, No. 1, Article . Publication date: August 2026.

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

3

However, in a purely frequency-domain representation, the temporal information is implicitly encoded and thus “hidden” in the sinusoids. As a result, it becomes difficult to locate signal features in time and assert whether a particular property holds within the signal at a certain point in time. To address this limitation and combine the benefits of both the time and frequency domains, several hybrid time-frequency representations have been proposed [10]. In a time-frequency representation, a signal is represented as a sequence of frequency components whose amplitudes and phases evolve over time. This representation enables reasoning jointly about the frequency-based shape-oriented features and their appearance at different points in time. The central hypothesis of this paper is that time-frequency representations provide a more suitable foundation for specifying CPS requirements on signal shapes. Using the time-frequency domain offers two potential benefits. First, it enables specifications to abstract from individual signal values and capture shape-related features more directly while preserving their location in time, thereby increasing their applicability across different signal shapes. Second, it improves the tolerance of monitoring algorithms to signal noise by enabling the isolation of the frequency components that encode the relevant system behaviour. Despite the widespread use of the frequency domain in control and robotics, its potential use in CPS specification languages remains under-explored. Existing specification languages are almost exclusively formulated over time-domain signals and therefore provide limited support for reasoning about signal shape independently of specific signal values. The only exception is TimeFrequency Logic (TFL) [23], which introduces assertions over time-frequency representations of signals. However, as the authors themselves acknowledge in their conclusions, TFL is largely timeoriented, and, to the best of our knowledge, it has been applied (through an extension called PTFL) to CPSs in only two subsequent works [9, 38] to perform anomaly detection. Consequently, there is currently little understanding of (i) which CPS requirements actually benefit from time-frequency representations, (ii) which language constructs are needed to express them, and (iii) whether such representations provide practical advantages for specification assessment. To address these questions, in this work, we first analyse existing taxonomies of signal-based CPS requirements [11, 28] to identify which CPS requirement classes can benefit from the use of the time-frequency representation. We observe that requirements concerning signal features and step-response behaviours can be naturally reformulated in terms of frequency-domain properties. Based on this observation, we then derive a set of desiderata for a specification language using time-frequency representations of signals. Notably, we contend that such a language shall support predicates over frequency intervals and express logical relations between frequency components of different signals. We observe that TFL does not satisfy these desiderata. Specifically, TFL predicates on individual frequency components, and lacks constructs for expressing logical relations over frequency intervals and between frequency components of different signals. To address this limitation, we propose Signal-Spectrum Temporal Logic (S2TL, read as “S-quare TL”). S2TL enables predicates over frequency intervals and the formulation of logical relations between frequency components of multiple signals. Using S2TL, we propose templates for the classes of CPS requirements that can benefit from time-frequency reasoning and compare them against corresponding STL formulations. We then operationalise the proposed semantics and implement a discrete-time offline monitoring algorithm for S2TL as an extension of the RTAMT monitoring tool [47]. We use our S2TL templates and STL templates from the literature [28] to formulate requirements for a drone and an aircraft. We then evaluate the resulting specifications on both realistic CPS traces and synthetic traces for which the ground-truth satisfaction of the requirements is known. We evaluate the resulting specifications along three complementary dimensions. First, we investigate their applicability, namely the set of traces for which the requirements can be meaningfully assessed. , Vol. 1, No. 1, Article . Publication date: August 2026.

4

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

Second, we assess expression fidelity, that is, how well the specifications capture the intended property. To enable this assessment of the expression fidelity, we use control theory to generate traces that intrinsically satisfy or violate the intended property. Third, we assess the noise tolerance of the specification monitoring. Our results show that, while time-domain specifications are applicable only to traces that contain step-like input changes or use constant interpolation between control points, time-frequency-based specifications can be applied also to traces generated through linear interpolation. This applicability extension is particularly important because linear interpolation is the standard choice in most CPS applications. For traces to which both representations are applicable, we observe comparable ability to capture the intended requirements, although with different trade-offs between soundness and precision. Finally, time-frequency-based specifications exhibit substantially greater tolerance to offset and high-frequency noise, while achieving comparable tolerance to white noise. To summarise, our contributions are the following: • An analysis of signal-based CPS requirement classes, identifying those that benefit from the time-frequency representation of signals. Based on this, we derive the desiderata for a specification language able to express them. • The formal definition of S2TL language in terms of its syntax and semantics, which enables time-frequency specifications with predicates over frequency intervals and logical relationships between frequency components. • A set of specification templates for expressing signal-based CPS requirement classes. • An empirical comparison—in terms of applicability, expression fidelity, and noise tolerance of monitoring—of time-frequency specifications expressed in S2TL and time-domain specifications expressed using STL templates from Kapinski et al. [28]. The rest of the paper is structured as follows. Section 2 introduces the relevant background on signal-based CPS requirements, as well as time-, frequency-, and time-frequency-domain signal representations. Section 3 discusses which CPS requirement classes can benefit from the use of the time-frequency domain and qualitatively explains how these requirements can be captured in this domain. Section 4 introduces the formal syntax and semantics of the S2TL language. Section 5 presents our S2TL templates for formulating the different requirement classes. Section 6 reports on our empirical comparison between time-domain and time-frequency-domain specifications. Section 7 discusses the implications of this work for software engineering researchers and practitioners. Section 8 discusses the related work. Finally, Section 9 concludes the paper. 2

BACKGROUND

In this section, we present the background on signal-based CPS requirements and their specification. First, we present an overview of the requirement classes based on two taxonomies from the literature [11, 28]. Second, we describe how signals are represented in the time, frequency, and time-frequency domains. Finally, we briefly illustrate STL and TFL, two state-of-the-art specification languages for expressing CPS requirements. 2.1

Signal-Based CPS Requirements

In the literature, two taxonomies of signal-based CPS requirements have been proposed based on applications in the automotive [28] and aerospace [11] domains. Table 1 lists the classes identified in the two works (left and centre columns). Despite the different context, the two taxonomies identify very similar classes, supporting their general validity across application domains. In this paper, we propose a “harmonised” classification (right column), with the nomenclature intended to , Vol. 1, No. 1, Article . Publication date: August 2026.

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

5

Table 1. Classes of signal-based CPS requirements proposed in the literature (left and centre columns), and their harmonization proposed in this paper (right column).

Boufaied et al. [11] UA TA FR TR SP OS SS RT OV ST

Data Assertion (Untimed) Data Assertion (Timed) Functional Relation Order Relation Spikes Oscillation (damped/driven) Rise/Fall Time Over/Under-shoot

Kapinski et al. [28]

Harmonised

Timed Relation Spikes (and glitches) Ringing Steady-State Error Rise/Fall Time Over/Under-shoot Settling Time

Untimed Data Assertion Timed Data Assertion Functional Relation Timed Relation Spikes Oscillation Steady-State Error Rise/Fall Time Over/Under-shoot Settling Time

unify previous taxonomies. Below, we briefly describe each class and give a representative example in the context of an aircraft control system. Untimed Data Assertion (UA): It specifies a constraint on the signal values that is expected to hold over time. Example: the desired altitude sent to the plane autopilot must always be at least 1000 m above ground level. Timed Data Assertion (TA): It specifies a constraint on signal values within specific time intervals. Example: the plane actual altitude shall remain above 1000 m from ground level from three minutes after takeoff until two minutes before landing. Functional Relation (FR): It captures a mathematical relation between two or more signals. Example: the fuel consumption of a plane shall be quadratic with the plane speed. Timed Relation (TR): It expresses precedence or response between events, values or signal patterns, possibly with constraints on the temporal distance of precedence or response. Example: if an aircraft pilot activates the autopilot, it must take full control of the aircraft within 10 s. Spike (SP): It is a sudden, short-lived and large change in signal values, typically undesired. Example: no spikes with an amplitude exceeding 100 V shall be sent to actuators. Oscillation (OS): It is the repetition of a pattern (e.g., sinusoidal or triangular) over a time period and around an average value. An oscillation may be damped (decreasing in amplitude) or driven (increasing in amplitude). Example: the plane yaw angle (informally, the direction of the plane “nose”) shall not exhibit oscillations with a period lower than 3 s for more than 10 s. Steady-State error (SS): It defines an upper bound of the steady-state error value, that is the difference between the desired value of a physical quantity and its actual one when the system is at steady state, i.e., when the two values have been constant for a while. Example: a plane cruising at constant altitude shall be at least within 10 m from the desired altitude. Rise/Fall Time (RT): It prescribes the time within which a physical signal should reach a value close to the desired one after a step-like change in the latter. It is usually defined as the time required for a signal to rise (or fall) from 10% to 90% of the step size [2]. Example: when a pilot issues a change in plane altitude from 8000 m to 10 000 m, the plane shall go from 8200 m to 9800 m within 180 s. Overshoot (OV): It prescribes how much the actual value can exceed the new desired value, after a step-like change in the desired value. Example: using the same scenario as for RT, the maximum , Vol. 1, No. 1, Article . Publication date: August 2026.

6

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

Frequency-Domain Representation

Time-Domain Representation

0 −0.5 −1

Frequency Hz

Magnitude

1

0.5

0.5 0

0 2 4 6 8 10 Time s

0

5 10 15 20 Frequency Hz

Fig. 1.a

Fig. 1.b

15

0.4

10

0.2

5 0

0 2 4 6 8 10 Time s

Magnitude

Amplitude

1

Time-Frequency-Domain Representation 20

0

Fig. 1.c

Fig. 1. Illustration of how a signal is represented in the time, frequency, and time-frequency domains.

accepted overshoot might be 20 m, meaning that, during the altitude change, the plane shall not go above 10 020 m. Settling Time (ST): It constrains the time it takes for a signal to enter and remain within a predefined range around its desired value after a step-like change. Example: using again the plane altitude example, it would be the time it takes for the plane to reach and stay within 10000 ± 10 m. 2.2

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

2.2.1 Time-Domain Representation of Signals. In the time domain, a signal is represented as a sequence of values over time [30]. Formally, given a time domain T, a signal 𝑠 is a function 𝑠 : T → R, where R is the set of real numbers. In this paper, we consider discrete-time signals, sampled at regular time intervals, and defined over a finite domain.1 This means that T is a finite set {𝑡 0, 𝑡 1 . . . 𝑡 max } of equally-spaced time values. The spacing dt = 𝑡𝑖 − 𝑡𝑖 −1 is called sampling time. In Figure 1.a, we show the time-domain representation of a signal that exhibits two temporary oscillations, the first with a period of 0.5 s in the interval [2s, 4s] and the second with a period of 0.166 s in the interval [6s, 8s], and that otherwise remains constant. As usual, the time-domain representation associates a signal value with each point in time. 2.2.2 Frequency-Domain Representation of Signals. In the frequency domain, a signal is represented as the sum of sinusoids of different frequencies.2 For each sinusoid—also called frequency component—this representation defines an amplitude and a phase, which can be represented as the modulus and phase of a complex number. This sequence of amplitudes and phases is called the signal’s frequency spectrum (or simply the spectrum), and is obtained from the time-domain representation using the Fourier transform F [·].3 Formally, given a frequency domain F, the Fourier transform of a signal 𝑠 is a function F [𝑠] : F → C, where C is the set of complex numbers. In the remainder of this paper, given the greater importance of the amplitude part of the spectrum compared to the phase part, when discussing the spectrum or specific frequency components of a signal in either the frequency or the time-frequency representation, we refer to their sole amplitudes, unless stated otherwise. In the case of discrete-time signals considered in this work, the 1 The assumption of a finite time domain is generally acceptable as most CPS applications have a time window within which

either the requirements are satisfied, or they will never be. 2 This section covers the fundamentals of Fourier analysis within the limits of what is needed for this work. A more complete discussion of Fourier analysis can be found in Bracewell [14]. 3We use the square brackets to distinguish transforms from functions. , Vol. 1, No. 1, Article . Publication date: August 2026.

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

7

frequency domain F is likewise discretised with equally spaced frequency values {0, 𝑓1, 𝑓2, . . . 𝑓max }. The spacing df = 𝑓𝑖 − 𝑓𝑖 −1 is the frequency resolution. When computing a spectrum using the Fourier transform, the sampling of the frequency axis (i.e., the frequency components used to represent the signal) is directly related to the sampling of the time axis of the original signal. Intuitively, a longer signal provides a better observation of slowly varying components. Formally, a longer signal (i.e., a signal with a larger 𝑡 max ) provides a higher frequency resolution, given by df = 1/𝑡 max . Conversely, the faster (i.e., more frequently) a signal is sampled, the better we can observe fast-changing (i.e., high-frequency) components. Specifically, the sampling interval dt determines the highest detectable frequency, according to the relation 𝑓max = 1/dt. At an intuitive level, the amplitude of a frequency component is a measure of how strongly the time-domain signal resembles the corresponding sinusoid. Accordingly, a slow-changing signal exhibit larger amplitudes for low-frequency components, while a fast-changing signal exhibit larger amplitudes for high-frequency components. This emphasis on how a signal changes, rather than on its values at individual time instants, makes the frequency domain well suited to concisely expressing properties related to signals shapes. On the other hand, the frequency domain hides the temporal localisation of signal features: it does not indicate when particular features occur within the signal. Intuitively, because each frequency component is a measure of similarity between the corresponding sinusoid and the signal as a whole, it is difficult to determine which specific portion of the signal gives rise to this component. For example, in Figure 1.b we show the frequencydomain representation of the signal introduced in the left-hand side plot. In this representation, the horizontal axis corresponds to the frequency components, and each frequency component is associated with an amplitude. The frequency spectrum of the signal exhibits two prominent spikes at 2 Hz and 6 Hz, corresponding to the inverse of the periods of the two oscillatory segments (representing sinusoids) in the signal. Although these peaks make the oscillations easy to identify, the spectrum alone does not reveal when they occur in the signal. Finally, in the frequency domain, when considering systems that transform input signals into output signals, it is often useful to compare the spectra of the input and output. In this context, a frequency component is said to be amplified if its amplitude is greater in the output than in the input, and attenuated (or filtered) if its amplitude is smaller. 2.2.3 Time-Frequency-Domain Representation of Signals. The time-frequency domain representation of a signal seeks to combine the ability of the frequency domain to capture shape-related features of a signal with the ability of the time domain to localise such features in time.4 In the timefrequency domain, a signal can be seen either as a sequence of spectra over time or, equivalently, as a set of signals describing the time-varying amplitudes of individual frequency components. This representation is obtained by applying a time-frequency transform W [·]. Formally, given a time domain T, and a frequency domain F, the time-frequency representation of a signal 𝑠 is a function W [𝑠] : T × F → C. Thus, for
a fixed time 𝑡¯, W [𝑠] (𝑡¯, 𝑓 ) is a frequency spectrum, whereas for a fixed frequency 𝑓¯, W [𝑠] 𝑡, 𝑓¯ is a signal representing the temporal evolution of that frequency component. There are numerous time-frequency representations of a signal, among which the most widely used are the Short-Time Fourier Transform (STFT), the Wavelet Transform (WT), and the WignerVille Distribution. The main differences between these representations concern (i) their frequency and time domain resolutions (i.e., the precise identification of individual frequency components, and their precise localisation in time, respectively), and (ii) the presence of artefacts known as cross-terms (i.e., interference artefacts that appear in the time-frequency representation between or around 4 The background presented in this subsection is based on Boashash [10].

, Vol. 1, No. 1, Article . Publication date: August 2026.

8

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

true signal components and do not correspond to actual physical features of the signal). Time and frequency resolutions are subject to an inherent trade-off arising from the Heisenberg uncertainty principle [17]. This means that, even theoretically, it is impossible to achieve arbitrarily high resolution in both domains simultaneously. Moreover, methods that provide high time-frequency resolution produce cross-terms. The presence of such terms may complicate the interpretation of the time-frequency representation and thus introduces an additional practical trade-off between their suppression and the achievable time and frequency resolutions. As a result, the choice of the appropriate time-frequency representation (precisely, the transform) is application-specific. In the remainder of this paper, we employ the STFT because it does not generate cross-terms, and is conceptually the closest extension of the Fourier transform; these properties make the STFT particularly straightforward to interpret as compared to other transforms.5 The STFT is based on the idea of “windowing” a signal with a kernel or window function to extract a local signal portion around a given point in time, and then applying the Fourier transform to obtain the local spectrum. The length and shape of the window function determine the resulting time-frequency resolution: a short window function provides higher time resolution, while a longer window provides higher frequency resolution. Further, the shape of the window determines how the signal samples are weighted and also influences the time-frequency resolution [41]. Common choices include rectangular and triangular windows: a rectangular window assigns equal weights to all the signal samples within the window, whereas a triangular window assigns greater weight to samples near its centre and linearly decreasing weight towards its edges. In general, a rectangular window offers better frequency resolution but is more prone to interference from nearby frequency components; conversely, a triangular window suppresses such interference more effectively, although this comes at the cost of reduced frequency resolution. Figure 1.c shows the time-frequency representation of the same signal as in the other two plots. In this example, we use the STFT with a triangular window of length 1 s. Since this representation is a function of both time and frequency, it is displayed as a two-dimensional colour map: the horizontal axis represents time, the vertical axis represents frequency, and the colour (according to the bar on the right) indicates the intensity of each frequency component at each point in time. From this plot, we can see that the time-frequency representation combines the benefits of both the time and frequency domains. In fact, it exhibits a first high-intensity (higher amplitudes) region in the time interval [2s, 4s] at 2 Hz, and a second one in the interval [6s, 8s] at 6 Hz. These regions correspond to the two oscillatory segments of the original signal, illustrating how the time-frequency representation simultaneously captures both the signal’s frequency content and time-locality of when the frequency components are present. 2.3

STL and TFL

2.3.1 STL (Signal Temporal Logic). The standard specification language for CPS is STL (Signal Temporal Logic) [30]. STL is based on Metric-Interval Temporal Logic (MITL) [1], a decidable fragment of Metric Temporal Logic (MTL) [29]. MTL extends Linear Temporal Logic (LTL) [42] with quantitative timing constraints. The syntax of MITL is: 𝜑 ::= 𝑝 |¬𝜑 |𝜑 1 ∨ 𝜑 2 |𝜑 1 U[𝑎,𝑏 ] 𝜑 2

(1)

where 𝑝 is a Boolean predicate, ¬ and ∨ denote logical negation and disjunction, respectively, and U[𝑎,𝑏 ] is the time-bounded until operator. STL extends MITL with predicates over signal values 𝜇1 (𝑥) , . . . 𝜇𝑛 (𝑥), with 𝜇𝑖 : R → B, which constitute the atomic propositions that the language builds upon. In practice, these predicates are typically inequalities involving signal values. During 5 It is important to note that alternative time-frequency representations can provide higher resolution when their associated

trade-offs are acceptable. , Vol. 1, No. 1, Article . Publication date: August 2026.

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

9

monitoring, the signal predicates can be used to translate signals into Boolean predicates, thereby allowing an STL formula to be interpreted as an MITL formula over time. Importantly, STL is used in one of the two CPS requirement taxonomies discussed in Section 2.1 to write formula templates capturing the different CPS requirement classes [28]. 2.3.2 TFL (Time-Frequency Logic). TFL (Time-Frequency Logic) further extends STL with predicates on the time-frequency representation of signals [23]. In practice, it introduces a set of operators that extract the amplitude of a given frequency from the
STFT of a signal. Using the notation from Section 2.2.3, these operators compute W𝑤,𝐿 [𝑠] 𝑡, 𝑓¯ , where 𝑓¯ is the frequency of interest, 𝑤 is the window shape, and 𝐿 is the window length. These operators enable a monitoring procedure
analogous to that of STL. For a given frequency 𝑓¯, the corresponding W𝑤,𝐿 [𝑠] 𝑡, 𝑓¯ operator defines a new time-domain signal whose value at each time instant is the amplitude of the corresponding frequency component. STL predicates 𝜇 can then be written on this derived signal, reducing the monitoring problem to that of evaluating the corresponding MITL formula. The original TFL paper applied the logic to the problem of identifying a musical melody within a song. Subsequent work [38] proposed a variant by replacing STFT with the WT, which offers higher time-frequency resolution, and applied it to the classification of abnormal data in a hydrogen fuel cell and an electrocardiogram. 3

CPS REQUIREMENTS IN THE FREQUENCY DOMAIN

In this section, we identify the classes of signal-based CPS requirements that can benefit from a frequency-domain representation of signals. Drawing on results from control theory [2], we describe how these requirement classes can be formalised using such representations. We conclude by defining a list of desiderata that a specification language should fulfill to support predicates over the time-frequency representation of signals. 3.1

Requirements Classes that Can Benefit from Using the Frequency-Domain

Among the requirement classes listed in Table 1, SP, OS, SS, RT, OV, and ST can benefit from the frequency-domain representation of signals. All of these classes define assertions about signal shapes, either for a single signal (SP and OS) or for the input and output signals of a CPS (SS, RT, OV, and ST). Specifically, SP and OS describe features that can appear in a signal shape. Conversely, SS, RT, OV, and ST describe the expected shape of the response of a physical quantity to a step-like change in its corresponding desired value. In other words, these requirements express an implication between a precondition on the set-point signal (namely, the presence of a step-like change) and a postcondition on the signal of the actual physical quantity. In the remainder of this paper, we refer to the SP and OS classes as the signal-feature requirement classes; and to the SS, RT, OV, and ST classes as the step-response requirement classes. In contrast, the remaining requirement classes (UA, TA, TR, and FR) generally may not benefit from a frequency-domain representation of signals. The main reason is that they specify properties directly in terms of signal values over time. Specifically, the UA and TA requirement classes define constraints on signal values. In practice, such constraints typically take the form of inequalities that must hold either at every point in time (for UA) or only within specific time intervals (for TA). Because these requirements directly define assertions on the time-domain values of a signal, they are most naturally specified using the time-domain representation of the signal. Among the remaining requirement classes, FR requirements can be seen as equality constraints between two signals, where one signal is generated by applying a function to another signal. For example, if the specification states that an aircraft’s fuel consumption should be quadratic to the speed, then the requirement is that the fuel consumption signal should be equal to the , Vol. 1, No. 1, Article . Publication date: August 2026.

10

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

Frequency Domain

Time Domain 1,000

1

500 0

1 0.5 0

SP

0.01

0 2 4 6 8 10 0.01 Fig. 2.a

Flat Spectrum

Matching Components

1 0.01

SS

0 2 4 6 8 10 time [s]

1

0.1

0.01

Fig. 2.c

0.1

1

frequency [Hz]

Frequency Domain

Time Domain 1 0 −1

OS

Spectrum Peak

0.01 0 2 4 6 8 10 0.01 Fig. 2.b OV

RT

0.01

ST

0 2 4 6 8 10 time [s]

1

0.1

1

1 0

1

𝑓𝑏 Amplified Component

0.01

Fig. 2.d

0.1

1

frequency [Hz]

Fig. 2. Illustration of the SP, OS, SS, OV, RT, and ST requirements in time and frequency domain.

signal obtained by squaring the speed signal. In practice, the equality between the two signals can be expressed as an inequality that constrains the difference between their values to lie within a prescribed tolerance. Because this comparison is performed directly on the signal values, the time-domain representation would be the most natural choice. In some specific cases, however, it may be beneficial to compare the signals in the frequency domain, for example to filter-out high-frequency noise or to remove low-frequency trends (i.e., to ignore differences in their average values). Since the usefulness of such an approach is application-dependent, we do not consider a frequency-domain specification of the FR requirement class in the scope of this work.6 Finally, TR requirements specify temporal relationships between events, signal values or signal patterns, and are therefore closely tied to the sequentiality of what they assert over time. In some applications, the “events and signal patterns” may be best captured using a frequency-domain representation. However, this affects only the definition of the atomic predicates, not the temporal relationships between them. Accordingly, we consider TR requirements to be most naturally expressed using the time-domain representation of signals. 3.2

Frequency-Domain Formulation of CPS Requirements

To illustrate how the requirements translate into the frequency domain, we use the representative signal traces in Figure 2. This figure shows four signals—a spike (Figure 2.a), a sinusoid (Figure 2.b), a CPS constant-input response (Figure 2.c), and a CPS step-input response (Figure 2.d)—each displayed in both the time (left) and frequency (right) domains. For the input-response requirements classes (Figure 2.c and Figure 2.d), the input signal is shown in black and the output signal in purple. The signal features relevant to assessing the requirements are highlighted in blue in both domains. SP: The defining feature of a spike is its sudden and large change in signal value. Such a rapid variation corresponds to large high-frequency components in the frequency domain. As shown in the right-hand plot of Figure 2.a, a spike exhibits a nearly “flat spectrum”, with the same amplitude across the frequency range, including the higher frequencies. Consequently, a requirement specifying 6 A frequency-domain formulation of FR requirements could be implemented using an approach similar to the one described

in §3.2 for SS requirements, where only selected frequency ranges of the two signals are compared. , Vol. 1, No. 1, Article . Publication date: August 2026.

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

11

the absence (or presence) of spikes can be reformulated in the frequency domain as an upper (or lower) bound on the amplitudes of the high-frequency components. Importantly, in the frequencydomain formulation, the requirement constrains any signal with large, rapid changes. This broader interpretation is often a desirable extension, as large and rapid signal changes can be harmful for hardware components or characterise sensor faults. OS: The frequency domain is well suited for identifying repeated signal patterns, as it is based on the representation of signals as sum of sinusoids, which are inherently periodic. As illustrated in Figure 2.b, a purely sinusoidal signal is translated to a sharp peak in the frequency spectrum. In general, periodic repetitions of any shape in the time-domain translate to sharp peaks in the frequency spectrum. Thus, assertions on the presence of oscillations in the time domain can be reformulated in the frequency domain as assertions on the presence of sharp peaks in the spectrum. Notably, detecting oscillations directly in the time domain typically requires comparing different parts of the signal or identifying recurring sequences of peaks and dips, making the analysis less straightforward. SS: A signal is in steady state when it maintains a constant value, typically after an initial transient (e.g., after a step-like change). In the left-hand plot of Figure 2.c, the desired-state signal (black) is constant, and therefore remains in steady state throughout the observation period. In contrast, the actual-state signal (purple) reaches steady state only after 5 s. From that point onward, the two signals are sufficiently close to satisfy the SS requirement, as shown by the dashed blue line. In the frequency domain, the constant desired-state signal contains only a low-frequency component (the component of amplitude 1 at 0.01 Hz), whereas the actual-state signal contains also some higher-frequency components which correspond to the initial transient oscillations. Therefore, to compare only the steady-state values and ignore the initial oscillations, we can compare the sole 0.01 Hz components of the two signals, and disregard the higher-frequency ones, as highlighted in the right-hand plot of Figure 2.c by the SS blue arrow. More generally, the SS requirements can be reformulated in the frequency domain as the matching of low-frequency components of the desired- and actual-state signals. Conversely, evaluating the same requirement in the time domain would require first distinguishing that the actual-state signal is at steady state only after 5 s, and then comparing the two signals only over that interval. OV: The OV requirement limits the extent to which the actual state can “overreact” to a change in the desired value. For example, in Figure 2.d, we observe that the actual-state signal (purple) temporarily exceeds the desired-state signal, as highlighted by the OV blue arrow. In the frequency domain, this overreaction manifests as an amplification of the frequency components of the actualstate signal relative to the corresponding components of the desired-state signal. Since such an amplification can happen during a transient, i.e., when the signals are changing, it concerns a higher frequency range. For example, in Figure 2.d, we observe that there is an amplified frequency component at 0.1 Hz. More generally, OV requirements can be defined in the frequency domain as constraints on the maximum allowed amplification between desired- and actual-state spectra. In the time domain, such requirements would involve first the identification of the transient (e.g., of the step change in the desired state and consequent change in the actual state), then the identification of the overshoot value, and finally its comparison with the accepted amplification. RT and ST: We discuss RT and ST together because both specify how quickly the actual state is expected to track a change in the desired state, and their frequency-domain formulations are closely related. In the time domain, the actual-state signal can be viewed as a “smoothed" version of the desired-state signal. For example, in Figure 2.d, the actual-state signal (purple) follows the step change of the desired-state signal (black), but with a gradual rather than abrupt transition. In the frequency domain, this smoothing corresponds to an attenuation of the high-frequency , Vol. 1, No. 1, Article . Publication date: August 2026.

12

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

components (i.e., a reduction in amplitude of the fast-changing part of the signal). In the spectrum shown in Figure 2.d, we highlight the so-called bandwidth 𝑓𝑏 , which is the frequency threshold above which we observe the signal attenuation. Below 𝑓𝑏 , we observe instead that the frequency components of the actual-state signal approximately match or exceed those of the desired-state signal. A large bandwidth corresponds to a fast tracking, as it indicates that higher-frequency components of the desired-state signal are found with equal or greater amplitude in the actual-state signal. Conversely, a small bandwidth indicates slow tracking, as larger part of the input signal is attenuated or filtered. Based on this observation, RT and ST requirements can be translated in the frequency domain as constraints on the value of 𝑓𝑏 . At times, for ST, this bandwidth constraint may also need to be combined with a constraint on the maximum amplification, since overshoot can induce oscillations that increase the settling time. On the contrary, in the time domain, similarly to OV requirements, ST and RT requirements involve first identifying the step-like transients, and then identifying the various thresholds that define the RT and ST (highlighted by the dashed lines in Figure 2.d). 3.3

Desiderata for a Frequency-Extended Logic

The qualitative discussion on the frequency-domain formulation of CPS requirements underlines that a specification language that predicates on the time-frequency representation of a signal must allow for (D1) assertions on frequency intervals of a signal’s spectrum, and (D2) logical predicates that relate corresponding frequency components in different signals. SP requirements require assertions over high-frequency ranges, SS over low-frequency ranges, and RT and ST requirements over a combination of the two to characterize the bandwidth 𝑓𝑏 . This motivates the need for assertions on frequency intervals. For OV requirements, we instead want to reason about the amplification between the desired- and actual-state signals. For example, we could formulate a predicate such as: “if a frequency component is present in the desired-state signal (i.e., it has a non-zero amplitude), then the corresponding component in the actual-state signal should not have a larger amplitude.” Such a requirement corresponds to a logical implication in the frequency dimension, i.e., an implication evaluated separately at each frequency of a given interval, and motivates the need for such logical relations. In TFL, these predicates would require their explicit formulation for each frequency component. Besides being tedious, such specifications are error-prone and impractical for real-world applications. This limitation motivates the need for a new specification language that provides native support for predicates over the frequency-domain representations of signals. Specifically, the language should enable concise expression of logical relations between corresponding frequency components of different signals and evaluate them over user-specified frequency intervals. 4

THE S2TL SPECIFICATION LANGUAGE

In this section, we introduce S2TL, a specification language designed to address the limitations of the state of the art discussed in Section 3.3. We define S2TL as an extension of STL with frequencydomain predicates. With these predicates, we pursue two objectives. First, we enable the encoding of logical relations between the spectra of one or more signals at a given point in time. Second, we enable the quantification of the frequency variable within specified frequency intervals. We first present the syntax of S2TL and then introduce its qualitative (Boolean) semantics. Finally, we present our implementation of the language as extension of the STL monitoring tool RTAMT, including some considerations about the monitoring complexity of the frequency predicates [40, 47]. , Vol. 1, No. 1, Article . Publication date: August 2026.

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

4.1

13

Syntax

Let T ⊂ R be the time domain and F ⊂ R be the frequency domain, S2TL is built on the following symbols and operators: • A set of signal symbols {𝑠 1, . . . , 𝑠𝑛 } where each 𝑠𝑖 is a function 𝑠𝑖 : T → R, • A set of signal-value constants 𝐶 = {𝑐 1, . . . , 𝑐𝑚 } in C, • A set of memoryless operators 𝑂 = {+, −, ·, abs () , . . . } over complex numbers, and • A time-frequency transform operator W [𝑠], of type (T → R) → (T × F → C). We consider two types of values and terms: time-domain and frequency-domain ones. We use Cyrillic letters throughout to distinguish frequency-domain values and terms from their timedomain counterpart. Specifically, we use the к (pronounced ka) to denote frequency-domain values and б (pronounced be) to denote frequency-domain terms. A time-domain value term may be a constant, a signal, or a value computed by applying an operator in 𝑂 to one or more time-domain value terms: 𝑣 ::= 𝑐 | 𝑠 | 𝑜 (𝑣 1, . . . , 𝑣𝑛 ) .

(2)

A frequency-domain value term may be a constant, the time-frequency transform of a signal, or a value computed by applying an operator in 𝑂 to one or more frequency-domain value terms: к ::= 𝑐 | W [𝑠] | 𝑜 (к1, . . . , к𝑛 ) .

(3)

We can then define frequency-domain predicates as Boolean combinations of inequalities over frequency-domain value terms: б ::= к1 >𝑎 к2 | к1 >𝑝 к2 | ¬б | б1 ∨ б2 .

(4)

Since the time-frequency transform of a signal is defined over the set of complex numbers, which is not naturally ordered, we define two different types of inequalities (>𝑎 and >𝑝 ), corresponding to comparisons based on amplitude and phase, respectively. Finally, in a similar fashion as for STL (Section 2.3.1), the entry points of S2TL (i.e., S2TL formulas) are formulas over time- and/or frequency-domain predicates, connected with Boolean operators and/or the until operator: 𝜑 ::= 𝑣 1 > 𝑣 2 | LбM

[ 𝑓𝑖 ,𝑓 𝑗 ]

| ¬𝜑 | 𝜑 1 ∨ 𝜑 2 | 𝜑 1 U[𝑡𝑖 ,𝑡 𝑗 ] 𝜑 2 ,

(5)

where 𝑣 expands based on Eq. 2 and б based on Eq. 4, and the time and frequency intervals are defined in the respective domains 𝑡𝑖 , 𝑡 𝑗 ∈ T and 𝑓𝑖 , 𝑓 𝑗 ∈ F. This syntax requires that every frequency predicate б is contained in the special parentheses L·M with an apex containing a frequency interval [𝑓𝑖 , 𝑓 𝑗 ]. In the remainder of the paper, we assume the standard definitions of the timed globally □ [𝑡𝑖 ,𝑡 𝑗 ] and eventually ^ [𝑡𝑖 ,𝑡 𝑗 ] operators in terms of the timed until operator, and the conjunction ∧ and implication ⇒ in terms of the logical connectives. 4.2

Qualitative Semantics

A trace 𝜏 is the interpretation of the signal symbols in {𝑠 1, . . . , 𝑠𝑛 } as functions over time, denoted as J𝑠𝑖 K𝜏 : T → R. The qualitative (Boolean) semantics of S2TL determines whether a trace 𝜏 satisfies a formula 𝜑 at a time instant 𝑡 ∈ T, denoted as (𝜏, 𝑡) |= 𝜑 and (𝜏, 𝑡) ⊭ 𝜑 otherwise. As in other linear temporal logics [25], a trace 𝜏 satisfies a formula 𝜑 if and only if (𝜏, 0) |= 𝜑. Given a trace 𝜏 and a time instant 𝑡, time-domain value terms are interpreted as follows: • constants evaluate to their corresponding values, independently of the trace and the time instant; • signal symbols evaluate to the value of the function defined by the trace 𝜏 at time 𝑡; and , Vol. 1, No. 1, Article . Publication date: August 2026.

14

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

• operators evaluate to the value obtained by applying the corresponding operator to the interpretations of their arguments. Formally, we denote the interpretation of a term for a given trace 𝜏 and time instant 𝑡 with J·K𝜏,𝑡 , and define it as J𝑐K𝜏,𝑡 = 𝑐

J𝑠K𝜏,𝑡 = J𝑠K𝜏 (𝑡)

(6) (7)

J𝑜 (𝑣 1, . . . , 𝑣𝑛 )K𝜏,𝑡 = 𝑜 J𝑣 1 K𝜏,𝑡 , . . . , J𝑣𝑛 K𝜏,𝑡 .

(8)

Frequency-domain values are instead interpreted, for a given trace and time instant, as functions of a frequency variable 𝑓 : • constants evaluate to their corresponding values, independently of the trace, the time instant, and the frequency; • time-frequency transform symbols evaluate to the spectrum W [𝑠𝑖 ] (𝑡, 𝑓 ), where 𝑡 is the time instant at which the value is interpreted and 𝑓 is a free frequency variable (that moves along the spectrum); and • operators evaluate pointwise over the frequency domain, that is, for each frequency value they evaluate to the result of applying the corresponding operator to the interpretations of their arguments at that frequency. Formally, we denote by J·K𝜏,𝑡 (𝑓 ) : F → C the interpretation of a frequency-domain value term for a given trace 𝜏 and time instant 𝑡 , defined as: J𝑐K𝜏,𝑡 (𝑓 ) = 𝑐

JW [𝑠]K𝜏,𝑡 (𝑓 ) = W𝑡 [J𝑠K𝜏 ] (𝑓 )

(9) (10)

J𝑜 (к1, . . . , к𝑛 )K𝜏,𝑡 (𝑓 ) = 𝑜 Jк1 K𝜏,𝑡 (𝑓 ) , . . . , Jк𝑛 K𝜏,𝑡 (𝑓 ) ,

(11)

where the frequency-domain value terms in Eq. 10 use the “time-curried” version of the signal’s time-frequency transform W𝑡 [𝑠] : F → C, defined as W𝑡 [𝑠] (𝑓 ) = W [𝑠] (𝑡, 𝑓 ). We can now define the satisfaction of the frequency-domain predicates with respect to the frequency variable 𝑓 . We denote with (𝜏, 𝑡) |= 𝑓 б that trace 𝜏 at time instant 𝑡 satisfies the formula 𝜑 for the frequency value 𝑓 , and (𝜏, 𝑡) ⊭ 𝑓 𝜑 otherwise. We then define the semantics of the frequency predicates as

(𝜏, 𝑡) |= 𝑓 к1 >𝑎 к2 ⇐⇒ abs Jк1 K𝜏,𝑡 (𝑓 ) > abs Jк2 K𝜏,𝑡 (𝑓 )

(𝜏, 𝑡) |= 𝑓 к1 >𝑝 к2 ⇐⇒ arg Jк1 K𝜏,𝑡 (𝑓 ) > arg Jк2 K𝜏,𝑡 (𝑓 )

(13)

(𝜏, 𝑡) |= 𝑓 б1 ∨ б2 ⇐⇒ (𝜏, 𝑡) |= 𝑓 б1 ∨ (𝜏, 𝑡) |= 𝑓 б2,

(15)

(𝜏, 𝑡) |= 𝑓 ¬б ⇐⇒ (𝜏, 𝑡) ⊭ 𝑓 б

(12) (14)

where Eq.s 12 and 13 compare respectively the amplitudes (with the function abs (·)) and phases (with the function arg (·)) of two complex values. In the remainder of the paper, when the subscript 𝑎 or 𝑝 is omitted from a frequency domain predicate, we implicitly refer to the comparison of the amplitudes—i.e., > is interpreted as >𝑎 . , Vol. 1, No. 1, Article . Publication date: August 2026.

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

15

Finally, we define the semantics of S2TL formulas as follows: (𝜏, 𝑡) |= 𝑣 1 > 𝑣 2 ⇐⇒ J𝑣 1 K𝜏,𝑡 > J𝑣 2 K𝜏,𝑡

(𝜏, 𝑡) |= LбM

[ 𝑓𝑖 ,𝑓 𝑗 ]

(16)

⇐⇒ ∀𝑓 ∈ [𝑓1, 𝑓2 ] (𝜏, 𝑡) |= 𝑓 б

(17)

(𝜏, 𝑡) |= ¬𝜑 ⇐⇒ (𝜏, 𝑡) ⊭ 𝜑

(𝜏, 𝑡) |= 𝜑 1 ∨ 𝜑 2 ⇐⇒ (𝜏, 𝑡) |= 𝜑 1 ∨ (𝜏, 𝑡) |= 𝜑 2 ′

(18) (19) ′

′′

′

′′

(𝜏, 𝑡) |= 𝜑 1 U[𝑡𝑖 ,𝑡 𝑗 ] 𝜑 2 ⇐⇒ ∃𝑡 ∈ [𝑡 + 𝑡𝑖 , 𝑡 + 𝑡 𝑗 ], (𝜏, 𝑡 ) |= 𝜑 2 ∧ ∀𝑡 ∈ [𝑡, 𝑡 ], (𝜏, 𝑡 ) |= 𝜑 1 .

(20)

Importantly, the terms in Eq. 17 define the interpretation of the frequency variable 𝑓 and universally quantify it to any value in the interval [𝑓1, 𝑓2 ]. Consequently, they implement a logical and operator along the frequency axis, meaning that the frequency-domain predicate is satisfied if and only if it holds for every frequency value in the specified interval. By the standard duality between universal and existential quantification, existential requirements can be expressed by negating the corresponding frequency-domain predicate.7 In summary, the evaluation of frequency predicates over frequency intervals, as defined by the semantics in Eq. 17, implements the desideratum (D1) described in Section 3.3. The frequency-domain predicates defined in Eq. 4 enable the specification of logical relations between corresponding frequency components in the the spectra of one or more signals, which fulfils desideratum (D2). For example, we can now write the example requirement mentioned in Section 3.3—which states that, if a frequency component is present in the desired-state signal 𝑟 , then the corresponding component in the actual-state signal 𝑥 should have a smaller amplitude—with the formula □ [0,𝑡max ] LW [𝑟 ] >𝑎 th ⇒ W [𝑥] <𝑎 W [𝑟 ] M

[ 𝑓1 ,𝑓2 ]

.

(21)

In this formula, starting from the left, the always operator □ [0,𝑡max ] requires the frequency predicate, [ 𝑓1 ,𝑓2 ]

i.e., the predicate contained in L·M , to hold at every time step. At a given time step 𝑡, the frequency predicate is satisfied if, for every frequency 𝑓 in the interval [𝑓1, 𝑓2 ], whenever the amplitude of a frequency component is greater than the given threshold th, i.e., abs (W [𝑟 ] (𝑡, 𝑓 )) > th, the corresponding output component W [𝑥] (𝑡, 𝑓 ) is smaller, i.e., abs (W [𝑟 ] (𝑡, 𝑓 )) > abs (W [𝑥] (𝑡, 𝑓 )). The ability to express implications between different frequency components and evaluate them over the frequency interval [𝑓1, 𝑓2 ] showcases how S2TL satisfies our desiderata. 4.3

S2TL Implementation and Monitoring Complexity

To have an executable semantics of S2TL, we extended RTAMT [40, 47], a state-of-the-art robustness monitoring tool for STL written in Python. Specifically, we implemented a discrete-time offline S2TL qualitative monitor.8 The discrete-time monitoring matches the application to sampled signals, while the offline monitoring circumvents the acausal (i.e., not causal) nature of the time-frequency transform (i.e., its dependency on future values of the signal).9 In practice, we extended RTAMT to support the frequency predicates of Eq. 17. This required extending the parser to recognize the new syntax and implementing the corresponding semantics [𝑓 ,𝑓 ]

LбM 𝑖 𝑗 , which requires б to hold at every frequency in [ 𝑓𝑖 , 𝑓 𝑗 ] (the universal [𝑓 ,𝑓 ] quantification), we can write the formula ¬L¬бM 𝑖 𝑗 to require that б holds for at least one frequency in [ 𝑓𝑖 , 𝑓 𝑗 ] (the

7 Concretely, starting from the formula

existential quantification). 8We used the Microsoft M365 Copilot Chat powered by the GPT-5 chat model to sketch individual functions, create templates of Python modules, and debug code. 9 The acausal nature of the time-frequency transform does not imply that there cannot be an online monitor for S2TL formulas. However, such a monitor would incur an intrinsic delay that depends on the chosen time-frequency transform. We leave the study of online monitoring for S2TL —or, more generally, for languages based on the time-frequency representation of signals—to future work. , Vol. 1, No. 1, Article . Publication date: August 2026.

16

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

(Eqs 9–15). To evaluate frequency-domain predicates, the specification object is associated with a user-provided time-frequency transform. During monitoring, when a frequency predicate is encountered, the monitor computes the time-frequency representation of the signals, checks the predicate over the specified frequency interval and produces a Boolean verdict. Then, the remainder of the formula can be treated as a standard STL one. Although a thorough complexity analysis of S2TL is outside the scope of this work, we observe that the cost associated with the frequency dimension depends on the chosen time-frequency transform. Intuitively, the introduction of frequency-domain predicates adds an additional frequency dimension to the monitored data. Intuitively, after applying a time-frequency transform, a signal of size |T| is represented over a domain of size |T| · |F|. Consequently, monitoring frequency predicates incurs additional computational and memory costs compared to standard STL monitoring. However, for each frequency predicate, we note that the relevant frequency range is known statically from the specification (i.e., the interval [𝑓1, 𝑓2 ] in Eq. 17). Consequently, in our implementation, we restricted the monitoring to the frequency components within this interval, reducing the effective size of the monitored representation from |T| · |F| to |T| · | [𝑓1, 𝑓2 ] |. In practice, we found that the additional overhead introduced by the frequency dimension did not significantly affect the experiments reported in Section 6. As further discussed below, the overall computational cost was dominated by the size of the experimental campaign, namely the number of traces and formula to be monitored. 5

EXPRESSING SIGNAL-BASED CPS REQUIREMENTS IN S2TL

In this section, building on the qualitative discussion in Section 3.2, we use S2TL to define templates for the requirement classes that benefit from the time-frequency domain representation of signals. Throughout the formulas, we use the following naming conventions for the recurring signals and constant values: • 𝑥 denotes the CPS output signal in the step-response requirements, i.e., the actual physical state, or the sole signal in the signal-feature requirements; • 𝑟 denotes the CPS input signal in the step-response requirements, i.e., the desired physical state; • 𝑒 denotes the control error signal, defined as 𝑒 = abs (𝑟 − 𝑥); and • 𝑓𝑏 denotes the expected system bandwidth (defined in Section 3.2, when discussing the RT and ST requirements). 5.1

Signal-Feature Requirements

5.1.1 Spike. SP requirements often concern the presence of large high-frequency components in a signal. In the context of CPS, “high-frequency” generally refers to frequencies above the system bandwidth. Accordingly, we constrain the existence of components whose frequencies exceed the expected system bandwidth. The corresponding S2TL formula for detecting a spike is: □ [0,𝜏 ] ¬LW [𝑥] < spM

[ 𝑓min ,𝑓max ]

,

(22)

where • 𝜏 is the minimum duration of the spike to be considered, • sp is the amplitude threshold above which a frequency component is considered large, and • 𝑓min , with 𝑓min > 𝑓𝑏 , is determined by the maximum duration of the spike that we want to consider, as longer spikes require lower-frequency components to be detected. 5.1.2 Oscillation. OS requirements concern the presence of oscillatory behaviour. In the frequency domain, an oscillation appears as a spike in the spectrum. Accordingly, we define an assertion on , Vol. 1, No. 1, Article . Publication date: August 2026.

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

17

the presence of an oscillation with frequency 𝑓𝑜 by requiring that at least one frequency component in the vicinity of 𝑓𝑜 exceeds a minimum amplitude threshold, while neighbouring frequency components remain sufficiently smaller. The resulting S2TL formula is:10 ¬LW [𝑥] < osM

[ 𝑓𝑜 −𝛿,𝑓𝑜 +𝛿 ]

∧ LW [𝑥] < 𝜈 M

[ 𝑓𝑜 −𝛼,𝑓𝑜 −𝛿 ]

∧ LW [𝑥] < 𝜈 M

[ 𝑓𝑜 +𝛿,𝑓𝑜 +𝛼 ]

,

(23)

where • os is the minimum amplitude threshold for the oscillation, • 𝛿 defines the frequency interval around 𝑓𝑜 within which the oscillation is detected, • 𝜈 is the threshold below which neighbouring frequency components are considered lowamplitude components (should be set as a fraction of os), and • 𝛼, with 𝛼 > 𝛿, defines the frequency interval around 𝑓𝑜 in which neighbouring frequency components are required to remain below 𝜈. 5.2

Step-Response Requirements

5.2.1 Steady-State Error. SS requirements are defined as an implication, in which the precondition is that the system is in steady state (i.e., the signals are approximately constant), and the postcondition is that the desired and actual physical states match within a specified tolerance. To express the precondition, we require that the high-frequency components of the input signal have small amplitudes. These components capture rapid variations in the signal; therefore, when they are sufficiently small, the signal can be considered to be in steady state. To express the postcondition, we require that the low-frequency components (i.e., the slowly varying part) of the error signal—i.e., the difference between input and output—also have small amplitudes. We distinguish low- and high-frequency components as those below and above the expected system bandwidth 𝑓𝑏 .11 The resulting S2TL formula is:   [ 𝑓𝑏 ,𝑓max ] [0,𝑓𝑏 ] □ [0,𝑡max ] LW [𝑟 ] < ssth M ⇒ LW [𝑒] < 𝑒 max M , (24)

where • ssth is the threshold value for the high-frequency components of the spectrum above which the signal is not considered to be in steady state, and • 𝑒 max is the maximum acceptable steady-state error.

5.2.2 Overshoot. OV requirements constrain the extent to which an input frequency component can be amplified in the output. Accordingly, we formulate them as an implication between a precondition capturing the presence of a frequency component in the input, and a postcondition that constrains its amplification in the output. The precondition specifies a lower bound on the amplitude of an input frequency component, while the postcondition defines an upper bound on the allowable amplification of the corresponding output component. Since the amplification usually concerns the spectrum around the bandwidth, we limit the predicate to a frequency interval around 𝑓𝑏 . The resulting S2TL formula is:

where

□ [0,𝑡max ] LW [𝑟 ] > ov th ⇒ W [𝑥] < ov amp · W [𝑟 ] M

[ 𝑓𝑏 −𝛿,𝑓𝑏 +𝛿 ]

,

(25)

10 The reported formula includes only a lower bound on the amplitude of the oscillation through ¬ W [𝑥 ] < os [𝑓𝑜 −𝛿,𝑓𝑜 +𝛿 ] . It

L

M

[𝑓 −𝛿,𝑓 +𝛿 ]

𝑜 can be extended to include an upper bound by replacing this constraint with ¬L W [𝑥 ] < osmin ∨W [𝑥 ] > osmax M 𝑜 . 11 This formulation can be somewhat restrictive, as it constrains the entire frequency ranges below and above 𝑓 for the input 𝑏 and output signals. In some applications, a less restrictive assessment of this requirement may be obtained by excluding a small frequency band around 𝑓𝑏 , for example by using the intervals [ 𝑓𝑏 + 𝛿, 𝑓max ] and [0, 𝑓𝑏 − 𝛿 ] instead.

, Vol. 1, No. 1, Article . Publication date: August 2026.

18

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

• ov th is the threshold used to identify relevant frequency components in the input spectrum, • ov amp is the maximum allowable amplification of the spectrum (e.g., 1.1 corresponds to an OV of 10%), and • 𝛿 defines the width of the frequency interval centred at the system bandwidth. 5.2.3 Rise Time. RT requirements are expressed in terms of the system bandwidth. The system bandwidth defines a frequency threshold below which the output is expected to accurately track the input (i.e., same frequency components in the input and output) and above which input frequency components should be attenuated. Accordingly, we formulate RT requirements as the conjunction of two frequency-domain predicates, capturing the low- and high-frequency ranges. For the lowfrequency tracking, we use a predicate similar to that of the SS requirements. However, because the system is not assumed to be at steady state, we allow a larger tracking error; thus a higher threshold for the allowable error. For the high-frequency attenuation, we use a predicate similar to that of the OV requirements, consisting of a precondition that captures the presence of a frequency component in the input, and a postcondition that requires the corresponding output component to have a smaller amplitude. Since frequency components around the system bandwidth may exhibit amplification, as discussed for the OV requirements, we exclude a frequency interval around the bandwidth from both predicates. The resulting S2TL formula is □ [0,𝑡max ]



LW [𝑒] < 𝑒lf M

[0,𝑓𝑏 −𝛿 ]

∧ LW [𝑟 ] > rt th ⇒ W [𝑥] < W [𝑟 ] M

[ 𝑓𝑏 +𝛿,𝑓max ]



,

(26)

where • 𝑒 lf is the maximum allowable low-frequency tracking error at all times, and • 𝛿 defines the width of the frequency interval around the system bandwidth that is excluded from the predicate. 5.2.4 Settling Time. ST requirements can be formulated as a combination of bandwidth and overshoot constraints. To avoid a repetition of the RT and OV requirements, we propose a slightly modified formulation of the ST requirements, that leverages a combination of time-domain and frequency-domain predicates. The original requirement constrains the time the output takes to reach and remain within a specified tolerance of the input. In contrast, our formulation constrains the time required for the output to reach steady state after a change in the input. This can be naturally expressed using the “until” operator together with predicates that characterize whether the input and output are in steady state. Specifically, whenever the input has remained at steady state for at least the settling time, the output is required to have also reached steady state, unless the input leaves the steady state before the settling time elapses. As for the SS requirements, we formulate the steady-state condition by constraining the amplitude of high-frequency components. The resulting S2TL formula is □ [0,𝑡max ]



[ 𝑓 ,𝑓

]



[ 𝑓 ,𝑓

]

[ 𝑓 ,𝑓

LW [𝑟 ] < 𝑠𝑠𝑡ℎ_𝑟 M 𝑏 max U[0,ST ] LW [𝑥] < 𝑠𝑠𝑡ℎ_𝑥 M 𝑏 max ∨ LW [𝑟 ] > 𝑠𝑠𝑡ℎ_𝑟 M 𝑏 max

]



, (27)

where • ST is the prescribed settling time, and • ssth is the threshold on the amplitude of high-frequency components above which the signal is not considered to be in steady state. This threshold is potentially different for the input and output signals, as the output can be affected by measurement noise. , Vol. 1, No. 1, Article . Publication date: August 2026.

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

6

19

EVALUATION

In this section, we compare the ability of the time and time-frequency domains to express signalbased requirements for CPSs. First, we evaluate the applicability of the two domains, namely, their ability to formulate step-response specifications that are applicable to a larger set of traces. As discussed in Section 3.1, step-response requirements are expressed as the combination of a precondition and a postcondition. When the precondition is not satisfied, the specification yields a trivial verdict—either positive or negative, depending on how the specification is formulated. Second, we evaluate the fidelity of the two domains, i.e., their ability to express the intended signal property. For example, RT and ST requirements constrain how quickly the output tracks the input. We therefore investigate whether the corresponding specifications are able to actually distinguish between systems with sufficiently fast responses and those with slower dynamics. Third, we evaluate the monitoring tolerance to signal noise of the two domains, that is, the ability of the monitoring to provide consistent verdicts in presence of signal noise. We express these three objectives with the following Research Questions (RQs): RQ1 Broader Applicability: What is the degree of applicability of the step-response requirements expressed in the time and time-frequency domains? RQ2 Expression Fidelity: What is the degree of fidelity to the intrinsic signal property of the requirements expressed in the time and time-frequency domains? RQ3 Noise Tolerance of Monitoring: What is the monitoring tolerance to signal noise of requirements expressed in the time and time-frequency domains? 6.1

Setup

To answer our research questions, we need (i) test subjects to generate CPS input and output traces, (ii) input traces to exercise the test subjects, and (iii) specification languages, templates and monitors for expressing and checking the various classes of requirements. 6.1.1 Test Subjects. As test subjects, we consider two representative CPSs: a drone and a lightweight aircraft. Since our specifications are defined over a single input-output pair, for the drone, we consider only the one-dimensional longitudinal dynamics rather than the full three-dimensional position. Consequently, each test input specifies a desired back-and-forth movement of the drone, while the corresponding output is its actual longitudinal position. To generate the traces, we use a simulation model of the Crazyflie drone, which has been shown in previous work to accurately reproduce the behaviour of the actual drone [31]. For the lightweight aircraft, we use a publicly available simulation model developed by MathWorks, which has been also been adopted in previous software testing research [32].12 The model includes an altitude controller. Accordingly, each test input consists of a sequence of desired altitudes, and the corresponding output is the aircraft’s actual altitude. In addition to the drone and lightweight aircraft, answering RQ2 requires systems that intrinsically satisfy or violate the considered step-response requirements. To obtain such systems, we rely on results from control theory, which provide analytical relationships between the parameters of linear system models and standard step-response characteristics. Specifically, we use the formulas reported by Astrom and Murray [2, Table 7.1, ch. 7, pg. 20], which explicitly relate between the model parameters to the values of SS, RT, OV, and ST. Using these formulas, we can systematically generate systems that intrinsically either satisfy or violate a given requirement by construction. Importantly, whether a system satisfies a requirement is independent of the specific input signal. This 12 https://nl.mathworks.com/help/aeroblks/lightweight-airplane-design.html

, Vol. 1, No. 1, Article . Publication date: August 2026.

20

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

allows us to generate multiple input-output traces from the same system, all of which consistently satisfy or violate the requirement. 6.1.2 Generation of Input Traces. To generate input traces, we use two complementary approaches. First, we generate traces that contain only a single step-like change in the input. These traces are important because they match the input shape assumed in the definition of the step-response requirement classes. Second, we generate traces that are representative of those produced by stateof-the-art CPS testing approaches. Specifically, we randomly sample control points—i.e., time and value pairs—and then interpolate between them using different interpolation methods [7, 27, 33, 34]. We consider three interpolation methods: linear interpolation (the signal changes linearly between two consecutive control points), constant interpolation (the signal value is held constant until next control point), and alternated interpolation (the signal changes linearly during first half of the interval between two control points and remains constant during the second half). 6.1.3 Specification Languages and Templates. To compare the expression of CPS requirements in the time and time-frequency domains, we use the specification language STL*, proposed in Brim et al. [15], and S2TL, introduced in this work. STL* extends STL (presented in Section 2.3.1) with a signal-value-freezing operator. Simply put, this operator enables the comparison of values of the same signal at different points in time. For the time-domain representation of signals, we choose STL* both because it is the standard language for specifying CPS properties, and because Kapinski et al. [28] provides templates for the requirement classes considered in this work.13 Below, we report the STL* formulas templates as used in our empirical evaluation. These are adapted from the STL templates proposed by Kapinski et al. [28]. We remark that in the original work [28], the formulas of the step-response requirements are written to be satisfied when a violation occurs. To simplify the comparison with the formulas presented in Section 5, here, we instead report equivalent formulas that are satisfied when the corresponding requirement is satisfied, documenting the changes that we applied. In the formulas below, we use the same conventions as in Section 5: 𝑟 is the input signal, 𝑥 is the output signal, and 𝑡 max is the total signal duration. SP: To detect spikes, we use the same formula proposed by Kapinski et al. [28] ^ [0,𝑡max ] ((𝑥¤ > 𝑚) ∧ ^ [0,𝑤 ] (𝑥¤ < −𝑚)),

(28)

where • 𝑥¤ is the discrete derivative of the signal computed as (𝑥 − prev(𝑥))/dt using the prev operator that returns the value of a variable at the previous time step, • 𝑤 is related to the spike width, and • 𝑚 · 𝑤 is proportional to the spike amplitude. OS: To detect oscillations, the formula proposed by Kapinski et al. [28] provides only an upper bound to the oscillation period. We use instead a formula adaptation that allows both upper and lower bounds on the period ^ [0,𝑡max ] (up ∧ ^ [2𝑑 −𝜀,2𝑑+𝜀 ] down),

(29)

where • up and down are respectively defined as ∗𝑑 𝑥 − 𝑥 > 𝑎 and 𝑥 − ∗𝑑 𝑥 > 𝑎, using the signal-valuefreezing operator ∗𝑑 from STL* to access the future value 𝑥 (𝑡 + 𝑑) at time 𝑡 • 𝑎 defines the minimum amplitude of the oscillation, 13 Strictly speaking, the authors of Kapinski et al. [28] use plain STL. However, in the OS specification, they assume access

to the value of a signal after a given number of time steps. To support this assumption while also obtaining more general versions of the formulas, we instead use STL* [15]. , Vol. 1, No. 1, Article . Publication date: August 2026.

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

21

• 4𝑑 corresponds to the oscillation period, and • 𝜀 is a small number used to have some margin in the assessment of the period.

Compared to the original formula, we changed the time interval of the ^ [2𝑑 −𝜀,2𝑑+𝜀 ] , which in the original paper is ^ [0,2𝑑 ] . This introduces a tighter bound in the distance between the up and down predicates, thus allowing a more precise specification of the period. SS: To check the SS requirement, we use the formula proposed by Kapinski et al. [28] and simply negate it
¬^ [0,𝑡max ] (abs (𝑟¤) < 𝜀 ∧ abs (𝑥) ¤ < 𝜀)U[𝜏,𝜏+𝛿 ] 𝑒 > 𝑒 max , (30) where • 𝑟¤ and 𝑥¤ are the input and output derivatives, defined as above, • 𝜀 is the derivative threshold below which the input and output are considered constant, • 𝜏 is the expected settling time, i.e., the time after which the output is expected to have reached steady state. The interval [𝜏, 𝜏 + 𝛿] defines the observation window over which the steady-state error is evaluated. • 𝑒 max is the maximum allowable steady-state error. OV: To check the OV requirements, we use the formula proposed by Kapinski et al. [28] and negate the constraint after the step detection. The adapted formula is ^ [0,𝑡max ] (step(𝑟 ) ∧ □ [0,𝜏 ] 𝑒 < ov max ),

(31)

where • step(𝑟 ) = abs (𝑟 − prev(𝑟 )) > 𝜎 checks whether a step-like change of amplitude at least 𝜎 has occurred in the input signal 𝑟 , • 𝜏 is the expected settling time. • ov max is the maximum allowable overshoot, usually computed proportionally to the step size, e.g., ov max = 0.2step_size(𝑟 ) corresponds to allowing a 20% overshoot with respect to the step size step_size(𝑟 ) = 𝑟 − prev(𝑟 ).

Compared to the original work [28], we changed □ [0,𝜏 ] 𝑒 < ov max , that negates the original ^ [0,𝜏 ] 𝑒 > ov max . RT: To check the RT requirements, we use the formula proposed by Kapinski et al. [28] and negate the constraint after the step detection. The adapted formula is ^ [0,𝑡max ] (step(𝑟 ) ∧ ^ [0,RT ] 𝑥 > 0.75 · step_size(𝑟 )),

(32)

where • RT is the required rise time, and • 0.75step_size(𝑟 ), using the same definition of step_size(𝑟 ) as above, is the threshold at which the rise time is checked.14 As remarked above, compared to the original work [28], we changed ^ [0,RT ] 𝑥 > 0.75 · step_size(𝑟 )), that negates the original □ [0,RT ] 𝑥 < 0.75 · step_size(𝑟 )). Further, we note that Eq. 32 implicitly assumes that the baseline output value before the step is zero (or has been de-trended to zero), we discuss the implications of this implicit assumption for our results in the threats to validity 6.6.1. 14 This definition measures the rise time from 0% to 75% of the step size. As described in Section 2.1, the standard definition

measures the rise time between 10% and 90% of the step size. Intuitively, the two quantities are closely related and can be converted approximately using the relation 𝑅𝑇0−75% ≈ 0.65𝑅𝑇10−90% . , Vol. 1, No. 1, Article . Publication date: August 2026.

22

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

ST: To check the ST requirements, we use the formula proposed by Kapinski et al. [28] and negate the constraint after the step detection. The adapted formula is ^ [0,𝑡max ] (step(𝑟 ) ∧ □ [ST,2ST ] (𝑒 < 𝛽step_size(𝑟 ))),

(33)

where • 𝛽 specifies the allowable error band once the settling time has elapsed, expressed as a fraction of the input step size, and • ST is the required settling time.

Compared to the original work [28], the modified part is □ [ST,2ST ] (𝑒 < 𝛽step_size(𝑟 )), that negates the original ^ [ST,𝑡max ] (𝑒 > 𝛽 · step_size(𝑟 )). Besides the negation, we also changed the time interval of the temporal operator from [𝑆𝑇 , 𝑡 max ] to [ST, 2ST ]. This makes the adapted formula more general, as it does not need to assume that the signal remains unchanged after the step. For the time-frequency domain part of the experiments, we choose S2TL, proposed in this work, together with the formula templates presented in Section 5. Using S2TL requires selecting a timefrequency transform. In our experimental evaluation, as discussed in Section 2.2.3, we use the STFT because it is simple and easy-to-interpret. When using the STFT, both the window function and window length must be specified. Since these parameters directly affect the semantics of the formulas, they must be chosen according to the application. Accordingly, the methodology for each RQ discusses the selected window shapes and lengths. 6.1.4 Monitoring Tool. To monitor the traces, we use the extended version of RTAMT [40, 47] presented in Section 4.3, which supports the monitoring of both STL* and S2TL. In this way, we use the same monitoring framework for both STL* and S2TL formulas, ensuring a fair comparison. 6.1.5 Settings. We ran the experiments on a MacBook Pro with M1 chip and 32 GB of memory running macOS 26 and Python 3.12.13. The experiments took around 14.5 h. 6.1.6 Data Availability. We provide a replication package containing (i) the extension of RTAMT presented in Section 4.3, (ii) the test subjects, (iii) the Python modules to generate the input traces and monitor them, and (iv) the scripts to run all the experiments.15 The self-contained replication package is available to the reviewers through this private link at: https://figshare.com/s/ 6efbb1ac0fe946381275. Upon paper acceptance, we will upload the code in a long-term archive and include its DOI. 6.2

RQ1: Broader Applicability

6.2.1 Methodology and Parameters Settings. To answer this RQ, we assess how many CPS testinput traces satisfy the preconditions of the step-response requirements. To this end, we generated test-input traces for our drone and lightweight aircraft test subjects using the input shapes discussed in Section 6.1.2. We then evaluated whether these traces satisfy the corresponding specification preconditions. For the time-domain specifications, the precondition is identical for the ST, OV, and RT requirements: the input must exhibit a step-like change. We verified this by monitoring the formula ^ [0,𝑡max ] abs (𝑟 − prev(𝑟 )) > 𝜎 (34) over the input signal 𝑟 . This formula corresponds to the definition of step(𝑟 ) introduced in Section 6.1.3. The SS requirement has a different precondition: the input trace must satisfy the input 15We used the Microsoft M365 Copilot Chat powered by the GPT-5 chat model to create script templates, write individual

functions, generate helper scripts, and debug code. , Vol. 1, No. 1, Article . Publication date: August 2026.

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

23

component of the first operand of the until operator. We verified this by monitoring the formula ^ [0,𝑡max ] □ [0,𝜏 ] abs (𝑟¤) < 𝜀.

(35)

For the time-frequency-domain specifications, the precondition differs across requirement classes. For SS, we checked that the input is at steady state by verifying that the amplitude of the highfrequency components remains below a threshold: ^ [0,𝑡max ] LW [𝑟 ] < ssth M

[ 𝑓𝑏 ,𝑓max ]

.

(36)

For OV, we checked that at least one input frequency component around the bandwidth is sufficiently large to trigger a transient response in the CPS, thereby enabling the assessment of overshoot: ^ [0,𝑡max ] ¬LW [𝑟 ] < ov th M

[ 𝑓𝑏 −𝛿,𝑓𝑏 +𝛿 ]

.

(37)

Similarly, for RT, we checked that at least one high-frequency component above the bandwidth is sufficiently large to enable the assessment of high-frequency filtering: ^ [0,𝑡max ] ¬LW [𝑟 ] < rt th M

[ 𝑓𝑏 +𝛿,𝑓max ]

.

(38)

Finally, for ST, we checked that the input remains at steady-state for at least the settling time: ^ [0,𝑡max ] □ [0,ST ] LW [𝑟 ] < ssth_r M

[ 𝑓𝑏 +𝛿,𝑓max ]

.

(39)

Appendix A.1 reports the parameters values used in the precondition formulas and explains how we selected each value for our test subjects. For the time-frequency transform, we used a rectangular window of length 15 s for the lightweight aircraft, and 4 s for the drone. Intuitively, the aircraft exhibits slower dynamics, and therefore requires a longer time window. More generally, the window should be long enough to capture the system dynamics, for example, the time required for the drone to change direction after receiving a new target position. We generated 200 input traces for each input type, yielding a total of 800 input traces per test subject. We then monitored each precondition specification over all traces and counted how many satisfy the corresponding precondition when the requirement is expressed in STL and in S2TL, respectively. 6.2.2 Results. Table 2 reports the results of evaluating the CPS requirements preconditions on the generated input traces. For each test subject, the rows report the results for the different preconditions, while the columns report the percentage of the 200 traces with a given input type that satisfy the corresponding precondition. For the preconditions expressed in S2TL, the satisfaction values are always either 100% or above 99%, demonstrating that these requirements are applicable to all the generated input traces. Similarly, the STL* precondition for SS is satisfied by all traces. In contrast, the STL* Step precondition is satisfied for almost all step and rand-const inputs—that is, traces generated using constant interpolation. However, only a small fraction of the linearly interpolated (rand-linear) and alternated interpolation (rand-alt) traces satisfy this precondition, with satisfaction rates of 1% and 0% for the drone, and 10% and 17% for the lightweight aircraft, respectively. This result is expected because these input types change gradually and therefore rarely exhibit the abrupt (step-like) changes required by the STL* step precondition (Eq. 34). This comparison is particularly relevant because linearly interpolated traces are among the most commonly used inputs for CPS testing. In fact, the abrupt step-like changes introduced by constant interpolation (and by step inputs) can place significant stress on CPS components, specifically the actuators, as they require sudden changes in the system state. These results therefore highlight an important advantage of the time-frequency signal representation: it extends the specification of step-response requirements to a much broader class of input traces. , Vol. 1, No. 1, Article . Publication date: August 2026.

24

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

Table 2. RQ1: Satisfaction of the STL* and S2TL Precondition in the Test Inputs of the Different Test Subjects. For each input type (corresponding to the columns), we generated 200 input traces. The reported percentage indicates how many of those traces satisfy each precondition (corresponding to the rows).

Test Subject

Drone Crazyflie

Lightweight Aircraft

Precondition

Step

Input Type Rand-Const Rand-Linear

Rand-Alt

Total

STL* Step STL* SS S2TL RT S2TL ST S2TL OV S2TL SS

100.0% 100.0% 100.0% 100.0% 100.0% 100.0%

97.0% 100.0% 99.0% 100.0% 99.5% 100.0%

1.0% 100.0% 100.0% 100.0% 100.0% 100.0%

0.0% 100.0% 99.5% 100.0% 100.0% 100.0%

49.5% 100.0% 99.6% 100.0% 99.9% 100.0%

STL* Step STL* SS S2TL RT S2TL ST S2TL OV S2TL SS

89.0% 100.0% 100.0% 100.0% 100.0% 100.0%

100.0% 100.0% 100.0% 100.0% 100.0% 100.0%

10.0% 100.0% 100.0% 100.0% 100.0% 100.0%

17.0% 100.0% 100.0% 100.0% 100.0% 100.0%

54.0% 100.0% 100.0% 100.0% 100.0% 100.0%

Summary: Our experiments show that expressing the ST, RT and OV requirements in S2TL extends their applicability to input traces generated using linear or alternated interpolation between control points, compared to their STL* counterparts. Specifically, we observe that, for our test subjects, while only 0%–17% of the linear and alternated interpolation traces satisfy the corresponding time-based STL* preconditions, nearly all of them (≥ 99%) satisfy the time-frequency-based S2TL preconditions. This applicability extension is particularly important because linear interpolation is the most commonly used method for generating CPS test inputs. At the same time, the time-frequency representation preserves applicability to step and constant-interpolation inputs. 6.3

RQ2: Requirements Expression Fidelity

6.3.1 Methodology and Parameters Settings. To answer RQ2, we compare the ability of STL* and S2TL specifications to detect requirement violations in signals that intrinsically satisfy or violate them. In this way, we assess the specifications’ fidelity to the intrinsic properties of the signals. We compare the specifications in terms of precision (the ability to report only violations), and soundness (the ability to report all violations) [36]. To build signals that intrinsically satisfy or violate the requirements, we adopted different approaches for the signal-feature and step-response requirement classes. For the signal-feature requirements (SP and OS), we generated signals that either contain or do not contain the relevant feature (i.e., spikes and oscillations) with prescribed parameters. To obtain a balanced dataset, we also generated an equal number of traces that either lack the feature altogether or contain it with parameters different from the prescribed ones (e.g., oscillations that are too slow or too fast). We generated these violating signals based on common violation patterns identified in the literature on diagnosis of signal-based requirements [12]. For SP, we considered three spike shapes: rectangular, triangular, and Gaussian. For each spike shape, we generated traces of length 20 s containing a single spike with prescribed ranges of amplitude values (between 10 and 20) and duration (between , Vol. 1, No. 1, Article . Publication date: August 2026.

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

25

Table 3. RQ2: Threshold values used to instantiate the specifications for each step-response requirement class, together with the corresponding response feature values used to synthesise satisfying and violating systems. Class (Response feature) RT (Rise Time) ST (Settling Time) OV (Overshoot) SS (Steady-State Error)

Specification Threshold

Satisfying System

Violating System

0.75 s 4.5 s 15% 0.1

0.5 s 3s 10% 0.05

1s 6s 20% 0.2

1 s and 2 s). Following Boufaied et al. [12], we also generated invalid spikes that are either too small (amplitude between 0 and 10) or too wide (duration between 2 s and 4 s). Traces that do not contain spikes instead consist of increasing, decreasing, or constant signals. For OS, we considered three oscillation shapes: sinusoidal, rectangular, and triangular. For each oscillation shape, we generated traces of length 20 s containing an oscillatory segment lasting between 5 s and 10 s, while the remainder of the trace is constant. The oscillations have a prescribed frequency between 0.9 Hz and 1.1 Hz and an amplitude between 10 and 20. We generated invalid oscillations that are either too large (amplitude between 20 and 40), too small (amplitude between 5 and 10), too slow (frequency 0.09 Hz and 0.9 Hz), or too fast (frequency between 1.1 Hz and 11 Hz). As for SP, following Boufaied et al. [12], we also generated traces that do not contain oscillations; these consist of increasing, decreasing, or constant signals. For each violation type and feature shape, we generated 30 traces, resulting in a total of 540 traces for SP and 900 for OS. As mentioned above, half of the traces contain a valid feature (equally distributed across the three shapes), while the other half either contain an invalid feature or no feature at all (equally distributed across the different shapes and violation types). Since the OS requirement class includes more types of invalid traces than SP, it requires a larger dataset; thus we generated more traces for this class. For the step-response requirements, we instead require traces containing both a test input and the corresponding output. Therefore, as described in Section 6.1.1, we used control theory to generate synthetic system models that either satisfy or violate the requirements. We then simulated these systems using different input signals to obtain satisfying and violating input-output traces. For each requirement class, we first selected a threshold value for the corresponding response feature (e.g., a desired rise time of 0.75 s for the RT class) that we used to instantiate the corresponding specification formula. We then synthesized two system models: one whose response exhibits a feature value that is strictly better than the threshold, and therefore satisfies the specification (e.g., a rise time of 0.5 s); and another whose response exhibits a feature value that is worse than the threshold, and therefore violates the specification (e.g., a rise time of 1 s). By simulating each system under different input signals, we obtain input-output traces that intrinsically satisfy or violate the corresponding requirement. Table 3 summarizes, for each requirement class, the selected threshold together with the response feature values exhibited by the synthesized satisfying and violating systems. Since, as mentioned above, assessing specifications on traces to which they are not applicable would lead to a trivial verdict, we considered only input traces to which both STL* and S2TL specifications are applicable. Based on the results of RQ1, for ST, RT, and OV requirement classes, we considered only step and constant-interpolation inputs. For SS, instead, we also considered linear and alternated interpolations. For each input type, we generated 30 traces, resulting in a total of 60 input traces for each system used to evaluate ST, RT, and OV; and 120 input traces for each , Vol. 1, No. 1, Article . Publication date: August 2026.

26

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

Table 4. RQ2: STL* and S2TL formulas used for RQ2, including the parameters values. Req. SP OS RT ST OV SS

Lang.

Formula

STL*

^ [0,20] ( (𝑥 − prev (𝑥 ) )/0.01 > 5 ∧ ^ [0,2] (𝑥 − prev (𝑥 ) )/0.01 < −5)

S2TL STL* S2TL STL* S2TL STL* S2TL STL* S2TL STL* S2TL

[0.5,4]

^ [0,20] □ [0,1] ¬L W [𝑥 ] < 1M ^ [0,20] ( (∗0.25 𝑥 − 𝑥 ) > 20 ∧ (∗0.25 𝑥 − 𝑥 ) < 40 ∧ (^ [0.48,0.52] ( (𝑥 − ∗0.25 𝑥 ) > 20 ∧ (𝑥 − ∗0.25 𝑥 ) < 40) ) ) [0.85,1.15]

∧ L W [𝑥 ] < 1M ^ [0,20] (¬L W [𝑥 ] < 4.5 ∨ W [𝑥 ] > 10M ^ [0,100] ( abs (𝑟 − prev (𝑟 ) ) > 1 ∧ (^ [0,0.75] 𝑥 < 0.75𝑟 ) ) [0,0.3]

[0.4,0.85]

□ [0,100] ( L W [𝑟 − 𝑥 ] < 0.25M ∧ L W [𝑟 ] > 0.1 ⇒ W [𝑥 ] < W [𝑟 ] M ^ [0,100] ( abs (𝑟 − prev (𝑟 ) ) > 1 ∧ □ [4.5,6] 𝑒 < 0.02𝑟 ) [0.15,4]

[0.15,4]

U [0,2.25] ( L W [𝑥 ] < 0.1M □ [0,100] ( L W [𝑟 ] < 0.1M ^ [0,100] ( abs (𝑟 − prev (𝑟 ) ) > 1 ∧ (□ [0,2] (𝑥 − 𝑟 ) < 0.15𝑟 ) )

∧ L W [𝑥 ] < 1M

[0.6,4]

[1.15,1.6]

)

)

∨ ¬L W [𝑟 ] < 0.1M

[0.15,4]

))

[1,3]

□ [0,100] L W [𝑥 ] > 0.05 ⇒ W [𝑥 ] < 1.15W [𝑟 ] M ¬^ [0,100] ( ( (𝑟 − prev (𝑟 ) )/0.01 < 0.01 ∧ (𝑥 − prev (𝑥 ) )/0.01 < 0.01) U [2,2.02] 𝑒 > 0.1) □ [0,100] ( L W [𝑟 ] < 0.01M

[0.5,4]

⇒ L W [𝑒 ] < 0.1M

[0,0.2]

)

system used to evaluate SS. For all the traces, we set a duration of 100 s, and randomly generated amplitude values (for the step-like changes and input control points) up to 10. In Table 4, we report the complete specification formulas used for this RQ. These formulas are based on the templates discussed in Section 5 for S2TL and Section 6.1.3 for STL* (i.e., on Kapinski et al. [28]). We chose the threshold values based on the value ranges of the valid signals discussed above or on known system parameters (e.g., the expected bandwidth 𝑓𝑏 ). In Appendix A.2, we detail how we selected each parameter of every formula for both STL* and S2TL. Here, we highlight one important rule of thumb that guided our parameter selection. When defining the thresholds for frequency-domain values, low-frequency components usually have amplitudes comparable to those of the corresponding time-domain signal, while higher-frequency components are usually one to two orders of magnitude smaller. Intuitively, fast changes in CPS traces tend to be less persistent than slow changes, resulting in lower amplitudes in the frequency domain. For monitoring the S2TL formulas, we used different time-frequency transforms depending on the requirement. In general, the window length must be sufficient to both capture the relevant system dynamics and provide adequate frequency resolution—as mentioned in Section 2.2.3, a longer time window yields higher frequency resolution. For the signal-feature requirements (SP and OS), which only need to detect the presence of a signal feature over 20 s traces, we used a triangular window of length 5 s. For ST and SS, we used a rectangular window because these requirements define assertions on slower signal dynamics, such as when the signals are at steady state (i.e., approximately constant signals). For OV and RT, we used a triangular window as they predicate on events that occur during the transient and therefore require frequency information about the signals more localised in time. For the step-response requirements, the system dynamics are on the order of a few seconds (corresponding to frequencies in the order of Hz); therefore, to achieve sufficient frequency resolution, we used a window of length 24 s. After generating the traces and monitoring them, we compute the precision and soundness of both STL* and S2TL formulas. We compute the precision as the percentage of traces detected as violating that are actual violations, i.e., Precision = 𝑐/(𝑐 + 𝑓 ), where 𝑐 is the number of correctly caught violations and 𝑓 is the number of non-violating traces incorrectly flagged as violating. We compute the soundness as the percentage of all violating traces that are detected, i.e., Soundness = 𝑐/(𝑐 +𝑚), where 𝑐 is the same as for the precision and 𝑚 is the number of missed violations. 6.3.2 Results. Table 5 reports the precision and soundness of the STL* and S2TL specifications when detecting spikes and oscillations (SP and OS rows, respectively), and assessing the stepresponse requirements (RT, ST, OV, and SS). The last row (“Total”) summarizes the results across all traces. , Vol. 1, No. 1, Article . Publication date: August 2026.

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

27

Table 5. RQ2: Requirements Expression Fidelity of STL* and S2TL for Different Requirement Classes.

Requirement Class

STL* Precision Soundness

S2TL Precision Soundness

SP

67.84%

100.00%

81.48%

97.78%

OS

71.57%

48.67%

80.11%

94.00%

RT

92.68%

63.33%

76.60%

60.00%

ST

93.33%

93.33%

100.00%

53.33%

OV

93.33%

70.00%

87.50%

81.67%

SS

58.17%

74.17%

89.66%

65.00%

Total

71.19%

70.00%

82.12%

86.47%

Table 6. RQ2: Requirements Expression Fidelity of S2TL for ST, RT, and OV requirement classes, using linear and alternate interpolation inputs.

Requirement Class

S2TL Precision Soundness

RT

92.86%

65.00%

ST

100.00%

66.67%

OV

100.00%

5.00%

Overall, the last row shows that the S2TL specifications achieve higher precision and soundness than the STL* specifications. Specifically, S2TL specifications attain a precision of 82.12% and a soundness of 86.47%, compared with 71.19% and 70%, respectively, for the STL* specifications. However, the comparison across the individual requirement classes is more nuanced. For SP, both STL* and S2TL achieve very high soundness (97.78% for S2TL and 100% for STL*). However, S2TL attains higher precision (81.48% compared with 67.84% for STL*), indicating that STL* detects more spikes than it should. This is due to its reliance on the derivative, which limits its ability to define assertions on the actual amplitude of the spike and, for example, leads to the incorrect detection of spikes that are too small. For OS, S2TL clearly outperforms STL* in both soundness (94% for S2TL against 48.67% for STL*) and precision (80.11% for S2TL against 71.57% for STL*). This result is expected, as the frequency domain is particularly well suited for describing oscillatory behaviour. For the step-response requirement classes, the comparison is less unilateral. For RT, STL* specifications outperform the S2TL specifications, particularly in terms of precision (76.60% for S2TL against 92.78% for STL*), while the soundness is comparable (60% for S2TL against 63.33% for STL*). For the remaining classes, the two languages exhibit different trade-offs between soundness and precision. For ST, S2TL achieves higher precision (100% against 93.33% for STL*), but substantially lower soundness (53.33% against 93.33% for STL*). Similarly, for SS, S2TL provides significantly higher precision (89.66% against 58.17% for STL*), but lower soundness (65% against 74.17% for STL*). In contrast, for OV, the trend is reversed: S2TL achieves higher soundness (81.67% against 70% for STL*), while STL* attains higher precision (93.33% against 87.50% for S2TL). , Vol. 1, No. 1, Article . Publication date: August 2026.

28

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

Overall, for the step-response requirement classes, neither specification language clearly outperforms the other. However, for RT, ST and OV, it is important to take into account the results of RQ1, which showed that the S2TL specifications are applicable also to test cases (i.e. input traces) generated using linear and alternated interpolation. In practice, this means that the STL* specifications can be more closely tailored to the specific traces and can therefore make stronger assumptions about the signal shapes. In Table 6, we report the precision and soundness of the S2TL specifications on test cases with linear and alternated interpolation. Across all three requirement classes, we observe high precision but comparatively lower soundness. Notably, the soundness for OV is very low, with a detection of only 5% of the violations. This is due to the nature of the overshoot requirement, which requires a strong excitation of the system to expose a violation. This excitation is more readily produced by step-like changes in the input rather than by linear or alternated interpolation. Summary: Our results show that, for detecting spikes and oscillations (the signal-feature requirement classes), S2TL outperforms STL* in both soundness and precision. In contrast, for the step-response requirement classes, the two specification languages exhibit comparable overall performance, although they generally present different trade-offs between soundness and precision. For RT, STL* outperforms S2TL, achieving both higher precision and soundness. For ST, STL* maintains a balanced trade-off between precision and soundness, whereas S2TL achieves higher precision compared to soundness. For OV, the opposite trend is observed: STL* favors precision over soundness, while S2TL provides a more balanced trade-off between the two. Finally, for SS, STL* achieves higher soundness, whereas S2TL attains higher precision. 6.4

RQ3: Noise Tolerance of Monitoring

6.4.1 Methodology. To answer this RQ, we inject increasing levels of noise into the traces and measure for which noise level the verdict changes. To compare the noise tolerance of the STL* and S2TL specifications, we selected from the traces used in RQ2 only those for which the specifications in both languages provide the correct verdict with respect to the ground truth, where the ground truth is given by whether each trace intrinsically satisfies or violates the requirement. Intuitively, if the initial verdict for the non-noisy trace is incorrect, a change is not necessarily undesirable, even if due to noise. In fact, the verdict would change to the correct one, and the noise could be interpreted to be “helping” the monitoring process rather than impairing it. However, whether this is desirable or not depends on the application context and therefore we excluded this scenario from the analysis. After applying this filtering step, we retained 379 traces for SP, 538 traces for OS, 65 traces for RT, 87 traces for ST, 82 traces for OV, and 110 traces for SS. We injected three standard types of noise commonly observed in CPS signals, typically arising from sensor noise or calibration errors: constant offset, Gaussian white noise, and Gaussian highfrequency noise. We define the noise level as a percentage of the signal’s value range. Specifically, for each signal, we computed its value range (i.e., the difference between its maximum and minimum values) and used a percentage of that range to define either the offset magnitude or the standard deviation of the Gaussian noise. We considered four equally spaced noise levels ranging from 5% to 30%. For the step-response specifications, we injected noise only into the output signal, as the input signal is generated by a user or other software components and is therefore not subject to sensor noise. However, this means that, for the SS requirement class, the offset affects the intrinsic satisfaction of the requirement or, in other words, affects the ground truth, thus making a verdict change actually desirable. A similar argument applies to the S2TL formulation of RT requirements, , Vol. 1, No. 1, Article . Publication date: August 2026.

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

29

Table 7. RQ3: Noise Tolerance of Monitoring. For each requirement class, we report the percentage of traces whose verdict changes due to noise (% Flipped) and the average noise level at which the verdict change occurs (Avg. Flip Level ).

Requirement Class SP OS RT ST OV SS

Metric % Flipped Avg. Flip Level % Flipped Avg. Flip Level % Flipped Avg. Flip Level % Flipped Avg. Flip Level % Flipped Avg. Flip Level % Flipped Avg. Flip Level

Offset STL* S2TL 0.00% 0.00% N/A N/A 64.37% 0.050 60.98% 0.083 N/A N/A

2.90% 0.202 0.37% 0.300 N/A N/A 0.00%

White Noise STL* S2TL

High-Freq. Noise STL* S2TL

30.08% 3.69% 30.08% 0.058 0.199 0.057 26.58% 31.04% 24.72% 0.228 0.232 0.234 29.23% 67.69% 29.23% 0.125 0.133 0.116 64.37% 57.47% 64.37% 0.050 0.205 0.050 10.98% 60.98% 59.76% 60.98% 0.207 0.065 0.074 0.068 N/A 52.73% 43.64% 52.73% N/A 0.050 0.135 0.050

0.00% 0.00% 6.15% 0.279 0.00% 2.44% 0.217 13.64% 0.206

which constrain the low-frequency correspondence between the input and output (Eq. 26). Since, in these cases, the information in the traces that is relevant to the requirement satisfaction changes, a verdict change may be actually desirable. For this reason, we excluded these scenarios from the analysis of noise tolerance of monitoring. 6.4.2 Results. Table 7 summarizes the results of the noise injection experiments. The columns correspond to the different types of noise and report the results for both STL* and S2TL, while the rows correspond to the different requirement classes. For each requirement class, we report the percentage of traces whose verdict changes for some noise level (% Flipped) and the average noise level at which the verdict change occurs (Avg. Flip Level). In the “% Flipped” row, a lower percentage indicates higher noise tolerance, whereas in the “Avg. Flip Level” row a higher average noise level indicates higher noise tolerance. When no verdict changes are observed, we leave the corresponding cell empty. We observe that, for the noise types “Offset” and “High-Frequency Noise”, S2TL exhibits higher noise tolerance than STL*. The only exceptions are the SP and OS requirement classes under offset noise; however, the performance difference in these cases is small, and S2TL still exhibits a very low percentage of flipped verdicts. The higher tolerance of S2TL to these noise types is related to the ability of the frequency-domain representation to isolate the frequency components that carry information relevant to the system behaviour from the ones that carry the noise. In particular, a constant offset affects only the low-frequency components, whereas high-frequency noise primarily affects the high-frequency components. When the specification does not constrain these components, perturbations to them have little or no effect on the monitoring outcome, and hence the frequency-domain specifications are not affected by them. In contrast, STL* specifications are based on thresholds over signal values at specific points in time and are therefore more sensitive to local changes in the signal induced by noise. For the white noise experiments, the STL* and S2TL specifications compare differently across the different requirement classes. For SP, ST and SS, S2TL consistently outperforms STL*, exhibiting either a lower percentage of flipped verdicts or changing the verdict only for higher levels of , Vol. 1, No. 1, Article . Publication date: August 2026.

30

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

noise. For OS and OV, the performance of the specifications written in the two languages is comparable. Finally, STL* outperforms S2TL for RT, with substantially fewer traces exhibiting a verdict change (29.23% versus 67.69%). Unlike offset and high-frequency noise, white noise affects the whole frequency spectrum, including the frequency components that encode the relevant system behaviour. As a result, also S2TL specifications cannot effectively filter out its effects, making them more susceptible to this type of noise. We observe that STL* specifications exhibit nearly identical percentage of flipped verdicts and average flip levels for white and high-frequency noises. A closer inspection of the data reveals that, in most cases, the same traces experience verdict changes under both types of noise. This indicates that STL* specifications are equally affected by white and high-frequency noise. In fact, since STL* specifications rely on signal values at specific points in time, they are influenced by the magnitude of the noise and cannot leverage its frequency characteristics (i.e., correlations between its values over time) to prevent it from affecting the monitoring. On the contrary, S2TL specifications exhibit a substantially higher noise tolerance for traces affected by high-frequency noise, when compared to white noise. This is because they can exploit the fact that high-frequency noise is confined to a specific region of the spectrum. Notably, with the high-frequency noise, only RT and SS exhibit more than a few flipped verdicts, with 6.15% and 13.64% of traces affected, respectively. This showcases the ability of the frequency-domain specifications to isolate the frequency components that encode the relevant system behaviour while ignoring components affected by noise. Further, this underlines the ability of the frequency domain representation to analyse the shape of a signal independently of its values at specific points in time. Summary: Our experiments show that, when signals are affected by constant offsets or highfrequency noise, the time-frequency-domain specifications are significantly more noise-tolerant than the time-domain ones. White noise, however, degrades also the performance of frequencydomain specifications. Nevertheless, also with white noise, the frequency domain specifications remain more noise-tolerant than their time-domain counterparts for most requirement classes (SP, ST and SS). For OS and OV specifications, the noise tolerance is comparable, whereas, for RT, the time domain performs better. 6.5

Discussion

The motivating hypothesis of this paper is that expressing signal-based CPS requirements using the time-frequency domain representations of signals can improve both the broader applicability of the requirements and the noise tolerance of their monitoring. The broader applicability is confirmed by the results of RQ1, which demonstrate the extension of the applicability of requirements expressed in time-frequency domain to input traces using linear or constant-linear alternate interpolation, when compared to the time-domain counterpart. The noise tolerance of monitoring is instead confirmed by the results of RQ3, which show that the time-frequency specifications are more tolerant to offset and high-frequency noise, while their tolerance to white noise is comparable to that of the time-domain specifications. These results are complemented by the results of RQ2, which compare the fidelity of timedomain and time-frequency-domain specifications to the intrinsic signal properties. The RQ2 results show that the relative performance of the two domains varies across different requirement classes. However, RQ2 considers only traces for which both sets of specifications are applicable. As discussed in the answer to RQ2 (Section 6.3.2), the pure time-domain specifications are more restrictive in their applicability, as shown in RQ1. This allows them to make stronger assumptions about the signal shape, making it easier to achieve higher requirement fidelity (in terms of precision , Vol. 1, No. 1, Article . Publication date: August 2026.

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

31

and soundness) in the specification formulation. In contrast, the time-frequency specifications are applicable also to traces that use linear and constant-linear alternate interpolation, and achieve good requirement fidelity, especially in terms of precision (Table 6). To conclude, the use of the time-frequency-domain representation of signals enables specifications that are applicable to a broader range of traces and monitoring that is more tolerant to noise with a known spectral profile, as is often the case in practice. However, pure time-domain specifications remain an effective choice for traces where strong assumptions about the signal shape can be made and the noise level is low. 6.6

Threats to Validity

6.6.1 Internal Validity. In terms of internal validity, the main threat is that the STL* specifications were adapted from Kapinski et al. [28], and the S2TL specifications were written by us using the templates proposed in Section 5. This poses a validity threat because alternative choices could be made to specify the requirements, potentially leading to different results. However, both the templates from Kapinski et al. [28] and our proposed templates are based either directly on the definitions of the requirements themselves or on well-established results from control theory [2]. This provides confidence that our formulas are representative among the plausible specification alternatives. Moreover, the selected parameter values are motivated by engineering considerations, which we documented in the appendices. Another threat to internal validity arises from the random generation of the noise used in RQ3. Different sampling of the noise values could have produced different results. However, our evaluation is based on a relatively large dataset, comprising 1252 traces in total and at least 65 traces for each requirement class. Because each trace was generated using an independently sampled noise sequence, the dataset covers a broad range of possible noise realisations. Furthermore, when comparing STL* and S2TL, we evaluate both specifications on the same noisy trace. As a result, the comparison is performed under identical conditions, ensuring its fairness. As noted when reporting for the time-domain formula of the RT requirement (Eq. 32), the STL* formula implicitly assumes that the step input starts from the value 0. This assumption holds for the step inputs used in RQ2 and RQ3, but does not necessarily hold for the inputs generated using constant interpolation. When the assumption is violated, the threshold used to evaluate the requirement is slightly lower than intended because the variable 𝑥 starts from a higher value. Consequently, the constraint becomes less restrictive, which may reduce the soundness of the formula, that is, its ability to detect all violations. Nevertheless, a higher soundness value would not alter our conclusions, as, for the RT, the time-domain representation already outperforms the time-frequency-domain representation. 6.6.2 External Validity. The external validity of our experiments depends on the extent to which the selected systems and generated test inputs are representative of real-world CPSs. For RQ1, we used two real CPSs to determine the parameters for generating the test inputs. This gives us confidence that the resulting input traces are realistic. For RQ2 and RQ3, we used instead synthetic systems for the generation of the test outputs. However, the mathematical model that we used (a second-order linear system) is generally considered a good approximation of a closed-loop control system [2]. Therefore, although the systems themselves are not instances of real CPSs, the generated input and output traces can be considered representative of those encountered in practice. For generating the input traces, we did not employ a specific test generation technique. Consequently, one could argue that the generated traces may not be representative of actual test cases. However, we generated the traces by random sampling using the standard parametrisation adopted by many state-of-the-art testing approaches [7, 27, 33, 34]. As such, our traces can be considered , Vol. 1, No. 1, Article . Publication date: August 2026.

32

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

representative of the inputs generated by these testing approaches. Moreover, we evaluated our approach on a large number of traces: 1600 for RQ1, 1920 for RQ2, and 1252 for RQ3. These sample sizes give us confidence that the observed results are not artefacts of a specific realisation of the random sampling. Further, for our input generation, we considered only non-negative signal values: step inputs ranged from 0 to a positive value, and the control points of other input signals were restricted to positive values. We made this choice because the time-domain specification templates we used assume non-negative signals; otherwise, the inequalities would no longer correctly capture the intended relations. However, this limitation does not affect our conclusion that the time-frequencydomain representation is a valuable extension of the traditional time-domain approach. In fact, considering also signals which take negative values would only reduce the applicability, fidelity and noise tolerance of the time-domain formulas. In contrast, the applicability, fidelity, and noise tolerance of the time-frequency-domain formulas would remain unchanged. In fact, the sign of a signal affects the phase of its spectrum, but our specification templates predicate only about the amplitude. Therefore, extending the evaluation to signals with negative values would only strengthen the conclusions drawn from our results.

7

OUTLOOK ON SOFTWARE ENGINEERING FOR CPS WITH TIME-FREQUENCY SPECIFICATIONS

In this section, we discuss the implications of the results presented in this paper for both researchers and practitioners. Our results show that the use of time-frequency signal representations extends the specifications applicability to a broader set of traces and improves the noise tolerance of monitoring. This has implications for all software engineering (SE) activities that leverage specification languages and runtime verification [4]. Among the various SE activities, we highlight the potential for new developments in requirements mining, falsification testing, and fault localisation. For requirements mining, researchers will need to investigate approaches for synthesising the time-frequency transforms used in specifications to capture relevant signal properties [37]. This challenge will also be closely intertwined with the learning of specification parameters. Falsification testing (i.e., the generation of test cases aimed at finding counterexamples to the satisfaction of a given specification) will require new test-generation approaches that explore system behaviours differing in their frequency content rather than merely in their signal values [46]. Finally, the use of time-frequency representations opens opportunities for developing new fault-localisation approaches based on changes in the spectral properties of signals caused by faults [6]. For practitioners, we foresee two main opportunities arising from the use of time-frequency signal representations. First, traditional software engineering activities can benefit from the results observed in this paper. Specifically, the increased applicability and noise tolerance of monitoring can make specification development and maintenance [13, 24] more cost-effective, as specifications can be used as oracles on a larger number of traces. Second, the use of a specification language based on this signal representation can simplify interactions among software engineers, systems engineers, and control engineers [32]. Indeed, the latter often work with frequency-domain representations of systems and signals. A formalism capable of expressing both time-domain and frequency-domain properties can provide common ground for software engineers to collaborate more effectively with experts from other disciplines. In conclusion, these opportunities make the industrial adoption [22] of formal specifications and runtime verification techniques more likely.

, Vol. 1, No. 1, Article . Publication date: August 2026.

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

8 8.1

33

RELATED WORK Time-Based Specification Languages

Researchers have proposed a variety of languages for specifying signal-based CPS requirements. Arguably, most state-of-the-art languages originate from Linear Temporal Logic (LTL) [42], which enables the expression of constraints over the temporal ordering of propositional variables, and its extension, Metric Temporal Logic (MTL) [29], which augments LTL with quantitative timing constraints. Motivated by applications to control systems and analog and mixed-signals circuits, MTL was further extended to Signal Temporal Logic (STL) [30], which enables expressing constraints over dense-timed, real-valued signals.16 At its core, STL introduces atomic propositions that express inequality constraints over signal values. Notably, STL is the specification language adopted by Kapinski et al. [28] to define templates for the specification classes in their taxonomy (discussed in Section 6.1.3). Despite its widespread adoption, researchers have highlighted several limitations of STL and have proposed numerous extensions. Based on two surveys [4, 11], we summarize the main extensions to STL and refer the reader to the original surveys for a more comprehensive overview and discussion. STL*: STL can only compare signals with constants or with other signals at the same time. As a result, it cannot express comparisons between a signal’s values at different points in time. For example, specifying a local maximum requires comparing the signal’s value at a given time instant with its values over adjacent time intervals. To address this limitation, Brim et al. [15] introduced STL*, which enables such comparisons through a “signal-value-freeze” operator. The authors highlight its usefulness for specifying local minima and maxima, which in turn can be used to express properties such as increasing or decreasing oscillations. HLS and SCSL: Hybrid Logic of Signals (HLS) is another language that extends STL [35]. Its objective is to facilitate the specification of constraints over both software and physical behaviours. To this end, HLS introduces quantification over both signal time stamps and time indexes, enabling more flexible reasoning about the temporal dimension. Later, HLS was integrated with Interprocedural Control-Flow Temporal Logic (iCFTL) [20] into the new language Source Code and Signal Logic (SCSL) [21]. This integration enables the combination of source-code level specifications from iCFTL with signal-based specifications from HLS. Besides the ones discussed above, we also mention three additional specification languages suitable for expressing signal-based CPS requirements that do not extend STL. SCL: Silvetti et al. [44] introduced Signal Convolution Logic (SCL) to specify properties that require a predicate to hold for only a given percentage of a time interval, while also enabling the filtering of noise. This is achieved through a convolution operator that convolves the signal with a kernel (allowing noise filtering) and evaluates whether the predicate holds for the required fraction of the interval. SFO: Bakhirkin et al. [3] introduced Signal First-Order Logic (SFO), which allows the use of quantifiers (existential and universal) over both value and time variables. This overcomes the limitation of STL that it requires comparing signals to known values (i.e., constants or other signals’ values). The authors highlight that the quantification over time variables eliminates the need for temporal operators like “finally”, “globally”, and “until”. Shape Expressions: To enable the description of signal shapes and their detection in signals, Ničković et al. [39] proposed Shape Expressions. In shape expressions, signal shapes are described

16 More precisely, STL extends Metric Interval Temporal Logic (MITL), which is a decidable fragment of MTL.

, Vol. 1, No. 1, Article . Publication date: August 2026.

34

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

as sequences of basic patterns, such as linear increase, exponential growth, or sinusoidal oscillations. These sequences can be written using a grammar similar to that of regular expressions. In terms of tools for runtime verification, to the best of our knowledge, among the works reported here, RTAMT [40, 47] (the one that we used in Section 6 to build an S2TL monitor) supports STL and its extension STL*. The authors of HLS and SCSL provide replication packages containing monitors for their proposed specification languages. All these tools are available under permissive open-source licenses. All the languages discussed above essentially address the common challenge of comparing the values of the same signal at different points in time. This capability is fundamental for describing signal shapes, which in turn are essential for expressing many CPS requirements. In this work, we address the same challenge, but take a fundamentally different approach by leveraging the timefrequency representation of signals rather than relying solely on their time-domain representation. 8.2

Use of the Frequency Domain for Signal-Based CPS Specifications

Chakarov et al. [16] were the first to propose the use of the frequency domain for specifying signalbased CPS requirements. In this preliminary work, the authors proposed to define constraints on the amplitude components of a signal’s frequency spectrum. They also addressed the signal generation problem by proposing an approach to generate signals that satisfy a given specification. The main limitation of this work is that it considers only periodic signals and relies exclusively on the Fourier transform, thereby completely discarding the temporal dimension of the signal. TFL: Donzé et al. [23] extended STL with the Short-Time Fourier Transform to introduce TimeFrequency Logic (TFL). Their objective was to handle non-periodic signals by enabling predicates over how a signal’s frequency spectrum evolves over time. Specifically, they extended STL with inequality constraints on the amplitude of individual frequency components. As a proof of concept, they applied TFL to automatically recognise a blues melody in a song. Subsequently, Nguyen et al. [38] enhanced TFL by replacing STFT with the Wavelet transform and defining a parametric version of the language (called Parametric Time Frequency Logic - PTFL), which allows for unknown parameters in the formulas that can be learned from traces rather than being set by the user. They used PTFL for anomaly detection in a hydrogen fuel cell and an electrocardiogram. Later, also Beg et al. [9] used PTFL for anomaly detection in electric microgrids. To the best of our knowledge, neither an implementation of TFL nor PTFL are available. Our work is closely related to TFL, as S2TL also leverages the time-frequency representation of signals. However, S2TL places a stronger emphasis on the frequency domain by supporting more expressive predicates over the time-frequency spectrum of one or more signals (Eq. 4), as well as predicates over frequency intervals rather than individual frequency components. As discussed in Section 3.3, these features are essential for specifying CPS requirements. Finally, we mention a few additional works that leverage the frequency-domain representation of signals in the context of CPS V&V. Rodionova et al. [43] proposed continuous-time LTI filters that implement the semantics of MTL. Basnet and Abbas [8] performed a Fourier analysis of STL monitors. Mandrioli et al. [32] and Bartocci et al. [7] exploited the frequency domain for test case generation. While these works do not directly address the specification of CPS requirements, they underline the relevance and potential of the frequency domain for the V&V of CPSs. 9

CONCLUSIONS

In this paper, we have investigated the use of time-frequency representation of signals for specifying signal-based CPS requirements. We have analysed existing taxonomies of CPS requirements and identified the requirement classes that can benefit from time-frequency representations. Based , Vol. 1, No. 1, Article . Publication date: August 2026.

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

35

on this analysis, we have derived the desiderata for a specification language operating on timefrequency representations and proposed Signal-Spectrum Temporal Logic, a logic that enables predicates over frequency intervals as well as logical relations between frequency components. We have further proposed specification templates for the identified requirement classes and used them to empirically compare the formulation of requirements in the time and time-frequency domains. Our empirical results show that the time-frequency representation substantially broaden the applicability of step-response requirements by eliminating their dependence on step-like inputs and enabling their evaluation on traces generated through linear interpolation. Moreover, requirements specified in the time-frequency domain exhibit increased tolerance to signal offsets and high-frequency noise while maintaining comparable fidelity in capturing the intended signal properties. Overall, our findings demonstrate that the time-frequency representations provide a valuable extension to the traditional time-domain representations for specifying CPS requirements, particularly by broadening the applicability and improving the noise tolerance of monitoring. In the future, we plan to investigate the practical aspects of using S2TL for specifying CPS requirements. Specifically, we will conduct a user study to understand its potential for adoption by software engineering practitioners in the field of CPS, investigating the understandability of S2TL specifications [18, 19]. At the same time, we plan to develop GUI-based tools to facilitate the use of S2TL, for example with graphical representations of the formulas in relation to the monitored signals. On the more theoretical side, we will investigate the possibility of implementing online monitors, in light of the discussion in Section 4.3. ACKNOWLEDGMENTS This work has received funding from the European Union’s Marie Skłodowska-Curie Actions – Postdoctoral Fellowships (PF) program under Grant Agreements No. 101148870 (ContTestCPS) and No. 101273739 (REACT-CPS). For the purpose of open access, and in fulfilment of the obligations arising from the grant agreements, the authors have applied a Creative Commons Attribution 4.0 International (CC BY 4.0) license to any Author Accepted Manuscript version arising from this submission. REFERENCES [1] Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. J. ACM, 43(1):116—-146, January 1996. ISSN 0004-5411. doi: 10.1145/227595.227602. URL https://doi.org/10.1145/227595.227602. [2] Karl Johan Astrom and Richard M. Murray. Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press, USA, 2008. ISBN 0691135762. [3] Alexey Bakhirkin, Thomas Ferrère, Thomas A. Henzinger, and Deian Ničkovićl. Keynote: The first-order logic of signals. In 2018 International Conference on Embedded Software (EMSOFT), pages 1–10, 2018. doi: 10.1109/EMSOFT.2018.8537203. [4] Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donzé, Georgios Fainekos, Oded Maler, Dejan Ničković, and Sriram Sankaranarayanan. Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications, pages 135–175. Springer International Publishing, Cham, 2018. ISBN 978-3-319-75632-5. doi: 10.1007/978-3-319-756325_5. URL https://doi.org/10.1007/978-3-319-75632-5_5. [5] Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to Runtime Verification, pages 1–33. Springer International Publishing, Cham, 2018. ISBN 978-3-319-75632-5. doi: 10.1007/978-3-319-75632-5_1. URL https://doi.org/10.1007/978-3-319-75632-5_1. [6] Ezio Bartocci, Leonardo Mariani, Dejan Nickovic, and Drishti Yadav. Search-based testing for accurate fault localization in CPS. In Proceedings of the 33rd IEEE International Symposium on Software Reliability Engineering (ISSRE), pages 145–156. IEEE, 2022. doi: 10.1109/ISSRE55969.2022.00024. [7] Ezio Bartocci, Leonardo Mariani, Dejan Nickovic, and Drishti Yadav. Signal feature coverage and testing for CPS dataflow models. ACM Trans. Softw. Eng. Methodol., 34(7), August 2025. ISSN 1049-331X. doi: 10.1145/3714467. URL https://doi.org/10.1145/3714467. [8] Niraj Basnet and Houssam Abbas. Logical signal processing: A fourier analysis of temporal logic. In Jyotirmoy Deshmukh and Dejan Ničković, editors, Runtime Verification, pages 359–382, Cham, 2020. Springer International , Vol. 1, No. 1, Article . Publication date: August 2026.

36

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

Publishing. ISBN 978-3-030-60508-7. [9] Omar Ali Beg, Luan Viet Nguyen, Taylor T. Johnson, and Ali Davoudi. Cyber-physical anomaly detection in microgrids using time-frequency logic formalism. IEEE Access, 9:20012–20021, 2021. doi: 10.1109/ACCESS.2021.3055229. [10] Boualem Boashash. Chapter i: The time-frequency approach: Essence and terminology. In Boualem Boashash, editor, Time-Frequency Signal Analysis and Processing (Second Edition), pages 3–29. Academic Press, Oxford, second edition edition, 2016. ISBN 978-0-12-398499-9. doi: 10.1016/B978-0-12-398499-9.09991-X. URL https://www.sciencedirect. com/science/article/pii/B978012398499909991X. [11] Chaima Boufaied, Maris Jukss, Domenico Bianculli, Lionel Claude Briand, and Yago Isasi Parache. Signal-based properties of cyber-physical systems: Taxonomy and logic-based characterization. Journal of Systems and Software, 174:110881, 2021. ISSN 0164-1212. doi: 10.1016/j.jss.2020.110881. URL https://www.sciencedirect.com/science/article/ pii/S0164121220302715. [12] Chaima Boufaied, Claudio Menghi, Domenico Bianculli, and Lionel C. Briand. Trace diagnostics for signal-based temporal properties. IEEE Transactions on Software Engineering, 49(5):3131–3154, 2023. doi: 10.1109/TSE.2023.3242588. [13] Jonathan P. Bowen, Peter T. Breuer, and Kevin Lano. Formal specifications in software maintenance: From code to z++ and back again. Information and Software Technology, 37(8):547–554, 1995. [14] Ronald N. Bracewell. The Fourier Transform and Its Applications. McGraw-Hill, New York, NY, 3 edition, 2000. ISBN 9780073039381. [15] L. Brim, P. Dluhoš, D. Šafránek, and T. Vejpustek. STL*: Extending signal temporal logic with signal-value freezing operator. Information and Computation, 236:52–67, 2014. ISSN 0890-5401. doi: 10.1016/j.ic.2014.01.012. URL https: //www.sciencedirect.com/science/article/pii/S0890540114000133. Special Issue on Hybrid Systems and Biology. [16] Aleksandar Chakarov, Sriram Sankaranarayanan, and Georgios Fainekos. Combining time and frequency domain specifications for periodic signals. In Sarfraz Khurshid and Koushik Sen, editors, Runtime Verification, pages 294–309, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. ISBN 978-3-642-29860-8. [17] Leon Cohen. Time-Frequency Analysis. Prentice Hall, Upper Saddle River, NJ, 1995. ISBN 0135945321. [18] Christoph Czepa and Uwe Zdun. How understandable are pattern-based behavioral constraints for novice software designers? ACM Trans. Softw. Eng. Methodol., 28(2):11:1–11:38, February 2019. doi: 10.1145/3306608. [19] Christoph Czepa and Uwe Zdun. On the understandability of temporal properties formalized in linear temporal logic, property specification patterns and event processing language. IEEE Transactions on Software Engineering, 46(1): 100–112, 2020. doi: 10.1109/TSE.2018.2859926. [20] J.H. Dawes and D. Bianculli. Specifying properties over inter-procedural, source code level behaviour of programs. In Proc RV’21, pages 23–41. Springer, 2021. [21] Joshua Heneage Dawes and Domenico Bianculli. Specifying source code and signal-based behaviour of cyber-physical system components. In Silvia Lizeth Tapia Tarifa and José Proença, editors, Formal Aspects of Component Software, pages 20–38, Cham, 2022. Springer International Publishing. ISBN 978-3-031-20872-0. [22] Joshua Heneage Dawes and Domenico Bianculli. Checking complex source code-level constraints using runtime verification. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, FSE 2024, page 255–265, New York, NY, USA, 2024. Association for Computing Machinery. ISBN 9798400706585. doi: 10.1145/3663529.3663845. URL https://doi.org/10.1145/3663529.3663845. [23] Alexandre Donzé, Oded Maler, Ezio Bartocci, Dejan Nickovic, Radu Grosu, and Scott Smolka. On temporal logic and signal processing. In Supratik Chakraborty and Madhavan Mukund, editors, Automated Technology for Verification and Analysis, pages 92–106, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. ISBN 978-3-642-33386-6. [24] Patrick Fennell, Harald Gall, et al. Same but different: Consistently developing and evolving software architecture specifications and implementations. In Proceedings of the European Conference on Software Architecture (ECSA 2020), Lecture Notes in Computer Science. Springer, 2020. doi: 10.1007/978-3-030-58617-1_6. [25] Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi. Modeling Time in Computing. Springer Publishing Company, Incorporated, 2012. ISBN 3642323316. [26] Sergio García, Daniel Strüber, Davide Brugali, Thorsten Berger, and Patrizio Pelliccione. Robotics software engineering: a perspective from the service robotics domain. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020, page 593–604, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450370431. doi: 10.1145/3368089.3409743. URL https://doi.org/10.1145/3368089.3409743. [27] Carl Hildebrandt, Sebastian Elbaum, Nicola Bezzo, and Matthew B. Dwyer. Feasible and stressful trajectory generation for mobile robots. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, page 349–362, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450380089. doi: 10.1145/ 3395363.3397387. [28] James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh, Alexandre Donze, Tomoya Yamaguchi, Hisahiro Ito, Tomoyuki Kaga, Shunsuke Kobuna, and Sanjit Seshia. ST-Lib: A library for specifying and classifying model behaviors. In SAE

, Vol. 1, No. 1, Article . Publication date: August 2026.

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

37

World Congress and Exhibition, SAE Technical Paper 2016-01-0621. SAE International, April 2016. [29] Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Syst., 2(4):255—-299, October 1990. ISSN 0922-6443. doi: 10.1007/BF01995674. URL https://doi.org/10.1007/BF01995674. [30] Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Yassine Lakhnech and Sergio Yovine, editors, Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pages 152–166, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. ISBN 978-3-540-30206-3. [31] Claudio Mandrioli, Max Nyberg Carlsson, and Martina Maggio. Testing abstractions for cyber-physical control systems. ACM Trans. Softw. Eng. Methodol., 33(1), nov 2023. ISSN 1049-331X. doi: 10.1145/3617170. URL https: //doi.org/10.1145/3617170. [32] Claudio Mandrioli, Seung Yeob Shin, Martina Maggio, Domenico Bianculli, and Lionel Briand. Stress testing control loops in cyber-physical systems. ACM Trans. Softw. Eng. Methodol., 33(2), dec 2023. ISSN 1049-331X. doi: 10.1145/3624742. URL https://doi.org/10.1145/3624742. [33] Claudio Mandrioli, Seung Yeob Shin, Domenico Bianculli, and Lionel Briand. Testing CPS with design assumptionsbased metamorphic relations and genetic programming. IEEE Transactions on Software Engineering, pages 1–19, 2025. doi: 10.1109/TSE.2025.3563121. [34] Reza Matinnejad, Shiva Nejati, Lionel C. Briand, and Thomas Bruckmann. Test generation and test prioritization for simulink models with dynamic behavior. IEEE Transactions on Software Engineering, 45(9):919–944, 2019. doi: 10.1109/TSE.2018.2811489. [35] Claudio Menghi, Enrico Viganò, Domenico Bianculli, and Lionel C. Briand. Trace-checking CPS properties: Bridging the cyber-physical gap. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE), pages 847–859, 2021. doi: 10.1109/ICSE43902.2021.00082. [36] Bertrand Meyer. Soundness and completeness defined with precision. https://cacm.acm.org/blogcacm/soundness-andcompleteness-defined-with-precision/, April 2019. CACM Blog. [37] Eleonora Nesterini, Ezio Bartocci, Alessio Gambi, Dejan Nickovic, Sanjit A. Seshia, and Hazem Torfah. Mining specifications for predictive safety monitoring. In Proceedings of the ACM/IEEE 16th International Conference on Cyber-Physical Systems (ICCPS ’25), pages 1–11. ACM, 2025. doi: 10.1145/3716550.3722021. [38] Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh, Ken Butts, and Taylor T. Johnson. Abnormal data classification using time-frequency temporal logic. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC ’17, pages 237—-242, New York, NY, USA, 2017. Association for Computing Machinery. ISBN 9781450345903. doi: 10.1145/3049797.3049809. URL https://doi.org/10.1145/3049797.3049809. [39] Dejan Ničković, Xin Qin, Thomas Ferrère, Cristinel Mateis, and Jyotirmoy Deshmukh. Shape expressions for specifying and extracting signal features. In Bernd Finkbeiner and Leonardo Mariani, editors, Runtime Verification, pages 292–309, Cham, 2019. Springer International Publishing. ISBN 978-3-030-32079-9. [40] Dejan Ničković and Tomoya Yamaguchi. RTAMT: Online robustness monitors from STL. In Automated Technology for Verification and Analysis: 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19–23, 2020, Proceedings, page 564–571, Berlin, Heidelberg, 2020. Springer-Verlag. ISBN 978-3-030-59151-9. doi: 10.1007/978-3-030-59152-6_34. URL https://doi.org/10.1007/978-3-030-59152-6_34. [41] Alan V. Oppenheim and Ronald W. Schafer. Discrete-Time Signal Processing. Pearson, Upper Saddle River, NJ, 3 edition, 2010. ISBN 9780131988422. [42] Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46–57, 1977. doi: 10.1109/SFCS.1977.32. [43] Alena Rodionova, Ezio Bartocci, Dejan Nickovic, and Radu Grosu. Temporal logic as filtering. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC ’16, pages 11—-20, New York, NY, USA, 2016. Association for Computing Machinery. ISBN 9781450339551. doi: 10.1145/2883817.2883839. URL https://doi.org/10.1145/2883817.2883839. [44] Simone Silvetti, Laura Nenzi, Ezio Bartocci, and Luca Bortolussi. Signal convolution logic. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis, pages 267–283, Cham, 2018. Springer International Publishing. ISBN 978-3-030-01090-4. [45] Houbing Song, Danda B. Rawat, Sabina Jeschke, and Christian Brecher, editors. Cyber-Physical Systems: Foundations, Principles and Applications. Academic Press, 2017. ISBN 9780128038017. [46] Jesper Winsten and Ivan Porres. Continuous Requirement Conformance Falsification for Cyber-Physical Systems via Cross-Revision Knowledge Transfer . In 2026 IEEE International Conference on Software Testing, Verification and Validation (ICST), pages 612–622, Los Alamitos, CA, USA, May 2026. IEEE Computer Society. doi: 10.1109/ICST69053. 2026.00083. URL https://doi.ieeecomputersociety.org/10.1109/ICST69053.2026.00083. [47] T. Yamaguchi, B. Hoxha, and D. Ničković. RTAMT – runtime robustness monitors with application to CPS and robotics. International Journal on Software Tools for Technology Transfer, 26:79–99, 2024. doi: 10.1007/s10009-023-00720-3.

, Vol. 1, No. 1, Article . Publication date: August 2026.

38

A

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

SETTING OF SPECIFICATIONS PARAMETERS

A.1

RQ1

Based on the observed step responses, the bandwidth 𝑓𝑏 is approximately 1 Hz for the drone and 0.2 Hz for the aircraft. Intuitively, these values correspond to reaction times on the order of seconds for the drone and tens of seconds for the aircraft. Table 8 reports the parameter values used in the precondition formulas for RQ1 (Section 6.2), together with the rationale for their selection. Table 8. Parameter values used in the precondition specifications. The “f.int.” rows indicate the frequency intervals selected for the frequency predicates.

A.2

Parameter

Drone

Aircraft

Explanation

𝑡 max

15 s

120 s

𝜎

0.1 m

50 m

𝜏 𝜀

3s 5 mm/s

9s 0.25 m/s

ssth

5 mm

0.05 m

SS f.int. ov th

[0.5, 2]Hz 5 mm

[0.1, 1]Hz 6m

OV f.int.

[0.25, 2]Hz

[0.05, 1]Hz

rt th RT f.int. ST

5 mm [0.8, 3]Hz 3s

0.05 m [1.15, 4]Hz 9s

ssth_𝑟 ST f.int.

5 mm [0.5, 2]Hz

0.05 m [0.1, 1]Hz

The drone completes manoeuvres in a few seconds; the aircraft in tens of seconds. A relevant input change for the drone is 10 cm and for the aircraft is 50 m. Set equal to the settling time. A rate of change below a few mm for the drone and a few dm for the aircraft practically corresponds to a constant signal. Similar to 𝜀. For the aircraft, a smaller threshold can be used because the signals are more stable. Frequency range around and above 𝑓𝑏 . Chosen to capture relevant input changes, but smaller than 𝜎 because these correspond to high-frequency components. Frequency range around 𝑓𝑏 . Wider than SS on the lower bound to better capture possible amplifications. Same as ssth . Frequency range above 𝑓𝑏 . Chosen based on the observed convergence time of the step responses. Same as ssth . Same frequency interval as for SS.

RQ2

All formulas begin with either a □ or ^ operator over a time interval covering the entire trace: 20 s for SP and OS, and 100 s for RT, ST, OV and SS. In the templates presented in Section 5, we used 𝑓max to denote the maximum frequency of the time-frequency representation. However, in practice, most high-frequency components have very small amplitude and carry little or no useful information. In our experiments, 𝑓𝑏 is typically around 1 Hz, with the relevant frequency components lying below 3 Hz. Therefore, in all formulas we set 𝑓max to 4 Hz, avoiding unnecessary evaluation of very high-frequency components that do not carry useful information. A.2.1

SP.

STL: The value 0.01 used to compute the discrete derivative corresponds to the sampling time. The 2 s time bound of the ^ operator represents an upper bound on the spike width. The amplitude threshold of 5 is adopted from the original work [28], which assumes an expected , Vol. 1, No. 1, Article . Publication date: August 2026.

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

39

spike amplitude of 10. Specifically, the threshold is chosen such that the product of the spike amplitude and the derivative threshold remains proportional to the expected amplitude. S2TL: The 1 s time bound of the □ operator represents a lower bound on the spike width. The threshold value of 1 for the time-frequency transform is derived from the actual expected spike amplitude of 10, but is reduced by one order of magnitude as it is a higher-frequency component. The frequency interval [0.5, 4] is chosen to include components above 0.5 Hz, as those include the expected longest spike duration of 2 s—in fact, the duration is inverse to the frequency. A.2.2

OS.

STL: The amplitude thresholds of 20 and 40 are based on the expected peak-to-peak amplitude (i.e., twice the expected amplitude range of 10 to 20). The time interval of the ^ operator is set to [0.48, 0.52]s, providing a small margin around half of the expected oscillation period. The time shift of the ∗ operator is set to 0.25 s, corresponding to half of the time interval of the ^ operator, as prescribed in the original work [28]. S2TL: The amplitude thresholds of 4.5 and 10 are set to approximately half of the expected amplitude of the oscillations to account for the scaling of the time-frequency representation. The frequency interval [0.85, 1.15]Hz is chosen to capture the expected oscillation period of 1 s, corresponding to a frequency of 1 Hz. The frequency intervals [0.4, 0.85]Hz and [1.15, 1.6]Hz are used to characterize the low-amplitude frequency intervals around the frequency range where we expect to see the oscillation. A.2.3

RT.

STL: The value of 1 specifies the minimum size of the considered step changes in the input. The time interval of the ^ operator is set to [0, 0.75]s, corresponding to the prescribed 0% to 75% rise time reported in Table 3. S2TL: The prescribed 0% to 75% rise time of 0.75 s corresponds to a bandwidth of approximately 0.3 Hz. Accordingly, for the low-frequency part of the specification we use a predicate over the interval [0, 0.3]Hz, while the high-frequency part considers frequencies above [0.6]Hz. The value of 0.25 for the low-frequency error is derived from the value for the SS requirement, but is increased because the RT predicates about the transients of the output tracking the input, where a larger tracking error is expected. Since the input amplitude can reach 10, a threshold of 0.25 corresponds to a maximum error of 2.5%. For the high-frequency part of the specification, which checks for filtering behaviour, we use a threshold of 0.1. Because the input amplitude can be as high as 10, this threshold excludes time-frequency components whose amplitudes are too small to support a reliable assessment. A.2.4

ST.

STL: The value of 1 specifies the minimum amplitude of the considered step changes in the input. The time interval [4.5, 6]s in the □ operator is based on the prescribed settling time of 4.5 s, allowing for an additional 1.5 s window during which the input-output difference is evaluated. The coefficient 0.02 is based on the 2%-range definition of the settling time. S2TL: The upper bound of the time interval [0, 2.25] in the until operator is chosen based on the prescribed settling time of 4.5 s. We use half of the actual settling time requirement because the time-frequency transform reduces the resolution along the time axis, and thus requires additional slack. Regarding the frequency intervals, the settling time of 4.5 s corresponds to an approximate bandwidth of 0.15 Hz. Thus, to check that the input and output are at steady state, we predicate over the frequency range [0.15, 4]Hz. The threshold of 0.1 is based on , Vol. 1, No. 1, Article . Publication date: August 2026.

40

Claudio Mandrioli, Drishti Yadav, and Domenico Bianculli

the minimum relevant unit changes, but reduced by one order of magnitude because the predicate operates on higher-frequency components. A.2.5 OV. STL: The value of 1 specifies the minimum magnitude of the considered step changes in the input. The time interval of the □ operator is set to [0, 2]s to fully capture the transient during which the output tracks an input change. The coefficient 0.15 is based on the maximum allowable overshoot (Table 3). S2TL: The predicate is evaluated over the frequency range [1, 3]Hz, corresponding to the system bandwidth of 2 Hz. Because the input and output changes are in the range of units while the predicate targets high-frequency components, we use a threshold of 0.05 to disregard insignificant output variations. The coefficient of 1.15 implements the allowable 15% overshoot by permitting an output amplification of up to (15%) relative to the input. A.2.6 SS. STL: To detect steady state, we select a threshold of 0.01 to the discrete derivative, which corresponds to a rate of change of 1 unit per second (analogous to the minimum input step of size 1 considered in the other specifications). Following the original formulation in [28], for the until operator, we consider the time interval [2, 2.02]s to evaluate the tracking error after the transient, as the generated system has a settling time of 2 s. The value of 0.1 corresponds to the maximum allowable static error specified in Table 3. S2TL: Since the settling time of 0.75 s corresponds to a frequency bandwidth of 1 Hz, to detect the steady-state behaviour of the input, we consider the frequency range [0.5, 4]Hz. The upper threshold on the high-frequency components of the input is set to 0.01, based on the allowable static error, but reduced because the predicate operates on high-frequency components. The time-frequency spectrum of the tracking error is bounded by 0.1, in accordance with the specification (Table 3), and is evaluated over the low-frequency range of [0, 0.2]Hz.

, Vol. 1, No. 1, Article . Publication date: August 2026.

Related documents

• A systems and control perspective of CPS security#199447
• FBSDEs with time delayed generators: Lp-solutions, differentiability, representation formulas and path regularity#350784
• Geometric Ceilings on Time-Frequency Masking for Single-Channel Separation#987842
• Reserved Type, Length and Value (TLV) Codepoints in Intermediate System to Intermediate System#135040
• Frame Constitution and Identity Tolerance: The Determination of δ_F in La Profilée#732023