离散事件系统分散状态推理与故障诊断/预测的统一方法
A unified method to decentralized state inference and fault diagnosis/prediction of discrete-event systems
摘要：
状态推断问题和故障诊断/预测问题是许多领域的基本课题。在本文中，我们考虑离散事件系统（DES）建模的有限状态自动机（FSA）。后一个问题的分散版本存在结果，但前一个问题的分散版本几乎没有结果。我们提出了一个分散版本的强可检测性称为co-detectability，这意味着一旦一个系统满足这一属性，对于每个生成的无限长的事件序列，至少有一个本地观察员可以确定当前和后续状态后，一个共同的观察时间延迟。我们证明了验证FSA的可检测性的问题是CONP困难的。此外，我们使用一个统一的并发合成方法，给出了PSPACE验证算法的可检测性，可诊断性，和可预测性的FSA，没有任何假设或修改的FSA正在考虑，其中可诊断性首先研究的[Debouk & Lafortune & Teneketzis 2000]，而可预测性首先研究的[Kumar \& Takai 2010]。通过我们提出的统一方法，可以看出，为了验证共同可检测性，与验证其他两个属性相比，将遇到更多的技术困难，因为在共同可检测性中，生成的输出被计数，但在后两个属性中，仅计数事件的发生。例如，当生成一个输出时，可能发生任何数量的不可观察事件。PSPACE-硬度验证共同诊断性是已知的文献。在本文中，我们证明了PSPACE-硬度验证的可预测性。
英文摘要：
The state inference problem and fault diagnosis/prediction problem are fundamental topics in many areas. In this paper, we consider discrete-event systems (DESs) modeled by finite-state automata (FSAs). There exist results for decentralized versions of the latter problem but there is almost no result for a decentralized version of the former problem. We propose a decentralized version of strong detectability called co-detectability which implies that once a system satisfies this property, for each generated infinite-length event sequence, at least one local observer can determine the current and subsequent states after a common observation time delay. We prove that the problem of verifying co-detectability of FSAs is coNP-hard. Moreover, we use a unified concurrent-composition method to give PSPACE verification algorithms for co-detectability, co-diagnosability, and co-predictability of FSAs, without any assumption or modifying the FSAs under consideration, where co-diagnosability is firstly studied by [Debouk & Lafortune & Teneketzis 2000], while co-predictability is firstly studied by [Kumar \& Takai 2010]. By our proposed unified method, one can see that in order to verify co-detectability, more technical difficulties will be met compared to verifying the other two properties, because in co-detectability, generated outputs are counted, but in the latter two properties, only occurrences of events are counted. For example, when one output was generated, any number of unobservable events could have occurred. The PSPACE-hardness of verifying co-diagnosability is already known in the literature. In this paper, we prove the PSPACE-hardness of verifying co-predictability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
