Average-based Robustness for Continuous-Time Signal Temporal Logic

Calin Belta; Cristian-Ioan Vasile; Noushin Mehdipour

REVIEW 4 major objections 6 minor 23 references

Average-based Robustness for Continuous-Time Signal Temporal Logic

T0 review · 4 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proposes a new average-based STL robustness score, AGIM, that agrees with standard STL semantics in sign while using every time and subformula.

desk verdict A promising average-based robustness score for continuous-time STL with a real definitional contribution, but the soundness theorem is overstated and the finite-sampling implementation falls short of the paper's own continuity claims. read the letter →

arxiv 1909.00898 v1 pith:IE623UKL submitted 2019-09-03 cs.FL cs.RO

Noushin Mehdipour , Cristian-Ioan Vasile , Calin Belta This is my paper · ORCID

classification cs.FLcs.RO

keywords SignalTemporalLogicrobustnesscontinuous-timesignalsfalsificationcontrolsynthesisarithmetic-geometricmeangeometricintegralmulti-agentsystems

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper replaces the worst-point min/max robustness of Signal Temporal Logic with an average-based score called Arithmetic-Geometric Integral Mean (AGIM), defined for continuous-time signals. It claims that the new score is sound in the usual STL sense: a strictly positive score means the specification is satisfied, and a strictly negative score means it is violated. Unlike the traditional score, which is determined by a single most extreme time point or subformula, AGIM uses arithmetic and geometric integral means so that every time and every subformula contributes. The authors show that this gives a smoother, more informative objective for falsification and control synthesis, and they demonstrate this on an automotive benchmark and multi-agent examples.

What carries the argument

The carrying object is the Arithmetic-Geometric Integral Mean score, built from two continuous averaging operations: the arithmetic integral mean $\frac{1}{b-a}\int_a^b f(\tau)\,d\tau$ and the geometric integral mean $\prod_a^b f(x)^{dx}=\exp\left(\int_a^b \ln f(x)\,dx\right)$, the continuous analog of a product. The key design choice is which mean is applied where: arithmetic means for disjunction and Eventually, where the total positive evidence matters, and geometric means for conjunction and Globally, where consistency across all times matters; negative evidence is averaged arithmetically. This split is what lets every subformula and every time contribute to the score while preserving sign-soundness with respect to the traditional semantics.

What would settle it

Run the AGIM algorithm on a continuous-time signal that contains a brief violation shorter than the implementation's sampling interval, such as a one-millisecond overshoot above the threshold in a step response sampled coarsely; if the sampled implementation returns a positive AGIM score for a Globally specification while the true continuous signal violates it, the practical soundness claim is falsified.

Watch

Extended reading notes

Core claim

The central claim is that a recursively defined average-based robustness $\eta(\phi,S,t)\in[-1,1]$ is sound and strictly more informative than the traditional STL robustness $\rho$. For predicates, $\eta(\mu,S,t)=\tfrac{1}{2}(s_i(t)-\pi)$; negation flips the sign; conjunction and Globally use the geometric integral of $(1+\eta)$ when all subformulae are positive, otherwise average the negative parts; disjunction and Eventually use the arithmetic mean of positive parts when some part is positive, otherwise a negative geometric form. Theorem 2 states that $\eta(\phi,S,t)>0 \iff \rho(\phi,S,t)>0$, and $\eta(\phi,S,t)<0 \iff \rho(\phi,S,t)<0$, so the sign of AGIM always agrees with the standard STL satisfaction relation while its magnitude summarizes the entire signal rather than one extreme point.

Load-bearing premise

The recursive AGIM evaluation must decide an 'any' condition over a continuous interval, for example whether there exists a time in $[t+a,t+b]$ where the subformula score is non-positive, and in the implemented versions this is checked only on finitely many simulation samples, so very short violations between samples can be missed.

Editorial extensions

If this is right

