{PSPACE} Automata with Blocking for Description Logics

F. BaaderF. Baader, J. HladikJ. Hladik, R. PenalozaR. Penaloza

Download

F. Baader, J. Hladik, R. Penaloza
{PSPACE} Automata with Blocking for Description Logics
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, volume LTCS-06-04, 2006. LTCS-Report

Details
Bibtex

KurzfassungAbstract
In Description Logics (DLs), both tableau-based and automata-based

 algorithms are frequently used to show decidability and complexity results
 for basic inference problems such as satisfiability of concepts. Whereas
 tableau-based algorithms usually yield worst-case optimal algorithms in the
 case of PSPACE-complete logics, it is often very hard to design optimal
 tableau-based algorithms for EXPTIME-complete DLs. In contrast, the
 automata-based approach is usually well-suited to prove EXPTIME
 upper-bounds, but its direct application will usually also yield an
 EXPTIME-algorithm for a PSPACE-complete logic since the (tree) automaton
 constructed for a given concept is usually exponentially large.  In the
 present paper, we formulate conditions under which an on-the-fly
 construction of such an exponentially large automaton can be used to obtain
 a PSPACE-algorithm.  We illustrate the usefulness of this approach by
 proving a new PSPACE upper-bound for satisfiability of concepts w.r.t.
 acyclic terminologies in the DL SI, which extends the basic DL ALC with

transitive and inverse roles.

Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ BaaHlaPen-LTCS-06,
  address = {Germany},
  author = {F. {Baader} and J. {Hladik} and R. {Penaloza}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-06-04},
  title = {{PSPACE} Automata with Blocking for Description Logics},
  type = {LTCS-Report},
  year = {2006},
}