On bisimulations for description logics

We study bisimulations for useful description logics. The simplest among the considered logics is ALCregALCreg (a variant of PDL). The others extend that logic with the features: inverse roles, nominals, qualified number restrictions, the universal role, and/or the concept constructor for expressing the local reflexivity of a role. They also allow role axioms. Our contributions are as follows. We propose to treat named individuals as initial states and give an appropriate bisimulation condition for that. We also give bisimulation conditions for the universal role and the concept constructor ∃r.Self∃r.Self. We prove that all of the bisimulation conditions for the features can be combined together to guarantee invariance of concepts and the Hennessy-Milner property for the whole class of studied description logics. We address and give results on invariance or preservation of ABoxes, RBoxes and knowledge bases in description logics. Independently from Lutz et al. [26] and [27] we also give results on invariance of TBoxes. We introduce a new notion called QS-interpretation, which is needed for dealing with minimizing interpretations in description logics with qualified number restrictions and/or the concept constructor ∃r.Self∃r.Self. We formulate and prove results on minimality of quotient interpretations w.r.t. the largest auto-bisimulations. We adapt Hopcroft’s automaton minimization algorithm to give an efficient algorithm for computing the partition corresponding to the largest auto-bisimulation of a finite interpretation in any description logic of the considered family. Using the invariance results we compare the expressiveness of the considered description logics w.r.t. concepts, TBoxes and ABoxes. Our results about separating the expressiveness of description logics are naturally extended to the case when instead of ALCregALCreg we have any sublogic of ALCregALCreg that extends ALCALC.