The Complexity of Regularity in Grammar Logics and Related Modal Logics

摘要

A modal reduction principle of the form [i_1]…[i_n]p→[j_1]…[j_n']p can be viewed as a production rule i_1· …·i-n→j_1·…·j_n' in a formal grammar. We study the extensions of the multimodal logic K_m with m independent K modal connectives by finite addition of axiom schemes of the above form such that the associated finite set of production rules forms a regular grammar. We show that given a regular grammar G and a modal formula φ, deciding whether the formula is satisfiable in the extension of K_m with axiom schemes for G can be done in deterministic exponential-time in the size of G and φ, and this problem is complete for this complexity class.