# Asymmetric Combination of Logics is Functorial: A Survey

Renato Neves, Alexandre Madeira, Luis S. Barbosa, Manuel A. Martins

► To cite this version:

Renato Neves, Alexandre Madeira, Luis S. Barbosa, Manuel A. Martins. Asymmetric Combination of Logics is Functorial: A Survey. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2016, Gregynog, United Kingdom. pp.39-55, 10.1007/978-3-319-72044-9_4. hal-01767465

HAL Id: hal-01767465

https://inria.hal.science/hal-01767465

Submitted on 16 Apr 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Asymmetric Combination of Logics is Factorial:
A Survey

Renato Neves¹, Alexandre Madeira¹, Luis S. Barbosa¹, and Manuel A. Martins²

¹ INESC TEC (HASLab) & Universidade do Minho, Portugal
nevrenato@di.uminho.pt, amadeira@inesctec.pt, lsb@di.uminho.pt

² CIDMA – Dep. of Mathematics, Universidade de Aveiro, Portugal
martins@ua.pt

**Keywords:** institution · hybridisation · probabilisation · temporalisation · asymmetric combination

**Abstract.** Asymmetric combination of logics is a formal process that develops the characteristic features of a specific logic on top of another one. Typical examples include the development of temporal, hybrid, and probabilistic dimensions over a given base logic. These examples are surveyed in the paper under a particular perspective — that this sort of combination of logics possesses a factorial nature. Such a view gives rise to several interesting questions. They range from the problem of combining translations (between logics), to that of ensuring property preservation along the process, and the way different asymmetric combinations can be related through appropriate natural transformations.

# 1 Introduction

## 1.1 Motivation and Context

It is well known that software's inherent high complexity renders formal design and analysis a difficult challenge, still largely unmet by the current engineering practices. Often, in fact, the formal specification of a non trivial software system calls for multiple logics so that specific types of requirements and design issues can be captured: if properties of data structures are typically encoded in an equational framework, behavioural issues will call for some sort of modal or temporal logic, whereas probabilistic reasoning will be required in order to predict or analyse faulty behaviour in distributed systems.

This fact explains the growing interest in the systematic combination of logics, an area whose overall aim can be summed up in a simple methodological principle: *identify the different natures of the requirements to be formalised, and combine whatever logics are suitable to handle them into a single logic for the whole system*. Its potential was already stressed in the eighties by J. Goguen and J. Meseguer, and the whole programme started to gain prominence in the following decade (cf. [3, 18]).
The current paper surveys a specific type of combination of logics, called *asymmetric*, in which the characteristic features of a logic are developed on top of another one. Probably the most famous example is the process of *temporalisation* [12], in which the features of a temporal logic are added to another logic; the latter is often referred to as the *base logic* in order to distinguish the original machinery from the one added along the process. In brief, temporalisation adds a temporal dimension to the models of a given logic and syntactical machinery to suitably handle this added dimension. The *hybridisation* [20] and *probabilisation* [2] processes are more recent examples. The former develops a *hybrid logic* [1] on top of the base one whereas the latter adds probabilistic features. Other examples include *quantisation* [4] and *modalisation* [11], bringing into the picture features of quantum and modal logic, respectively.

Is there a common characterisation of these different combinations, able to
provide a suitable setting to discuss their properties at a generic level? Such is
the question addressed in this paper through the identification of their common
functorial nature. This perspective structures the whole survey presented here.

Our approach is based on the theory of *institutions* [17], an abstract char-
acterisation of logical systems that encompasses syntax, semantics, and satis-
faction. Put forward by J. Goguen and R. Burstall in the late seventies, its
original aim was to develop as much Computing Science as possible in a general,
uniform way, independently of any particular logical system, in response to the
“population explosion among the logical systems used in Computing Science” [17].
Since then this goal has been achieved to an extent even greater than originally
thought. Indeed, institutions underlie the foundations of algebraic specification
methods, and are most useful in handling and combining different sorts of log-
ical systems. The universal character and resilience of institutions is witnessed
by the wide set of logics formalised and subsequently explored within the frame-
work. Examples go from standard classical logics, to more unconventional ones,
typically capturing modern specification and programming paradigms — exam-
bles include *process algebras* [23], *temporal logics* [8], the ALLOY language [25],
*coalgebraic logics* [9], functional and imperative languages [30], among many
others.

## 1.2 Contributions and Roadmap

Institutions are objects of a well known category **I** whose arrows are the so-
called *institution comorphisms* (cf. [21, 30]). In this setting we argue that an
asymmetric combination of logics can, very often, be seen as an *endofunctor*
over **I**. Three examples (*temporalisation*, *hybridisation*, and *probabilisation*) are
discussed in detail, with their definitions (slightly) reworked to fit in the general
picture. Such a functorial perspective has several advantages: an interesting one
is the possibility to lift the combination process from logics to their translations,
which allows for the characterisation of natural transformations between asym-
metric combinations. Another interesting possibility is the study of adjoints, and
preservation of properties such as conservativity, equivalence, and (co)limits.
We initiate this survey with a brief overview of common approaches to com-
bination of logics, in Section 2. From there on, the focus is placed on asymmetric
combinations and the characterisation of their functorial nature.

Thus, in Section 3 we recall the category of institutions I and revisit the three combinations of logics discussed in the paper. Then, in Section 4, these examples are made functorial. For the sake of simplicity and conciseness, we define an institutional notion of asymmetric combination and make, to a large extent, the necessary proofs at this level of abstraction. We stress, however, that the paper’s main objective is not to introduce such a notion, but rather to survey the functorial nature of a number of asymmetric combinations and to show that the functorial perspective paves the way to several interesting mechanisms and research lines.

In the same section we study property preservation by these three (new) func-
tors in what concerns conservativity (an important property in the validation of
specifications) and the equivalence of institutions. We also discuss natural trans-
formations between asymmetric combinations. Finally, in Section 5, we conclude
and suggest future lines of research.

This paper assumes a basic knowledge of Category Theory. Whenever found
suitable, we will omit subscripts in natural transformations and denote the un-
derlying class of objects of a category C by |C| or just C. All proofs of the
paper's results are detailed in [24].

## 2 Combination of logics: A brief overview

The entry on *Combining Logics* in the *Stanford Encyclopedia of Philosophy* [7] stresses the role of Computing Science applications as a main driving force for research in obtaining new logical systems from old, integrating features and preserving properties to a reasonable extent: *“One of the main areas interested in the methods for combining logics is software specification. Certain techniques for combining logics were developed almost exclusively with the aim of applying them to this area.”* The aforementioned hybridisation and temporalisation methods, for example, were originally developed with concrete applications to Computing Science in mind, but interestingly they can be more broadly understood as a specific way of combining logics at a model theoretical level.

