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
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
Executable Behaviour and the π-Calculus (extended abstract)
反应式图灵机扩展了经典的图灵机，具有对可观察的交互行为进行建模的功能。当且仅当一个行为在行为上等价于反应式图灵机的行为时，我们称之为可执行行为。在本文中，我们研究的可执行行为和行为之间的关系，可以指定的π演算。我们建立了所有可执行的行为可以指定在π演算的分歧保持分支双相似性。然而，由于反应式图灵机模型的（预期的）限制，相反的情况是不正确的。也就是说，π演算允许指定的行为是不可执行的分歧保持分支双相似性。出于对可执行性的直观理解，我们考虑对与每个pi项可执行行为相关联的pi演算的操作语义的限制，至少到不需要保持发散的分支双相似性的版本。
2015-08-20 cs.LO
Unique Parallel Decomposition in Branching and Weak Bisimulation Semantics
我们考虑了唯一并行分解、模分支和弱双相似性的性质。首先，我们表明，无限的行为可能无法有平行的分解。然后，我们证明，完全规范的行为总是有平行的分解，但这些不一定是唯一的。最后，我们建立了弱有界行为有唯一的平行分解。我们从关于部分交换幺半群中唯一分解的一般定理中得到后一个结果。
2015-07-28 cs.LO
A Linear-Time Branching-Time Spectrum for Behavioral Specification Theories
我们提出了行为规范理论的线性时间-分支时间谱中的大多数等价物。几乎所有以前的工作规范理论的重点是双相似性，但有一个明确的兴趣规范理论的其他前序和等价。我们表明，规范理论的前序不能存在和发展的一般计划，使我们能够定义行为规范理论的基础上，析取模态转换系统，大多数等价的线性时间-分支时间谱。
2019-10-18 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
Divergence and unique solution of equations
本文研究基于方程唯一解的双相似性证明技术，借鉴Roscoe的结果，将其移植到CCS操作语义，并扩展至不同等价关系及名称传递演算，用于完善Milner编码的完全抽象证明。
2019-08-06 cs.LO
A General Completeness Theorem for Skip-free Star Algebras
本文针对以等式理论T为参数的分支过程代数，在特定条件下公理化双相似性，抽象了早期论证，为概率分支的无跳跃过程代数提供新完备性定理并涵盖已有结果。
2025-01-25 cs.LO
A Branching Time Model of CSP
我提出了一个分支时间模型的CSP，是比迄今为止提出的所有其他模型的CSP。它是通过从线性时间分支时间谱中取一个语义等价，即保持发散的耦合相似性，并证明它是CSP算子的同余而得到的。这种等价属于语义等价的互模拟家族，在这个意义上，在没有内部动作的转换系统上，它与强双相似性相一致。然而，足够的方程法CSP仍然获得一个完整的axiomatisation封闭，递归自由条款。
2017-02-25 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
A Complete Axiomatisation for Divergence Preserving Branching Congruence of Finite-State Behaviours
我们提出了一个有限状态表达式的方程推理系统，并证明了该系统是健全的和完整的关于分歧保持分支同余，关闭一个问题，自1993年以来一直开放。推理系统完善罗布范Glabbeek的简单而优雅的完整的公理化分支互模拟同余的有限状态行为加入四个简单的公理后，下降一个公理，这是不健全的更精细的发散敏感的语义。
2021-05-17 cs.LO
Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps
该研究首次给出带静默步骤的van Glabbeek线性时间-分支时间谱的广义博弈刻画，用多维能量博弈一次性刻画判定多类弱行为等价，并结合Hennessy-Milner逻辑的八维表达力证明其正确性。
2024-10-07 cs.GT cs.LO
Analyzing Divergence for Nondeterministic Probabilistic Models
本文系统比较了非确定性概率系统中细化分支和弱概率互模拟的分歧敏感行为等价关系，并给出了这些等价关系的高效检验算法。
2024-12-28 cs.LO
Graded Monads and Graded Logics for the Linear Time -- Branching Time Spectrum
并发系统的基于状态的模型传统上被认为是在各种概念下的进程等价。在标记的过渡系统的特定情况下，这些等价的范围从跟踪等价（强）的双相似性，并组织在什么是所谓的线性时间分支时间谱。通用的共代数和分级单子的组合提供了一个通用的框架，在该框架中，并发的语义可以参数化的分支类型的底层过渡系统和粒度的进程等价。我们表明，在本文件中，这一框架的分级语义subanimate最重要的等价物从线性时间分支时间谱。分级语义的一个重要特征是它允许特征模态逻辑的原则性提取。我们已经建立了这些分级逻辑的不变性下，在早期的工作中给定的分级语义，在本文中，我们扩展了逻辑框架与一个明确的命题层，并提供了一个通用的表达标准，概括了经典的亨尼西-米尔纳定理粗糙的概念过程等价。我们提取分级逻辑的一系列分级语义标记的过渡系统和概率系统，并给出示例性的证明，他们的表现力的基础上，我们的通用标准。
2020-10-20 cs.LO math.CT
Computation Tree Logic with Deadlock Detection
研究了在没有下一状态模态的计算树逻辑（CTL-X）中满足相同公式的标号迁移系统的状态等价关系。这个关系是由De Nicola & Vaandrager通过将标记转移系统转化为Kripke结构而得到的，同时解除了对后者的总体性限制。他们将其描述为发散敏感分支互模拟等价。我们发现，这种等价未能成为一个交错并行组合的同余。原因是，CTL-X的非总Kripke结构的拟议应用缺乏表现力，以应付死锁属性是重要的，在并行组合的上下文中。我们提出了一个扩展的CTL-X，或替代治疗的非整体，填补这一空白。等价诱导我们的扩展的特点是分支互模拟等价与明确的分歧，这是，此外，示出的粗同余包含在分歧敏感的分支互模拟等价。
2009-12-22 cs.LO
