Tree automata are often used for satisfiability testing in the area of description logics, which usually yields ExpTime complexity results. We examine conditions under which this result can be improved, and we define two classes of automata, called segmentable and weakly-segmentable, for which emptiness can be decided using space logarithmic in the size of the automaton (and thus polynomial in the size of the input). The usefulness of segmentable automata is demonstrated by reproving the known PSpace result for satisfiability of ALC concepts with respect to acyclic TBoxes
Hladik, J., Peñaloza, R. (2006). PSpace automata for description logics. In Proceedings of the 2006 International Workshop on Description Logics (DL'06) (pp.74-85). CEUR.
PSpace automata for description logics
Peñaloza, R
2006
Abstract
Tree automata are often used for satisfiability testing in the area of description logics, which usually yields ExpTime complexity results. We examine conditions under which this result can be improved, and we define two classes of automata, called segmentable and weakly-segmentable, for which emptiness can be decided using space logarithmic in the size of the automaton (and thus polynomial in the size of the input). The usefulness of segmentable automata is demonstrated by reproving the known PSpace result for satisfiability of ALC concepts with respect to acyclic TBoxesI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.