In falsification, minimizing AGIM instead of traditional robustness finds executions with more severe violations, because violations at every time and in every subformula contribute; the paper demonstrates this on an automatic transmission benchmark.
In control synthesis, maximizing AGIM makes agents enter assigned regions quickly and stay near their centers, because the time averages reward sustained satisfaction; the paper demonstrates this in two multi-agent examples.
The score is smooth almost everywhere and has non-zero gradient wherever it is smooth, making it compatible with gradient-based optimization for STL tasks.
Because sign agreement with traditional robustness holds, any AGIM-positive trajectory is guaranteed to satisfy the specification and any AGIM-negative trajectory is guaranteed to violate it, so the score can be used as a sound optimization objective.
AGIM distinguishes signals that the traditional score judges equally, such as two step responses with the same peak overshoot but very different overshoot durations.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Inference: a production-grade implementation of AGIM would need a certified way to evaluate the ANY conditions over continuous intervals, such as interval arithmetic or reachability analysis; otherwise the sampled implementation can miss short violations, the exact failure mode the paper uses to motivate continuous-time scoring.
Inference: the same arithmetic/geometric split could be applied to other quantitative semantics, for example robustness under parameter perturbations, yielding a score that is less brittle to noise; the paper does not explore this extension.
Inference: the numerical behavior of the geometric integral near zero scores is worth a dedicated test, since the logarithm in $\ln(1+\eta)$ or $\ln(1-\eta)$ could distort gradients when a subformula is close to its satisfaction boundary.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The AGIM robustness is a real addition to the STL toolkit. Pairing arithmetic means with F/∨ and geometric means with G/∧ is a well-motivated design that avoids the masking and locality of the standard min/max score and gives a normalized score that stays sign-sound in the sense that positive means satisfaction and negative means violation. That alone is a useful step beyond the discrete AGM and the earlier average-based scores, which either used arithmetic means only or lost soundness.

The paper is good at explaining the intuition: for an eventually, averaging the satisfying values rewards staying satisfying for longer, while for a globally, the geometric mean correctly weighs the worst near-violation. The falsification and multi-agent examples support the qualitative claim that the new score differentiates behaviors the traditional score cannot.

But the paper overclaims in two places. First, Theorem 2 states a biconditional: η>0 iff ρ>0 and η<0 iff ρ<0. The negative direction fails under the stated Lebesgue-integrable assumption for signals that are not continuous: a violation that occurs at a single instant gives η=0 while ρ<0. The paper calls η=0 inconclusive, which saves the implications but not the iff. If the authors assume continuity, they should say so and the theorem becomes cleaner. As written, the equivalence is false.

Second, and more important, Algorithm 1 requires an exact ANY test over a continuum, but the case studies clearly evaluate on finite Simulink samples. A violation shorter than the sample spacing is invisible, so the computed score can be positive while the continuous-time signal violates the formula. This is precisely the discretization failure the paper's own motivating example warns against. Remark 1 asserts that efficient representations exist, but no method is given and no code is released. The reader is left with a soundness theorem for an idealized score and an implementation that does not obviously inherit that soundness. That gap deserves a serious response.

The proofs are also sketches—only the G case is shown for Theorem 2, and the smoothness proof is asserted by induction. That might be acceptable in a conference, but for a theorem-driven paper it is thin. The experimental comparisons in Table I are useful but appear to be single-run numbers without statistics.

I would send this to review. With a tightened theorem, a rigorous proof, and some discussion of the finite-sampling approximation—or an exact ANY for the chosen signal representation—the AGIM score could be a solid contribution. Right now it is a promising idea with overclaimed guarantees.

Referee Report

4 major / 6 minor

Summary. The paper proposes Arithmetic-Geometric Integral Mean (AGIM) robustness for continuous-time Signal Temporal Logic (STL), replacing the min/max operations of traditional robustness with operator-dependent arithmetic and geometric integral means. The score is normalized to the interval [−1, 1], and the paper claims that its sign is equivalent to the sign of traditional robustness, hence sound with respect to the usual STL satisfaction relation. The authors argue that averaging over the full signal and all subformulae avoids the masking effect and locality of the traditional score, and they demonstrate the approach on a Simulink automatic-transmission falsification benchmark and on multi-agent control synthesis problems with temporal tasks. Theorem 2 (soundness) is proved only by a sketch covering the Globally case, and several appealing properties (idempotence, commutativity, monotonicity, De Morgan laws, smoothness) are stated with proofs deferred to structural induction.

