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

一种完全抽象的PSI演算符号语义

A Fully Abstract Symbolic Semantics for Psi-Calculi

Magnus Johansson, Björn Victor, Joachim Parrow

摘要:

我们提出了一个符号转换系统和PSI演算的互模拟等价,并证明了它是完全抽象的非符号语义的互模拟同余。psi演算是pi演算的扩展,具有用于数据结构和用于表示关于数据的事实的逻辑断言的名义数据类型。这些可以在进程之间传输,并且它们的名称可以使用标准的pi演算机制进行静态作用域,以允许范围迁移。PSI演算可以比其他提出的pi演算的扩展更一般,例如应用pi演算,pi演算,融合演算或并发约束pi演算。符号语义对于在探索状态空间的自动化工具中有效地实现微积分是必要的,并且完全抽象属性意味着过程的语义不会从原始的改变。

英文摘要:

We present a symbolic transition system and bisimulation equivalence for psi-calculi, and show that it is fully abstract with respect to bisimulation congruence in the non-symbolic semantics. A psi-calculus is an extension of the pi-calculus with nominal data types for data structures and for logical assertions representing facts about data. These can be transmitted between processes and their names can be statically scoped using the standard pi-calculus mechanism to allow for scope migrations. Psi-calculi can be more general than other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, or the concurrent constraint pi-calculus. Symbolic semantics are necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means the semantics of a process does not change from the original.

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

↑