Finite Entailment of UCRPQs over ALC Ontologies

TL;DR

This paper studies the finite entailment problem for UCRPQs over ALC ontologies, providing a tight 2EXPTIME complexity bound using a novel automata-based approach.

Contribution

It introduces a new automata-based decision procedure for finite entailment of UCRPQs over ALC ontologies, establishing a tight complexity bound.

Findings

Decidability of finite entailment for UCRPQs over ALC

Tight 2EXPTIME upper bound for the problem

Novel automata-based stratification technique

Abstract

We investigate the problem of finite entailment of ontology-mediated queries. We consider the expressive query language, unions of conjunctive regular path queries (UCRPQs), extending the well-known class of union of conjunctive queries, with regular expressions over roles. We look at ontologies formulated using the description logic ALC, and show a tight 2EXPTIME upper bound for entailment of UCRPQs. At the core of our decision procedure, there is a novel automata-based technique introducing a stratification of interpretations induced by the deterministic finite automaton underlying the input UCRPQ