Subsumption in $\mathcal{FL}_{\bot \mathit{reg}}$ with TBoxes Is in ExpTime

TL;DR

This paper analyzes the computational complexity of concept subsumption in certain description logics, establishing that with TBoxes, the problem is ExpTime-complete, using a novel reduction to parity pushdown games.

Contribution

It provides the first complexity classification for subsumption in $l_{ot reg}$ with TBoxes, showing it is ExpTime-complete, and introduces a new reduction technique.

Findings

Subsumption in $l_{ot reg}$ with TBoxes is ExpTime-complete.

Subsumption without TBoxes is PSpace-complete.

The complexity results are derived via a reduction to parity pushdown games.

Abstract

Description logics (DL) are a family of formal languages for representing and reasoning about structured knowledge in terms of concepts and their relationships. A central reasoning problem in DL is concept subsumption. Although this problem has been widely studied, important open problems remain for certain logics. The expressive power of DLs depends on the constructors available for building complex concepts. In this work, we investigate subsumption in the restricted logic $\mathcal{FL}_{\bot \mathit{reg}}$ and its related fragments $\mathcal{FL}_\mathit{reg}$, $\mathcal{FL}_\bot$, and $\mathcal{FL}_0$. These logics support value restrictions over role names, where the subscript $\bot$ denotes the presence of the empty concept and ${reg}$ denotes the use of regular expressions over roles. None of these logics includes concept negation. We show that deciding subsumption between two concept descriptions in $\mathcal{FL}_{\bot \mathit{reg}}$ and $\mathcal{FL}_\mathit{reg}$ is PSpace-complete. When subsumption is considered with respect to a TBox (i.e., a set of axioms), the complexity increases to ExpTime-complete. Our results are obtained via a novel reduction to parity pushdown games.