论文标题
通信系统可逆计算的结构等价(口腔通信)
Structural Equivalences for Reversible Calculi of Communicating Systems (Oral communication)
论文作者
论文摘要
工艺代数的形式化通常始于其过渡系统的运算符和规则的最小核心,然后放松系统以提高其可用性并简化证明。在通信系统(CCS)的计算中,结构一致性通过使例如并行组成的交换性和关联性:没有它,该系统将很麻烦,并且可以证明这种变化在精确的技术意义上是无害的。对于两个可逆的计算CCS,情况不太清楚:带有通信键(CCSK)的CC首先是在没有任何结构一致性的情况下定义的,然后赋予了CCS一致性的片段。可逆的CCS(RCC)选择了“在”结构对等上的“支持”,这成为系统的“最小核心”的一部分。在这种简短的口头交流中,我们想重新考虑一般结构一致性的状态和作用,特别是质疑其在RCC中的作用,并提出对结构等价合法性的更一般性问题。
The formalization of process algebras usually starts with a minimal core of operators and rules for its transition system, and then relax the system to improve its usability and ease the proofs. In the calculus of communicating systems (CCS), the structural congruence plays this role by making e.g. parallel composition commutative and associative: without it, the system would be cumbersome to use and reason about, and it can be proven that this change is innocuous in a precise technical sense. For the two reversible calculi extending CCS, the situation is less clear: CCS with Communication Keys (CCSK) was first defined without any structural congruence, and then was endowed with a fragment of CCS's congruence. Reversible CCS (RCCS) made the choice of "backing in" the structural equivalence, that became part of the "minimal core" of the system. In this short oral communication, we would like to re-consider the status and role of the structural congruence in general, to question its role in RCCS in particular, and to ask the more general question of the structural equivalences legitimacy.