The Expressive Power of Modal Dependence Logic

TL;DR

This paper explores the expressive capabilities of modal dependence logic and related logics, revealing their definability conditions, equivalences, and complexity implications for translations.

Contribution

It characterizes the properties definable in modal logic with intuitionistic disjunction and shows their equivalence with extended modal dependence logic.

Findings

Properties definable are downward closed and closed under team k-bisimulation.

Modal logic with intuitionistic disjunction and extended modal dependence logic have the same expressive power.

Translations from extended modal dependence logic to modal logic with intuitionistic disjunction can cause exponential formula size increase.

Abstract

We study the expressive power of various modal logics with team semantics. We show that exactly the properties of teams that are downward closed and closed under team k-bisimulation, for some finite k, are definable in modal logic extended with intuitionistic disjunction. Furthermore, we show that the expressive power of modal logic with intuitionistic disjunction and extended modal dependence logic coincide. Finally we establish that any translation from extended modal dependence logic into modal logic with intuitionistic disjunction increases the size of some formulas exponentially.