Hybrid Modal Operators for Definite Descriptions

TL;DR

This paper investigates the computational complexity and expressive power of modal operators for definite descriptions, revealing their impact on satisfiability complexity and their relation to hybrid and counting logics.

Contribution

It introduces and analyzes the complexity and expressiveness of modal operators for definite descriptions, comparing them with hybrid and counting logics.

Findings

Adding modal operators for descriptions increases satisfiability complexity from PSpace to ExpTime.

Descriptions with Boolean formulas do not increase complexity.

Operators for descriptions are more expressive than hybrid but less than counting operators.

Abstract

In this paper, we study computational complexity and expressive power of modal operators for definite descriptions, which correspond to statements `the modal world which satisfies formula \(varphi\)'. We show that adding such operators to the basic (propositional) modal language has a price of increasing complexity of the satisfiability problem from PSpace to ExpTime. However, if formulas corresponding to descriptions are Boolean only, there is no increase of complexity. Furthermore, we compare definite descriptions with the related operators from hybrid and counting logics. We prove that the operators for definite descriptions are strictly more expressive than hybrid operators, but strictly less expressive than counting operators. We show that over linear structures the same expressive power results hold as in the general case; in contrast, if the linear structures are isomorphic to integers, definite descriptions become as expressive as counting operators.