Metrics for Signal Temporal Logic Formulae
Metrics for Signal Temporal Logic Formulae
复制标题
信号时态逻辑公式的度量
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
C. Belta
中科院分区：
文献类型：
--
作者：
C. Madsen;P. Vaidyanathan;Sadra Sadraddini;C. Vasile;Nicholas A. DeLateur;Ron Weiss;D. Densmore;C. Belta
信号时序逻辑（STL）是一种形式语言，用于描述信息物理系统中广泛的实值时序属性。虽然对于从STL需求进行验证和控制综合已有大量研究，但没有用于比较两个STL公式的正式框架。在本文中，我们表明在温和的假设下，STL公式存在一个度量空间。我们基于以下两点在此空间上提出两种度量：i）庞贝乌 - 豪斯多夫距离，ii）对称差度量，并给出计算它们的算法。除了说明性示例外，我们还将这些度量作为设计质量度量进行应用，用于比较设计系统（例如合成基因电路）的所有时序行为与“期望”规范。
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 an application of these metrics as design quality measures where they are used to compare all the temporal behaviors of a designed system, such as a synthetic genetic circuit, with the “desired” specification.