Extending ALCQIO with reachability
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Synthetic Organic Chemistry Methods
