Journal of Logic and Computation, Volume 11, Issue 6, pp. 933960: Abstract.
The Complexity of Regularity in Grammar Logics and Related Modal LogicsStéphane Demri^{} ^{}Lab. Spécification et Vérification, ENS de Cachan & CNRS UMR 8643, 61 Av. Pdt. Wilson, 94235 Cachan Cedex, France. Email: demri@lsv.enscachan.fr
A modal reduction principle of the form [i_{1}] ... [_{n}i]p [rArr] [j_{1}] ... [_{n}j[prime]]p can be viewed as a production rule i_{1} · ... ·_{n}i > j_{1} · ... · _{n}j[prime] 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 from G can be done in deterministic exponentialtime in the size of G and Ø, and this problem is complete for this complexity class. Such an extension of K_{m} is called a regular grammar logic. The proof of the exponentialtime upper bound is extended to PDLlike extensions of K_{m} and to global logical consequence and global satisfiability problems. Using an equational characterization of contextfree languages, we show that by replacing the regular grammars by linear ones, the above problem becomes undecidable. The last part of the paper presents nontrivial classes of exponential time complete regular grammar logics.
Keywords: Computational complexity, modal logic, formal grammar, regular language, finite automaton
