Linear and Branching System Metrics
Linear and Branching System Metrics
复制标题
DOI：
10.1109/tse.2008.106
复制
发表时间：
2009-03-01
影响因子：
7.4
通讯作者：
Stoelinga, Marielle
中科院分区：
文献类型：
--
作者：
de Alfaro, Luca;Faella, Marco;Stoelinga, Marielle
我们将经典的包含、等价、模拟和双模拟的系统关系扩展到一个定量的设定，在这个设定中，命题不是被解释为布尔值，而是作为任意度量空间的元素。微量包裹体和等效体产生不对称和对称的线性距离，模拟和双模拟产生不对称和对称的分支距离。我们研究了这些距离之间的关系，并根据LTL和mu微积分的定量版本提供了距离的完整逻辑表征。我们表明，虽然确定性布尔转换系统的痕量包含（分别，等效）与模拟（分别，双模拟）一致，但确定性度量转换系统的线性和分支距离并不一致。最后，我们提供了在有限系统上计算距离的算法，以及一个匹配的低复杂度界。
We extend the classical system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as elements of arbitrary metric spaces. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. We study the relationships among these distances and we provide a full logical characterization of the distances in terms of quantitative versions of LTL and mu-calculus. We show that, while trace inclusion (respectively, equivalence) coincides with simulation (respectively, bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic metric transition systems. Finally, we provide algorithms for computing the distances over finite systems, together with a matching lower complexity bound.