The Completeness Problem for Modal Logic

被引：2

作者：

Achilleos, Antonis ^{[1
]}

机构：

[1] Reykjavik Univ, Sch Comp Sci, Reykjavik, Iceland

来源：

LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS 2018) | 2018年 / 10703卷

关键词：

Modal logic; Completeness; Computational complexity; Bisimulation; COMPLEXITY; FORMULAS;

D O I：

10.1007/978-3-319-72056-2_1

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We introduce the completeness problem for Modal Logic and examine its complexity. For a definition of completeness for formulas, given a formula of a modal logic, the completeness problem asks whether the formula is complete for that logic. We discover that completeness and validity have the same complexity - with certain exceptions for which there are, in general, no complete formulas. To prove upper bounds, we present a non-deterministic polynomial-time procedure with an oracle from PSPACE that combines tableaux and a test for bisimulation, and determines whether a formula is complete.

引用

页码：1 / 21

页数：21

共 21 条

[11] A MODAL CHARACTERIZATION OF OBSERVATIONAL CONGRUENCE ON FINITE TERMS OF CCS
GRAF, S
SIFAKIS, J
[J]. INFORMATION AND CONTROL, 1986, 68 (1-3): : 125 - 145
[12] Characterizing the NP-PSPACE gap in the satisfiability problem for modal logic
Halpern, Joseph Y.
Rego, Leandro Chaves
[J]. JOURNAL OF LOGIC AND COMPUTATION, 2007, 17 (04) : 795 - 806
[13] A GUIDE TO COMPLETENESS AND COMPLEXITY FOR MODAL-LOGICS OF KNOWLEDGE AND BELIEF
HALPERN, JY
MOSES, Y
[J]. ARTIFICIAL INTELLIGENCE, 1992, 54 (03) : 319 - 379
[14] ALGEBRAIC LAWS FOR NONDETERMINISM AND CONCURRENCY
HENNESSY, M
MILNER, R
[J]. JOURNAL OF THE ACM, 1985, 32 (01) : 137 - 161
[15] Ladner R. E., 1977, SIAM Journal on Computing, V6, P467, DOI 10.1137/0206033
[16] Massacci F, 2000, J AUTOM REASONING, V24, P319, DOI 10.1023/A:1006155811656
[17] Milner R., 1989, Communication and concurrency
[18] Finite models constructed from canonical formulas
Moss, Lawrence S.
[J]. JOURNAL OF PHILOSOPHICAL LOGIC, 2007, 36 (06) : 605 - 640
[19] Muller-Olm M., 1998, ELECT NOTES THEOR CO, V18, P159, DOI DOI 10.1016/S1571-0661(05)80257-9
[20] 3 PARTITION REFINEMENT ALGORITHMS
PAIGE, R
TARJAN, RE
[J]. SIAM JOURNAL ON COMPUTING, 1987, 16 (06) : 973 - 989

← 1 2 3 →