Bisimulation和模态逻辑在pi演算的证明搜索规范
摘要：有限π计算的操作语义和同步关系在一个逻辑中被指定，该逻辑包含了用于编码泛型判断和定义的“nabla”量词，以及用于编码固定点的定义。由于限制在有限情况下，逻辑的展开固定点的能力使得该逻辑对于操作语义的归纳性质和同步关系的共归纳性质都是完备的。 “nabla”量词有助于处理π计算表达式和它们的执行（证明）中与变量的作用域相关的微妙问题。我们展示了这个逻辑允许的逻辑规范的几个优点：它们是自然和声明性的；它们不包含关于变量名称的任何副条件，同时完全形式地处理这样的变量；晚期和开放的同步关系之间的差异源于熟悉的逻辑区别；三个量词（对于所有，存在和nabla）及其作用域之间的相互作用可以解释早期和晚期同步关系以及基于绑定输入和输出动作的各种模态操作符之间的差异；证明搜索涉及推理规则的应用，解一致性和回溯可以为一步转换、同步关系和模态逻辑的满足提供完备的证明系统。我们还展示了如何在具有归纳和共归纳的扩展逻辑中对π计算进行复制编码。
作者：Alwen Tiu and Dale Miller
论文ID：0805.2785
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2009-02-16