Model-based diagnosis has been an active research topic in different communities including artificial intelligence, formal methods, and control. This has led to a set of disparate approaches addressing different classes of systems and seeking different forms of diagnoses. In this paper, we resolve such disparities by generalising Reiter's theory to be agnostic to the types of systems and diagnoses considered. This more general theory of diagnosis from first principles defines the minimal diagnosis as the set of preferred diagnosis candidates in a search space of hypotheses. Computing the minimal diagnosis is achieved by exploring the space of diagnosis hypotheses, testing sets of hypotheses for consistency with the system's model and the observation, and generating conflicts that rule out successors and other portions of the search space. Under relatively mild assumptions, our algorithms correctly compute the set of preferred diagnosis candidates. The main difficulty here is that the search space is no longer a powerset as in Reiter's theory, and that, as consequence, many of the implicit properties (such as finiteness of the search space) no longer hold. The notion of conflict also needs to be generalised and we present such a more general notion. We present two implementations of these algorithms, using test solvers based on satisfiability and heuristic search, respectively, which we evaluate on instances from two real world discrete event problems. Despite the greater generality of our theory, these implementations surpass the special purpose algorithms designed for discrete event systems, and enable solving instances that were out of reach of existing diagnosis approaches.
翻译:基于模型的诊断一直是人工智能、形式化方法和控制等多个领域的热门研究课题。这导致了针对不同系统类别和寻求不同诊断形式的一系列分散方法。在本文中,我们通过将Reiter的理论泛化为对系统和诊断类型无关的理论,从而解决了这些分散性问题。这种更通用的基于第一原理的诊断理论将最小诊断定义为在假设搜索空间中的一组优选诊断候选方案。计算最小诊断通过探索诊断假设空间,测试假设组合与系统模型和观察结果的一致性,并生成排除搜索空间后继节点及其他部分的冲突来实现。在相对温和的假设下,我们的算法能正确计算优选诊断候选方案集。主要困难在于搜索空间不再是Reiter理论中的幂集,因此许多隐含性质(如搜索空间的有限性)不再成立。冲突概念也需要泛化,我们提出了这种更通用的概念。我们分别使用基于可满足性和启发式搜索的测试求解器实现了两种算法,并在来自两个真实世界离散事件问题的实例上进行了评估。尽管我们的理论具有更高的通用性,但这些实现超越了专为离散事件系统设计的专用算法,并能够解决现有诊断方法无法触及的实例。