1-安全 Petri 网与特殊立方复形:等价性及应用

Nielsen、Plotkin 和 Winskel(1981)证明了每个 1-安全 Petri 网 $N$ 可展开为事件结构 $\mathcal{E}_N$。由 Thiagarajan(1996 和 2002)的结果,这些展开恰好是迹正则事件结构。Thiagarajan(1996 和 2002)猜想正则事件结构恰好对应于迹正则事件结构。在最近的一篇论文(Chalopin 和 Chepoi, 2017, 2018)中,我们基于事件结构定义域、中位图与 CAT(0) 立方复形之间的显著双射,反驳了该猜想。另一方面,在 Chalopin 和 Chepoi(2018)中我们证明了该猜想对定义域为(虚拟)有限特殊立方复形的通用覆盖的主滤子的正则事件结构成立。在本文中,我们证明逆命题:对任意有限 1-安全 Petri 网 $N$,可构造有限特殊立方复形 ${X}_N$,使得事件结构 $\mathcal{E}_N$(作为 $N$ 的展开得到)的定义域是其通用覆盖 $\widetilde{X}_N$ 的主滤子。这建立了 1-安全 Petri 网与有限特殊立方复形之间的双射,并给出了迹正则事件结构的组合刻画。利用该双射以及图论与几何中的技术(图的 MSO 理论、有界树宽、有界双曲性),我们反驳了 Thiagarajan 的另一个猜想(出自其与 S. Yang 2014 年的论文):1-安全 Petri 网的单调二阶逻辑可判定当且仅当其展开无网格。我们的反例是源自虚拟特殊方形复形 $\dot Z$ 的迹正则事件结构 $\mathcal{\dot E}_Z$。$\mathcal{\dot E}_Z$ 的定义域无网格(因其双曲),但事件结构 $\mathcal{\dot E}_Z$ 的 MSO 理论不可判定。