Decidability or complexity issues about the consistency problem for description logics with concrete domains have already been analysed with tableaux-based or type elimination methods. Concrete domains in ontologies are essential to consider concrete objects and predefined relations. In this work, we expose an automata-based approach leading to the optimal upper bound EXPTIME, that is designed by enriching the transitions with symbolic constraints. We show that the nonemptiness problem for such automata belongs to EXPTIME if the concrete domains satisfy a few simple properties. Then, we provide a reduction from the consistency problem for ontologies, yielding EXPTIME-membership. Thanks to the expressivity of constraint automata, the results are extended to additional ingredients such as inverse roles, functional role names and constraint assertions, while maintaining EXPTIME-membership, which illustrates the robustness of the approach
翻译:关于具有具体域的描述逻辑一致性问题的可判定性或复杂性,已通过基于表或类型消除方法进行了分析。本体中的具体域对于考虑具体对象和预定义关系至关重要。在本工作中,我们提出了一种基于自动机的方法,通过用符号约束丰富转移关系,实现了最优上界EXPTIME。我们证明,若具体域满足若干简单性质,此类自动机的非空性问题属于EXPTIME。随后,我们提供了从本体一致性问题的归约,从而得到EXPTIME成员性。得益于约束自动机的表达能力,该结果可扩展至逆角色、函数角色名和约束断言等附加要素,同时保持EXPTIME成员性,这体现了该方法的鲁棒性。