# Metrics for Signal Temporal Logic Formulae

arXiv: https://arxiv.org/abs/1808.03315 · HTML: https://mlsanity.com/paper/1808.03315/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Aug 2018.

## Built on by (most cited first, 9 of 9)

- [Temporal Logic Specification-Conditioned Decision Transformer for Offline Safe Reinforcement Learning](https://mlsanity.com/paper/2402.17217/) (2024)
- [Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge](https://mlsanity.com/paper/2505.20658/) (2025)
- [Grammar-Forced Translation of Natural Language to Temporal Logic using LLMs](https://mlsanity.com/paper/2512.16814/) (2025)
- [Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes](https://mlsanity.com/paper/2201.09928/) (2022)
- [STL Robustness Risk over Discrete-Time Stochastic Processes](https://mlsanity.com/paper/2104.01503/) (2021)
- [Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite](https://mlsanity.com/paper/2507.00877/) (2025)
- [stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic](https://mlsanity.com/paper/2405.14389/) (2024)
- [ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification](https://mlsanity.com/paper/2605.01209/) (2026)
- [SPoRt -- Safe Policy Ratio: Certified Training and Deployment of Task Policies in Model-Free RL](https://mlsanity.com/paper/2504.06386/) (2025)

## Abstract (arXiv)

Signal Temporal Logic (STL) is a formal language for describing a broad range of real-valued, temporal properties in cyber-physical systems. While there has been extensive research on verification and control synthesis from STL requirements, there is no formal framework for comparing two STL formulae. In this paper, we show that under mild assumptions, STL formulae admit a metric space. We propose two metrics over this space based on i) the Pompeiu-Hausdorff distance and ii) the symmetric difference measure, and present algorithms to compute them. Alongside illustrative examples, we present applications of these metrics for two fundamental problems: a) design quality measures: to compare all the temporal behaviors of a designed system, such as a synthetic genetic circuit, with the "desired" specification, and b) loss functions: to quantify errors in Temporal Logic Inference (TLI) as a first step to establish formal performance guarantees of TLI algorithms.