Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 11, Issue 6, pp. 933-960: Abstract.

The Complexity of Regularity in Grammar Logics and Related Modal Logics

Stéphane Demri

Lab. Spécification et Vérification, ENS de Cachan & CNRS UMR 8643, 61 Av. Pdt. Wilson, 94235 Cachan Cedex, France. E-mail: demri@lsv.ens-cachan.fr

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

  Full-Text PDF  (343 KB)


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.