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

Baader, F., Hladik, J., Peñaloza, R. (2007). Blocking automata for PSpace DLs. In Proceedings of the 2007 International Workshop on Description Logics (DL'07) (pp.17-28). CEUR.

Blocking automata for PSpace DLs

Peñaloza, R
2007

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
Si
paper
automata, reasoning, description logics
English
International Workshop on Description Logics, DL 2007 8 - 10 June
Baader, F., Hladik, J., Peñaloza, R. (2007). Blocking automata for PSpace DLs. In Proceedings of the 2007 International Workshop on Description Logics (DL'07) (pp.17-28). CEUR.
Baader, F; Hladik, J; Peñaloza, R
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/234230
Citazioni
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
Social impact