Abstract: The temporal description logic introduces the description abilities of the description logic into the proposition temporal logic．It’s suitable for describing the temporal properties of relevant systems under the semantic Web environment．To verify the temporal properties efficiently,the model checking problem of temporal description logic based on ALC-LTL was investigated in this paper．On the one hand,the temporal description logic ALC-LTL formula was used to express the specification to be checked．On the other hand,the description logic ALC was used to model the system which is investigated．For the resulted model checking problems,a model checking algorithm based on label büchi automation was presented．This algorithm composes of three steps．Firstly,the negation of the specification and the model of the system are constructed as two separate label büchi automation,and then constructing a product automation for the two label büchi automations,and the reasoning mechanisms of ALC is embedded in the process of constructing in this step,finally,detecting the emptiness problem for the product automation．Compared with the model checking of propositional temporal logic LTL,the model checking of ALC-LTL is provided with the representation ability and reasoning mechanisms of description logics,and therefore is suitable for the semantic Web environment．

Key words: Linear temporal description logic,Model checking,Label büchi automation,ALC-type,Product automation,Emptiness problem,Semantic Web