Temporal Description Logics: A Survey <s> Theorem 2 ([38]). Concept satisfiability in LTL ALC with expanding domains is PSPACE-complete without TBoxes and EXPTIME-complete with TBoxes. <s> We consider the complexity of satisfiability and determination of truth in a particular finite structure for different propositional linear temporal logics. We show that both the above problems are NP-complete for the logic with F operator and are PSPACE-complete for the logics with F,X, with U, with U,S,X, and Wolper's extended logic with regular operators [Wo81]. <s> BIB001 </s> Temporal Description Logics: A Survey <s> Theorem 2 ([38]). Concept satisfiability in LTL ALC with expanding domains is PSPACE-complete without TBoxes and EXPTIME-complete with TBoxes. <s> We show that the terminological logic ACC comprising Boolean operations on concepts and value restrictions is a notational variant of the propositional modal logic K(m)- To demonstrate the utility of the correspondence, we give two of its immediate by-products, Namely, we axiomatize ACC and give a simple proof that subsumption in ACC is PSPACE-complete, replacing the original six-page one. ::: ::: Furthermore, we consider an extension of ACC additionally containing both the identity role and the composition, union, transitive-reflexive closure, range restriction, and inverse of roles. It turns out that this language, called TSL, is a notational variant of the propositional dynamic logic converse-PDL. Using this correspondence, we prove that it suffices to consider finite TSL-models, show that TSL-subsumption is decidable, and obtain an axiomatization of TSL By discovering that features correspond to deterministic programs in dynamic logic, we show that adding them to TSC preserves decidability, although violates its finite model property. Additionally, we describe an algorithm for deciding the coherence of inverse-free TSC-concepts with features. Finally, we prove that universal implications can be expressed within TSC. <s> BIB002
Recall that satisfiability in LTL is PSPACE-complete BIB001 and satisfiability in ALC is PSPACE-complete without TBoxes  and EXPTIME-complete with TBoxes BIB002 . Thus, LTL ALC is computationally rather well-behaved: concept satisfiability is not harder than in the component logics. Additionally, the characterization in terms of fusion models opens a way to practical reasoning systems that are not too different from standard ALC reasoners.