The Inverse Method Implements the Automata Approach for Modal Satisfiability

Franz BaaderFranz Baader, Stephan TobiesStephan Tobies

Datei:BaaderTobies-LTCS-01-03.ps.gz

Download

Franz Baader, Stephan Tobies
The Inverse Method Implements the Automata Approach for Modal Satisfiability
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume 01-03, 2001. LTCS-Report

Details
Bibtex

KurzfassungAbstract
Tableaux-based decision procedures for satisfiability of modal and description logics behave quite well in practice, but it is sometimes hard to obtain exact worst-case complexity results using these approaches, especially for EXPTIME-complete logics.In contrast, automata-based approaches often yield algorithms for which optimal worst-case complexity can easily be proved. However, the algorithms obtained this way are usually not only worst-case, but also best-case exponential: they first construct an automaton that is always exponential in the size of the input, and then apply the (polynomial) emptiness test to this large automaton. To overcome this problem, one must try to construct the automaton ``on-the-fly while performing the emptiness test. In this paper we will show that Voronkov's inverse method for the modal logic K can be seen as an on-the-fly realization of the emptiness test done by the automata approach for K. The benefits of this result are two-fold. First, it shows that Voronkov's implementation of the inverse method, which behaves quite well in practice, is an optimized on-the-fly implementation of the automata-based satisfiability procedure for K. Second, it can be used to give a simpler proof of the fact that Voronkov's optimizations do not destroy completeness of the procedure. We will also show that the inverse method can easily be extended to handle global axioms, and that the correspondence to the automata approach still holds in this setting. In particular, the inverse method yields an EXPTIME-algorithm for satisfiability in K w.r.t. global axioms.
Bemerkung: Note: See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ BaaderTobies-LTCS-01-03,
  address = {Germany},
  author = {F. {Baader} and S. {Tobies}},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {01-03},
  title = {The Inverse Method Implements the Automata Approach for Modal Satisfiability},
  type = {LTCS-Report},
  year = {2001},
}