Reasoning on temporal class diagrams: Undecidability results

This paper introduces a temporal class diagram language useful to model temporal varying data. The atemporal portion of the language contains the core constructors available in both EER diagrams and UML class diagrams. The temporal part of the language is able to distinguish between temporal and atemporal constructs, and it has the ability to represent dynamic constraints between classes. The language is characterized by a model-theoretic (temporal) semantics. Reasoning services as logical implication and satisfiability are also defined. We show that reasoning on finite models is different from reasoning on unrestricted ones. Then, we prove that reasoning on temporal class diagrams is an undecidable problem on both unrestricted models and on finite ones.