接口模拟距离
软件工程
2012-10-10 v1 计算机科学中的逻辑
摘要
系统组件行为接口的经典(布尔)细化概念是交替细化预序。在本文中,我们定义了一种称为接口模拟距离的接口距离度量。它通过在交替模拟博弈中容忍错误(同时进行计数),使交替细化预序定量化。我们证明了接口模拟距离满足三角不等式;两个接口之间的距离在与第三个接口并行组合下不会增加;并且两个接口之间的距离可以通过这两个接口的抽象之间的距离进行上下界约束。我们通过两个案例研究说明了该框架,以及接口距离在接口组合下的性质。
引用
@article{arxiv.1210.2450,
title = {Interface Simulation Distances},
author = {Pavol Černý and Martin Chmelík and Thomas A. Henzinger and Arjun Radhakrishna},
journal= {arXiv preprint arXiv:1210.2450},
year = {2012}
}
备注
In Proceedings GandALF 2012, arXiv:1210.2028