Expressive Power of Definite Descriptions in Modal Logics

Motivated by applications in knowledge representation and reasoning, modal and description logics have been recently extended with definite description operators. Such operators provide us with a tool for referring to a particular element of a model by stating a property satisfied only by this element. This mechanism resembles the way we refer to objects in natural language, which makes it an attractive component of ontology and query languages. In this paper, we aim to provide a tool for analysing the expressive power of logics with definite descriptions. In particular, we introduce an adequate bisimulation notion for the basic modal logic extended with definite descriptions. We exploit the introduced bisimulation to relate expressive power of definite descriptions to other operators and we develop an algorithm for computing the maximal bisimulation between a pair of models. Furthermore, we consider a simplified setting, where expressions used in definite descriptions do not mention modal operators. We show how this restriction impacts our results.