Journal of Logic and Computation, Volume 11, Issue 6, pp. 933-960: Abstract.
The Complexity of Regularity in Grammar Logics and Related Modal Logics
Lab. Spécification et Vérification, ENS de Cachan & CNRS UMR 8643, 61 Av. Pdt. Wilson, 94235 Cachan Cedex, France. E-mail: email@example.com
A modal reduction principle of the form [i1] ... [ni]p [rArr] [j1] ... [nj[prime]]p can be viewed as a production rule i1 · ... ·ni -> j1 · ... · nj[prime] in a formal grammar. We study the extensions of the multimodal logic Km 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 Km with axiom schemes from G can be done in deterministic exponential-time in the size of G and Ø, and this problem is complete for this complexity class. Such an extension of Km is called a regular grammar logic. The proof of the exponential-time upper bound is extended to PDL-like extensions of Km and to global logical consequence and global satisfiability problems. Using an equational characterization of context-free languages, we show that by replacing the regular grammars by linear ones, the above problem becomes undecidable. The last part of the paper presents non-trivial classes of exponential time complete regular grammar logics.
Keywords: Computational complexity, modal logic, formal grammar, regular language, finite automaton