Completing the Picture: Complexity of Graded Modal Logics with Converse

作     者：Bednarczyk, Bartosz Kieronski, Emanuel Witkowski, Piotr 

作者机构：Tech Univ Dresden Computat Log Grp Dresden Germany Univ Wroclaw Inst Comp Sci Wroclaw Poland 

出 版 物：《THEORY AND PRACTICE OF LOGIC PROGRAMMING》 (逻辑程序设计理论与实践)

年 卷 期：2021年第21卷第4期

页      面：493-520页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Polish Ministry of Science and Higher Education program "Diamentowy Grant" [DI2017 006447] Polish National Science Centre [2016/21/B/ST6/01444] 

主　　题：modal logic complexity graded modalities satisfiability 

摘      要：A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames has already been established. By traditional classes of frames, we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper, we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular, we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.