首页/论文/1402.0050

arXiv 1402.00502014-02cs.LO

PRS的分支双相似性检验

Branching Bisimilarity Checking for PRS

Qiang Yin, Yuxi Fu, Chaodong He, Mingzhang Huang, Xiuting Tao

备注：: 18 pages, 6 Figures

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

最近的研究表明，分支双相似性是可判定的nBPP（赋范基本并行进程）和nBPA（赋范基本进程代数）。这些结果导致的问题，如果有任何其他模型的PRS（过程重写系统）的层次结构的分支双相似性是可判定的。本文证明了nOCN（normed One Counter Net）和nPA（normed Process Algebra）的分支双相似性是不可判定的。这些结果基本上意味着这个问题有一个否定的答案。

英文摘要：

Recent studies reveal that branching bisimilarity is decidable for both nBPP (normed Basic Parallel Process) and nBPA (normed Basic Process Algebra). These results lead to the question if there are any other models in the hierarchy of PRS (Process Rewrite System) whose branching bisimilarity is decidable. It is shown in this paper that the branching bisimilarity for both nOCN (normed One Counter Net) and nPA (normed Process Algebra) is undecidable. These results essentially imply that the question has a negative answer.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

通过最小化模型和分支互模拟的图像空间模型检测

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-01cs.LO

有限图中互模拟和模型检验的复杂性

The Complexity of Bisimilarity and Model Checking in Finitary Diagrams

Max Planck Institute for Informatics（马克斯·普朗克Informatics研究所）；Saarland University（萨尔兰大学）

本文通过改进ETIM问题的随机算法，将有限图的互模拟判定上界降至NEXP，图路径逻辑模型检验上界降至NP，并证明后者是NP难的。

2026-06-16cs.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-08cs.LO

量子过程的符号互模拟

Symbolic bisimulation for quantum processes

利用文献中提出的互模拟概念，为了检验两个量子过程是否互相似，我们必须用任意量子态实例化它们的自由量子变量，并验证结果组态的互相似性。这使得从算法的角度来看，检查双相似性是不可行的，因为量子态构成了一个连续统。在本文中，我们直接在量子操作层次上引入了一种量子过程的符号操作语义，它允许我们描述量子过程之间的互模拟，而无需求助于量子态。我们表明，这里定义的符号互模拟是等价的开放互模拟量子过程在以前的工作中，当考虑强互模拟。提出了一种符号基双相似性检验算法。基于Hennessy-Milner逻辑对量子过程的扩展，我们给出了量子双相似性的模态逻辑刻画。

2012-02-21cs.LO

参数化高阶过程双相似性的可判定性

On Decidability of the Bisimilarity on Higher-order Processes with Parameterization

具有参数化的高阶过程能够抽象和应用（从微积分迁移而来），因此在计算上更具表现力。对于最小高阶并发性，众所周知，强双相似性（即，强互模拟相等）在没有参数化的情况下是可判定的。相比之下，对于参数化高阶过程，强双相似性是否仍然是可判定的仍然不清楚。在本文中，我们关注这个问题。基本上有两种参数化：一种是关于名称，另一种是关于进程。我们表明，强双相似性确实是可判定的高阶过程配备了这两种参数化。然后，我们展示了如何适应的决策方法来建立一个公理系统的强双相似性。在这些结果的基础上，我们提供了一个算法的双相似性检查。

2021-08-24cs.LO

可判定的PDA与不可判定的PDKEEPAAA的分界线

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-28cs.LO

更多相关论文收起更多论文

判定全赋范BPA上分支双相似性的多项式时间算法

A Polynomial Time Algorithm for Deciding Branching Bisimilarity on Totally Normed BPA

赋范BPA上的强双相似是多项式时间可判定的，而完全赋范BPA上的弱双相似是NP-困难的。很自然地会问，全赋范BPA上分支双相似性的计算复杂性在哪里。本文证明了该问题是多项式时间可判定的。据我们所知，在存在无声转移的情况下，这是第一个在多项式时间内运行的无限状态系统上的双相似性检查算法。该结果发现了一个实例，其中分支双相似性和弱双相似性都是可判定的，但属于不同的复杂性类别（除非NP=P），这是以前未知的。该算法采用分区细化方法，最终实现可以被认为是Czerwienski和Lasota以前的算法的推广。然而，出乎意料的是，该算法的正确性不能直接从以前的工作推广，正确性证明原来是微妙的。证明依赖于存在一个精心定义的细化操作适合我们的算法和精心开发的技术，这是从以前的作品完全不同的建议。

2014-11-15cs.LO

用有界区域历史图检验时间互模拟--技术报告

Checking Timed Bisimulation with Bounded Zone-History Graphs -- Technical Report

时间自动机（TA）是一个行之有效的形式化描述离散状态/连续时间行为的时间临界反应系统。关于基本分析问题的候选人的实现对规范进行比较，都给定为TA，它已被证明，定时跟踪等价是不可判定的，而定时互模拟等价是可判定的。相应的证明利用区域图，一个有限的，但通常非常占用空间的TA语义表征。因此，大多数实用的TA工具利用区域图，而不是符号和一般更有效的表示TA语义，自动化分析任务。然而，区域图只产生声音的分析任务的结果被简化为平原可达性问题，从而检查定时双相似性太不精确。在本文中，我们提出了有界区域历史图，一种新的表征TA语义促进可调的权衡精度和可扩展性之间的时间双相似性检查。据我们所知，我们的工具TimBrCheck是目前唯一可用的工具，用于有效地检查定时双相似性，甚至支持无声移动的非确定性TA。我们进一步提出了实验结果，从应用我们的工具收集的社区基准，提供洞察精度和效率之间的权衡，取决于绑定值。

2020-09-16cs.FLcs.LO

Petri 网中的资源互模拟是可判定的

Resource Bisimilarity in Petri Nets is Decidable

本文针对 Petri 网中的资源互模拟关系，提出判定算法，证明其可判定性，并给出相似但不互模拟的实例，区别于不可判定的资源相似性。

2022-10-03cs.LO

Place Bisimilarity is Decidable, Indeed!（位置互模拟确实可判定！）

Place Bisimilarity is Decidable, Indeed!

本文证明了有限 Petri 网上的位置互模拟可判定性，提出简单扫描算法，并引入更粗的 d-位置变体，为分布式系统形式化验证铺路。

2024-03-15cs.LO

基于余递归代数的范畴活性检验

Categorical Liveness Checking by Corecursive Algebras

最终余代数作为“范畴最大不动点”在余代数理论中起着核心作用。有些类似的，大多数证明方法研究集中在最大的定点性质，如安全性和双相似性。在这里，我们做了一个步骤，以明确的证明方法至少不动点性质的动力系统建模为余代数。具体而言，我们寻求一个明确的公理化著名的证明方法的活性，即排名功能（在不确定性的设置）和排名上鞅（在概率）。我们找到了一个答案，在一个合适的组合coalgebraic模拟（研究以前的作者）和corecursive代数作为分类（非）良好的基础。

2017-04-17cs.LO