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

Michał Zawidzki; Renate A. Schmidt; Dmitry Tishkovsky

doi:10.1016/j.ipl.2012.09.007

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

Michał Zawidzki, Renate A. Schmidt, Dmitry Tishkovsky

Research output: Contribution to journal › Article › peer-review

Abstract

This paper provides a proof of NExpTime-completeness of the satisfiability problem for the logic 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 K(E n) has the exponential-size model property and the lower bound follows from reducibility of exponential bounded tiling problem to K(E n). © 2012 Elsevier B.V. All rights reserved.

Original language	English
Pages (from-to)	34-38
Number of pages	4
Journal	Information Processing Letters
Volume	113
Issue number	1-2
DOIs	https://doi.org/10.1016/j.ipl.2012.09.007
Publication status	Published - Jan 2013

Keywords

Computational complexity
Counting quantifiers
Finite model property
Modal logic
Theory of computation
Tiling problem

Access to Document

10.1016/j.ipl.2012.09.007

http://www.cs.man.ac.uk/ schmidt/publications/ZawidzkiSchmidtTishkovsky12.html

Cite this

@article{c0173a11184142629f075d231bafbf88,

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

abstract = "This paper provides a proof of NExpTime-completeness of the satisfiability problem for the logic 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 K(E n) has the exponential-size model property and the lower bound follows from reducibility of exponential bounded tiling problem to K(E n). {\textcopyright} 2012 Elsevier B.V. All rights reserved.",

keywords = "Computational complexity, Counting quantifiers, Finite model property, Modal logic, Theory of computation, Tiling problem",

author = "Micha{\l} Zawidzki and Schmidt, {Renate A.} and Dmitry Tishkovsky",

year = "2013",

month = jan,

doi = "10.1016/j.ipl.2012.09.007",

language = "English",

volume = "113",

pages = "34--38",

journal = "Information Processing Letters",

issn = "0020-0190",

publisher = "Elsevier BV",

number = "1-2",

}

TY - JOUR

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

AU - Zawidzki, Michał

AU - Schmidt, Renate A.

AU - Tishkovsky, Dmitry

PY - 2013/1

Y1 - 2013/1

N2 - This paper provides a proof of NExpTime-completeness of the satisfiability problem for the logic 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 K(E n) has the exponential-size model property and the lower bound follows from reducibility of exponential bounded tiling problem to K(E n). © 2012 Elsevier B.V. All rights reserved.

AB - This paper provides a proof of NExpTime-completeness of the satisfiability problem for the logic 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 K(E n) has the exponential-size model property and the lower bound follows from reducibility of exponential bounded tiling problem to K(E n). © 2012 Elsevier B.V. All rights reserved.

KW - Computational complexity

KW - Counting quantifiers

KW - Finite model property

KW - Modal logic

KW - Theory of computation

KW - Tiling problem

U2 - 10.1016/j.ipl.2012.09.007

DO - 10.1016/j.ipl.2012.09.007

M3 - Article

SN - 0020-0190

VL - 113

SP - 34

EP - 38

JO - Information Processing Letters

JF - Information Processing Letters

IS - 1-2

ER -

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

Abstract

Keywords

Access to Document

Fingerprint

Cite this