## Full Satisfiability of UML Class Diagrams

**Alessandro Artale, Diego Calvanese, and Angelica
Ibanez-Garcia**
*Proc. of the 29th Int. Conf. on Conceptual Modeling (ER
2010). Volume 6412 of Lecture Notes in Computer Science.*
2010.

UML class diagrams (UCDs) are the de-facto standard formalism
for the analysis and design of information systems. By adopting
formal language techniques to capture constraints expressed by UCDs
one can exploit automated reasoning tools to detect relevant
properties, such as schema and class satisfiability and subsumption
between classes. Among the reasoning tasks of interest, the basic
one is detecting full satisfiability of a diagram, i.e., whether
there exists an instantiation of the diagram where all classes and
associations of the diagram are non-empty and all the constraints
of the diagram are respected. In this paper we establish tight
complexity results for full satisfiability for various fragments of
UML class diagrams. This investigation shows that the full
satisfiability problem is ExpTime-complete in the full scenario,
NP-complete if we drop ISA between relationships, and
NLogSpace-complete if we further drop covering over classes.

@inproceedings{ER-2010,
title = "Full Satisfiability of UML Class Diagrams",
year = "2010",
author = "Alessandro Artale and Diego Calvanese and Angelica
Ibanez-Garcia",
booktitle = "Proc. of the 29th Int. Conf. on Conceptual Modeling
(ER 2010)",
pages = "317--331",
volume = "6412",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
doi = "10.1007/978-3-642-16373-9_23",
}

pdf
url