We present a translation of (one-way and two-way) alternating automata into description logics, thus reducing the emptiness problem for alternating automata to satisfiability of the target description logic. The latter problem can then be decided using highly optimised, tableau-based description logic reasoners. The translation is a step towards the understanding of the relationship between automataand tableau-based decision procedures for description and modal logics. Moreover, it yields some by-products: (i) a program deciding the emptiness problem for alternating automata and thus the satisfiability problem for logics with automata-based decision procedures; and (ii) tight complexity bounds for the target description logic.
['Jan Hladik', 'Ulrike Sattler']
A translation of looping alternating automata into description logics