Automata, Languages and Programming
Automata, Languages and Programming
复制标题
自动机、语言和编程
DOI：
10.1007/978-3-540-70583-3_9
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Berger M
中科院分区：
文献类型：
--
作者：
Berger M
我们研究的扩展Hennessy-Milner逻辑的π演算，给出了一个健全的和完整的表征代表性的行为前序和等价的类型化过程。引入了新的连接词来表示实际和假设的类型化并行组合和隐藏。我们研究了三个组合证明系统，描述了May/Must测试前序和双相似性的特征。证明系统统一适用于不同类型的学科。逻辑公理提炼了Amadio和Dam研究的并行组合的证明规则。我们证明了我们的逻辑的表达能力，通过验证状态转移在多方的互动和充分抽象的嵌入程序逻辑高阶函数。
We study an extension of Hennessy-Milner logic for theπ-calculus which gives a sound and complete characterisation of representative behavioural preorders and equivalences over typed processes. New connectives are introduced representing actual and hypothetical typed parallel composition and hiding. We study three compositional proof systems, characterising the May/Must testing preorders and bisimilarity. The proof systems are uniformly applicable to different type disciplines. Logical axioms distill proof rules for parallel composition studied by Amadio and Dam. We demonstrate the expressiveness of our logic through verification of state transfer in multiparty interactions and fully abstract embeddings of program logics for higher-order functions.