Decidability and Complexity of ALCOIF with Transitive Closure (and More)

We prove that satisfiability and finite satisfiability in the description logic ALCOIFreg are NExpTime-complete when every regular role expression of the form α∗ contains either no functional role or only a single role name (and possibly its inverse). Notably, this encompasses the extension of ALCOIF with transitive closure of roles and the modal logic of linear orders and successor, with converse.