by Zawidzki, M., Schmidt, R. A. and Tishkovsky, D.
Abstract:
This paper provides a proof of NExpTime-completeness of the satisfiability problem for the logic 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) has the exponential-size model property and the lower bound follows from reducibility of exponential bounded tiling problem to K(En).
Reference:
Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is NExpTime-Complete (Zawidzki, M., Schmidt, R. A. and Tishkovsky, D.), In Information Processing Letters, volume 113, 2013.
Bibtex Entry:
@ARTICLE{ZawidzkiSchmidtTishkovsky13,
AUTHOR = {Zawidzki, M. and Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2013},
TITLE = {Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is {NExpTime}-Complete},
JOURNAL = {Information Processing Letters},
VOLUME = {113},
NUMBER = {1--2},
PAGES = {34--38},
DOI = {http://dx.doi.org/10.1016/j.ipl.2012.09.007},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/ZawidzkiSchmidtTishkovsky12.html},
ABSTRACT = {This paper provides a proof of NExpTime-completeness of the
satisfiability problem for the logic 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) has the
exponential-size model property and the lower bound follows from
reducibility of exponential bounded tiling problem to K(En).},
}