幺半群上标记加权自动机的可检测性

本文首次给出了一般幺半群上标记加权自动机(简记为 $\mathcal{A}^{\mathfrak{M}}$)的四种基本可检测性概念的刻画,这四种概念分别为强(周期)可检测性(SD 与 SPD)和弱(周期)可检测性(WD 与 WPD)。首先,我们为 $\mathcal{A}^{\mathfrak{M}}$ 表述了并发复合、观测器和检测器的概念。其次,我们使用并发复合给出 SD 的等价条件,使用检测器给出 SPD 的等价条件,并使用观测器给出 WD 和 WPD 的等价条件,均针对一般 $\mathcal{A}^{\mathfrak{M}}$ 且不作任何假设。第三,我们证明了对于幺半群 $(\mathbb{Q}^k,+)$ 上的标记加权自动机(记为 $\mathcal{A}^{\mathbb{Q}^k}$),通过建立 $\mathcal{A}^{\mathbb{Q}^k}$ 与 NP 完全精确路径长度问题([Nykänen and Ukkonen, 2002] 证得)及 Presburger 算术某一子类之间的新联系,其并发复合、观测器和检测器可分别在 NP、$2$-EXPTIME 和 $2$-EXPTIME 内计算。据此我们证明,对于 $\mathcal{A}^{\mathbb{Q}^k}$,SD 可在 coNP 内验证,而 SPD、WD 和 WPD 可在 $2$-EXPTIME 内验证。最后,我们证明在幺半群 $(\mathbb{N},+)$ 上确定性、无死锁且无散度的 $\mathcal{A}^{\mathbb{N}}$ 的 SD 与 SPD 验证问题均为 coNP-hard。所发展的原创方法将为刻画 $\mathcal{A}^{\mathfrak{M}}$ 的其他基本性质(如可诊断性、不透明性)提供基础。我们还初步探索了标记时间自动机中的可检测性,并证明 SD 验证问题是 PSPACE-完全的,而 WD 和 WPD 不可判定。