Title: Canonical Models and the Complexity of Modal Team Logic,
Abstract: We study modal team logic MTL, the team-semantical extension of modal logic
ML closed under Boolean negation. Its fragments, such as modal dependence,
independence, and inclusion logic, are well-understood. However, due to the
unrestricted Boolean negation, the satisfiability problem of full MTL has been
notoriously resistant to a complexity theoretical classification. In our
approach, we introduce the notion of canonical models into the team-semantical
setting. By construction of such a model, we reduce the satisfiability problem
of MTL to simple model checking. Afterwards, we show that this approach is
optimal in the sense that MTL-formulas can efficiently enforce canonicity.
Furthermore, to capture these results in terms of complexity, we introduce a
non-elementary complexity class, TOWER(poly), and prove that it contains
satisfiability and validity of MTL as complete problems. We also prove that the
fragments of MTL with bounded modal depth are complete for the levels of the
elementary hierarchy (with polynomially many alternations). The respective
hardness results hold for both strict or lax semantics of the modal operators
and the splitting disjunction, and also over the class of reflexive and
transitive frames.