Checking Full Satisfiability of Conceptual Models

Proc. of the 23rd Int. Workshop on Description Logics (DL 2010). Volume 573 of CEUR Workshop Proceedings, https://ceur-ws.org/. 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 all classes and associations of the diagram can be simultaneously populated without violating any constraints of the diagram. While the complexity of class satisfiability has been studied extensively, full satisfiability received less attention. In this paper we establish tight upper and lower bounds 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. Thus, full satisfiability has the same computational complexity as class satisfiability.

@inproceedings{DL-2010-uml,
   title = "Checking Full Satisfiability of Conceptual Models",
   year = "2010",
   author = "Alessandro Artale and Diego Calvanese and Angelica
Ibanez-Garcia",
   booktitle = "Proc. of the 23rd Int. Workshop on Description Logics
(DL 2010)",
   pages = "55--66",
   volume = "573",
   publisher = "CEUR-WS.org",
   series = "CEUR Workshop Proceedings, https://ceur-ws.org/",
}