The Complexity of Reasoning with Boolean Modal Logics (Extended Version)

Carsten Lutz, Ulrike Sattler
The Complexity of Reasoning with Boolean Modal Logics (Extended Version)
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-00-02, 2000. LTCS-Report

Details
Bibtex

KurzfassungAbstract
Boolean Modal Logics extend multi-modal K by allowing the use of boolean operators to define complex relation terms. In this paper, we investigate the complexity of reasoning with various such logics. The main results are that
(1) adding negation of modal parameters to K makes reasoning ExpTime-complete, which is shown by using an automata-theoretic approach, and that (2) adding atomic negation and conjunction to K even yields a NExpTime- complete logic, which is shown by a reduction of a variant of the domino problem.
The last result is relativized by the fact that it depends on an infinite number of modal parameters to be available. If the number of modal parameters is bounded, full Boolean Modal Logic becomes ExpTime-complete. This is shown by a reduction to K enriched with the universal modality.
Bemerkung: Note: See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ Lutz-Sattler-LTCS-00-02,
  address = {Germany},
  author = {C. {Lutz} and U. {Sattler}},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-00-02},
  title = {The Complexity of Reasoning with Boolean Modal Logics (Extended Version)},
  type = {LTCS-Report},
  year = {2000},
}

The Complexity of Reasoning with Boolean Modal Logics (Extended Version)

The Complexity of Reasoning with Boolean Modal Logics (Extended Version)

Carsten LutzCarsten Lutz, Ulrike SattlerUlrike Sattler