2ATAs make DLs easy
Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini · 2002
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.