Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is NExpTime-Complete

Zawidzki, M. and Schmidt, R. A. and Tishkovsky, D. (2013)

Information Processing Letters 113 (1-2) 34-38. BiBTeX, DOI.

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).


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 24 Sep 13
Copyright © 2013 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk