  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.
