转移系统归约的应用：导出定量互模拟的逻辑刻画
计算机科学中的逻辑
2017-04-25 v1
摘要
加权标记转移系统（WLTSs）是一种成熟的元模型，旨在为诸如非确定性、随机和概率系统等多种系统提供通用结果与工具。为了涵盖结合多个定量方面的过程，进一步提出了WLTS框架的扩展，状态到函数转移系统（FuTSs）和一致标记转移系统（ULTraSs）是两个突出例子。在本文中，我们表明这一元模型层次在互模拟相干编码视角下发生坍塌。利用这些归约，我们从WLTS的完全抽象逻辑推导出了FuTSs的完全抽象Hennessy-Milner风格逻辑，即刻画定量互相似性的逻辑。
引用
@article{arxiv.1704.07181,
title = {Reductions for Transition Systems at Work: Deriving a Logical Characterization of Quantitative Bisimulation},
author = {Marino Miculan and Marco Peressotti},
journal= {arXiv preprint arXiv:1704.07181},
year = {2017}
}