赋范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]的意义上）;特别是，它表明，所提到的等价可以通过计算确定性有限转换器的规范形式来决定。另一个目的是提供一个完整的描述，包括一个非正式的概述，这也应该清楚傅的想法是如何使用的，并以一种可读和易于验证的形式给出所有证据。
英文摘要：
The paper presents an elaborated and simplified version of the structural result for branching bisimilarity on normed BPA (Basic Process Algebra) processes that was the crux of a conference paper by Czerwinski and Jancar (arxiv 7/2014 and LiCS 2015). That paper focused on the computational complexity, and a NEXPTIME-upper bound has been derived; the authors built on the ideas by Fu (ICALP 2013), and strengthened his decidability result. Later He and Huang announced the EXPTIME-completeness of this problem (arxiv 1/2015, and LiCS 2015), giving a technical proof for the EXPTIME membership. He and Huang indirectly acknowledge the decomposition ideas by Czerwinski and Jancar on which they also built, but it is difficult to separate their starting point from their new ideas. One aim here is to present the previous decomposition result of Czerwinski and Jancar in a technically new framework, noting that branching bisimulation equivalence on normed BPA processes corresponds to a rational monoid (in the sense of [Sakarovitch, 1987]); in particular it is shown that the mentioned equivalence can be decided by normal-form computing deterministic finite transducers. Another aim is to provide a complete description, including an informal overview, that should also make clear how Fu's ideas were used, and to give all proofs in a form that should be readable and easily verifiable.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
