通信系统可逆演算中的结构等价性（口头报告）
形式语言与自动机理论
2020-05-15 v1 计算机科学中的逻辑
逻辑
摘要
进程代数的形式化通常始于一个极小的算子核心及其转移系统的规则，然后放宽系统以提升可用性与证明简便性。在通信系统演算（CCS）中，结构同余通过使例如并行组合满足交换与结合 law 来扮演此角色：若无它，系统将繁琐难用且难以推理，并且可从精确的技术意义上证明这一改动是无害的。对于扩展 CCS 的两个可逆演算，情况则不甚清晰：带通信密钥的 CCS（CCSK）最初定义时无任何结构同余，随后被赋予 CCS 同余的一个片段。可逆 CCS（RCCS）选择了将结构等价“内建”进来，使其成为系统“极小核心”的一部分。在这篇简短的口头报告中，我们愿重新审视结构同余在一般情况下的地位与作用，尤其质疑其在 RCCS 中的作用，并提出关于结构等价合法性的更一般问题。
引用
@article{arxiv.2005.06818,
title = {Structural Equivalences for Reversible Calculi of Communicating Systems (Oral communication)},
author = {Clément Aubert and Ioana Cristescu},
journal= {arXiv preprint arXiv:2005.06818},
year = {2020}
}