作为有理幺半群的赋范 BPA 过程的分支互模拟
计算机科学中的逻辑
2019-03-14 v3 形式语言与自动机理论
摘要
本文给出了关于赋范 BPA(基本进程代数)过程上分支互模拟的结构性结果的详尽且简化版本，该结果是 Czerwinski 和 Jancar 会议论文(arxiv 2014年7月及 LiCS 2015)的核心。该论文关注计算复杂性，并推导出了 NEXPTIME 上界；作者基于 Fu (ICALP 2013) 的思想，强化了其可判定性结果。后来 He 和 Huang 宣布了该问题的 EXPTIME-完备性(arxiv 2015年1月及 LiCS 2015)，给出了 EXPTIME 成员性的技术证明。He 和 Huang 间接承认了他们所基于的 Czerwinski 和 Jancar 的分解思想，但很难将他们的出发点与新思想区分开。本文的一个目标是在技术新颖的框架中呈现 Czerwinski 和 Jancar 先前的分解结果，指出赋范 BPA 过程上的分支互模拟等价对应于一个有理幺半群(据 [Sakarovitch, 1987] 的意义)；特别地，表明上述等价可由计算正规形式的确定性有限转换器判定。另一个目标是提供完整的描述，包括非正式的概述，以阐明 Fu 的思想是如何被使用的，并以可读且易于验证的形式给出所有证明。
引用
@article{arxiv.1602.05151,
title = {Branching Bisimilarity of Normed BPA Processes as a Rational Monoid},
author = {Petr Jancar},
journal= {arXiv preprint arXiv:1602.05151},
year = {2019}
}
备注
The version accepted to LMCS