Significance. The core idea is attractive: an average-based, normalized, sign-sound robustness score is a principled way to make STL robustness more informative for optimization while preserving the meaning of satisfaction and violation. The paper explicitly states a soundness theorem against the independent traditional semantics, which is the right property to establish, and the falsification and synthesis case studies show that the score can distinguish signals that traditional robustness treats as equal. The main value would be in gradient-friendly falsification and control synthesis for continuous-time systems, where a sound score that uses more of the signal could improve optimization landscapes. However, the manuscript as written leaves a significant gap between the exact continuous-time definition, for which soundness is proved, and the finite-sample evaluation actually used in the experiments, and the soundness theorem itself is stated under regularity assumptions that are too weak for the claimed equivalence. The approach is promising and the central claims appear defensible after a substantial revision.

major comments (4)

[Algorithm 1, line 19; Sections V–VI] The exact AGIM score is defined via continuum ANY tests, for example whether there exists τ in [t+a, t+b] with η(ϕ,S,τ) ≤ 0, but the paper provides no exact decision procedure for such tests. Remark 1 only asserts that efficient representations exist. In the falsification and synthesis experiments, the robustness is evaluated on the finite time samples produced by the Simulink simulation and by the piecewise-constant input discretization in Eq. (8). A violation whose duration is shorter than the sampling spacing is invisible to the ANY test, so the computed score can be positive while the underlying continuous-time signal violates the formula. This is precisely the discretization failure that the motivating example (Fig. 1) attributes to discrete-time scores. Consequently, Theorem 2 proves soundness for the idealized exact η, but not for the quantity actually optimized in Sections V and VI. The authors should either implement an exact ANY test for the signal representation used or explicitly present the experimental score as an approximation whose soundness is not claimed.
[Theorem 2, Eq. (5); Section IV assumptions] The claimed equivalence η(ϕ,S,t) < 0 ⇔ ρ(ϕ,S,t) < 0 fails under the stated assumption that signals are bounded and Lebesgue integrable, because a predicate violation on a set of measure zero gives η = 0 while ρ < 0. The proof sketch's converse step, which infers the existence of τ with η(ϕ,τ) < 0 from ρ < 0, is not valid in this generality. The theorem should either assume enough regularity, e.g., continuous or one-sided continuous signals so that a negative robustness implies a violation of positive measure, or state only the one-sided implications η > 0 ⇒ ρ > 0 and η < 0 ⇒ ρ < 0.
[Eq. (4); Algorithm 1, lines 19–32; Eq. (1)] The central definition is not self-consistent as printed. In Eq. (4) and Algorithm 1, the G and F cases use the interval [a,b] in both the ANY condition and the integral bounds, whereas the syntax G[a,b]ϕ at time t and the proof sketch of Theorem 2 use [t+a, t+b]. As written, the score does not depend on t. Additionally, the STL syntax in Eq. (1) includes the Until operator, but Definition 2 and Algorithm 1 define no case for ϕ1 U[a,b] ϕ2, even though Theorem 2 is stated for arbitrary STL formulas. The authors should fix the time offset in the definition and either extend the robustness definition to Until or explicitly restrict the paper's claims to the F/G fragment.
[Section IV-C, Smoothness Properties] The smoothness claims are load-bearing for the paper's motivation, since the score is proposed as an improvement for gradient-based optimization, but the proof sketch is not adequate. The claim that left-continuity implies only a countable set of discontinuities does not by itself establish differentiability almost everywhere of the recursively defined integrals, and the time-dependent interval endpoints in the G and F cases require a separate argument. The gradient-nonzero claim also should be stated with the precise conditions under which it holds. Provide complete proofs or weaken the claims to what is actually needed for the optimization experiments.

minor comments (6)

[Eq. (4)] The violation-branch integrals for both G and F contain the placeholder t'_k; this should be τ.
[Theorem 2, Eq. (5)] The statement 'η>0 ⇔ ρ>0 ⇒ S ⊨ ϕ' is ambiguous; use parentheses, e.g., 'η>0 iff ρ>0, and ρ>0 implies S ⊨ ϕ'.
[Remark 1] Remark 1 is too vague: it should name concrete dense-time monitoring algorithms or data structures that realize the ANY test exactly, since the paper's continuous-time claim depends on this.
[Section VI, Table I] The empirical comparisons are single-run examples without confidence intervals or repeated trials; Table I reports averages without variance, so the runtime and performance claims are not statistically supported.
[Section II and Definition 2] Section II allows arbitrary continuous predicates µ := l(S) ≥ 0, but Definition 2 only defines the AGIM score for predicates of the form si ≥ π; the syntax and the robustness definition should be reconciled.
[References] Reference [21] lists 'H. A. Bardh Hoxha and G. Fainekos'; verify the author list, which appears malformed.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: AGIM soundness is derived from the new definition, not assumed or fit.

