CSP-Agda的迹与稳定失败语义
编程语言
2017-09-15 v1 分布式、并行与集群计算
计算机科学中的逻辑
摘要
CSP-Agda 是一个库，它使用协归纳数据类型在交互式定理证明器 Agda 中形式化了进程代数 CSP。在 CSP-Agda 中，CSP 进程采用单子形式，这支持进程的模块化开发。本文在 CSP-Agda 中实现了 CSP 的两个主要模型，即迹语义和稳定失败语义，并定义了相应的精化(refinement)与等价关系。由于单子设置，需要做一些调整。作为示例，我们证明了外部选择算子关于迹语义的交换性，以及关于稳定失败语义的精化是一个偏序。所有证明和定义都已在 Agda 中通过类型检查。代数定律的进一步证明将在 CSP-Agda 代码库中获取。
引用
@article{arxiv.1709.04714,
title = {Trace and Stable Failures Semantics for CSP-Agda},
author = {Bashar Igried and Anton Setzer},
journal= {arXiv preprint arXiv:1709.04714},
year = {2017}
}
备注
In Proceedings CoALP-Ty'16, arXiv:1709.04199