进程代数中方程唯一解的形式化
计算机科学中的逻辑
2017-12-29 v1 编程语言
摘要
本论文基于HOL88中的早期工作，在HOL定理证明器（HOL4）中对Milner的通信系统演算（亦称CCS）进行了全面形式化。这包括强/弱互模拟等价与观察同余的所有经典性质、CCS的同余理论、多种“互模拟upto”技术，以及若干深刻定理，即“弱等价中包含的最粗同余”与Milner著作中“方程唯一解”定理的三个版本。本工作进一步扩展以支持并发理论的最新进展，即由博洛尼亚大学Davide Sangiorgi教授发现的“收缩”关系及相关的“收缩唯一解”定理。作为结果，本论文也形式化了CCS中相当完整的“收缩”（及一种称为“展开”的类似关系）理论。此外，作者在此工作期间基于已有收缩关系发现了一种称为“观察收缩”的收缩新变体。我们形式化证明了这一新关系在CCS进程的直接和下保持，并且具有不依赖任何CCS文法限制的更优雅形式的“收缩唯一解”定理。
引用
@article{arxiv.1712.09402,
title = {A Formalization of Unique Solutions of Equations in Process Algebra},
author = {Chun Tian},
journal= {arXiv preprint arXiv:1712.09402},
year = {2017}
}
备注
250 pages, Master degree thesis of Computer Science in University of Bologna