一句话：将规范 BPA 过程的分支互模拟等价刻画为有理幺半群，并给出由正规形确定有限转换器判定的分解框架。
本文重新阐述并简化了 Czerwinski 与 Jancar 关于规范 BPA（Basic Process Algebra）过程上分支互模拟等价的结构性分解结果。此前该结果主要用于推导计算复杂度，并给出了 NEXPTIME 上界，其思路建立在 Fu 的工作之上；He 与 Huang 随后宣布了该问题的 EXPTIME 完全性。本文的目标之一是在一个新的技术框架中呈现原有分解：指出规范 BPA 过程上的分支互模拟等价对应 Sakarovitch 意义下的有理幺半群，特别地，该等价可由正规形计算确定有限转换器判定。另一个目标是给出包括非形式概述在内的完整描述，厘清 Fu 的思想如何被使用，并将所有证明以易读、易验证的形式给出。该版本发表于 LMCS。
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.Comment: The version accepted to LMCS
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Jancar17,
title = {Branching Bisimilarity of Normed BPA Processes as a Rational Monoid},
author = {Petr Jancar},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:17)2017}
}