arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2005.06818cs.FLcs.LOmath.LO
收藏

交流系统可逆演算的结构等价性(口语交流)

Structural Equivalences for Reversible Calculi of Communicating Systems (Oral communication)

Clément Aubert, Ioana Cristescu

摘要:

进程代数的形式化通常是从其转移系统的最小运算符和规则核开始,然后放松系统以提高其可用性和简化证明。在通信系统演算(CCS)中,结构一致性通过使并行组合成为可交换和可关联的来扮演这个角色:没有它,系统将难以使用和推理,并且可以证明这种变化在精确的技术意义上是无害的。对于扩展CCS的两个可逆演算,情况不太清楚:具有通信密钥的CCS(CCSK)首先被定义为没有任何结构同余,然后被赋予CCS的同余的片段。可逆CCS(RCCS)选择了“支持”结构等效,这成为系统的“最小核心”的一部分。在这个简短的口头交流中,我们想重新考虑一般的结构一致性的地位和作用,特别是质疑它在RCCS中的作用,并提出更普遍的结构等效合法性问题。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