As already mentioned, an asymmetric combination of logics develops specific
features of a logic ‘on top’ of another one. This sort of combination was gen-
eralised by C. Caleiro, A. Sernadas and C. Sernadas in [6], in a method called
parameterisation. In brief, a logic is parametrised by another one if the atomic
part of the former is replaced by the latter: thus, the method distinguishes a
parameter to fill (the atomic part), a parametrised logic (the ‘top’ logic) and a
parameter logic (the logic inserted within). More recently, J. Rasga et al. [29]
proposed a method for importing logics by exploiting a graph-theoretic approach.

From a wider perspective, combination of logics is increasingly recognised
as a relevant research domain, driven not only by philosophical enquiry on the
nature of logics or strict mathematical questions, but also from applications in
Computing Science and Artificial Intelligence. The first methods appeared in the context of modal logics. This includes *fusion* of the underlying languages [33], pioneered by M. Fitting in a 1969 paper combining alethic and deontic modalities [13], and *product of logics* [31]. Both approaches can be characterised as *symmetric*. Product of logics, for example, amounts to pairing the Kripke semantics, i.e. the accessibility relations, of both logics. With a wider scope of application, i.e. beyond modal logics, *fibring* [14] was originally proposed by D. Gabbay, and contains fusion as a particular case. From a syntactic point of view the language of the resulting logic is freely generated from the signatures of the combined logics, symbols from both of them appearing intertwined in an arbitrary way.

Reference [5] offers an excellent roadmap for the several variants of fibring in the literature. A particularly relevant evolution was the work of A. Sernadas and his collaborators resorting to universal constructions from category theory to characterise different patterns of connective sharing, as documented in [32]. In the simplest case, where no constraint is imposed by sharing, fibring is the least extension of both logics over the coproduct of their signatures, which basically amounts to a coproduct of logics. This approach, usually referred to as *algebraic fibring*, makes heavy use of categorial constructions as a source of genericity to provide more general and wide applicable methods.

# 3 Asymmetric combination of logics (institutionally)

## 3.1 Institutions

Let us recall the core notions of the theory of institutions and revisit the three working examples of combinations.

**Definition 1.** An institution $\mathcal{J}$ is a tuple $(\mathrm{Sign}^{\mathcal{J}}, \mathrm{Sen}^{\mathcal{J}}, \mathrm{Mod}^{\mathcal{J}}, (\models_{\Sigma}^{\mathcal{J}})_{\Sigma \in |\mathrm{Sign}^{\mathcal{J}}|})$ where

- $\mathrm{Sign}^{\mathcal{J}}$ is a category whose objects are signatures and arrows signature morphisms.

- $\mathrm{Sen}^{\mathcal{J}} : \mathrm{Sign}^{\mathcal{J}} \to \mathbf{Set}$, is a functor that for each signature $\Sigma \in |\mathrm{Sign}^{\mathcal{J}}|$ returns a set of $\Sigma$-sentences,

- $\mathrm{Mod}^{\mathcal{J}} : (\mathrm{Sign}^{\mathcal{J}})^{op} \to \mathbf{Cat}$, is a functor that for each signature $\Sigma \in |\mathrm{Sign}^{\mathcal{J}}|$ returns a category whose objects are $\Sigma$-models and the arrows are $\Sigma$-model homomorphisms.

- $\models_{\Sigma}^{\mathcal{J}} \subseteq |\mathrm{Mod}^{\mathcal{J}}(\Sigma)| \times \mathrm{Sen}^{\mathcal{J}}(\Sigma)$, is a satisfaction relation such that for each signature morphism $\varphi : \Sigma \to \Sigma'$ the following property holds

