进程代数 CCS 在 HOL4 中的形式化
计算机科学中的逻辑
2017-06-20 v2
摘要
一个关于进程代数 CCS（无值传递，带显式重标记算子）的旧形式化已从 HOL88 定理证明器移植到 HOL4（Kananaskis-11 及后续版本）。CCS 进程间的转换由结构化操作语义（SOS）推理规则定义，随后所有代数定律（包括展开定理）均基于 SOS 转换规则得到证明。我们利用 HOL4 新的余归纳关系支持重新定义了强互模拟等价和弱互模拟等价，并证明了新定义与旧定义等价。最后，提供了用于自动检测 CCS 转换的判定过程。其目标是提供一个最新的、可靠且有效的工具来支持 CCS 的验证与推理，并为并发理论的进一步发展提供形式逻辑基础。
引用
@article{arxiv.1705.07313,
title = {A Formalization of the Process Algebra CCS in HOL4},
author = {Chun Tian},
journal= {arXiv preprint arXiv:1705.07313},
year = {2017}
}
备注
26 pages