Madsen, CurtisVaidyanathan, PrashantSadraddini, SadraVasile, Cristian-IoanDeLateur, Nicholas A.Weiss, RonDensmore, DouglasBelta, Calin2020-05-112020-05-112018-01-01Curtis Madsen, Prashant Vaidyanathan, Sadra Sadraddini, Cristian-Ioan Vasile, Nicholas A DeLateur, Ron Weiss, Douglas Densmore, Calin Belta. 2018. "Metrics for Signal Temporal Logic Formulae." 2018 IEEE CONFERENCE ON DECISION AND CONTROL (CDC), pp. 1542 - 1547 (6).0743-1546https://hdl.handle.net/2144/40745Signal 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.p. 1542 - 1547en-USScience & technologyAutomation & control systemsEngineering, electrical & electronicRobustnessLogic in computer scienceFormal languages and automata theoryArticle396573