The expressive power of modal logic with inclusion atoms

Abstract

Modal inclusion logic is the extension of basic modal logic with inclusion atoms, and its semantics is defined on Kripke models with teams. A team of a Kripke model is just a subset of its domain. In this paper we give a complete characterisation for the expressive power of modal inclusion logic: a class of Kripke models with teams is definable in modal inclusion logic if and only if it is closed under k-bisimulation for some integer k, it is closed under unions, and it has the empty team property. We also prove that the same expressive power can be obtained by adding a single unary nonemptiness operator to modal logic. Furthermore, we establish an exponential lower bound for the size of the translation from modal inclusion logic to modal logic with the nonemptiness operator.

In Proceedings GandALF 2015, arXiv:1509.06858

References in corpus (3)

• The Expressive Power of Modal Dependence Logic
• Complexity of validity for propositional dependence logics
• Satisfiability of Modal Inclusion Logic: Lax and Strict Semantics

Cited by in corpus (6)

• Propositional Team Logics
• State-based Modal Logics for Free Choice
• Axiomatizing modal inclusion logic and its variants
• On the Succinctness of Atoms of Dependency
• Validity and Entailment in Modal and Propositional Dependence Logics
• Characterizing Relative Frame Definability in Team Semantics via the Universal Modality