Metrics for signal temporal logic formulae
Files
Published version
Date
2018-01-01
DOI
Authors
Madsen, Curtis
Vaidyanathan, Prashant
Sadraddini, Sadra
Vasile, Cristian-Ioan
DeLateur, Nicholas A.
Weiss, Ron
Densmore, Douglas
Belta, Calin
Version
Published version
OA Version
Citation
Curtis 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).
Abstract
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.