Abstract
In this paper we demonstrate that two-way alternating automata on infinite trees (2ATAs) provide a very elegant and effective formal tool for addressing reasoning in expressive DLs. Indeed, the encoding of a DL concept (to be checked for satisfiability) into an automaton (to be checked for non-emptiness) is: (i) intuitive, indeed, comparable to tableaux rules; (ii) modular, since each construct is dealt with separately; (iii) short, since the encoding is polynomial; and (iv) computationally adequate, i.e., optimally w.r.t. the complexity class of reasoning. To make these claims concrete, we illustrate the use of 2ATAs to decide satisfiability of three expressive DLs of increasing complexity, namely ALCFI reg, which corresponds to converse-pdl with local functionality, ALCFIb reg , which extends ALCFI reg with boolean combinations of roles, and ALCQIb reg , which further extends ALCFIb reg with qualified number restrictions.