Extending ALCQIO with reachability

TL;DR

This paper introduces an extended description logic, ALCQIO_{b,Re}, that incorporates reachability assertions, enabling expressive modeling of complex data structures for software verification while maintaining decidability and manageable computational complexity.

Contribution

It extends ALCQIO with reachability, proving that finite satisfiability and implication are NEXPTIME-complete, and is the first logic to combine these features while remaining decidable on finite structures.

Findings

ALCQIO_{b,Re} can describe complex data structures with sharing.

Finite satisfiability reduces to ALCQIO, ensuring decidability.

The logic is NEXPTIME-complete for finite satisfiability and implication.

Abstract

We introduce a description logic ALCQIO_{b,Re} which adds reachability assertions to ALCQIO, a sub-logic of the two-variable fragment of first order logic with counting quantifiers. ALCQIO_{b,Re} is well-suited for applications in software verification and shape analysis. Shape analysis requires expressive logics which can express reachability and have good computational properties. We show that ALCQIO_{b,Re} can describe complex data structures with a high degree of sharing and allows compositions such as list of trees. We show that the finite satisfiability and implication problems of ALCQIO_{b,Re}-formulae are 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. Description logics with transitive closure constructors have been studied before, but ALCQIO_{b,Re} is the first description logic that remains decidable on finite structures while allowing at the same time nominals, inverse roles, counting quantifiers and reachability assertions,