混合 CSP 的近似互模拟与离散化
计算机科学中的逻辑
2016-09-09 v2
摘要
混合通信顺序进程（HCSP）是一种用于混合系统的强大形式化建模语言，它是 CSP 的扩展，引入了微分方程来建模连续演化，并引入中断来建模连续动态与离散动态之间的交互。本文从操作语义的角度研究 HCSP 的语义基础，提出了近似互模拟的概念，为刻画具有连续和离散行为的 HCSP 进程之间的等价性提供了一个合适的判据。我们给出了一个算法来判断两个 HCSP 进程是否近似互模拟。此外，基于此，我们提出了一种离散化 HCSP 的方法，即给定一个 HCSP 进程 A，构造另一个不包含任何连续动态的 HCSP 进程 B，使得 A 和 B 在给定精度下近似互模拟。这为将已验证的控制模型转换为正确的程序模型提供了一种严格的方法，填补了嵌入式系统设计中的空白。
引用
@article{arxiv.1609.00091,
title = {Approximate Bisimulation and Discretization of Hybrid CSP},
author = {Gaogao Yan and Li Jiao and Yangjia Li and Shuling Wang and Naijun Zhan},
journal= {arXiv preprint arXiv:1609.00091},
year = {2016}
}
备注
FM 2016, Proof Appendix, HCSP, approximately bisimilar, hybrid systems, discretization