# Blocking Automata for PSPACE DLs

From International Center for Computational Logic

# Blocking Automata for PSPACE DLs

##### Franz BaaderFranz Baader, J. HladikJ. Hladik, R. PeñalozaR. Peñaloza

Franz Baader, J. Hladik, R. Peñaloza

In D. Calvanese and E. Franconi and S. Tessaris, eds.,

**Blocking Automata for PSPACE DLs**In D. Calvanese and E. Franconi and S. Tessaris, eds.,

*Proceedings of the 2007 International Workshop on Description Logics*, CEUR-WS, 2007**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 concept satisfiability. 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.**Forschungsgruppe:****Research Group:**Automatentheorie

```
@inproceedings{ BaaHlaPen-DL-07,
author = {F. {Baader} and J. {Hladik} and R. {Pe{\~n}aloza}},
booktitle = {Proceedings of the 2007 International Workshop on Description Logics},
editor = {D. {Calvanese} and E. {Franconi} and S. {Tessaris}},
series = {CEUR-WS},
title = {Blocking Automata for {PSPACE} {DLs}},
year = {2007},
}
```