# A Characterization Theorem for a Modal Description Logic

## TL;DR

This paper establishes a precise characterization of the expressive power of a modal description logic called S5-ALC with local roles, linking it to bisimulation-invariant fragments of a corresponding modal first-order logic.

## Contribution

It proves a modal characterization theorem for S5-ALC, showing its exact expressive power as the bisimulation-invariant fragment of S5-FOL, extending prior foundational results.

## Key findings

- S5-ALC with local roles is bisimulation invariant.
- The logic precisely captures the bisimulation-invariant fragment of S5-FOL.
- The characterization holds over both finite and unrestricted models.

## Abstract

Modal description logics feature modalities that capture dependence of knowledge on parameters such as time, place, or the information state of agents. E.g., the logic S5-ALC combines the standard description logic ALC with an S5-modality that can be understood as an epistemic operator or as representing (undirected) change. This logic embeds into a corresponding modal first-order logic S5-FOL. We prove a modal characterization theorem for this embedding, in analogy to results by van Benthem and Rosen relating ALC to standard first-order logic: We show that S5-ALC with only local roles is, both over finite and over unrestricted models, precisely the bisimulation invariant fragment of S5-FOL, thus giving an exact description of the expressive power of S5-ALC with only local roles.