Satisfiability problem for modal logic with global counting operators coded in binary is NExpTime-complete

This paper provides a proof of NExpTime-completeness of the satisfiability problem for the logic K(En)K(En) (modal logic K with global counting operators), where number constraints are coded in binary. Hitherto the tight complexity bounds (namely ExpTime-completeness) have been established only for this logic with number restrictions coded in unary. The upper bound is established by showing that K(En)K(En) has the exponential-size model property and the lower bound follows from reducibility of exponential bounded tiling problem to K(En)K(En).

► We prove NExpTime-completeness of modal logic with counting operators coded in binary.
► We establish the upper bound by proving the exponential-size model property with a precise bounding function.
► We establish the lower bound by encoding the bounded tiling problem within the logic.
► We draw possible extensions of the complexity proof on the logics defined over various frame classes.