Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability

ABSTRACT. Program Analysis requires expressive logics enjoying good computational properties and capable of describing graph-structured information. In particular, logical representation of standard dynamic data structures like lists or trees requires some form of reachability assertions. However, reachability is usually not expressible in decidable logics for graphs such as guarded first-order logic (GF), and thus in Description Logics (DLs), which are mainly fragments of GF. In this work, we introduce the DL $ALCQIO_{b,Re}$ that extends the Boolean $ALCQIO$ KBs with reachability assertions and is tailored for reasoning over programs with dynamic data structures. $ALCQIO_{b,Re}$ is powerful enough to express (an unbounded number of) lists and trees, can describe complex data structures with a high degree of sharing, and also allows compositions like trees of lists or lists of trees. We show that finite model reasoning in $ALCQIO_{b,Re}$ is polynomial-time reducible to finite satisfiability of $ALCQIO$-formulae. As a consequence, we get that finite satisfiability and finite implication in $ALCQIO_{b,Re}$ are NEXPTIME-complete. Extensions of DLs with reachability have been studied previously (mainly in terms of fix-points and regular expressions), but $ALCQIO_{b,Re}$ is the first such enriched DL that remains decidable in the simultaneous presence of nominals, inverse roles and counting quantifiers.