The most relevant work is the approach of Cohn and Gooday [5] which also proposes formal semantics for PJ. In contrast to the current state of our work they already developed formal operational semantics in accordance with the graphical transformation rules of PJ. However, their specifications still rely on full predicate logic and cannot gain from the advantages of our DL approach. As far as we know, they currently do not support mechanical verification processes. We also argue that the DL notation featuring concept and role definitions with inheritance is much more suitable for human and even mechanical inspection.
Citrin et al. [4] also present work on formal semantics of completely visual languages. They developed formal operational semantics for control in the object-oriented language VIPR.
Another approach to reasoning with pictorial concepts is based on a different, type-theoretic framework [12,13]. An important distinction is that our framework is more expressive with respect to concept definitions. For instance, in [12] the authors suggest to extend their type-theoretic approach by notions such as parameterization for construction of generic concepts and type dependency for describing pictures consisting of parts of other pictures. Our DL framework already handles the intended effects of parameterization and type dependency since its reasoning component automatically maintains a taxonomy of subsuming concept definitions which may share common subparts.