$$ \mathrm{Mod}^{\mathcal{J}}(\varphi)(M) \models_{\Sigma}^{\mathcal{J}} \rho \text{ iff } M \models_{\Sigma', \mathrm{Sen}^{\mathcal{J}}(\varphi)}^{\mathcal{J}} \rho $$
for any $M \in |\mathbf{Mod}^J(\Sigma')|$, $\rho \in \mathbf{Sen}^J(\Sigma)$. Diagrammatically,

<figure><img src="image_2.png" /></figure>

If the tuple does not necessarily respect the satisfaction condition above then we
call it a pre-institution.

**Notation 1.** In the sequel we will refer to $\mathbf{Mod}^J(\varphi)(M)$ as the $\varphi$-reduct of $M$
and denote it by $M \upharpoonright_\varphi$. When clear from the context, both the subscript and
superscript in the satisfaction relation will be dropped.

**Definition 2.** Consider two institutions $\mathcal{J}, \mathcal{J}'$. A comorphism $(\Phi, \alpha, \beta) : \mathcal{J} \to \mathcal{J}'$ is a triple such that

- $\Phi: \mathrm{Sign}^J \to \mathrm{Sign}^{J'}$ is a functor,

- $\alpha: \mathrm{Sen}^J \to \mathrm{Sen}^{J'} \cdot \Phi$ is a natural transformation,

- $\beta: \mathbf{Mod}^J \cdot \Phi^{op} \to \mathbf{Mod}^J$ is a natural transformation $^3$,

- and for any $\Sigma \in |\mathrm{Sign}^J|$, $M \in |\mathbf{Mod}^{J'} \cdot \Phi^{op}(\Sigma)|$ and $\rho \in \mathbf{Sen}^J(\Sigma)$

$$
\beta_{\Sigma}(M) \models_{\Sigma}^{J} \rho \quad \text{iff} \quad M \models_{\Phi(\Sigma)}^{J'} \alpha_{\Sigma}(\rho)
$$

Diagrammatically, for each $\Sigma \in |\mathrm{Sign}^J|$

<figure><img src="image_3.png" /></figure>

**Definition 3.** Let us consider two comorphisms $(\Phi_1, \alpha_1, \beta_1) : \mathcal{J} \to \mathcal{J}'$, and $(\Phi_2, \alpha_2, \beta_2) : \mathcal{J}' \to \mathcal{J}''$. Their composition $(\Phi_2, \alpha_2, \beta_2) ; (\Phi_1, \alpha_1, \beta_1) : \mathcal{J} \to \mathcal{J}''$ is defined as $(\Phi_2, \alpha_2, \beta_2) ; (\Phi_1, \alpha_1, \beta_1) \triangleq (\Phi_2 \cdot \Phi_1, (\alpha_2 \circ 1_{\Phi_1}) \cdot \alpha_1, \beta_1 \cdot (\beta_2 \circ 1_{\Phi_1^{op}}))$ where the white circle denotes the Godement (horizontal) composition of natural transformations. Thus,

$$
\Phi_2 \cdot \Phi_1 : \mathrm{Sign}^J \to \mathrm{Sign}^{J''},
$$

$$
(\alpha_2 \circ 1_{\Phi_1}) \cdot \alpha_1 : \mathrm{Sen}^J \to \mathrm{Sen}^{J''} \cdot \Phi_2 \cdot \Phi_1,
$$

$$
\beta_1 \cdot (\beta_2 \circ 1_{\Phi_1^{op}}) : \mathbf{Mod}^{J''} \cdot \Phi_2^{op} \cdot \Phi_1^{op} \to \mathbf{Mod}^J.
$$

Each institution $\mathcal{J}$ has as the identity comorphism the triple $(1_{\mathcal{Sign}^J}, 1_{\mathcal{Sen}^J}, 1_{\mathcal{Mod}^J})$.

As mentioned in the Introduction, institutions and respective comorphisms
form a category **I**.

<footnote>$^3$ ($\_\cdot$)$^{op}$ applied to a functor $F : \mathbf{C} \to \mathbf{D}$ induces a functor $F^{op} : \mathbf{C}^{op} \to \mathbf{D}^{op}$ such that
for any object or arrow $a$ in $\mathbf{C}$, $F^{op}(a) = F(a)$.</footnote>
## 3.2 An institutional rendering of asymmetric combinations of logics

Consider the following abstract characterisation of what is an asymmetric combination of logics. Start with arbitrary categories $Sign_1$, $Sign_2$, and two functors

$$M^e : (Sign_1)^{op} \to \mathbf{Cat}, M^j : (Sign_2)^{op} \to \mathbf{Cat}.$$

Assume that, for each $\Delta \in |Sign_1|$, there is a functor $U_{(M^e, \Delta)} : M^e(\Delta) \to \mathbf{Set}$. Whenever no ambiguities arise, we will drop the subscript of $U_{(M^e, \Delta)}$. Let us further assume that given a morphism $\varphi : \Delta \to \Delta'$ of $Sign_1$, the induced functor $M^e(\varphi)$ makes the following diagram commute.

<figure><img src="image_4.png" /></figure>

This leads to a functor $M^e(M^j) : (Sign_1 \times Sign_2)^{op} \to \mathbf{Cat}$ such that given a pair $(\Delta, \Sigma) \in Sign_1 \times Sign_2$, $M^e(M^j)(\Delta, \Sigma)$ forms a discrete category whose objects are triples $(S, R, m)$ where $R \in M^e(\Delta)$, $U(R) = S$, and $m : S \to M^j(\Sigma)$. Moreover, given a signature morphism $\varphi_1 \times \varphi_2 : (\Sigma, \Delta) \to (\Sigma', \Delta')$ we have $M^e(M^j)(\varphi_1 \times \varphi_2)(S, R, m) \triangleq (S, M^e(\varphi_1)(R), M^j(\varphi_2) \cdot m)$.

**Definition 4.** An asymmetric combination $\mathcal{C}$ is a tuple $(Sign^e, Sen^e, M^e, \models^e)$ such that

- $Sign^e$ is a category of signatures.

- $Sen^e$ is a family of functions

$$Sen_{Sign}^{\mathcal{C}} : (Sign \to \mathbf{Set}) \to (Sign^{\mathcal{C}} \times Sign \to \mathbf{Set})$$

indexed by the categories $Sign$ in $\mathbf{Cat}$.

- $M^e$ is a functor $M^e : (Sign^e)^{op} \to \mathbf{Cat}$ as assumed above.

- Given functors $M^j : Sign^{op} \to \mathbf{Cat}$, $Sen^j : Sign \to \mathbf{Set}$, $\models^e$ is a family of relation liftings ($\models^{\mathcal{C}}(\Delta, \Sigma)(\Delta, \Sigma) \in Sen^e \times Sen^e$)

$$\models^{\mathcal{C}}(\Delta, \Sigma) : |M^j(\Sigma)| \times Sen^j(\Sigma) \to |M^e(M^j)(\Delta, \Sigma)| \times Sen^e(Sen^j)(\Delta, \Sigma)$$

Given an institution $\mathcal{J}$, a pre-institution $\mathcal{C}\mathcal{J}$, corresponding to a specific combination, is obtained as follows.

- $Sign^{\mathcal{C}\mathcal{J}} \triangleq Sign^e \times Sen^j$.

- $Sen^{\mathcal{C}\mathcal{J}} \triangleq Sen^e(Sen^j)$. We will assume that the sentences given by $Sen^{\mathcal{C}\mathcal{J}}$ are inductively defined (i.e. are generated by a grammar) so that we can define recursive maps on them. Intuitively, their atoms include the sentences of the base logic.

- $Mod^{\mathcal{C}\mathcal{J}} \triangleq M^e(M^j)$.

- Given a signature $(\Delta, \Sigma) \in |Sign^{\mathcal{C}\mathcal{J}}|$, $\models^{\mathcal{C}\mathcal{J}}(\Delta, \Sigma) \triangleq \models^{\mathcal{C}}(\Delta, \Sigma) (\models^{\mathcal{J}}(\Sigma))$.
**Temporalisation.** We are now ready to recast the three aforementioned combinations of logics in the institutional setting. We start with temporalisation since it is the simplest of the three.

**Definition 5.** Given an institution $\mathcal{J}$ the temporalisation process returns a pre-institution $\mathcal{L}\mathcal{J} = (\mathrm{Sign}^{\mathcal{L}\mathcal{J}}, \mathrm{Sen}^{\mathcal{L}\mathcal{J}}, \mathrm{Mod}^{\mathcal{L}\mathcal{J}}, \models^{\mathcal{L}\mathcal{J}})$ defined as

- **SIGNATURES.** $\mathrm{Sign}^{\mathcal{L}\mathcal{J}} \triangleq \mathrm{Sign}^{\mathcal{L}} \times \mathrm{Sign}^{\mathcal{J}}$, where $\mathrm{Sign}^{\mathcal{L}}$ is the one object category 1. Since $\mathrm{Sign}^{\mathcal{L}\mathcal{J}} \cong \mathrm{Sign}^{\mathcal{J}}$, no distinction will be made, unless stated otherwise, between the two signature categories.

- **SENTENCES.** Given a signature $\Sigma \in |\mathrm{Sign}^{\mathcal{L}\mathcal{J}}|$, $\mathrm{Sen}^{\mathcal{L}\mathcal{J}}(\Sigma)$ is the smallest set generated by grammar

$$ \rho \supset \psi | \neg \rho | \rho \wedge \rho | X\rho | \rho U\rho $$

where $\psi \in \mathrm{Sen}^{\mathcal{J}}(\Sigma)$. For a signature morphism $\varphi : \Sigma \to \Sigma'$, $\mathrm{Sen}^{\mathcal{L}\mathcal{J}}(\varphi)$ is a function that, provided a sentence $\rho \in \mathrm{Sen}^{\mathcal{L}\mathcal{J}}(\Sigma)$, replaces the base sentences $\psi$ (i.e. elements of $\mathrm{Sen}^{\mathcal{J}}(\Sigma)$) occurring in $\rho$ by $\mathrm{Sen}^{\mathcal{J}}(\varphi)(\psi)$; in symbols $\mathrm{Sen}^{\mathcal{L}\mathcal{J}}(\varphi)(\rho) = \rho[\psi \in \mathrm{Sen}^{\mathcal{J}}(\Sigma) / \mathrm{Sen}^{\mathcal{J}}(\varphi)(\psi)]$ (recall that sentences are assumed to be inductively defined).

- **MODELS.** Given the object $\star \in |1|$, $M^{\mathcal{L}}(\star)$ is the category whose (unique) element is the pair $(\mathbb{N}, \mathrm{suc} : \mathbb{N} \to \mathbb{N})$ ($\mathbb{N}$ denotes the set of natural numbers) and $U (\mathbb{N}, \mathrm{suc} : \mathbb{N} \to \mathbb{N})$ is $\mathbb{N}$. Hence, the elements of category $\mathrm{Mod}^{\mathcal{L}\mathcal{J}}(\Sigma)$ are triples $(\mathbb{N}, \mathrm{suc} : \mathbb{N} \to \mathbb{N}, m)$ (often denoted by letter $M$) where $m : \mathbb{N} \to |\mathrm{Mod}^{\mathcal{L}\mathcal{J}}(\Sigma)|$. We will often denote $m(n)$ by $M_n$.

- **SATISFACTION.** Given a signature $\Sigma \in |\mathrm{Sign}^{\mathcal{L}\mathcal{J}}|$, $M \in |\mathrm{Mod}^{\mathcal{L}\mathcal{J}}(\Sigma)|$, $\rho \in \mathrm{Sen}^{\mathcal{L}\mathcal{J}}(\Sigma)$, $M \models \rho$ iff $M \models^0 \rho$ where

$$ M \models^j \psi \quad \text{iff} \quad M_j \models \psi \text{ for } \psi \in \mathrm{Sen}^{\mathcal{J}}(\Sigma) $$

$$ M \models^j \rho \wedge \rho' \quad \text{iff} \quad M \models^j \rho \text{ and } M \models^j \rho' $$

$$ M \models^j \neg \rho \quad \text{iff} \quad M \models^j \rho $$

$$ M \models^j X\rho \quad \text{iff} \quad M \models^{j+1} \rho $$

$$ M \models^j \rho U \rho' \quad \text{iff for some } k \ge j, M \models^k \rho' \text{ and for all } j \le i < k, M \models^i \rho $$

Note that temporalised propositional logic coincides with the classic linear temporal logic (cf. [12]).

**Theorem 1.** Temporalised $\mathcal{J}$ (i.e. $\mathcal{L}\mathcal{J}$) is an institution.

In the sequel we show that the other two asymmetric combinations enjoy the same property, which is essential for their characterisation as endofunctors. Of course, this also entails the possibility of combining a logic an arbitrary number of times, using any of these three processes.

**Probabilisation.** In order to handle probabilistic systems (e.g. Markov chains) probabilisation [2] adds a probabilistic dimension to logics. In institutional terms,

**Definition 6.** Consider an arbitrary institution $\mathcal{J}$. Its probabilised version $\mathcal{P}\mathcal{J} = (\mathrm{Sign}^{\mathcal{P}\mathcal{J}}, \mathrm{Sen}^{\mathcal{P}\mathcal{J}}, \mathrm{Mod}^{\mathcal{P}\mathcal{J}}, \models^{\mathcal{P}\mathcal{J}})$ is defined as follows
- SIGNATURES. $\mathbf{Sign}^{\mathcal{P}^J} \triangleq \mathbf{Sign}^{\mathcal{P}} \times \mathbf{Sign}^J$, where $\mathbf{Sign}^{\mathcal{P}}$ is the one object category 1. Since $\mathbf{Sign}^{\mathcal{P}^J} \cong \mathbf{Sign}^J$, no distinction will be made, unless stated otherwise, between the two signature categories.

- SENTENCES. For a signature $\Sigma \in |\mathbf{Sign}^{\mathcal{P}^J}|$, $\mathbf{Sen}^{\mathcal{P}^J}(\Sigma)$ is the smallest set generated by grammar

$$ \rho \ni t < t | \neg \rho | \rho \wedge \rho $$

for $t \in \mathbf{T}(\Sigma)$ ($\mathbf{T} : \mathbf{Sign}^{\mathcal{P}^J} \to \mathbf{Set}$). $\mathbf{T}(\Sigma)$ is generated by grammar

$$ t \ni r | \int \psi | t + t | t . t $$

where $r \in \mathbb{R}$ is a real number, and $\psi \in \mathbf{Sen}^J(\Sigma)$. Also, we have

$$ \mathbf{Sen}^{\mathcal{P}^J}(\varphi)(\rho) \triangleq \rho[t \in \mathbf{T}(\Sigma) / \mathbf{T}(\varphi)(t)], \text{ where} \\ \mathbf{T}(\varphi)(t) \triangleq t[\psi \in \mathbf{Sen}^J(\Sigma) / \mathbf{Sen}^J(\varphi)(\psi)] $$

- MODELS. $\mathbf{Mod}^{\mathcal{P}}(\star)$ is the discrete category whose elements are probability spaces $(S, \mathcal{P} : 2^S \to [0,1])$. **Functor U** returns the carrier set. Hence, models in $\mathbf{Mod}^{\mathcal{P}^J}(\Sigma)$ are triples $(S, \mathcal{P}, m)$ where $m : S \to \mathbf{Mod}^J(\Sigma)$. For each sentence $\psi \in \mathbf{Sen}^J(\Sigma)$ we set $m^{-1}[\psi] \triangleq \{s \in S : m(s) \models \psi\}$.

- SATISFACTION. Finally, given a signature $\Sigma \in |\mathbf{Sign}^{\mathcal{P}^J}|$, a model $M \in |\mathbf{Mod}^{\mathcal{P}^J}(\Sigma)|$, and $\rho \in \mathbf{Sen}^{\mathcal{P}^J}(\Sigma)$, define

$$ \begin{align*} M_r &= r \\ M(\int_{\psi}) &= p(m^{-1}[\psi]) & M &\models t < t' \text{ iff } M_t < M_{t'} \\ M(t+t') &= M_t + M_{t'} & M &\models \neg \rho \text{ iff } M \not\models \rho \\ M(t.t') &= M_t . M_{t'} & M &\models \rho \wedge \rho' \text{ iff } M \models \rho \text{ and } M \models \rho' \end{align*} $$

**Theorem 2.** Probabilised $\mathcal{J}$ (i.e. $\mathcal{P}\mathcal{J}$) is an institution.

**Example 1.** PROBABILISED PROPOSITIONAL LOGIC ($\mathcal{PPL}$). The probabilisation of propositional logic is the following logic:

- SIGNATURES. Signatures are sets of propositional symbols $P$.

- SENTENCES. Sentences are generated by grammar $\rho \ni t < t | \neg \rho | \rho \wedge \rho$ where $t$ is a term generated by grammar $t \ni r | \int \psi | t + t | t . t$ for $r \in \mathbb{R}$ and $\psi$ a propositional sentence.

- MODELS. Models are probability spaces equipped with a function whose domain is the set of outcomes and the codomain the universe of propositional models.

Intuitively, $\mathcal{PPL}$ offers a probabilistic 'flavour' to propositions. For instance, one may say that the probability of $p$ holding is less than probability of $q$ holding, $\int p < \int q$. Other examples of probabilised logics are discussed in [2].
**Hybridisation.** Hybridisation [20] (and its variations e.g. [15]) provides the foundations for handling different kinds of reconfigurable systems (i.e. computational systems that change their execution modes throughout their lifetime) in a systematic manner: in brief, the hybrid machinery relates and pinpoints the different execution modes while the base logic specifies the properties that are supposed to hold in each particular mode.

Since hybridisation was originally defined in institutional terms we will just recall here its definition but without nominal quantification, which yields an asymmetric fragment of the process. Such a fragment is adopted in [20] to define parametrised translations from hybridised institutions into first-order logic — the authors of [10] extended this work to accommodate nominal quantification as well. The same fragment is the one adopted in [19] to provide a general characterisation of equivalence and refinement for hybridised logics.

**Definition 7.** Given an institution $\mathcal{I}$, $\mathcal{HJ} = (\text{Sign}^{\mathcal{HJ}}, \text{Sen}^{\mathcal{HJ}}, \text{Mod}^{\mathcal{HJ}}, \models^{\mathcal{HJ}})$ is defined as

- **SIGNATURES.** $\text{Sign}^{\mathcal{HJ}} \triangleq \text{Sign}^{\mathcal{H}} \times \text{Sign}^{\mathcal{J}}$, where $\text{Sign}^{\mathcal{H}}$ is the category **Set** $\times$ **Set** whose objects are pairs of sets $(\text{Nom}, \Lambda)$. $\text{Nom}$ denotes a set of nominal symbols, and $\Lambda$ a set of modality symbols.

- **SENTENCES.** For a signature $(\Delta, \Sigma) \in |\text{Sign}^{\mathcal{HJ}}|$ (with $\Delta = (\text{Nom}, \Lambda)$), $\text{Sen}^{\mathcal{HJ}}(\Delta, \Sigma)$ is the smallest set generated by grammar

$$ \rho \ni i | \psi | \neg \rho | \rho \wedge \rho | \text{@}_i \rho | \langle \lambda \rangle \rho $$

where $i \in \text{Nom}$, $\psi \in \text{Sen}^{\mathcal{J}}(\Sigma)$, $\lambda \in \Lambda$. For a signature morphism $\varphi_1 \times \varphi_2 : (\Delta, \Sigma) \to (\Delta', \Sigma')$, nominals, modalities, and base sentences of $\rho \in \text{Sen}^{\mathcal{HJ}}(\Delta, \Sigma)$ are replaced according to $\varphi_1 \times \varphi_2$ by $\text{Sen}^{\mathcal{HJ}}(\varphi_1 \times \varphi_2)$.

- **MODELS.** Given a signature $\Delta \in |\text{Sign}^{\mathcal{H}}|$, $M^{\mathcal{H}}(\Delta)$ is the discrete category whose elements are triples $(S, (R_i)_{i \in \text{Nom}}, (R_\lambda)_{\lambda \in \Lambda})$ such that $R_i \in S$, and $R_\lambda \subseteq S \times S$. **Functor U** forgets the last two elements, keeping just the carrier set. For any signature morphism $(\varphi_1, \varphi_2) : (\text{Nom}, \Lambda) \to (\text{Nom}', \Lambda')$, we have $M^{\mathcal{H}}(\varphi_1, \varphi_2)(S, (R'_i)_{i \in \text{Nom}'}, (R'_\lambda)_{\lambda \in \Lambda'}) \triangleq (S, (R_i)_{i \in \text{Nom}}, (R_\lambda)_{\lambda \in \Lambda})$, where

$$ R_i = R'_{\varphi_1(i)} \text{ and } R_\lambda = R'_{\varphi_2(\lambda)} $$

- **SATISFACTION.** Given $(\Delta, \Sigma) \in |\text{Sign}^{\mathcal{HJ}}|$, a model $M \in |\text{Mod}^{\mathcal{HJ}}(\Delta, \Sigma)|$ and a sentence $\rho \in \text{Sen}^{\mathcal{HJ}}(\Sigma)$, the satisfaction relation is defined as

$$ M \models \rho \text{ iff } M \models^w \rho \text{ for all } w \in S $$

where

$M \models^w i$ iff $R_i = w$ for $i \in \text{Nom}$

$M \models^w \psi$ iff $m(w) \models \psi$ for $\psi \in \text{Sen}^{\mathcal{J}}(\Sigma)$

$M \models^w \neg \rho$ iff $M \models^w \rho$

$M \models^w \rho \wedge \rho'$ iff $M \models^w \rho$ and $M \models^w \rho'$

$M \models^w \text{@}_i \rho$ iff $M \models^{R_i} \rho$

$M \models^w \langle \lambda \rangle \rho$ iff there is some $w' \in W$ such that $(w, w') \in R_\lambda$ and $M \models^{w'} \rho$
The proof that, for any institution $\mathcal{I}$, hybridisation yields another institution is given in reference [20].

**Example 2.** HYBRIDISED PROPOSITIONAL LOGIC (HPL). *Hybridisation of propositional logic returns the following logic.*

- SIGNATURES. *Signatures are triples (Nom, Λ, P) where Nom is a set of nominal symbols, Λ a set of modality symbols, and P a set of propositional symbols.*

- SENTENCES. *Sentences are generated by grammar*

$$ \rho \ni i | \psi | \neg \rho | \rho \wedge \rho | \mathring{@}_i \rho | \langle \lambda \rangle \rho $$

where *i* is a nominal, *λ* is a modality, and *ψ* a propositional sentence. Note that we have two levels of Boolean connectives: the ones from propositional logic, and the ones introduced by hybridisation. One can, however, ‘collapse’ them since they semantically coincide.

- MODELS. *Models are triples (W, R, m) such that W defines the set of worlds, R describes the transitions between worlds and names states. Moreover each world w ∈ W points to a propositional model m(w).*

# 4 Asymmetric combinations of logics as functors

## 4.1 Lifting comorphisms

In the previous section three combinations of logics were revisited under the light of the theory of institutions. We intend now to discuss them as translations between logics. We will do this at the level of the abstract definition of a combination of logics given above, leading thus to more powerful results, applicable not only to the three combinations discussed, but also to any other fitting the characterisation.

Formally, given a comorphism $(\Phi, \alpha, \beta) : \mathcal{I} \to \mathcal{I}'$ a combination process maps $(\Phi, \alpha, \beta)$ into $\mathcal{C}(\Phi, \alpha, \beta) : \mathcal{C}\mathcal{I} \to \mathcal{C}\mathcal{I}'$. The strategy for such a lifting is simple: when transforming signatures, sentences or models, we keep the top level structure and change the bottom level according to the base comorphism. Thus,

**Definition 8.** A comorphism $(\Phi, \alpha, \beta) : \mathcal{I} \to \mathcal{I}'$ is lifted to a mapping $(\mathcal{C}\Phi, \mathcal{C}\alpha, \mathcal{C}\beta) : \mathcal{C}\mathcal{I} \to \mathcal{C}\mathcal{I}'$ as follows:

- SIGNATURES. $\mathcal{C}\Phi : \mathrm{Sign}^{\mathcal{C}\mathcal{I}} \to \mathrm{Sign}^{\mathcal{C}\mathcal{I}'},$

$$ \mathcal{C}\Phi \triangleq 1_{\mathrm{Sign}^e} \times \Phi. $$

- SENTENCES. $\mathcal{C}\alpha : \mathrm{Sen}^{\mathcal{C}\mathcal{I}} \to \mathrm{Sen}^{\mathcal{C}\mathcal{I}'} \cdot \mathcal{C}\Phi,$

$$ (\mathcal{C}\alpha)_{(\Delta, \Sigma)}(\rho) \triangleq \rho [ \psi \in \mathrm{Sen}^{\mathcal{J}}(\Sigma) / \alpha_{\Sigma}(\psi) ], $$

for any $(\Delta, \Sigma) \in |\mathrm{Sign}^{\mathcal{C}\mathcal{I}}|.$
$$
\begin{array}{l}
\text{-- MODELS. } \mathcal{C}\beta : \mathrm{Mod}^{\mathcal{C}\mathcal{J}'} \cdot \mathcal{C}\Phi^{\mathrm{op}} \to \mathrm{Mod}^{\mathcal{C}\mathcal{J}}, \\
\qquad (\mathcal{C}\beta)_{(\Delta, \Sigma)} \triangleq \mathrm{id} \times \mathrm{id} \times (\beta_{\Sigma} \cdot), \\
\text{for any } (\Delta, \Sigma) \in |\mathrm{Sign}^{\mathcal{C}\mathcal{J}}|.
\end{array}
$$

Clearly, $\mathcal{C}\Phi$ is a functor and both $\mathcal{C}\alpha$, and $\mathcal{C}\beta$ are natural transformations.

**Lemma 1.** *The lifting process, as defined above, preserves identities and dis- tributes over composition.*

To conclude that the three combinations are endofunctors one step still remains: to show that the lifted arrows are comorphisms. This, however, entails the need to inspect each specific combination on its own, as they all lift the satisfaction relation in different ways. Certainly a fully generic definition would be an interesting result. However, this turned out to be a surprisingly complex issue, which furthermore is not essential for the message that we want this paper to convey.

**Theorem 3.** If $(\Phi, \alpha, \beta)$ is a comorphism then, for any of the three combinations $\mathcal{C}$ discussed above, $(\mathcal{C}\Phi, \alpha, \beta)$ is a comorphism as well.

**4.2 Property preservation (conservativity and equivalence)**

The characterisation of asymmetric combinations as endofunctors over the category of institutions I provides a sound basis for the study of property preservation by them. Such a study is illustrated in this section in which it is shown that temporalisation, probabilisation, and hybridisation preserve conservativity and equivalence. We start with the former case.

In Computing Science a main reason to study under what conditions a logic may be translated into another is to seek for the existence of (better) computational proof support. In the institutional setting, suitable translations are often defined by comorphisms, which in many cases should obey the following condition: whenever completeness is required, i.e. whenever one demands the validation of the specification against all possible scenarios (models), then the comorphisms involved must be conservative. Formally,

**Definition 9.** A comorphism $(\Phi, \alpha, \beta)$ is conservative whenever, for each signature $\Sigma \in |\mathrm{Sign}^J|$, $\beta_\Sigma$ is surjective on objects.

Let us describe in more detail the relevance of conservativity for validation. Recall the satisfaction condition placed upon comorphisms. For a signature $\Sigma \in |\mathrm{Sign}^J|$, $M \in |\mathrm{Mod}^{J'} \cdot \Phi^{\mathrm{op}}(\Sigma)|$, and $\rho \in \mathrm{Sen}^J(\Sigma)$ we have $\beta_\Sigma(M) \models_{\Sigma}^J \rho$ iff $M \models_{\Phi(\Sigma)}^{J'} \alpha_\Sigma(\rho)$. Graphically, for each $\Sigma \in |\mathrm{Sign}^J|$

$$
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    \mathrm{Mod}^J(\Sigma) \arrow[r, "\models_\Sigma^J"] & \mathrm{Sen}^J(\Sigma) \arrow[d, "\alpha_\Sigma"] \\
    \beta_\Sigma \arrow[u, "\models_{\Sigma'}^J"] & \mathrm{Mod}^{J'} \cdot \Phi^{\mathrm{op}}(\Sigma) \arrow[u, "\models_{\Phi(\Sigma)}^{J'}", "\cong"]
\end{tikzcd}
$$
Suppose we want to verify that a sentence $\rho \in Sen^J(\Sigma)$ is satisfied by all models $M \in |Mod^J(\Sigma)|$. For this we resort to the comorphism by translating the sentence (through $\alpha$) into the target logic. The satisfaction condition, once verified, ensures that if the sentence is satisfied by all models there, then all models in the image of $\beta_\Sigma$ will satisfy the original sentence. Of course, if $\beta_\Sigma$ is surjective on objects its image will coincide with $|Mod^J(\Sigma)|$, thus proving that the original sentence is satisfied by all models in $|Mod^J(\Sigma)|$.

**Theorem 4.** A *lifted conservative comorphism is still conservative*.

Next we show that the application of temporalisation, probabilisation, and hybridisation to two equivalent logics yields again two equivalent logics. First, recall the definition of equivalence of categories.

**Definition 10.** Two categories C, D are equivalent if there are two functors $F: C \to D, G: D \to C$ and two natural isomorphisms $\epsilon: FG \to 1_D, \eta: 1_C \to GF$. In these circumstances, an equivalence of categories, G (resp. F) is the inverse up to isomorphism of F (resp. G)

**Definition 11.** A comorphism $(\Phi, \alpha, \beta)$ is an equivalence of institutions if the following conditions hold.

- SIGNATURES. $\Phi$ forms an equivalence of categories.

- SENTENCES. $\alpha$ has an inverse up to semantical equivalence, i.e. a natural transformation $\alpha^{-1}: Sen^{J'} \cdot \Phi \to Sen^J$ such that for any sentence $\rho \in Sen^J(\Sigma)$,

$$ (\alpha^{-1} \cdot \alpha)(\rho) \models \rho, \quad \rho \models (\alpha^{-1} \cdot \alpha)(\rho) $$

or more concisely, $(\alpha^{-1} \cdot \alpha)(\rho) \models \rho$.

Moreover, for any sentence $\rho \in Sen^{J'} \cdot \Phi(\Sigma)$, $(\alpha \cdot \alpha^{-1})(\rho) \models \rho$.

- MODELS. $\beta$ has an inverse up to isomorphism, i.e., a natural transformation $\beta^{-1}$ such that for any $\Sigma \in |Sign^J|$, functor $\beta_{\Sigma}^{-1}$ is the inverse up to isomorphism of $\beta_\Sigma$.

More about equivalence of institutions can be found in e.g. document [21].

**Theorem 5.** A *lifted equivalence of institutions is still an equivalence of institutions*.

## 4.3 Natural transformations

We consider now natural transformations between asymmetric combinations of logics, which seem to fit nicely into the picture: while lifted comorphisms map the bottom level and keep the top one, such natural transformations map the top and keep the bottom. For example, take a natural transformation $\tau: \mathcal{L} \to \mathcal{H}$. It is
clear that each institution $\mathcal{J}$, induces a comorphism $\tau_{\mathcal{J}} : \mathcal{L}\mathcal{J} \to \mathcal{H}\mathcal{J}$. Furthermore, naturality expresses the commutativity of the diagram below

<figure><img src="image_5.png" /></figure>

for each comorphism $(\Phi, \alpha, \beta)$. This means that when translating a logic whose levels are both mapped by a composition of natural transformations and lifted comorphisms, it does not matter which one of the top or bottom levels is taken first.

Let us illustrate this construction through the natural transformation $\tau : \mathcal{L} \to \mathcal{H}$, which relates temporalisation to hybridisation. We will, for now, disregard the until ($U$) constructor associated with $\mathcal{L}$, in order to keep the construction simple. First consider a signature $N \in |\text{Sign}^{\mathcal{H}}|$ such that $N \triangleq (\{\text{Init}\}, \{\text{After}, \text{After}^*, \text{Next}\})$. Then for any signature $(N, \Sigma) \in |\text{Sign}^{\mathcal{H}\mathcal{I}}|$ define the full subcategory of $\text{Mod}^{\mathcal{H}\mathcal{J}}(N, \Sigma)$ (denoted in the sequel by $\mathcal{M}^{\mathcal{N}\mathcal{J}}(N, \Sigma)$) whose objects are triples $(S, R, m)$ subjected to the following rules:

$$ 
\begin{array}{l@{\qquad}l}
S = \mathbb{N} & \\
R_{\text{Init}} = 0 & (a, b) \in R_{\text{After}} \text{ iff } a < b \\
(a, b) \in R_{\text{Next}} \text{ iff } b = \text{suc}(a) & (a, b) \in R_{\text{After}^*} \text{ iff } a \le b.
\end{array}
$$

**Definition 12.** Given an institution $\mathcal{J}$, define an arrow $\tau_{\mathcal{J}} = (\tau_{\mathcal{J}}\Phi, \tau_{\mathcal{J}}\alpha, \tau_{\mathcal{J}}\beta)$ where

- **SIGNATURES.** $\tau\Phi : \text{Sign}^{\mathcal{L}\mathcal{J}} \to \text{Sign}^{\mathcal{H}\mathcal{J}}$ is a functor such that $\tau\Phi(\Sigma) \triangleq (N, \Sigma)$ and, for any signature morphism $\varphi : \Sigma \to \Sigma'$

$$ \tau\Phi(\varphi) : (N, \Sigma) \to (N, \Sigma'), \quad \tau\Phi(\varphi) \triangleq \text{id} \times \varphi $$

- **SENTENCES.** Given a signature $\Sigma \in |\text{Sign}^{\mathcal{L}\mathcal{J}}|$, $\tau\alpha : \text{Sen}^{\mathcal{L}\mathcal{J}}(\Sigma) \to \text{Sen}^{\mathcal{H}\mathcal{J}}$. $\tau\Phi(\Sigma)$ is a function such that $\tau\alpha(\rho) \triangleq \text{@}_{\text{Init}}\sigma(\rho)$ where

$$ 
\begin{array}{l@{\qquad}l}
\sigma(\psi) = \psi, \text{ for } \psi \in \text{Sen}^{\mathcal{J}}(\Sigma) & \sigma(\rho \wedge \rho') = \sigma(\rho) \wedge \sigma(\rho') \\
\sigma(\neg\rho) = \neg\sigma(\rho) & \sigma(X\rho) = [\text{Next}] \sigma(\rho)
\end{array}
$$

The proof that $\tau\alpha$ is a natural transformation follows through routine calculation.

- Finally, given a signature $\Sigma \in |\text{Sign}^{\mathcal{L}\mathcal{J}}|$, arrow $\tau\beta : \text{Mod}^{\mathcal{H}\mathcal{J}} \cdot (\tau\Phi)^{op} \to \text{Mod}^{\mathcal{L}\mathcal{J}}$ is a functor such that

$$ \tau\beta(S, R, m) \triangleq (\mathbb{N}, \text{suc} : \mathbb{N} \to \mathbb{N}, m) $$

Clearly, $\tau\beta$ is a natural transformation.
**Theorem 6.** $\tau: \mathcal{L} \to \mathcal{H}$ forms a natural transformation whenever $\mathrm{Mod}^{\mathcal{H}}$ (for any institution $\mathcal{I}$) is equal to $\mathrm{Mod}^{\mathcal{N}\mathcal{I}}$.

In order to include the *until* constructor we need to add *nominal quantification* to hybridisation, which would yield the translation

$$ \sigma(\rho U \rho') = \exists x . (\langle \mathit{After}^* \rangle (x \wedge \sigma(\rho')) \wedge [\mathit{After}^*](\langle \mathit{After} \rangle x \Rightarrow \sigma(\rho))) $$

Actually, the proof that hybridisation with nominal quantification is also an endofunctor (and the satisfaction condition for *until* associated with $\tau$ holds) boils down to a routine calculation. This means that the theorem above can be replicated, taking care of the *until* operator, in a straightforward manner.

# 5 Conclusions and future work

Asymmetric combination of logics is a promising tool for the (formal) development of complex, heterogeneous software systems. This justifies their study at an abstract level, paving the way to general results on, for example, property preservation along the combination process. Often such a study has been made on a case-by-case basis e.g. [11, 27, 28]. This paper, on the other hand, surveys a more general, functorial perspective using three different asymmetric combinations of logics as case-studies. In particular, it provided their characterisation as endofunctors over the category of institutions by showing how to lift comorphisms and proving that the lifted arrows obey the functorial laws. This made clear that not only logics, but also their translations can be combined.

The development of an institutional, abstract notion of asymmetric combination of logics proposed in the paper, hints at a set of directions for future research. For example, we saw at the abstract level that conservativity (an important property for safely 'borrowing' a theorem prover) and equivalence are preserved by combination. However, a full study is still to be done in what regards preservation of (co)limits, e.g. to discuss whether the combination of the product of two logics is equivalent to the product of their respective combinations

Another research direction was set by J. Goguen in his Categorial Manifest [16]: "if you have found an interesting functor, you might be well advised to investigate its adjoints". We studied natural transformations between such functors and showed that they nicely complement the lifting of comorphisms: while the latter maps the bottom level and keeps the top one, the former maps the top and keeps the bottom. We gave an example of a natural transformation between temporalisation and hybridisation, but others deserve to be studied as well. For example, in document [20] it is shown how, given a comorphism from an institution $\mathcal{I}$ to $\mathrm{FOL}$, a comorphism from $\mathcal{H}\mathcal{I}$ to $\mathrm{FOL}$ can be obtained. More generally, the current paper shows that comorphisms can be built by lifting the original comorphism and then composing it with the 'flat' natural transformation
$E: \mathcal{C} \to 1_J$ (whenever it exists). Diagrammatically,

<figure><img src="image_6.png" /></figure>

On a more speculative note, the perspective taken in this paper also suggests to look at ‘trivial’ asymmetric combinations. For example, it is straightforward to define *identisation*, in which the added layer has a trivial structure, but also *trivialisation* (*J*), which turns a logic into the trivial one (technically, the initial object in the category *I* of institutions). The latter case implies that there is a (unique) natural transformation *J* → *C* to any combination *C*.

From a pragmatic point of view, the incorporation of these ideas into the HETS platform [22] paves the way for its effective use in Software Engineering. HETS is often described as a “motherboard” of logics where different “expansion cards” can be plugged in. These refer to individual logics (with their particular analysers and proof tools) as well as to logic translations. To make them compatible, logics are formalised as institutions and translations as comorphisms. Therefore HETS provides an interesting setting for the implementation of the theory developed in this paper. Again, a specific case — that of *hybridisation* — was already implemented in the HETS platform [26].

## Acknowledgments

This work is financed by the ERDF - European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within projects POCI-01-0145-FEDER-016692 and UID/MAT/04106/2013. Further support was provided by Norte Portugal Regional Operational Programme (NORTE 2020), under the PORTUGAL 2020 Partnership Agreement through the ERDF in the context of project NORTE-01-0145-FEDER-000037. Renato Neves was also sponsored by FCT grant SFRH/BD/52234/2013, and Alexandre Madeira by FCT grant SFRH/BPD/103004/2014.

## References

1. Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics. Elsevier (2006)

2. Baltazar, P.: Probabilization of logics: Completeness and decidability. Logica Universalis 7(4), 403–440 (2013)

3. Blackburn, P., de Rijke, M.: Why combine logics? Studia Logica 59(1), 5–27 (1997)
4. Caleiro, C., Mateus, P., Sernadas, A., Sernadas, C.: Quantum institutions. In: Futatsugi, K., Jouannaud, J.P., Meseguer, J. (eds.) Algebra, Meaning, and Computation, Lecture Notes in Computer Science, vol. 4060, pp. 50–64. Springer Berlin Heidelberg (2006)

5. Caleiro, C., Sernadas, A., Sernadas, C.: Fibring logics: Past, present and future. In: Artëmov, S.N., Barringer, H., d'Avila Garcez, A.S., Lamb, L.C., Woods, J. (eds.) We Will Show Them! Essays in Honour of Dov Gabbay, Volume One. pp. 363–388. College Publications (2005)

6. Caleiro, C., Sernadas, C., Sernadas, A.: Parameterisation of logics. In: Fiadeiro, J.L. (ed.) WADT, Selected papers. Lecture Notes in Computer Science, vol. 1589, pp. 48–62. Springer (1998)

7. Carnielli, W., Coniglio, M.E.: Combining logics. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Winter 2011 edn. (2011)

8. Cengarle, M.V.: The temporal logic institution. Tech. Rep. 9805, Ludwig-Maximilians-Universität München, Institut für Informatik (November 1998)

9. Cîrstea, C.: An institution of modal logics for coalgebras. Journal of Logic and Algebraic Programming 67(1-2), 87–113 (2006)

10. Diaconescu, R., Madeira, A.: Encoding hybridized institutions into first-order logic. Mathematical Structures in Computer Science 26(5), 745–788 (2016)

11. Diaconescu, R., Stefaneas, P.: Ultraproducts and possible worlds semantics in institutions. Theoretical Computer Science 379(1-2), 210–230 (Jul 2007)

12. Finger, M., Gabbay, D.: Adding a temporal dimension to a logic system. Journal of Logic, Language and Information 1(3), 203–233 (1992)

13. Fitting, M.: Logics with several modal operators. Theoria 35, 259–266 (1969)

14. Gabbay, D.: Fibred semantics and the weaving of logics: Part 1. Journal of Symbolic Logic 61(4), 1057–1120 (1996)

15. Găină, D.: Birkhoff style calculi for hybrid logics. Formal Asp. Comput. pp. 1–28 (2017)

16. Goguen, J.A.: A categorical manifesto. Mathematical Structures in Computer Science 1(1), 49–67 (1991)

17. Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39, 95–146 (January 1992)

18. Goguen, J.A., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT '87, Lecture Notes in Computer Science, vol. 250, pp. 1–22. Springer Berlin Heidelberg (1987)

19. Madeira, A., Martins, M.A., Barbosa, L.S., Hennicker, R.: Refinement in hybridised institutions. Formal Asp. Comput. 27(2), 375–395 (2015)

20. Martins, M.A., Madeira, A., Diaconescu, R., Barbosa, L.S.: Hybridization of institutions. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO. Lecture Notes in Computer Science, vol. 6859, pp. 283–297. Springer (2011)

21. Mossakowski, T., Goguen, J., Diaconescu, R., Tarlecki, A.: What is a logic? In: Beziau, J.Y. (ed.) Logica Universalis, pp. 111–133. Birkhäuser Basel (2007)

22. Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS. Lecture Notes in Computer Science, vol. 4424, pp. 519–522. Springer (2007)

23. Mossakowski, T., Roggenbach, M.: Structured CSP – a process algebra as an institution. In: Fiadeiro, J.L., Schobbens, P.Y. (eds.) Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science, vol. 4409, pp. 92–110. Springer Berlin Heidelberg (2007)
24. Neves, R., Madeira, A., Barbosa, L.S., Martins, M.A.: Asymmetric combination of logics is functorial: A survey (extended version). arXiv preprint arXiv:1611.04170 (2017)

25. Neves, R., Madeira, A., Martins, M., Barbosa, L.: An institution for Alloy and its translation to second-order logic. In: Integration of Reusable Systems, pp. 45–75. Springer (2014)

26. Neves, R., Madeira, A., Martins, M.A., Barbosa, L.S.: Hybridisation at work. In: CALCO TOOLS. Lecture Notes in Computer Science, vol. 8089. Springer (2013)

27. Neves, R., Madeira, A., Martins, M.A., Barbosa, L.S.: Proof theory for hybrid(ised) logics. Science of Computer Programming 126, 73–93 (2016)

28. Neves, R., Martins, M.A., Barbosa, L.S.: Completeness and decidability results for hybrid(ised) logics. In: Braga, C., Martí-Oliet, N. (eds.) SBMF. Lecture Notes in Computer Science, vol. 8941, pp. 146–161 (2015)

29. Rasga, J., Sernadas, A., Sernadas, C.: Importing logics: Soundness and completeness preservation. Studia Logica 101(1), 117–155 (2013)

30. Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. EATCS Monographs on theoretical computer science, Springer (2012)

31. Segerberg, K.: Two-dimensional modal logic. Journal of Philosophical Logic 2(1), 77–96 (1973)

32. Sernadas, A., Sernadas, C., Caleiro, C.: Fibring of logics as a categorial construction. J. Log. Comput. 9(2), 149–179 (1999)

33. Thomason, R.H.: Combinations of tense and modality. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic: Volume II: Extensions of Classical Logic, pp. 135–165. Reidel, Dordrecht (1984)