full rationale

The paper's claimed derivation is self-contained. Definition 2 and Eq. (4) fully define the AGIM score eta recursively, and Theorem 2 is proved by structural induction from this definition against the independently defined STL robustness rho of Ref. [9]; the atomic case is eta(mu) = 1/2(s_i - pi), a positive rescaling of rho for the restricted predicate set, and the Boolean/temporal cases are written so the sign of the aggregate agrees with the min/max sign of rho. No parameter is fitted and no empirical quantity is called a prediction after being used as an input. The only self-citation [19] ('In [19], we defined AGM robustness for discrete signals...') is background for the continuous extension; the extension is defined and proved here, so the citation is not load-bearing. Remark 1's claim that efficient ANY representations exist is an unproved implementation assertion, and the finite-sampling realization in Sections V-VI can miss short violations; that is a correctness/completeness gap in the implementation, not a circularity of the definition. Thus no circular step is present.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper introduces no new physical entities. Its central load-bearing inputs are the standard STL semantics, a bounded-signal normalization, and the practical decidability of the ANY predicate on continuous intervals, the last of which is only approximated in the implementations.

assumptions (3)

domain assumption Signals are bounded, Lebesgue integrable in the additive and multiplicative senses, with components normalized to [-1,1].
Section IV states this assumption before the definition. It ensures the geometric integral means are well-defined and the score is normalized.
standard math The traditional STL robustness semantics (Definition 1) and its soundness (Theorem 1) are taken as background.
The AGIM soundness proof uses traditional robustness ρ as the ground truth.
domain assumption The ANY condition over a continuous interval, i.e., the existence of a time τ with η(ϕ,τ) ≤ 0 for G (or > 0 for F), can be evaluated.
Algorithm 1 relies on this. In practice it is approximated on a finite grid, which can miss short violations.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Average-based Robustness for Continuous-Time Signal Temporal Logic." pith.science (2026). https://pith.science/paper/IE623UKL

@misc{pith2026190900898,
  author       = {Pith},
  title        = {Pith review of: Average-based Robustness for Continuous-Time Signal Temporal Logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IE623UKL}},
  note         = {Machine review of arXiv:1909.00898}
}

read the original abstract

We propose a new robustness score for continuous-time Signal Temporal Logic (STL) specifications. Instead of considering only the most severe point along the evolution of the signal, we use average scores to extract more information from the signal, emphasizing robust satisfaction of all the specifications' subformulae over their entire time interval domains. We demonstrate the advantages of this new score in falsification and control synthesis problems in systems with complex dynamics and multi-agent systems.

Figures

Figures reproduced from arXiv: 1909.00898 by the authors.

