A Polynomial Time Algorithm for Deciding Branching Bisimilarity on Totally Normed BPA
赋范BPA上的强双相似是多项式时间可判定的，而完全赋范BPA上的弱双相似是NP-困难的。很自然地会问，全赋范BPA上分支双相似性的计算复杂性在哪里。本文证明了该问题是多项式时间可判定的。据我们所知，在存在无声转移的情况下，这是第一个在多项式时间内运行的无限状态系统上的双相似性检查算法。该结果发现了一个实例，其中分支双相似性和弱双相似性都是可判定的，但属于不同的复杂性类别（除非NP=P），这是以前未知的。该算法采用分区细化方法，最终实现可以被认为是Czerwienski和Lasota以前的算法的推广。然而，出乎意料的是，该算法的正确性不能直接从以前的工作推广，正确性证明原来是微妙的。证明依赖于存在一个精心定义的细化操作适合我们的算法和精心开发的技术，这是从以前的作品完全不同的建议。
2014-11-15 cs.LO
Weighted and Branching Bisimilarities from Generalized Open Maps
在双相似性的开放映射方法中，给定的基于状态的系统中的路径和它们的运行是一等公民，双相似性成为一个派生概念。虽然开放映射被成功地用于非确定性系统中的双相似性建模，但该方法无法描述定量系统等效性，如概率双相似性。在目前的工作中，我们看到，这确实是不可能的，因此，我们推广的概念，开放的地图，也适应加权和概率的双相似性。此外，扩展到这个新的框架中的强路径和路径互模拟的概念，我们表明，分支的双相似性可以捕获这个扩展的理论，它可以被看作是弱双相似性的历史保持限制。
2023-01-17 cs.LO
Branching Bisimilarity for Processes with Time-outs
该研究将分支互模拟适配到带超时的反应式系统，给出多种等价定义、模态刻画与同余性证明，并提出了无不可观察动作无限序列的受保护进程的完备公理化。
2024-08-19 cs.LO
Dormancy-aware timed branching bisimilarity, with an application to communication protocol analysis
本文提出了一种比标准概念更粗的离散相对定时进程分支互模拟性变体，利用带抽象的ACP版本证明其能同时分析PAR协议的功能正确性与性能属性，并用单一公理模式刻画了其与标准概念的差异。
2023-08-09 cs.LO
One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics
本文首次用单一多维能量博弈统一刻画并判定带静默步的线性时间—分支时间谱系中从分支互模拟到弱迹等价的行为等价，并通过 Hennessy–Milner 逻辑的八个表达力维度建立正确性。
2024-11-21 cs.LO
A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice
本文为非确定概率进程提出分支互模拟概念，并通过等式理论给出一个基本无递归进程语言的完全公理化，其完备性证明结合了强概率互模拟完备性与具体进程概念。
2025-02-08 cs.LO
A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems
本文提出一种更简单的 O(m log n) 算法用于带标签转移系统上的分支双相似性，结合现有思想，在基准测试中更快且更省内存，成为分支双相似性最小化和弱双相似性预处理的最佳选择。
2019-11-06 cs.LO
Concrete Branching Bisimilarity for Processes with Time-outs
本文提出一种适用于带超时反应式系统的分支互模拟，不允许省略超时转移，给出多个等价定义、模态特征刻画、同余性证明及守护进程的完备公理化。
2024-10-07 cs.LO
Relating Apartness and Branching Bisimulation Games
本文建立分离关系与回合制双人博弈之间的联系，证明在图像有限和有限迁移系统中，Spoiler 玩家的获胜配置对应分离证明，为强互模拟和分支互模拟提供新的证明视角。
2024-11-05 cs.LO
Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity
Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, Consiglio Nazionale delle Ricerche（意大利国家研究委员会信息科学与技术研究所）；Eindhoven University of Technology（埃因霍温理工大学）
提出基于分支互模拟的准离散闭包模型最小化方法，通过编码为标记迁移系统加速空间模型检测，并开发原型工具VoxMinX验证其有效性。
2026-07-01 cs.LO
Branching Bisimilarity of Normed BPA Processes is in NEXPTIME
赋范BPA过程的分支双相似性最近被Yuxi Fu证明是可判定的（ICALP 2013），但他的证明没有提供任何复杂性上限。我们提出了一个更简单的方法，基于相对素分解，导致一个不确定的指数时间算法，这是接近已知的指数时间的下限。
2015-12-18 cs.FL cs.LO
On the Axiomatisation of Branching Bisimulation Congruence over CCS
在本文中，我们调查的方程理论（限制，重新标记，和递归自由片段）CCS模扎根分支双相似性，这是一个经典的，基于bisimulation的概念等价的抽象过程中的行为从内部计算步骤。首先，我们证明了CCS不是基于模所考虑的同余。作为一个关键步骤的独立利益的证明，否定的结果，我们证明了每个CCS进程有一个独特的并行分解成不可分解的过程模分支双相似性。作为第二个主要贡献，我们表明，当一组行动是有限的，根分支双相似性有一个有限的方程基础上CCS丰富的左合并和通信合并运营商从ACP。
2022-06-28 cs.LO
Reactive Turing Machines
我们提出了反应式图灵机（RTMs），扩展经典的图灵机与过程理论的概念的互动，并使用它来定义一个概念的可执行的过渡系统。我们表明，每一个可计算的过渡系统与有界的分支度模拟模发散保持分支双相似性的RTM，和每个有效的过渡系统模拟模分支双相似性的变体，不需要发散保持。从这些结果中，我们得出结论，（通信）RTMs的并行组合物可以模拟由一个单一的RTM。我们证明了存在通用RTM模分支双相似性，但这些基本上采用发散，能够模拟RTM的任意分支度。我们还证明了模发散保持分支双相似性有RTMs是普遍的到自己的分支度。最后，我们在一个简单的进程演算中建立了可执行性和有限可定义性之间的对应关系。
2013-03-05 cs.FL cs.LO
Two Lower Bounds for BPA
赋范基本过程代数（BPA）上的分支双相似性在以前的文献中被认为是EXPTIME-困难的，但没有任何明确的证明。最近，扬卡尔提醒说，这种说法并不可靠。本文给出了赋范BPA上分支双相似性的EXPTIME-困难性的一个新的完整证明。我们还证明了赋范BPA上的伴随正则性问题是PSPACE-困难的，并且是EXPTIME的。这改进了先前的P-hard和NEXPTIME结果。
2017-02-18 cs.LO
Dividing Line between Decidable PDA's and Undecidable Ones
Senizergues已经证明了语言等价对于不相交的ε-确定性PDA是可判定的。Stirling证明了强双相似性对于PDA是可判定的。在消极的一面Srba证明，弱双相似性是不可判定的赋范PDA。后来，Jancar和Srba建立了不相交epsilon-pushing PDA和不相交epsilon-popping PDA的弱双相似性的不可判定性。本文推广了这些可判定性和不可判定性结果。扩展是通过查看PDA的几个变体的分支双相似性的等价性检查问题来完成的。
2014-04-28 cs.LO
Divide and Congruence II: From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity
本文提出了一种分解具有内部作用$τ$的过程的模态公式的方法，并在此分解方法的基础上导出了分支和$η$ -双相似的同余格式。其思想是，语义的一致格式必须确保该语义的模态表征中的公式总是被分解为再次处于该模态表征中的公式。在这个后续文件中的分解方法进行了增强，以处理包含一个模态$\langleε\rangle\langle a\rangleϕ$的模态特征，推导出一致格式的延迟和弱双相似性。
2017-12-21 cs.LO
On Bisimulation in Absence of Restriction
我们重新审视标准的互模拟等式的过程模型的限制运营商。众所周知，一般来说，弱双相似性比强双相似性更粗糙，因为它抽象了内部动作。在没有限制的情况下，这些内部行为变得有些可见，所以人们可能会怀疑弱双相似性是否仍然是“弱”的。我们表明，在两个CCScore（即，Milner的没有$τ$ -前缀、求和和重新标记的标准CCS）及其高阶变体（命名为HOCCScore），弱双相似性确实保持弱，即，即使没有限制算子，仍然严格地比强双相似性粗糙。这些结果可以推广到其他一阶或高阶过程模型。本质上，这是由于复制操作的直接或间接存在，它可以保持进程保持其状态（即，互动能力）。凭借这些意见，我们研究了一个变种的弱双相似性，称为准强双相似性。这种准强双相似性要求内部动作的匹配以强方式进行，如强双相似性，并且可见动作的匹配没有尾随的内部动作。我们表明，在CCScore没有限制算子，弱双相似性完全崩溃到这个准强双相似性，这是此外，以符合分支双相似性。这些结果表明，在没有限制操作的情况下，弱双相似性的某些成分确实变成了强的，特别是内部动作的匹配。
2022-10-19 cs.LO
Branching Bisimilarity of Normed BPA Processes as a Rational Monoid
本文给出了赋范BPA（基本过程代数）过程上分支双相似性的结构结果的详细和简化版本，这是Czerwinski和Jancar（arxiv 7/2014和LiCS 2015）的会议论文的关键。该论文关注计算复杂性，并导出了NEXPTIME上界;作者基于Fu（ICALP 2013）的思想，并加强了他的可判定性结果。后来He和Huang宣布了这个问题的EXPTIME-完全性（arxiv 1/2015，和LiCS 2015），给出了EXPTIME成员资格的技术证明。他和黄间接承认了Czerwinski和Jancar的分解思想，他们也建立在这个基础上，但很难将他们的出发点与他们的新思想分开。这里的一个目的是在一个技术上新的框架中提出Czerwinski和Jancar以前的分解结果，注意到赋范BPA过程上的分支互模拟等价对应于一个有理幺半群（在[Sakarovitch，1987]的意义上）;特别是，它表明，所提到的等价可以通过计算确定性有限转换器的规范形式来决定。另一个目的是提供一个完整的描述，包括一个非正式的概述，这也应该清楚傅的想法是如何使用的，并以一种可读和易于验证的形式给出所有证据。
2017-11-27 cs.FL cs.LO
Unique Parallel Decomposition in Branching and Weak Bisimulation Semantics
我们考虑了唯一并行分解、模分支和弱双相似性的性质。首先，我们表明，无限的行为可能无法有平行的分解。然后，我们证明，完全规范的行为总是有平行的分解，但这些不一定是唯一的。最后，我们建立了弱有界行为有唯一的平行分解。我们从关于部分交换幺半群中唯一分解的一般定理中得到后一个结果。
2015-07-28 cs.LO
Weak MSO: Automata and Expressiveness Modulo Bisimilarity
证明了弱一元二阶逻辑的互模拟不变片段等价于模态$μ$ -演算的片段，其中最小不动点算子$μp.φ$的应用仅限于在$p$中连续的公式$φ$.我们的证明是自动机理论的性质，特别是，我们引入了一类自动机的特点的表达能力的WMSO树模型的任意分支度。这些自动机的转换映射是根据逻辑$\mathrm{FOE}_1^\infty$定义的，该逻辑是具有广义量词$\exists^\infty$的一阶逻辑的扩展，其中$\exists^\infty x. ϕ$意味着有无限多个对象满足$ϕ$。我们的工作的一个重要组成部分是$\mathrm{FOE}_1^\infty$的模型理论分析。
2014-01-22 cs.LO
A Linear-Time Branching-Time Spectrum for Behavioral Specification Theories
我们提出了行为规范理论的线性时间-分支时间谱中的大多数等价物。几乎所有以前的工作规范理论的重点是双相似性，但有一个明确的兴趣规范理论的其他前序和等价。我们表明，规范理论的前序不能存在和发展的一般计划，使我们能够定义行为规范理论的基础上，析取模态转换系统，大多数等价的线性时间-分支时间谱。
2019-10-18 cs.LO
Bisimilarity of Open Terms in Stream GSOS
流GSOS是一种用于无穷序列上的运算和演算的规范格式。双相似性的概念提供了一个规范的证明技术，在这种规格说明中的封闭项的等价性。在本文中，我们专注于开放的条款，其中可能包含变量，这是等价的，每当他们表示相同的流为每一个可能的实例化的变量。我们的主要贡献是捕捉等价的开放条款的双相似性在某些Mealy机，提供了一个具体的证明技术。此外，我们介绍了这种技术的增强，称为互模拟高达替换，并展示了如何将其与其他高达技术相结合，以获得一个强大的方法来证明等价的开放条款。
2019-02-12 cs.LO
Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP
1987年，Ernst-Rüdiger Olderog为CCSP的一个子集提供了一个操作Petri网语义，CCSP是Milner的CCS和Hoare的CSP的结合。它为子集中的每个过程项分配一个标记的安全位置/转换网络。为了证明该方法的正确性，Olderog建立了以下协议：（1）与CCSP的标准交织语义达到强互模拟等价，（2）与CCSP算子在Petri网方面的标准指称解释达到适当的语义等价，完全尊重网的因果结构。对于后者，他采用了线性时间语义等价，即具有相同的因果网。本文加强（2），采用这种语义的一种新的分支时间版本-结构保持双相似性-而且保持必然性。我确定这是CCSP运营商的一致性。
2015-09-19 cs.LO
Modal Logic Characterizations of Forward, Reverse, and Forward-Reverse Bisimilarities
本文在顺序非确定性可逆进程演算上，利用前向与反向模态词刻画前向、反向及前向-反向互模拟，并建立其与迹等价和分支互模拟的联系。
2023-10-02 cs.LO
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
本文证明了（强）全并发互模拟性和i-因果网互模拟性在有限有界Petri网上是可判定的，其核心方法是对Vogler的有序标记证明技术进行推广。
2023-12-20 cs.LO
Weak Simplicial Bisimilarity and Minimisation for Polyhedral Model Checking
University of Amsterdam（阿姆斯特丹大学）；Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, Consiglio Nazionale delle Ricerche（意大利国家研究委员会信息科学与技术研究所（A. Faedo））；Andrea Razmadze Mathematical Institute, I. Javakhishvili Tbilisi State University（伊万·贾瓦希什维利第比利斯国立大学安德烈·拉兹马泽数学研究所）；Eindhoven University of Technology（埃因霍温理工大学）
本文提出弱单纯形双射和弱±双射，用于多面体模型和单元格poset模型的最小化，通过编码到LTSs并利用分支双射实现高效模型检查。
2026-01-08 cs.LO
A Branching Time Model of CSP
我提出了一个分支时间模型的CSP，是比迄今为止提出的所有其他模型的CSP。它是通过从线性时间分支时间谱中取一个语义等价，即保持发散的耦合相似性，并证明它是CSP算子的同余而得到的。这种等价属于语义等价的互模拟家族，在这个意义上，在没有内部动作的转换系统上，它与强双相似性相一致。然而，足够的方程法CSP仍然获得一个完整的axiomatisation封闭，递归自由条款。
2017-02-25 cs.LO
Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
我们提出了一个框架，规范的行为保留的重新配置系统建模为Petri网。该框架是基于开放的网络，一个温和的泛化普通的地方/过渡网适合模型开放的系统，可能会与周围的环境相互作用，并赋予一个colimit为基础的组合操作。我们表明，自然的概念开网的双相似性是同余的组合操作。所考虑的行为等效性因观察结果的选择而异，这些观察结果可以是单次击发或并行步骤。此外，我们认为这种等价的弱形式，在不可观察的行动的存在下产生的。我们还提供了一个最多的技术，以促进双相似性证明。该理论是用来确定合适的类的重新配置规则（在双推出重写方法），其应用程序保留了观察语义的网。
2008-10-21 cs.LO
RPO, Second-order Contexts, and Lambda-calculus
首先，我们扩展了Leifer-Milner RPO理论，给出了获得IPO标记的过渡系统（和双相似性）的一般条件，减少了一组过渡，并可能出现分支。此外，我们还研究了Leifer-Milner理论的弱变体，给出了弱双相似是同余的一般条件。然后，我们将这种扩展的RPO技术应用到具有懒惰和按值调用的Reduction策略的λ演算中。我们表明，相反的过程演算，可以直接处理的λ演算语法和应用Leifer-Milner技术一类的背景下，只要我们的工作框架中的弱双相似性。然而，即使在具有最小上下文的转换系统的情况下，所得到的双相似性也是无限分支的，这是因为在标准上下文范畴中，参数规则（如beta规则）只能由无限多个基本规则表示。为了克服这个问题，我们引入了二阶上下文范畴的一般概念。我们表明，通过在这种情况下进行RPO建设，懒惰的观测等价可以被捕获为一个弱的双相似等价的一个分支过渡系统。这个结果是通过考虑组合逻辑中的一种编码来实现的。
2009-08-06 cs.LO cs.PL
Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps
该研究首次给出带静默步骤的van Glabbeek线性时间-分支时间谱的广义博弈刻画，用多维能量博弈一次性刻画判定多类弱行为等价，并结合Hennessy-Milner逻辑的八维表达力证明其正确性。
2024-10-07 cs.GT cs.LO
Reducing Weak to Strong Bisimilarity in CCP
并发约束编程（ccp）是一个成熟的并发模型，它突出了异步系统的基本方面，异步系统的代理（或进程）通过在全局介质中发布和查询（部分）信息来进化。双相似性是并发理论中的标准行为等价。然而，直到最近才提出了一个良好的行为概念的双相似性的CCP，和CCP分区细化算法，用于决定强版本的等价性。弱双相似性是进程演算中的一个核心行为等价，它是从强情况下通过只考虑系统中可观察到的动作而获得的。通常，标准划分细化也可以用于简单地通过使用米尔纳从弱到强双相似性的减少来确定弱双相似性;一种称为饱和的技术。在本文中，我们证明，由于它涉及标记跃迁，上述饱和技术不适用于ccp。我们给出了一个替代减少从弱CCP双相似性强，使我们能够使用CCP分区细化算法来决定这种等价性。
2012-12-17 cs.LO cs.PL
Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes
Broadbent和Göller（FSTTCS 2012）证明了无ε二阶下推自动机生成的过程的互模拟等价性的不可判定性。我们添加了一些关于所使用的证明技术的注释，称为Defender's forcing，以及具有ε转换的一阶下推自动机的相关不可判定性证明（Jančar and Srba，JACM 2008）。
2013-03-04 cs.FL cs.LO
Axiomatizing GSOS with Predicates
在本文中，我们介绍了一个扩展的GSOS规则格式的谓词，如终止，收敛和发散。对于这种格式，我们推广了Aceto，Bloom和Vaandrager提出的技术，用于自动生成GSOS系统的双相似性的地面完整公理化。我们的程序是在一个工具，接收SOS规范作为输入，并自动导出相应的公理化。这为通过定理证明技术检查过程项的强双相似性铺平了道路。
2011-08-16 cs.LO
Modal Reasoning = Metric Reasoning, via Lawvere
分级模态类型、系统和协同效应正在成为处理上下文相关计算的标准形式，其中代码使用起着核心作用。然而，模态语言和协同语言的程序等价理论，如果与这些语言的指称语义和操作语义相比，则相当不发达。这就提出了一个问题，即普通程序等价的理论在多大程度上可以在模态场景中给出。在这项工作中，我们表明，共归纳等价可以扩展到一个模态设置，我们这样做，通过推广阿布拉姆斯基的应用双相似coeffective行为。为了实现这一目标，我们开发了一个通用的理论，三元程序关系的基础上的新概念的comonadic宽松的扩展，在此之上，我们定义了一个模态扩展的Abramsky的应用bisimilarity（我们称之为模态应用bisimilarity）。我们证明这样的关系是一个一致性，这种方式获得一个组合技术推理模态和coeffective行为。但这并不是故事的结束：我们还建立了模态程序关系和程序距离之间的对应关系。这种对应关系表明模态应用双相似性和（适当扩展的）应用双相似性距离一致，这种方式揭示了模态程序等价性和程序距离只是同一枚硬币的两面。
2021-03-05 cs.LO
Coinduction up to in a fibrational setting
互模拟增强了双相似性的共归纳证明方法，为检验不同类型系统的性质提供了有效的证明技术。我们证明了这种技术的合理性，在一个fibrational设置，建立在Hermida和雅各布斯的开创性工作。这使我们能够系统地获得最多的技术，不仅双相似性，但为一大类的共归纳谓词建模为coalgebras。通过调整我们的框架的参数，我们获得了新的技术，一元谓词和名义自动机，GSOS规则格式的相似性的变体，和一个新的分类处理弱双相似性。
2014-05-15 cs.DM cs.LO
On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version)
我们研究互模拟和上下文等价的概率$λ$演算。本文的贡献有三个方面。首先，我们展示了一种证明概率应用双相似同余的技术。虽然该技术遵循豪的方法，但一些技术细节是完全不同的，依赖于实数集的非平凡“解开”属性。其次，我们表明，虽然双相似性是在一般情况下严格比上下文等价，这两个关系之间的重合达到纯$λ$ -条款。由此产生的等式是由Levy-Longo树诱导的等式，通常被认为是在懒惰制度下纯$λ$ -项上的最好的扩展等价。最后，我们推导出一个共归纳特征的上下文等价的整个概率语言，通过一个扩展，其中条款类似于分布可能会出现在redex的位置。扩展的另一个动机是它的操作语义允许我们实验不同的一致性技术，即逻辑双相似性。
2013-11-07 cs.LO cs.PL
Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines
本文通过将范式互模拟、应用互模拟和上下文等价内化到抽象机中，构造了按名调用和按值调用λ-演算到极简高阶进程演算HOcore的完全抽象编码，并证明该方法可扩展到带控制算子的λμ-演算。
2024-07-02 cs.LO
Graded Monads and Graded Logics for the Linear Time -- Branching Time Spectrum
并发系统的基于状态的模型传统上被认为是在各种概念下的进程等价。在标记的过渡系统的特定情况下，这些等价的范围从跟踪等价（强）的双相似性，并组织在什么是所谓的线性时间分支时间谱。通用的共代数和分级单子的组合提供了一个通用的框架，在该框架中，并发的语义可以参数化的分支类型的底层过渡系统和粒度的进程等价。我们表明，在本文件中，这一框架的分级语义subanimate最重要的等价物从线性时间分支时间谱。分级语义的一个重要特征是它允许特征模态逻辑的原则性提取。我们已经建立了这些分级逻辑的不变性下，在早期的工作中给定的分级语义，在本文中，我们扩展了逻辑框架与一个明确的命题层，并提供了一个通用的表达标准，概括了经典的亨尼西-米尔纳定理粗糙的概念过程等价。我们提取分级逻辑的一系列分级语义标记的过渡系统和概率系统，并给出示例性的证明，他们的表现力的基础上，我们的通用标准。
2020-10-20 cs.LO math.CT
Verification of Quantum Protocols Adopting Physically Admissible Schedulers
IMT School for Advanced Studies Lucca（卢卡高等研究学院）；University of Pisa（比萨大学）；IRIF, CNRS – Université Paris Cité（巴黎西岱大学国家科学研究中心信息学与图像自动化研究所）
本文提出lqCCS过程演算，整合并发、非确定性和量子能力，通过分布语义约束概率组合，验证饱和双模拟的适配性，并分析现实量子通信协议。
2026-04-26 cs.LO
Divergence and unique solution of equations
本文研究基于方程唯一解的双相似性证明技术，借鉴Roscoe的结果，将其移植到CCS操作语义，并扩展至不同等价关系及名称传递演算，用于完善Milner编码的完全抽象证明。
2019-08-06 cs.LO
Bisimulation Equivalence of First-Order Grammars
本文给出了一阶文法（重写一阶项根的标号规则的有限集合）互模拟等价性的可判定性证明。该等价性推广了DPDA（deterministic pushdown automata）等价性，其结果与Senizergues（1998，2005）在方程图框架下的结果或在PDA框架下的结果一致.经典一阶项的框架似乎特别有用，可以为更广泛的受众提供可以理解的证明。我们还讨论了Fu和Yin（2014）宣布的分支双相似性的扩展。
2014-05-30 cs.FL cs.LO
Applicative Bisimulation and Quantum $λ$-Calculi (Long Version)
应用互模拟是一种在高阶函数式语言中检验程序等价性的共归纳技术。就上下文对等而言，它是合理的，有时是完整的。在本文中，我们表明，应用互模拟也工作时，底层语言的程序采取的形式的线性$λ$ -演算扩展的功能，如概率二进制选择，但也量子数据，后者是一个设置中的线性发挥作用。的主要结果是证明所获得的概念的双相似性的合理性。
2015-06-22 cs.LO
Unique Solutions of Contractions, CCS, and their HOL Formalisation
收缩的唯一解是一种双相似性的证明技术，它克服了米尔纳的“方程的唯一解”技术的某些语法限制。本文概述了一个相当全面的形式化的核心理论CCS的HOL定理证明（HOL4），重点对理论的唯一解决方案的收缩。(The形式化由大约20，000行标准ML的证明脚本组成。理论本身的一些改进。特别是，我们删除的限制总和，这必须是弱保护，通过移动到根收缩，也就是说，包含在收缩预序的coarthorough precongruence。
2018-08-27 cs.LO
Eager Functions as Processes (long version)
我们研究Milner将按值调用$λ$演算编码为$π$演算。我们表明，通过调整编码的$π$ -演算（内部$π$和异步本地$π$）的两个子演算，等价的$λ$ -条款引起的编码符合拉森的渴望正规形式的双相似性，扩展到处理$η$ -平等。作为$π$演算中的行为等价，我们考虑上下文等价和带刺同余。我们还将结果推广到了前序。一个关键的技术成分的证明是最近推出的技术的唯一解决方案的方程，本文进一步发展。在这方面，本文也打算是一个扩展的案例研究的适用性和表现力的技术。
2022-02-07 cs.LO
Eager Functions as Processes
我们研究Milner将按值调用$λ$演算编码为$π$演算。我们表明，通过调整编码的$π$ -演算（内部$π$和异步本地$π$）的两个子演算，等价的$λ$ -条款引起的编码符合拉森的渴望正规形式的双相似性，扩展到处理$η$ -平等。作为$π$演算中的行为等价，我们考虑上下文等价和带刺同余。我们还将结果推广到了前序。一个关键的技术成分的证明是最近推出的技术的唯一解决方案的方程，本文进一步发展。在这方面，本文也打算是一个扩展的案例研究的适用性和表现力的技术。
2021-12-15 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
Proving Soundness of Extensional Normal-Form Bisimilarities
本文提出一种系统方法，证明外延范式互模拟及其上下文上至技术的可靠性，并应用于三个按值调用λ-演算，结果已在Coq中形式化。
2019-03-28 cs.LO cs.PL
Analyzing Divergence for Nondeterministic Probabilistic Models
本文系统比较了非确定性概率系统中细化分支和弱概率互模拟的分歧敏感行为等价关系，并给出了这些等价关系的高效检验算法。
2024-12-28 cs.LO
