Automata Can Show {PSPACE} Results for Description Logics

Franz BaaderFranz Baader, Jan HladikJan Hladik, Rafael PeñalozaRafael Peñaloza

Download

Franz Baader, Jan Hladik, Rafael Peñaloza
Automata Can Show {PSPACE} Results for Description Logics
Information and Computation, Special Issue: First International Conference on Language and Automata Theory and Applications ({LATA'07}), 206(9--10):1045--1056, 2008

Details
Bibtex

KurzfassungAbstract
In the area of Description Logic (DL), 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 with
 respect to acyclic terminologies in the DL SI, which extends the basic DL

ALC with transitive and inverse roles.

Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ BaaHlaPen-IC-08,
  author = {Franz {Baader} and Jan {Hladik} and Rafael {Pe{\~n}aloza}},
  journal = {Information and Computation, Special Issue: First International Conference on Language and Automata Theory and Applications ({LATA'07})},
  number = {9--10},
  pages = {1045--1056},
  title = {Automata Can Show {PSPACE} Results for Description Logics},
  volume = {206},
  year = {2008},
}