正则表达式的进程解释之像在互模拟折叠下不封闭
摘要
对于带有死锁0和空步1的整类正则表达式，其关于互相似性的Milner进程语义（1984）的公理化与可表达性问题已被证明是困难的。我们报告一种现象，该现象源于在可用0时额外引入1，并将造成此困难的一个关键原因凸显出来。具体而言，虽然无1正则表达式的解释在互模拟折叠下封闭，但任意正则表达式的解释并非如此。无1正则表达式的进程图解释满足环存在与消除性质LEE，且该性质在互模拟折叠下保持。LEE的这些特性曾被用于证明：关于互相似性的无1正则表达式的等式证明系统是完全的，且判定一个进程图是否与某个无1正则表达式的解释互相似可在多项式时间内完成。虽然正则表达式的解释一般不满足LEE性质，我们证明可通过带1-转移的精化解释（类似于自动机的静默步）来恢复LEE。这表明LEE对于一般的公理化与可表达性问题也可能是便利的。但出现了需解决的新现象：进程图“可被精化为带1-转移且具LEE的进程图”这一性质在互模拟折叠下不保持。我们给出一个含两个1-转移的10顶点图，其满足LEE，且其中一对互相似顶点在保持精化性质的前提下无法折叠到一起。这意味着正则表达式的进程解释之像在互模拟折叠下不封闭。
引用
@article{arxiv.2303.08553,
title = {The Image of the Process Interpretation of Regular Expressions is Not Closed under Bisimulation Collapse},
author = {Clemens Grabmayer},
journal= {arXiv preprint arXiv:2303.08553},
year = {2023}
}
备注
Report (14 p. + 10 p. app) written for a submission in Jan 2021 (now with added explanation of relation with subsequent work that was published earlier) concerning the crucial observation underlying the crystallization process in arXiv:2209.12188 version 2: extension of Prop. 2.12 to "under star 1-free" expressions, and correction in its proof (added termination subterm to extraction function)