Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features

Bartosz Bednarczyk

TL;DR

The paper investigates how lifting regular path constraints to non-regular languages affects decidability in description logics, focusing on $\mathcal{ALC}_{\textsf{vpl}}$ and its extensions. It provides strong undecidability results for $\mathcal{ALC}_{\textsf{vpl}}$ when augmented with the $\mathsf{Self}$ operator or with nominals, and it shows undecidability for query entailment with non-regular atoms. The authors also relate these findings to classical undecidability results via reductions from DOCA intersection non-emptiness and domino tiling problems, while noting positive results like $2^{\text{ExpTime}}$-completeness for certain query entailments in restricted settings. The work highlights the delicate boundary between decidability and undecidability in expressive DLs with path constraints and non-regular languages, and it outlines open problems regarding finite satisfiability and other extensions.

Abstract

We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics extending ALC. Our primary objects of interest are ALCreg and ALCvpl, the extensions of with path expressions employing, respectively, regular and visibly-pushdown languages. The first one, ALCreg, is a notational variant of the well-known Propositional Dynamic Logic of Fischer and Ladner. The second one, ALCvpl, was introduced and investigated by Loding and Serre in 2007. The logic ALCvpl generalises many known decidable non-regular extensions of ALCreg. We provide a series of undecidability results. First, we show that decidability of the concept satisfiability problem for ALCvpl is lost upon adding the seemingly innocent Self operator. Second, we establish undecidability for the concept satisfiability problem for ALCvpl extended with nominals. Interestingly, our undecidability proof relies only on one single non-regular (visibly-pushdown) language, namely on r#s# := { r^n s^n | n in N } for fixed role names r and s. Finally, in contrast to the classical database setting, we establish undecidability of query entailment for queries involving non-regular atoms from r#s#, already in the case of ALC-TBoxes.

Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features

TL;DR

The paper investigates how lifting regular path constraints to non-regular languages affects decidability in description logics, focusing on and its extensions. It provides strong undecidability results for when augmented with the operator or with nominals, and it shows undecidability for query entailment with non-regular atoms. The authors also relate these findings to classical undecidability results via reductions from DOCA intersection non-emptiness and domino tiling problems, while noting positive results like -completeness for certain query entailments in restricted settings. The work highlights the delicate boundary between decidability and undecidability in expressive DLs with path constraints and non-regular languages, and it outlines open problems regarding finite satisfiability and other extensions.

Abstract

We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics extending ALC. Our primary objects of interest are ALCreg and ALCvpl, the extensions of with path expressions employing, respectively, regular and visibly-pushdown languages. The first one, ALCreg, is a notational variant of the well-known Propositional Dynamic Logic of Fischer and Ladner. The second one, ALCvpl, was introduced and investigated by Loding and Serre in 2007. The logic ALCvpl generalises many known decidable non-regular extensions of ALCreg. We provide a series of undecidability results. First, we show that decidability of the concept satisfiability problem for ALCvpl is lost upon adding the seemingly innocent Self operator. Second, we establish undecidability for the concept satisfiability problem for ALCvpl extended with nominals. Interestingly, our undecidability proof relies only on one single non-regular (visibly-pushdown) language, namely on r#s# := { r^n s^n | n in N } for fixed role names r and s. Finally, in contrast to the classical database setting, we establish undecidability of query entailment for queries involving non-regular atoms from r#s#, already in the case of ALC-TBoxes.
Paper Structure (12 sections, 13 theorems, 11 equations, 2 figures, 2 tables)

This paper contains 12 sections, 13 theorems, 11 equations, 2 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Basics on $\mathcal{ALC}$.
  4. $\mathcal{ALC}$ with extras.
  5. $\mathcal{ALC}$ with path expressions.
  6. Visibly-pushdown languages.
  7. The logic $\mathcal{ALC}_{\textsf{vpl}}$.
  8. The query entailment problem.
  9. Tree models.
  10. Undecidability results for extensions of $\mathcal{ALC}_{\textsf{vpl}}$ that follow from the literature.
  11. Negative results I: The Seemingly innocent Self operator
  12. Negative results II: Nominals meet rnsn

Key Result

Corollary 2.2

Every satisfiable $\mathcal{ALC}_{\textsf{vpl}}$-TBox $\mathcal{T}$ has a single-role tree-like model.The original work considers concepts only. However, all their results transfer immediately to the case of TBoxes, as TBoxes can be internalised in concepts in the presence of regular expressions 200

Figures (2)

  • Figure 1: An example $\Sigma$-friendly $(\mathcal{I}, \mathrm{d})$ encoding the word $\mathtt{abbac}$.
  • Figure 2:

Theorems & Definitions (26)

  • Example 2.1
  • Corollary 2.2: Consequence of the proof of Prop. 8 of LodingLS07
  • Corollary 2.3
  • Corollary 2.4
  • Lemma 3.1
  • proof : Proof sketch.
  • Lemma 3.3
  • proof
  • Lemma 3.4
  • proof
  • ...and 16 more