Dynamic Linear Time Temporal Description Logics

In the application of logics to semantic Web services, there are needs for formalizing compounded actions and temporal properties of dynamic domains. In this paper, by adding a dynamic dimension to linear time temporal description logics, we propose a family of dynamic, temporal extensions of description logics. The extended logics contain strengthened until operators, which are indexed with regular programs for describing composition structures of actions. We analyze the syntax, semantics of an ALC-based logic in the family and present a tableau algorithm for it. With the method of quasimodels, we prove the tableau algorithm is correct, complete and terminable. Our logics can be applied in ontology based, dynamic applications as formalisms for reasoning about actions and time.