**Figure 4.** Falsifying execution ( [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗

**Figure 5.** Falsifying execution (RPM Left, Speed Right) minimizing robustness η determined by the areas colored in red. is 0.34 ms for the traditional robustness and 0.41 ms for the AGIM robustness. Note that the time in the first column includes the time of generating the input, running the simulink for the generated input at each evaluation, generating resulting trajectories and calculating robustness. B. Control Synthesis W… view at source ↗

Figures from the paper (4 more)

**Figure 6.** Figure 6: (Right) shows the agents’ trajectories satisfying φ2 and avoiding the obstacle. Note that the trajectories are updated to avoid the obstacle, and due to the constraints on time and control input, the agents visit region Y ellow (robustness is positive) but do not reach…

**Figure 7.** Figure 7: Scores related to each agent visiting assigned regions for the [PITH_FULL_IMAGE:figures/full_fig_p007_7.png]

**Figure 8.** Figure 8: Agents’ trajectories satisfying φ3 with agents staying in the center of assigned regions as long as possible. Triangles in cyan show the formation at t = 5, t = 13, t = 19 and t = 28 formed due to ufi while the agents meet their temporal requirements, and the black tri…

**Figure 9.** Figure 9: Scores related to each agent visiting assigned regions for the [PITH_FULL_IMAGE:figures/full_fig_p008_9.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

23 extracted references · 20 canonical work pages

[1]

Belta, B

C. Belta, B. Yordanov, and E. A. Gol, Formal methods for discrete- time dynamical systems . Springer, 2017, vol. 89

work page 2017
[2]

The temporal logic of programs,

A. Pnueli, “The temporal logic of programs,” in 18th Annual Sympo- sium on Foundations of Computer Science , Oct 1977, pp. 46–57

work page 1977
[3]

Specifying real-time properties with metric temporal logic,

R. Koymans, “Specifying real-time properties with metric temporal logic,” Real-time systems, vol. 2, no. 4, pp. 255–299, 1990

1990
[4]

Time window temporal logic,

C.-I. Vasile, D. Aksaray, and C. Belta, “Time window temporal logic,” Theoretical Computer Science , vol. 691, pp. 27–54, 2017

work page 2017
[5]

Monitoring temporal properties of contin- uous signals,

O. Maler and D. Nickovic, “Monitoring temporal properties of contin- uous signals,” in Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 2004, pp. 152–166

2004
[6]

Sampling-based Synthesis of Maximally-Satisfying Controllers for Temporal Logic Speciﬁcations,

C. I. Vasile, V . Raman, and S. Karaman, “Sampling-based Synthesis of Maximally-Satisfying Controllers for Temporal Logic Speciﬁcations,” in IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), Vancouver, BC, Canada, 2017, pp. 3840–3847

work page 2017
[7]

Prescribed performance control for signal temporal logic speciﬁcations,

L. Lindemann, C. K. Verginis, and D. V . Dimarogonas, “Prescribed performance control for signal temporal logic speciﬁcations,” in 2017 IEEE 56th Annual Conference on Decision and Control (CDC) , Dec 2017, pp. 2997–3002

work page 2017
[8]

Cooper- ative planning for coupled multi-agent systems under timed temporal speciﬁcations,

A. Nikou, D. Boskos, J. Tumova, and D. V . Dimarogonas, “Cooper- ative planning for coupled multi-agent systems under timed temporal speciﬁcations,” in 2017 American Control Conference (ACC) . IEEE, 2017, pp. 1847–1852

work page 2017

Show all 23 references

[9]

Robust satisfaction of temporal logic over real-valued signals,

A. Donz ´e and O. Maler, “Robust satisfaction of temporal logic over real-valued signals,” in International Conference on Formal Modeling and Analysis of Timed Systems . Springer, 2010, pp. 92–106

2010
[10]

Spatial-temporal pattern synthesis in a network of locally interacting cells,

N. Mehdipour, D. Briers, I. Haghighi, C. M. Glen, M. L. Kemp, and C. Belta, “Spatial-temporal pattern synthesis in a network of locally interacting cells,” in 2018 IEEE Conference on Decision and Control (CDC). IEEE, 2018, pp. 3516–3521

2018
[11]

Convergence proofs for Simulated An- nealing falsiﬁcation of safety properties,

H. Abbas and G. Fainekos, “Convergence proofs for Simulated An- nealing falsiﬁcation of safety properties,” in Allerton Conference on Communication, Control, and Computing , 2012, pp. 1594–1601

2012
[12]

Randomized kinodynamic plan- ning,

S. M. LaValle and J. J. Kuffner Jr, “Randomized kinodynamic plan- ning,” The International Journal of Robotics Research , vol. 20, no. 5, pp. 378–400, 2001

2001
[13]

Model predictive control with signal temporal logic speciﬁcations,

V . Raman, A. Donz ´e, M. Maasoumy, R. M. Murray, A. Sangiovanni- Vincentelli, and S. A. Seshia, “Model predictive control with signal temporal logic speciﬁcations,” in 53rd IEEE Conference on Decision and Control, Dec 2014, pp. 81–87

2014
[14]

An MILP approach for real-time optimal controller synthesis with metric temporal logic speciﬁcations,

S. Saha and A. A. Julius, “An MILP approach for real-time optimal controller synthesis with metric temporal logic speciﬁcations,” in American Control Conference (ACC) . IEEE, 2016, pp. 1105–1110

2016
[15]

Smooth operator: Control using the smooth robustness of temporal logic,

Y . V . Pant, H. Abbas, and R. Mangharam, “Smooth operator: Control using the smooth robustness of temporal logic,” inIEEE Conference on Control Technology and Applications (CCTA) , 2017, pp. 1235–1240

2017
[16]

A policy search method for temporal logic speciﬁed reinforcement learning tasks,

X. Li, Y . Ma, and C. Belta, “A policy search method for temporal logic speciﬁed reinforcement learning tasks,” in Annual American Control Conference (ACC). IEEE, 2018, pp. 240–245

2018
[17]

Time robustness in mtl and expressivity in hybrid system falsiﬁcation,

T. Akazaki and I. Hasuo, “Time robustness in mtl and expressivity in hybrid system falsiﬁcation,” in International Conference on Computer Aided Veriﬁcation. Springer, 2015, pp. 356–374

2015
[18]

Robust control for signal temporal logic speciﬁcations using discrete average space robustness,

L. Lindemann and D. V . Dimarogonas, “Robust control for signal temporal logic speciﬁcations using discrete average space robustness,” Automatica, vol. 101, pp. 377–387, 2019

2019
[19]

Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Speciﬁcations,

N. Mehdipour, C.-I. Vasile, and C. Belta, “Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Speciﬁcations,” 2019 American Control Conference(ACC) , arXiv preprint at https:// arxiv.org/abs/1903.05186

2019 arXiv
[20]

Multiplicative calculus and its applications,

A. E. Bashirov, E. M. Kurpınar, and A. ¨Ozyapıcı, “Multiplicative calculus and its applications,” Journal of Mathematical Analysis and Applications, vol. 337, no. 1, pp. 36–48, 2008

2008
[21]

Benchmarks for temporal logic requirements for automotive systems,

H. A. Bardh Hoxha and G. Fainekos, “Benchmarks for temporal logic requirements for automotive systems,” Proceedings of applied veriﬁcation for continuous and hybrid systems , 2014

2014
[22]

Consensus of multi- agent systems with double-integrator dynamics in the presence of moving obstacles,

N. Mehdipour, F. Abdollahi, and M. Mirzaei, “Consensus of multi- agent systems with double-integrator dynamics in the presence of moving obstacles,” in 2015 IEEE Conference on Control Applications (CCA). IEEE, 2015, pp. 1817–1822

2015
[23]

Flocking for multi-agent dynamic systems: Algo- rithms and theory,

R. Olfati-Saber, “Flocking for multi-agent dynamic systems: Algo- rithms and theory,” California Inst. of Tech. Pasadena Control and Dynamical System, Tech. Rep., 2004

2004

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Belta, B

C. Belta, B. Yordanov, and E. A. Gol, Formal methods for discrete- time dynamical systems . Springer, 2017, vol. 89

work page 2017

[2] [2]

The temporal logic of programs,

A. Pnueli, “The temporal logic of programs,” in 18th Annual Sympo- sium on Foundations of Computer Science , Oct 1977, pp. 46–57

work page 1977

[3] [3]

Specifying real-time properties with metric temporal logic,

R. Koymans, “Specifying real-time properties with metric temporal logic,” Real-time systems, vol. 2, no. 4, pp. 255–299, 1990

1990

[4] [4]

Time window temporal logic,

C.-I. Vasile, D. Aksaray, and C. Belta, “Time window temporal logic,” Theoretical Computer Science , vol. 691, pp. 27–54, 2017

work page 2017

[5] [5]

Monitoring temporal properties of contin- uous signals,

O. Maler and D. Nickovic, “Monitoring temporal properties of contin- uous signals,” in Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 2004, pp. 152–166

2004

[6] [6]

Sampling-based Synthesis of Maximally-Satisfying Controllers for Temporal Logic Speciﬁcations,

C. I. Vasile, V . Raman, and S. Karaman, “Sampling-based Synthesis of Maximally-Satisfying Controllers for Temporal Logic Speciﬁcations,” in IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), Vancouver, BC, Canada, 2017, pp. 3840–3847

work page 2017

[7] [7]

Prescribed performance control for signal temporal logic speciﬁcations,

L. Lindemann, C. K. Verginis, and D. V . Dimarogonas, “Prescribed performance control for signal temporal logic speciﬁcations,” in 2017 IEEE 56th Annual Conference on Decision and Control (CDC) , Dec 2017, pp. 2997–3002

work page 2017

[8] [8]

Cooper- ative planning for coupled multi-agent systems under timed temporal speciﬁcations,

A. Nikou, D. Boskos, J. Tumova, and D. V . Dimarogonas, “Cooper- ative planning for coupled multi-agent systems under timed temporal speciﬁcations,” in 2017 American Control Conference (ACC) . IEEE, 2017, pp. 1847–1852

work page 2017