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

被引：3

作者：

Zawidzki, Michal ^{[1
,2
]}

Schmidt, Renate A. ^{[2
]}

Tishkovsky, Dmitry ^{[2
]}

机构：

[1] Univ Lodz, Dept Log, PL-90131 Lodz, Poland

[2] Univ Manchester, Sch Comp Sci, Manchester M13 9PL, Lancs, England

来源：

INFORMATION PROCESSING LETTERS | 2013年 / 113卷 / 1-2期

基金：

英国工程与自然科学研究理事会;

关键词：

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

D O I：

10.1016/j.ipl.2012.09.007

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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). (C) 2012 Elsevier B.V. All rights reserved.

引用

页码：34 / 38

页数：5

共 10 条

[1] A NExpTime-complete Description Logic strictly contained in C2
Tobies, S
COMPUTER SCIENCE LOGIC, PROCEEDINGS, 1999, 1683 : 292 - 306
[2] On Satisfiability Problem in Modal Logic S5
Salhi, Yakoub
PROCEEDINGS OF THE 35TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING (SAC'20), 2020, : 948 - 955
[3] A Recursive Shortcut for CEGAR: Application to the Modal Logic K Satisfiability Problem
Lagniez, Jean-Marie
Le Berre, Daniel
de Lima, Tiago
Montmirail, Valentin
PROCEEDINGS OF THE TWENTY-SIXTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2017, : 674 - 680
[4] Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic
Halpern, Joseph Y.
Rego, Leandro Chaves
20TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2007, : 2306 - 2311
[5] Characterizing the NP-PSPACE gap in the satisfiability problem for modal logic
Halpern, Joseph Y.
Rego, Leandro Chaves
JOURNAL OF LOGIC AND COMPUTATION, 2007, 17 (04) : 795 - 806
[6] On the Satisfiability Problem for a 4-level Quantified Syllogistic and Some Applications to Modal Logic
Cantone, Domenico
Asmundo, Marianna Nicolosi
FUNDAMENTA INFORMATICAE, 2013, 124 (04) : 427 - 448
[7] Solving the Satisfiability Problem of Modal Logic S5 Guided by Graph Coloring
Huang, Pei
Liu, Minghao
Wang, Ping
Zhang, Wenhui
Ma, Feifei
Zhang, Jian
PROCEEDINGS OF THE TWENTY-EIGHTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2019, : 1093 - 1100
[8] A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem
Caridroit, Thomas
Lagniez, Jean-Marie
Le Berre, Daniel
de Lima, Tiago
Montmirail, Valentin
THIRTY-FIRST AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2017, : 3864 - 3870
[9] BINARY CONNECTIVES FUNCTIONALLY COMPLETE BY THEMSELVES IN S5 MODAL LOGIC
MASSEY, GJ
JOURNAL OF SYMBOLIC LOGIC, 1967, 32 (01) : 91 - &
[10] Modal control in the synthesis problem of binary dynamic systems in linear trigger logic
Kiryushin, A.A.
Rassvetalova, L.A.
Ushakov, A.V.
Avtomatika i Telemekhanika, 1993, (08): : 149 - 156

← 1 →