Psi-演算的完全抽象符号语义
计算机科学中的逻辑
2010-02-16 v1
摘要
我们为psi-演算提出了一个符号迁移系统和互模拟等价,并证明它在非符号语义中关于互模拟同余是完全抽象的。Psi-演算是pi-演算的扩展,它使用名义数据类型来表示数据结构,以及表示关于数据事实的逻辑断言。这些可以在进程之间传输,并且它们的名称可以使用标准的pi-演算机制进行静态作用域限定,以实现作用域迁移。Psi-演算可以比pi-演算的其他扩展(如应用pi-演算、spi-演算、融合演算或并发约束pi-演算)更通用。符号语义对于在探索状态空间的自动化工具中高效实现该演算是必要的,而完全抽象性质意味着进程的语义不会改变原始语义。
引用
@article{arxiv.1002.2867,
title = {A Fully Abstract Symbolic Semantics for Psi-Calculi},
author = {Magnus Johansson and Björn Victor and Joachim Parrow},
journal= {arXiv preprint arXiv:1002.2867},
year = {2010}
}