赋范BPA过程的分支双相似性在NEXPTIME中

Branching Bisimilarity of Normed BPA Processes is in NEXPTIME

Wojciech Czerwiński, Petr Jančar

备注：: This is the same text as in July 2014, but only with some acknowledgment added due to administrative needs

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

赋范BPA过程的分支双相似性最近被Yuxi Fu证明是可判定的（ICALP 2013），但他的证明没有提供任何复杂性上限。我们提出了一个更简单的方法，基于相对素分解，导致一个不确定的指数时间算法，这是接近已知的指数时间的下限。

英文摘要：

Branching bisimilarity on normed BPA processes was recently shown to be decidable by Yuxi Fu (ICALP 2013) but his proof has not provided any upper complexity bound. We present a simpler approach based on relative prime decompositions that leads to a nondeterministic exponential-time algorithm; this is close to the known exponential-time lower bound.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

赋范BPA上的分支双相似性是EXPTIME-完全的

Branching Bisimilarity on Normed BPA Is EXPTIME-complete

提出了一种判定赋范BPA（Bacis Process Algebra）系统分支双相似性的指数时间算法。赋范BPA上的分支（或弱）双相似性的判定问题是一个长期存在的未解决的问题。EXPTIME硬度是对Richard Mayr提出的约化的轻微修改的推论。我们的结果表明，这个问题是EXPTIME-完全的。

2015-03-17cs.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

赋范BPA过程作为有理幺半群的分支双相似性

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-27cs.FLcs.LO

BPA的两个下界

Two Lower Bounds for BPA

赋范基本过程代数（BPA）上的分支双相似性在以前的文献中被认为是EXPTIME-困难的，但没有任何明确的证明。最近，扬卡尔提醒说，这种说法并不可靠。本文给出了赋范BPA上分支双相似性的EXPTIME-困难性的一个新的完整证明。我们还证明了赋范BPA上的伴随正则性问题是PSPACE-困难的，并且是EXPTIME的。这改进了先前的P-hard和NEXPTIME结果。

2017-02-18cs.LO

基本进程代数的双相似性在2- ExpTime中（一个显式证明）

Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)

Burkart，Caucal，Steffen（1995）给出了一个在基本进程代数（BPA）中确定进程互模拟等价的过程，即由上下文无关文法生成的顺序进程。他们改进了Christensen，Hüttel，Stirling（1992）先前的可判定性结果，因为他们的过程显然具有基本的时间复杂度，并且作者声称仔细分析会揭示双指数上界。这里给出了2-ExpTime中成员资格的自包含直接证明。这是通过一个证明反驳游戏，其中显示，有一个交替的图灵机决定指数空间中的问题。证明使用类似的成分（大小措施，分解，基地）作为以前的证明，但一个新的简化因素是一个明确的无限正规字符串添加到状态空间。辅助索赔也显示了显式指数上界的等价水平的nonbisilimited赋范BPA过程。由于已知的下限从PSpace（Srba，2002）转移到ExpTime（Kiefer，2012），澄清BPA双相似性的2-ExpTime上限的重要性最近有所增加。

2013-03-05cs.FLcs.LO