About partiality in institutions (co-)morphisms

FABIO GADDUCCI; AGUSTÍN E. MARTINEZ SUÑÉ; MAIBAUM, THOMAS S. E.; LOPEZ POMBO, CARLOS GUSTAVO

Gregynog

Workshop; Worshop on Algebraic Development Techniques; 2016

Swansea University

The nature of modern software is intrinsically heterogeneous. Such heterogene- ity is derived from the diversity of properties and characteristics that software sys- tems have, which is in turn witnessed by the diversity of specification formalisms and languages that are used to describe them. Institutions [1] was introduced as a formalisation of the abstract model-theory of logical formalisms and was proved adequate for taming such variety. The possibility to relate institutions via suitable mappings [2,3], which can e.g. interpreted as semantics-preserving translations, allowed to consider diagrams of institutions as heterogeneous logical environments [4] and to use them as formal foundations for tools like HETS [5].Following the original definitions of such connections between logical languages, those mappings between signatures, sentences and models are forced to be total. However, it is well-known that many logics relate in a partial way. Among others, the relation between CTL [6] and LTL [7] is a classical example of logics that share an equipollent proper fragment, while there is no total semantics-preserving mapping in either direction.