标记的最大加自动机的可诊断性
摘要：关于具有标签的最大加自动机$mathcal{A}^{mathcal{D}}$在时域系统中的可诊断性的表征 诊断性被描述为一种实时系统。为了表示时间流逝，考虑了一个特殊类的对角线，称为progressive，其中存在一个总的规范次序，至少有一个大于$ extbf{1}$的元素，大于$ extbf{1}的充分多的元素的积是任意大的，且满足可消去定律。然后对progressive对角线下的$mathcal{A}^{mathcal{D}}$的可诊断性提出了一个概念。通过发展并发组合的概念，给出了$mathcal{A}^{mathcal{D}}$可诊断性的充分必要条件。还证明了验证$mathcal{A}^{underline{mathbb{Q}}}$可诊断性的问题是coNP完全的，其中连同对于确定的无死锁和无发散的$mathcal{A}^{underline{mathbb{N}}}$也是coNP难的，其中$underline{mathbb{Q}}$和$underline{mathbb{N}}$是具有元素在$mathbb{Q}cup{-infty}$和$mathbb{N}cup{-infty}$中的最大加对角线。
作者：Kuize Zhang, Joerg Raisch
论文ID：2109.07125
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2021-09-16