Work by Curtis Madsen, Prashant Vaidyanathan, Sadra Sadraddini, Cristian-Ioan Vasile, Nicholas A. DeLateur, Ron Weiss, Douglas Densmore, and Calin Belta, IEEE CDC 2018

Keywords: Signal Temporal Logic, Metric Spaces

Summary

The authors discuss how STL formulae can admit a metric space under mild assumptions. They present two metrics: the Pompeiu-Hausdorff (PH) and the Symmetric Difference (SD) metrics. The PH distance measures how much the language of one formula needs to be enlarged to include the other. The SD distance measures the overlap between the two formulae. The PH distance can be formulated as a Mixed-Integer Linear Programming (MILP) optimization problem which can be computed fairly quickly (although complexity grows exponentially with the number of predicates are formulae horizon). The SD distance is computed using a recursive algorithm based on the area of satisfaction. Its complexity depends on the complexity of the norm operation.

Read the paper on arXiv here.