  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.
