Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
我们指定的操作语义和互模拟关系的有限π演算内的逻辑，其中包含的nabla量词编码通用的判断和定义编码不动点。由于我们只限于有限的情况，逻辑展开不动点的能力使得这个逻辑对于操作语义的归纳性质和互模拟的共归纳性质都是完备的。nabla量词有助于解决π演算表达式中变量范围及其执行（证明）的微妙问题。我们说明了这种逻辑所允许的逻辑规范的几个优点：它们是自然的和说明性的;它们不包含关于变量名的副条件，同时保持对这些变量的完全形式化处理;后期互模拟关系和开放互模拟关系之间的差异来自于熟悉的逻辑区别;三个量词之间的相互作用（对于所有，存在，（nabla）它们的作用域可以解释早期互模拟和晚期互模拟之间的差异以及基于约束输入和输出行为的各种模态算子之间的差异;并且涉及推理规则、统一和回溯的应用的证明搜索可以为模态逻辑中的一步转换、互模拟和满足提供完整的证明系统。我们还说明了如何可以编码的π演算与复制，在一个扩展的逻辑与归纳和共归纳。
2009-02-16 cs.LO
History-Preserving Bisimulations on Reversible Calculus of Communicating Systems
历史互模拟和遗传互模拟（HPB和HHPB）是并发指称模型的等价关系。在进程代数中寻找它们的对应物是一个开放的问题，有一些部分的成功：在通信系统演算（CCS）中存在一个基于因果树的等价物，对应于HPB。在可逆CSS（RCCS）中，有一个对应于HHPB的互模拟，但它只考虑没有自动并发的进程。我们提出了等价的CCS与自动并发对应的HPB和HHPB，和他们所谓的“弱”的变种。等价性不仅利用了RCCS的可逆性，而且利用了RCCS的记忆机制。
2018-04-27 cs.DC cs.FL cs.LO
Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $π$-Calculus
本文展示了我们如何利用异步转换系统来定义所应用的$π$ -演算的非交织语义，该系统的转换用事件标记，并且配备了事件独立性的概念。我们定义的最重要的概念是：开始-终止或ST-双相似性，保留事件的持续时间;和历史保留或HP-双相似性，保留因果关系。我们指出，相应的相似前序暴露这些语义之间的区别。我们提请特别注意HP故障相似性的区分能力，并讨论它如何影响攻击者的威胁模型，我们验证的安全性和隐私属性。我们还比较现有的概念，位于双相似性的定义，我们介绍。
2022-09-06 cs.CR cs.DC cs.LO
A Strong Bisimulation for a Classical Term Calculus
本文通过引入修订的 λμ-演算 ΛM 和关系 ≃，解决了 Laurent 的 ≃σ-等价在经典项演算中无法构成强互模拟的问题，并证明 ≃ 是 ΛM 归约下的强互模拟。
2024-04-17 cs.LO
Capturing Bisimulation-Invariant Exponential-Time Complexity Classes
奥托定理将图上的互模拟不变PTIME查询描述为可以在多元μ演算中制定的那些查询，它依赖于Immerman-Vardi定理，Immerman-Vardi定理通过具有最少不动点的一阶逻辑来描述PTIME（有序结构）。这种连接已经通过在谓词上使用函数的polyadic μ演算的扩展到了具有最小不动点的双模拟不变EXPTIME，利用Immerman的二阶逻辑对EXPTIME的表征。在本文中，我们表明，在指数时间层次中的所有类的互模拟不变的版本有逻辑对应的出现作为扩展的polyadic μ演算的高阶函数。这利用了高阶逻辑（k+1阶）对k-EXPTIME的特征化，具有最少的不动点，这是由Freire和Martins提出的。
2022-09-21 cs.CC cs.LO
A Bisimulation-Invariance-Based Approach to the Separation of Polynomial Complexity Classes
Technical University of Munich（慕尼黑工业大学）；University of Kassel（卡塞尔大学）
本文提出基于仿射不变性的方法，通过相对正则性概念探讨多项式复杂度类的分离问题，并指出其在理论上的挑战与优势。
2026-01-27 cs.LO
Tree algebras and bisimulation-invariant MSO on finite graphs
CNRS, IRIF, Université Paris Cité（法国国家科学研究中心，信息研究与交叉研究所，巴黎西岱大学）；CNRS, LIP, ENS Lyon（法国国家科学研究中心，高等师范学校里昂分校计算与语言实验室）
该研究解决了悬而未决数十年的问题，证明有限转换系统上互模拟不变的MSO片段与模态μ演算表达等价，完善了无限树正则语言的代数理论。
2026-09-02 cs.LO
Comparing the expressive power of the Synchronous and the Asynchronous pi-calculus
异步pi演算，最近由Boudol提出，并独立地由Honda和Tokoro提出，是pi演算的一个子集，它不包含用于选择和输出前缀的显式运算符。然而，这种演算的通信机制足够强大，可以模拟输出前缀，如Boudol所示，以及输入保护选择，如Nestmann和Pierce最近所示。于是，一个自然的问题就产生了，是否有可能在其中嵌入完整的π演算。我们表明，这是不可能的，即不存在任何统一的，并行保存，翻译从π演算到异步π演算，任何“合理”的概念的等价。这个结果是基于异步π演算无法打破初始通信图中可能存在的某些对称性。通过类似的论证，我们证明了π演算和CCS之间的分离结果。
1998-09-02 cs.LO cs.PL
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars
并发程序设计语言的比较和并发环境下程序转换的正确性是本文研究的重点。作为标准，我们使用的上下文语义适应并发，在那里可能-以及应该-收敛观察。本文研究了并发Haskell（CH）核心语言与同步π演算的关系。上下文语义一方面对操作语义的细节给予宽容，另一方面对翻译后过程之间的相互作用提出了强烈的要求。我们的结果是，CH包含同步π演算。我们的主要任务是通过CH的并发原语（MVars）来发现和证明π演算通道编码的正确性。它们的行为类似于（阻塞）1位缓冲区，对共享内存进行建模。第一个开发的翻译使用一个额外的私人MVar的每一个通信。我们还自动生成和检查潜在的正确的翻译，重用MVar，其中一个MVar包含的消息和两个额外的MVar同步用于模拟一个通道的同步通信的pi演算。我们的自动实验结果导致推测，一个额外的MVar是不够的。
2020-08-31 cs.LO cs.PL
Bisimulations for Delimited-Control Operators
本文系统研究了带分隔控制算子 shift 和 reset 的无类型 λ-演算的行为理论，定义了上下文等价并提出了多种双相似关系来刻画它，并探讨了扩展方向。
2019-05-23 cs.LO
Proving Soundness of Extensional Normal-Form Bisimilarities
本文提出一种系统方法，证明外延范式互模拟及其上下文上至技术的可靠性，并应用于三个按值调用λ-演算，结果已在Coq中形式化。
2019-03-28 cs.LO cs.PL
Generating Witness of Non-Bisimilarity for the pi-Calculus
在逻辑编程范式中，很难开发出一个优雅的解决方案来生成证明两个π演算过程之间的开放双相似性失败的区分公式;这是出乎意料的，因为π演算和开放互模拟的语义已经在高阶逻辑编程系统中被优雅地指定。我们使用Haskell的解决方案将公式生成定义为从所有不确定互模拟步骤的森林到一对区分公式的树变换。由于Haskell中的惰性，只生成树转换函数所需的必要路径。我们的工作表明，Haskell和它的库提供了一个有吸引力的平台，象征性地分析等价性标记的过渡系统在环境敏感的设置。
2017-05-31 cs.LO
A Fully Abstract Symbolic Semantics for Psi-Calculi
我们提出了一个符号转换系统和PSI演算的互模拟等价，并证明了它是完全抽象的非符号语义的互模拟同余。psi演算是pi演算的扩展，具有用于数据结构和用于表示关于数据的事实的逻辑断言的名义数据类型。这些可以在进程之间传输，并且它们的名称可以使用标准的pi演算机制进行静态作用域，以允许范围迁移。PSI演算可以比其他提出的pi演算的扩展更一般，例如应用pi演算，pi演算，融合演算或并发约束pi演算。符号语义对于在探索状态空间的自动化工具中有效地实现微积分是必要的，并且完全抽象属性意味着过程的语义不会从原始的改变。
2010-02-15 cs.LO
Encoding call-by-push-value in the pi-calculus
本研究定义了CBPV到π演算的编码，针对pi-i-calculus优化以解决形式化难题，证明其可靠完备且满足优良编码标准，并启动了Coq形式化验证工作。
2025-06-12 cs.CL cs.LO
Feasible reactivity in a synchronous pi-calculus
反应性是同步程序的一个基本属性。非正式地说，它保证了在每一个时刻，输入的程序将“反应”产生一个输出。在目前的工作中，我们考虑一个完善的财产，我们称之为“可行的反应性”。除了反应性之外，这个属性保证了在每个时刻，程序的大小和反应时间都受到计算开始时参数大小和最大输入大小的多项式的限制。我们提出了一种方法来注释程序，我们开发了相关的静态分析技术，保证可行的反应程序中表示的S-π演算。后者是基于SL同步编程模型的pi演算的同步版本。
2007-02-11 cs.LO
Determinacy in a synchronous pi-calculus
S-pi-演算是基于SL模型的同步pi-演算。后者是Esterel模型的放松，其中对一瞬间内没有信号的反应只能发生在下一瞬间。在目前的工作中，我们提出并证明了一个组合语义的S-pi演算标记的过渡系统和互模拟的基础上适当的概念。基于这个语义框架，我们探讨了确定性的概念和相关的（局部）汇合。
2008-02-11 cs.LO
Proof-relevant pi-calculus
形式化π演算是对逻辑框架和机械化元理论系统的表达能力的启发性测试，因为存在名称绑定、带有名称挤出的标记转换、互模拟和结构一致性。形式化已经在各种系统中进行，主要集中在充分研究（和具有挑战性）的属性，如过程互模拟理论。我们提出了一个形式化的Agda，而不是探讨理论的并发转换，残留，因果等价的痕迹，这是以前没有正式的π演算。我们的形式化采用德Bruijn指数和依赖类型的语法，并对齐的“证明转换”提出的Boudol和Castellani在CCS的上下文中与自然存在的Agda的表示标记的过渡关系的证明条款。我们的主要贡献是证明了“钻石引理”的剩余的并发过渡和一个正式的定义等价的轨迹置换的过渡。
2015-07-29 cs.LO
Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics
我们证明了模型检验问题对于认知μ演算的一个片段是可判定的。该片段允许自由变量的范围内的认知模态的限制形式，避免构建公式体现任何形式的共同知识。我们的演算包含已知的可判定的片段的认识CTL/LTL。它的模态变体可以表示两人博弈中的获胜策略，其中一个玩家具有不完美信息和不可观察的目标，并且，通过适当的编码，具有不完美信息和完美召回的ATL的模型检验问题的可判定实例可以编码为这种认知μ-演算的模型检验问题的实例。
2012-07-14 cs.LO
(Towards a) Statistical Probabilistic Lazy Lambda Calculus
本文研究了统计概率编程语言模型的需求，提出通过结合开放互模拟和概率模拟等传统工具即可满足这些需求。
2024-03-22 cs.LO
On the Validity of Encodings of the Synchronous in the Asynchronous $π$-calculus
进程演算可以通过它们之间的编码来比较它们的表达能力。Gorla提出了一个被广泛接受的定义，定义了什么构成了一个有效的编码，用于证明过程演算之间的相对表达性结果。在这项工作之前，不同的编码和分离结果通常是使用不同的，往往是不兼容的，编码的质量标准。有效编码的教科书例子是Boudol和Honda & Tokoro提出的将同步无选择$π$ -演算编码到其异步片段中的编码，说明后者的表达能力不亚于前者。在这里，我正式确定这些编码确实满足Gorla的标准。
2018-04-26 cs.LO
Modular coinduction up-to for higher-order languages via first-order transition systems
本文通过完全抽象翻译将一阶LTS上的up-to双模拟技术推广到高阶语言（π-演算、λ-演算及带引用的λ-演算），仅需手动验证新语言特有技术的相容性。
2021-09-16 cs.LO cs.PL
Synchrony vs Causality in the Asynchronous Pi-Calculus
我们研究了进程结石之间的关系，不同的同步或异步的相互作用机制。具体地说，我们感兴趣的条件下，同步交互可以实现仅使用异步交互的π演算。我们假设一些最小的条件是指戈尔拉的工作：一个“好”的编码必须是组合的，并保留和反映计算，死锁，分歧和成功。在这些条件下，我们表明，它是不可能的编码同步的相互作用，而不引入额外的因果关系的翻译。
2011-08-23 cs.LO
Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics
我们确定了一个子问题的模型检查问题的认知μ演算是可判定的。在这个子问题的实例中，公式允许在认知模态的范围内以限制的形式存在自由变量，以避免体现任何形式的共同知识。我们的子问题包含已知的可判定片段的认知CTL/LTL，可以表示获胜策略，在两个玩家的游戏中，一个玩家有不完美的信息和不可观察的目标，并与一个合适的编码，可判定的实例的模型检查问题的ATLiR。
2013-10-23 cs.GT cs.LO
Synchronous Games, Simulations and lambda-calculus
我们完善了一个模型的线性逻辑的基础上两个众所周知的成分：游戏和模拟。我们已经表明，通常的模拟关系形成了博弈之间态射的可靠概念;我们可以用这种方式解释所有线性逻辑。一个特别有趣的观点是，我们通过对游戏的同步操作来解释乘法连接词。我们完善这项工作，我们的模拟关系的计算内容。为了实现这一点，我们需要限制到直觉线性逻辑。这允许在一个建设性的环境中工作，从而保持证明的计算内容。然后，我们通过展示如何解释指数的一些附加结构来扩展它。更确切地说，我们首先给出了类型化λ演算的指称模型，然后给出了Ehrhard和Regnier的微分λ演算的指称模型.这两个模型都被建设性地证明是正确的。
2009-05-25 cs.LO math.LO
Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness
这项工作提出了易于处理的双向模拟高阶π演算会话原语（HOPI），并提供了一个完整的研究其最重要的子演算的表达能力。首先，我们开发了三种类型的互模拟，这是符合上下文对等。这些特征表明，仅观察高阶值的特定有限集合（其存在于会话类型中）作为输入就足以推理HOp过程。接下来，我们确定HO，一个最小的，二阶的HOPI子演算，其中高阶的应用程序/抽象，名称传递和递归是缺席的。我们表明，HO可以编码HOPI扩展高阶应用程序和抽象，一阶会话π演算可以编码HOPI。这两种编码都是完全抽象的。我们还证明了会话π演算与共享名称的传递不能被编码到HOPI没有共享名称。我们表明，HOPI，HO和PI是同样的表达; HO的表达能力，使有效的推理类型等价的高阶过程。
2015-02-10 cs.LO
Comparing the Expressive Power of the Synchronous and the Asynchronous pi-calculi
异步π演算由Honda和Tokoro（1991）以及Boudol（1992）独立提出，是π演算（Milner，1992）的一个子集，它不包含用于选择和输出前缀的显式运算符。然而，这种演算的通信机制足够强大，可以模拟输出前缀，如Honda和Tokoro（1991）和Boudol（1992）所示，以及输入保护选择，如Nestmann和Pierce（2000）所示。于是，一个自然的问题出现了，它是否和完整的π演算一样富有表现力。我们表明，这是不是这样的。更确切地说，我们表明，不存在任何统一的，完全分布式的翻译从π演算到异步π演算，任何“合理”的概念的等价性。这个结果是基于异步π演算无法打破可能存在于初始通信图中的某些对称性。通过类似的论点，我们证明了一个分离的结果之间的pi演算和CCS，和pi演算和pi演算与内部流动性，一个子集的pi演算提出的Sangiorgi的输出动作只能传输私有名称。
2013-07-08 cs.DC cs.LO
On the Preciseness of Subtyping in Session Types
并发子类型是类型论中最有趣的问题之一，自20世纪90年代以来得到了广泛的研究。子类型关系的正确性通常被认为是类型安全的可靠性。相反的方向，完整性，在很大程度上被忽略了，尽管它的有用性，以定义最大的子类型关系，确保类型安全。本文形式化的精确性（即健全性和完整性）的子类型的移动进程和研究它的同步和异步会话演算。我们首先证明了著名的会话子类型，分支选择子类型，是健全的和完整的同步演算。接下来，我们证明了在异步演算中，这种子类型对于类型安全是不完整的：也就是说，存在会话类型T和S，使得T可以安全地被认为是S的子类型，但是T < S不能由子类型导出。然后，我们提出了一个异步子类型系统，这是健全的和完整的异步演算。该方法给出了一个一般性的指导，以设计严格的通道为基础的子类型尊重所需的安全性能。同步演算和异步演算都是首先考虑线性通道，然后扩展到会话初始化和表达式计算（包括共享通道）。
2017-06-29 cs.LO
Stronger Validity Criteria for Encoding Synchrony
本文分析两种从同步π演算到异步π演算的无选择翻译，考察文献中的编码质量标准对其有效性的支持，并基于更强标准证明其有效性，表明两者表达能力相当。
2025-02-13 cs.LO
Equational Reasonings in Wireless Network Gossip Protocols
本文提出一种基于概率定时进程演算的组合分析技术，并配备非对称模拟理论，用于证明代数定律以估计闲聊协议网络的性能，特别适用于系统非近似等价的情形。
2018-09-27 cs.LO
On affine usages in signal-based communication
我们描述了一个类型系统的同步π演算正式的概念，仿射使用基于信号的通信。特别是，我们确定了数量有限的用法，保持亲和力，可以组成。作为一个主要的应用程序的系统，我们表明，类型化的程序是确定性的。
2008-09-03 cs.LO
