# PSPACE Automata with Blocking for Description Logics

From International Center for Computational Logic

# PSPACE Automata with Blocking for Description Logics

##### Franz BaaderFranz Baader, J. HladikJ. Hladik, R. PenalozaR. Penaloza

Franz Baader, J. Hladik, R. Penaloza

Technical Report,

**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***Kurzfassung****Abstract**

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},
}
```