标号状态-函数转移系统的余代数互模拟
计算机科学中的逻辑
2017-01-11 v2
摘要
标号状态-函数转移系统（简称 FuTS）的特征在于其转移将状态与一般半环上以状态为变量的函数相关联，并配备了一组丰富的高阶算子。因此，FuTS 构成了一种便捷的建模工具，用于处理进程语言及其定量扩展。在本文中，从余代数的角度探讨了由 FuTS 引出的互模拟概念。建立了一个对应结果，指出 FuTS 互模拟与相关函子的行为等价相一致。作为一般性示例，将主要定量进程代数实例的实质片段所隐含的等价关系与特定 FuTS 的互模拟联系起来。这些示例涵盖从随机进程语言 PEPA 到交互式马尔可夫链语言 IML、（离散）时间进程语言 TPC 以及马尔可夫自动机语言 MAL。这些语言隐含的等价关系与其特定 FuTS 的互模拟相关联。通过该对应结果，获得了这些演算的等价关系的余代数证明。特定的语言选择不仅涵盖了涉及量的各种进程交互模型和建模选择，还使我们能够展示不同类别的 FuTS，即所谓的简单 FuTS、组合 FuTS、嵌套 FuTS 和一般 FuTS。
引用
@article{arxiv.1511.05866,
title = {Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically},
author = {Diego Latella and Mieke Massink and Erik P De Vink},
journal= {arXiv preprint arXiv:1511.05866},
year = {2017}
}