EXPLORING NON-REGULAR EXTENSIONS OF PROPOSITIONAL DYNAMIC LOGIC WITH DESCRIPTION-LOGICS FEATURES.

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 ALC_reg and ALC_vpl, the extensions of ALC with path expressions employing, respectively, regular and visibly-pushdown languages. The first one, ALC_reg, is a notational variant of the well-known Propositional Dynamic Logic of Fischer and Ladner. The second one, ALC_vpl, was introduced and investigated by Löding and Serre in 2007. The logic ALC_vpl generalises many known decidable non-regular extensions of ALC_reg. We provide a series of undecidability results. First, we show that decidability of the concept satisfiability problem for ALC_vpl is lost upon adding the seemingly innocent Self operator. Second, we establish undecidability for the concept satisfiability problem for ALC_vpl extended with nominals. Interestingly, our undecidability proof relies only on one single non-regular (visibly-pushdown) language, namely on r^#s^# := {rⁿsⁿ | n ∈ 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. [ABSTRACT FROM AUTHOR]