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 $\mathrm{K}({‐{E}}_n)$ (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 $\mathrm{K}({‐{E}}_n)$ has the exponential‐size model property and the lower bound follows from reducibility of exponential bounded tiling problem to $\mathrm{K}({\mathsf{E}}_n)$ .