Abstract:The two most important properties of a logic are its expressive power and the complexity of reasoning, which are also an opposing relation in the logic. Bisimulations between interpretations are effective way to characterize the expressive power, and the van Benthem characterization theorem is a classical result which gives an exact condition for when a first-order formula with one free variable is equivalent to a modal logic formula. This paper provides a simulation for εLU (including atomic concept, top concept, conjunction concept, disjunction concept, and existential quantification). Based on the simulation, the characterization theorems of expressive power for concept descriptions and TBoxes are established to give the sufficient and necessary conditions for when a first-order formula is equivalent to a concept description or a TBox are set up. The above results provide effective supports for the tradeoff between the expressive power and the complexity of reasoning problems.