An Institutional Foundation for the $\mathbb {K}$ Semantic Framework

Abstract

We advance an institutional formalisation of the logical systems that underlie the $\mathbb {K}$ semantic framework and are used to capture both structural properties of program configurations through pattern matching, and changes of configurations through reachability rules. By defining encodings of matching and reachability logic into the institution of first-order logic, we set the foundation for integrating $\mathbb {K}$ into logic graphs of heterogeneous institution-based specification languages such as $\textsc {HetCasl}$. This will further enable the use of the $\mathbb {K}$ tool with other existing formal specification and verification tools associated with Hets.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The $\mathbb {K}$ framework [19] is an executable semantic framework based on rewriting and used for defining programming languages, computational calculi, type systems and formal-analysis tools. It was developed as an alternative to the existing operational-semantics frameworks and over the years has been employed to define actual programming languages, to study runtime verification methods and to develop analysis tools such as type checkers, type inferencers, model checkers and verifiers based on Hoare-style assertions. A comprehensive overview of the framework can be found in [20]. Its associated tool [6] enables the development of modular and executable definitions of languages, and moreover, it allows the user to test programs and to explore their behaviour in an exhaustive manner, facilitating in this way the design of new languages. Driven by recent developments on the theoretical foundations of the $\mathbb {K}$ semantic framework [18, 21] and on the established connections with other semantic frameworks and formal systems such as reduction semantics, Hoare logic and separation logic, we propose an institutional formalisation [10] of the logical systems on which the $\mathbb {K}$ framework is based: matching and reachability logic. This would allow us to extend the usage of $\mathbb {K}$ by focusing on its potential as a formal specification language, and furthermore, through its underlying logics, to establish rigorous mathematical relationships between $\mathbb {K}$ and other similar languages, enabling the integration of their verification tools and techniques.

Matching logic [18] is a formal system used to express properties about the structure of mathematical objects and language constructs, and to reason about them by means of pattern matching. Its sentences, called patterns, are built in an inductive manner, similar to the terms of first-order logic, using operation symbols provided by a many-sorted signature, as well as Boolean connectives and quantifiers. The semantics is defined in terms of multialgebras, which interpret patterns as subsets of their carriers. This leads to a ternary satisfaction relation between patterns, multialgebras and elements (or states) of multialgebras.

Unlike first-order logic, matching logic is difficult to formalise faithfully as an institution due to the ternary nature of its satisfaction relation and to the fact that patterns are classified by sorts, much in the way the sentences of branching temporal logics are classified into state or path sentences and evaluated accordingly. We overcome these limitations by relying on the concept of stratified institution developed in [2], which extends institutions with an abstract notion of model state and defines a parameterised satisfaction relation that takes into account the states of models. We further develop this concept by adding classes, which are determined by signatures, associated with sentences, and parameterise both the stratification of models and the satisfaction relation. We show that both matching and computation-tree logic can be described as stratified institutions with classes, and we adapt the canonical construction of an ordinary institution from a stratified one presented in [2] to take into consideration the role of classes.

The main advantage of using stratified institutions with classes to formalise matching logic is that we can extend the construction of reachability logic described in [21] from matching to other logical systems. Reachability logic is a formalism for program verification through which transition systems that correspond to the operational semantics of programming languages can be described using reachability rules; these rules rely on patterns and generalise Hoare triples in order to specify transitions between program configurations (similarly to term-rewrite rules). Therefore, reachability logic can be seen as a language-independent alternative to the axiomatic semantics and proof systems particular to each language. We define an abstract institution of reachability logic over an arbitrary stratified institution with classes such that by instantiating this parameter with matching logic we recover the original notion of reachability.

This paper is based on the Master’s thesis of the first author [5], which additionally contains detailed proofs of the results presented herein.

2 Preliminaries

2.1 Institution Theory

The concept of institution [10] formalises the intuitive notion of logic by abstracting the alphabet, syntax, semantics and satisfaction relation. In the following, we assume familiarity with the basics of category theory. The reader is referred to the book [14] of Mac Lane and Eilenberg for further reading.

Definition 1

An institution $\mathbf {I} = ( \mathrm {\mathbb {S}ig}^{\mathbf {I}}, \mathrm {Sen}^{\mathbf {I}}, \mathrm {Mod}^{\mathbf {I}}, \models ^{\mathbf {I}})$ consists of

• a category $\mathrm {\mathbb {S}ig}^{\mathbf {I}}$ whose objects are called signatures,

• a sentence functor $\mathrm {Sen}^{\mathbf {I}} :\mathrm {\mathbb {S}ig}^{\mathbf {I}} \rightarrow \mathrm {\mathbb {S}et}$ giving for every signature $\varSigma$ the set $\mathrm {Sen}^{\mathbf {I}}(\varSigma )$ of $\varSigma$-sentences and for every signature morphism $\phi :\varSigma \rightarrow \varSigma '$ the sentence translation map $\mathrm {Sen}^{\mathbf {I}}(\phi ) :\mathrm {Sen}^{\mathbf {I}}(\varSigma ) \rightarrow \mathrm {Sen}^{\mathbf {I}}(\varSigma ')$,

• a model functor $\mathrm {Mod}^{\mathbf {I}} :(\mathrm {\mathbb {S}ig}^{\mathbf {I}})^{\mathrm {op}} \rightarrow \mathrm {\mathbb {C}at}$ defining for every signature $\varSigma$ the category $\mathrm {Mod}^{\mathbf {I}}(\varSigma )$ of $\varSigma$-models and $\varSigma$-model homomorphisms, and for every signature morphism $\phi$ the reduct functor $\mathrm {Mod}^{\mathbf {I}}(\phi ) :\mathrm {Mod}^{\mathbf {I}}(\varSigma ') \rightarrow \mathrm {Mod}^{\mathbf {I}}(\varSigma )$,

• a satisfaction relation ${ \models ^{\mathbf {I}}_{\varSigma }} \subseteq {|\mathrm {Mod}^{\mathbf {I}}(\varSigma ) | \times \mathrm {Sen}^{\mathbf {I}}(\varSigma ) }$ for every signature $\varSigma$,

such that the satisfaction condition

$$\begin{aligned} M' \models ^{\mathbf {I}}_{\varSigma '} \mathrm {Sen}^{\mathbf {I}}(\phi )(\rho ) \quad \text { iff } \quad \mathrm {Mod}^{\mathbf {I}}(\phi )(M') \models ^{\mathbf {I}}_{\varSigma } \rho \end{aligned}$$

holds for any signature morphism $\phi :\varSigma \rightarrow \varSigma '$, $\varSigma '$-model $M'$ and $\varSigma$-sentence $\rho$.

We may omit the sub/superscripts in the notations of institutions when there is no risk of confusion: for example, $\models ^{\mathbf {I}}_{\varSigma }$ may be denoted by $\models$ if the institution $\mathbf {I}$ and the signature $\varSigma$ are clear. The sentence translation $\mathrm {Sen}^{\mathbf {I}}(\phi )$ and the reduct functor $\mathrm {Mod}^{\mathbf {I}}(\phi )$ may also be denoted by $\phi (\_)$ and $\_\mathord {\upharpoonright }_{\phi }$. When $M = M'\mathord {\upharpoonright }_{\phi }$ we say that $M$ is a $\phi$-reduct of $M'$ and that $M'$ is a $\phi$-expansion of $M$.

First-order logic constitutes a long-established example of an institution [10].

Example

(Many-sorted first-order logic with equality (FOL)). Signatures. A (many-sorted) first-order signature $(S,F,P)$ consists of a set $S$ of sorts, a family $F$ of sets $F_{w \rightarrow s}$, for $w \in S^{*}$ and $s \in S$, of operation symbols with arity $w$ and sort $s$ (when the arity is empty, $F_{\lambda \rightarrow s}$ denotes the set of constants of sort $s$), and a family $P$ of sets $P_w$, for $w \in S^{*}$, of relation symbols with arity $w$ indexed by arities. A signature $(S, F, P)$ is algebraic when $P$ is empty.

Signature Morphisms. The morphisms of signatures $\phi :(S,F,P) \rightarrow (S',F',P')$ consist of functions $\phi ^{\mathrm {st}} :S \rightarrow S'$ between the sets of sorts, $\phi ^{\mathrm {op}}_{w \rightarrow s} :F_{w \rightarrow s} \rightarrow F'_{\phi ^{\mathrm {st}}(w) \rightarrow \phi ^{\mathrm {st}}(s)}$, for $w \in S^{*}$ and $s \in S$, between the sets of operation symbols, and $\phi ^{\mathrm {rel}}_{w} :P_{w } \rightarrow P'_{\phi ^{\mathrm {st}}(w)}$, for $w \in S^{*}$, between the sets of relation symbols.

Models. For every signature $(S,F,P)$, a model $M$ interprets every sort symbol $s$ as a set $M_s$, called the carrier set of sort$s$, every operation symbol $\sigma \in F_{w \rightarrow s}$ as a function $M_{\sigma } :M_{w} \rightarrow M_s$, where $M_w = M_{s_1} \times \cdots \times M_{s_n}$ for $w = s_1\cdots s_n$, with $s_1,\cdots ,s_n \in S$, and every relation symbol $\pi \in P_w$ as a subset $M_{\pi } \subseteq M_{w}$.

A homomorphism of $(S,F,P)$-models $h :M \rightarrow N$ is an indexed family of functions $\{h_s :M_s \rightarrow N_s \mid {s \in S}\}$ such that

• h is an $(S,F)$-algebra homomorphism, that is $h_s(M_\sigma (m)) = N_{\sigma }(h_w(m))$, for every $\sigma \in F_{w \rightarrow s}$ and $m \in M_{w}$, where $h_w :M_w \rightarrow N_w$ is the canonical component-wise extension of $h$ to tuples, and

• $h_w(m) \in N_{\pi }$ if $m \in M_{\pi }$, i.e., $h_{w}(M_{\pi }) \subseteq N_{\pi }$, for every $\pi \in P_w$.

Model Reducts. For every signature morphism $\phi :\varSigma \rightarrow \varSigma '$, the reduct $M'\mathord {\upharpoonright }_{\phi }$ of a $\varSigma '$-model $M'$ is defined by ${(M'\mathord {\upharpoonright }_{\phi })}_\alpha = M'_{\phi (\alpha )}$ for every sort, function, or relation symbol $\alpha$ from $\varSigma$. The reducts of homomorphisms are defined likewise.

Sentences. The sentences are usual first-order sentences built from equational and relational atoms by applying in an iterative manner Boolean connectives and first-order quantifiers. The existential and universal quantification are over sets of first-order variables, which are triples $\langle x,s(S,F,P)\rangle$ sometimes denoted by $x \,\mathord {:}\,{s}$, where $x$ is the name of the variable and $s \in S$ is its sort: for any $(S,F\uplus X,P)$-sentence $\rho$, $\exists X.\rho$ and $\forall X.\rho$ are $(S,F,P)$-sentences, where $(S,F \uplus X, P)$ denotes the extension of $(S,F,P)$ with the elements of $X$ as new symbols of constants. Note that different variables in $X$ should have different names.

Sentence Translations. Every signature morphism $\phi :(S,F,P) \rightarrow (S',F',P')$ induces a sentence translation $\mathrm {Sen}(\phi ) :\mathrm {Sen}(S,F,P) \rightarrow \mathrm {Sen}(S',F',P')$ that is defined inductively on the structure of sentences and renames the symbols of $(S,F,P)$ according to $\phi$. For instance, the translation of an existentially quantified sentence is $\mathrm {Sen}(\phi )(\exists X.\rho ) = \exists X^{\phi }.\mathrm {Sen}(\phi ^{X})(\rho )$, where $X^{\phi } = \{ x \,\mathord {:}\,{\phi ^{\mathrm {st}}(s)} \mid x\,\mathord {:}\,{s} \in X\}$ and $\phi ^{X} :(S,F \uplus X, P) \rightarrow (S',F'\uplus X^{\phi },P')$ extends $\phi$ canonically.

Satisfaction. The satisfaction relation between models and sentences is the usual Tarskian satisfaction defined inductively on the structure of sentences. For existentially quantified sentences, for example, given a model $M$ of a signature $(S,F,P)$, $M \models \exists X.\rho$ if and only if there exists an expansion $M'$ of $M$ along the signature inclusion $(S,F,P) \hookrightarrow (S,F \uplus X, P)$ such that $M' \models \rho$.

Model Amalgamation. Model amalgamation will prove to be crucial in adding quantifiers over an arbitrary institution. Essentially, it allows us to combine models of different signatures whenever they are compatible with respect to a common sub-signature. Many logical systems of interest for specification theory have model amalgamation, including the examples considered in this paper.

Definition 2

In any institution, a commuting square of signature morphisms

is a weak amalgamation square if, for each $\varSigma _1$-model $M_1$ and $\varSigma _2$-model $M_2$ such that $\mathrm {Mod}(\varphi _1)(M_1) = \mathrm {Mod}(\varphi _2)(M_2)$, there exists a $\varSigma '$-model $M'$, called an amalgamation of $M_1$ and $M_2$, such that $\mathrm {Mod}(\theta _1)(M') = M_1$ and $\mathrm {Mod}(\theta _2)(M') = M_2$. When $M'$ is unique, the above square is called an amalgamation square.

We say that an institution has (weak) model amalgamation if and only if each pushout square of signature morphisms is a (weak) amalgamation square.

Therefore, in order to have model amalgamation, the square of signature morphisms must not identify entities of $\varSigma _1$ and $\varSigma _2$ that do not come from $\varSigma$ via the signature morphisms $\varphi _1$ and $\varphi _2$. Moreover, to guarantee the uniqueness of the amalgamation, $\varSigma '$ must contain only entities that come from $\varSigma _1$ or $\varSigma _2$.

Presentations. The presentations over an institution represent one of the simplest forms of specifications over that logic being formed merely of a signature and a (usually finite) set of its sentences. We will use presentations in our paper to encode reachability logic into first-order logic.

Definition 3

The presentations of an institution $\mathbf {I} = (\mathrm {\mathbb {S}ig},\mathrm {Sen},\mathrm {Mod},\models )$ are pairs $(\varSigma , E)$ consisting of a signature $\varSigma$ and a set $E$ of $\varSigma$-sentences. They form a category $\mathbb {P}\mathrm {res}$ whose arrows $\phi :(\varSigma ,E) \rightarrow (\varSigma ',E')$ are signature morphisms $\phi :\varSigma \rightarrow \varSigma '$ such that $E' \models \phi (E)$. By extending the sentence functor, the model functor and the satisfaction relation from the signatures of $\mathbf {I}$ to presentations we obtain an institution $\mathbf {I}^{\mathrm {pres}} = (\mathbb {P}\mathrm {res},\mathrm {Sen}^{\mathrm {pres}},\mathrm {Mod}^{\mathrm {pres}},\models ^{\mathrm {pres}})$ of $\mathbf {I}$ presentations.

Moving Between Institutions. In order to use institutions as formalisations of logical systems in a heterogeneous setting, one needs to define formally a notion of map between institutions. Several concepts have been defined over the years, including semi-morphisms, morphisms, and comorphisms, some of which can be found in [23]. In our work, we focus only on comorphisms [15, 24], which reflect the intuition of embedding simpler institutions into more complex ones.

Definition 4

Given two institutions $\mathbf {I}$ and $\mathbf {I}'$, a comorphism $(\varPhi , \alpha , \beta ) :\mathbf {I} \rightarrow \mathbf {I}'$ consists of

• a signature functor $\varPhi :\mathrm {\mathbb {S}ig}\rightarrow \mathrm {\mathbb {S}ig}'$,

• a natural transformation $\alpha :\mathrm {Sen}\Rightarrow \varPhi \mathbin {;}\mathrm {Sen}'$, and

• a natural transformation $\beta :\varPhi ^{\mathrm {op}} \mathbin {;}\mathrm {Mod}' \Rightarrow \mathrm {Mod}$

such that the following satisfaction condition holds for any $\mathbf {I}$-signature $\varSigma$, $\varPhi (\varSigma )$-model $M'$, and $\varSigma$-sentence $\rho$: $M' \models ^{\mathbf {I'}}_{\varPhi (\varSigma )} \alpha _{\varSigma }(\rho ) \text { iff } \beta _{\varSigma }(M') \models ^{\mathbf {I}}_{\varSigma } \rho .$

2.2 $\mathbb {K}$ Semantic Framework

The $\mathbb {K}$ framework [20] is an executable semantic framework based on rewriting and used for defining programming languages, computational calculi, type systems and formal analysis tools. It was developed as an alternative to the existing operational-semantics (SOS) frameworks and has been employed to define actual programming languages such as C [9], Python [12], and Java [3].

In defining semantics for programming languages, $\mathbb {K}$ handles cell-like structures named configurations and relies on computational structures – computations – to model transitions between these configurations by applying local rewriting rules. To illustrate how language specifications can be written in the $\mathbb {K}$ semantic framework, we consider the following running example of the (partial) definition of IMP [1], an elementary imperative programming language.

In the following sections we introduce two logics in order to formalize the $\mathbb {K}$ framework. Matching logic will be used to define the syntactic constructs – the syntax of the specified programming languages – and the patterns matched in the semantic rules, and to partially capture the semantics of the programming languages by defining the states of the running programs. Subsequently, we build reachability logic upon matching logic to capture the semantic rules. Its sentences, defined over the signatures of matching logic, correspond to the rules in the $\mathbb {K}$ modules, while the models represent implementations of programming languages. The language definitions written in $\mathbb {K}$ will thus be seen, leaving aside some parsing instructions without logical interpretation, as formal specifications over reachability logic.

3 Matching Logic

The generality of institutions allows them to accommodate a great variety of logical systems. As a downside however, and as it would be expected for such an abstract notion, certain logics cannot be captured in full detail by institutions; that is, by considering them only as institutions we lose precious information. An example is computation-tree logic, for which we lose the distinction between state and path sentences (which, in fact, do not belong to the sentences of computation-tree logic formalised as an institution).

Matching logic falls into the same category, but this time, we lose the sorts of patterns and the states of models. To palliate this, we extend institutions with notions of classes (for sorts) and stratification of models (for states). The end result – the concept of stratified institution with classes – is obtained as a combination of the institutions with classes described in Definition 5 with the stratified institutions introduced in [2].

3.1 Stratified Institutions with Classes

Definition 5

An institution with classes is a tuple $(\mathrm {\mathbb {S}ig}, \mathrm {Cls}, \mathrm {Sen}, \kappa , \mathrm {Mod}, \models )$, where

• $(\mathrm {\mathbb {S}ig}, \mathrm {Sen}, \mathrm {Mod}, \models )$ is an institution,

• $\mathrm {Cls}:\mathrm {\mathbb {S}ig}\rightarrow \mathrm {\mathbb {S}et}$ is a functor giving for each signature a set whose elements are called classes of that signature, and

• $\kappa :\mathrm {Sen}\Rightarrow \mathrm {Cls}$ is a natural transformation giving a class for each sentence.

We will use the notation $\mathrm {Sen}(\varSigma )_{c}$ for $\kappa ^{-1}(c)$, $c \in \mathrm {Cls}(\varSigma )$ to denote the set of $\varSigma$-sentences of class $c$.

Example

An immediate example of an institution with classes is the atomic fragment of equational first-order logic. In this case, $\mathrm {Cls}$ is the forgetful functor that maps every signature $(S,F)$ to its underlying set of sorts $S$, and $\kappa _{(S,F)}$ is the function that assigns to each atom $t = t'$ the common sort of $t$ and $t'$.

Definition 6

A stratified institution with classes is a tuple $\underline{\mathrm {I}} = (\mathrm {\mathbb {S}ig}, \mathrm {Cls}, \mathrm {Sen}, \kappa , \mathrm {Mod}, [\![\_ ]\!], \models )$ consisting of:

• a category $\mathrm {\mathbb {S}ig}$ of signatures and signature morphisms,

• a class functor $\mathrm {Cls}:\mathrm {\mathbb {S}ig}\rightarrow \mathrm {\mathbb {S}et}$, giving for every signature a set of classes,

• a sentence functor $\mathrm {Sen}:\mathrm {\mathbb {S}ig}\rightarrow \mathrm {\mathbb {S}et}$, defining for every signature a set of sentences,

• a natural transformation $\kappa :\mathrm {Sen}\Rightarrow \mathrm {Cls}$, associating a class to each sentence,

• a model functor $\mathrm {Mod}:\mathrm {\mathbb {S}ig}^{op} \rightarrow \mathrm {\mathbb {C}at}$, defining a category of models for every signature,

• a stratification $[\![\_ ]\!]$ giving

  • for every signature $\varSigma$, a family of functors $[\![\_ ]\!]_{\varSigma , c} :\mathrm {Mod}(\varSigma ) \rightarrow \mathrm {\mathbb {S}et}$, indexed by classes $c \in \mathrm {Cls}(\varSigma )$, and

  • for every signature morphism $\phi :\varSigma \rightarrow \varSigma '$, a functorial family of natural transformations $[\![\_ ]\!]_{\phi ,c} :[\![\_ ]\!]_{\varSigma ',\mathrm {Cls}(\phi )(c)} \Rightarrow \mathrm {Mod}(\phi ) \mathbin {;}[\![\_ ]\!]_{\varSigma , c}$, indexed by classes $c \in \mathrm {Cls}(\varSigma )$, such that $[\![M' ]\!]_{\phi ,c}$ is surjective for every $M' \in |\mathrm {Mod}(\varSigma ') |$, and

• a satisfaction relation between models and sentences, parameterised by model states and classes: $M \models ^{m}_{\varSigma ,c} \rho$, where $\varSigma$ is a signature, $c \in \mathrm {Cls}(\varSigma )$, $M \in |\mathrm {Mod}(\varSigma ) |$, $m \in [\![M ]\!]_{\varSigma , c}$, and $\rho \in \mathrm {Sen}(\varSigma )_c$

such that the following properties are equivalent:

• i. $\mathrm {Mod}(\phi )(M') \models ^{[\![M' ]\!]_{\phi ,c}(m')}_{\varSigma ,c} \rho$

• ii. $M' \models _{\varSigma ',\mathrm {Cls}(\phi )(c)}^{m'} \mathrm {Sen}(\phi )(\rho )$,

for every signature morphism $\phi :\varSigma \rightarrow \varSigma '$, every class $c \in \mathrm {Cls}(\varSigma )$, every model $M' \in |\mathrm {Mod}(\varSigma ') |$, every state $m' \in [\![M' ]\!]_{\varSigma ', \mathrm {Cls}(\phi )(c)}$, and every $\rho \in \mathrm {Sen}(\varSigma )_c$.

The functoriality of $[\![\_ ]\!]_{\phi ,c} :[\![\_ ]\!]_{\varSigma ',\mathrm {Cls}(\phi )(c)} \Rightarrow \mathrm {Mod}(\phi ) \mathbin {;}[\![\_ ]\!]_{\varSigma , c}$ means that for every signature morphisms $\phi :\varSigma \rightarrow \varSigma '$, $\phi ' :\varSigma ' \rightarrow \varSigma ''$, every $\varSigma ''$-model $M''$, and every class $c \in \mathrm {Cls}(\varSigma )$, $[\![M'' ]\!]_{\phi \mathbin {;}\phi ',c} = [\![M'' ]\!]_{\phi ',\phi (c)} \mathbin {;}[\![M''\mathord {\upharpoonright }_{\phi '} ]\!]_{\phi ,c}$.

Proposition 1

Every stratified institution with classes $\underline{\mathrm {I}} = (\mathrm {\mathbb {S}ig}, \mathrm {Cls}, \mathrm {Sen}, \kappa , \mathrm {Mod}, [\![\_ ]\!], \models )$ determines an institution denoted $\mathbf {\flat I}$ whose category of signatures is $\mathrm {\mathbb {S}ig}$, sentence functor is $\mathrm {Sen}$, model functor is $\mathrm {Mod}$, and satisfaction relation $\models _{\varSigma } \ \subseteq |\mathrm {Mod}(\varSigma ) | \times \mathrm {Sen}(\varSigma )$ is defined, for every signature $\varSigma \in |\mathrm {\mathbb {S}ig} |$, as follows:

$$\begin{aligned} M \models _{\varSigma } \rho \quad \text { iff } \quad M \models _{\varSigma , c}^{m} \rho \text { for every } m \in [\![M ]\!]_{\varSigma ,c}, \text { where } c =\kappa _{\varSigma }(\rho ). \end{aligned}$$

Computation-Tree Logic (CTL) . We formalise computation-tree logic as a first example of a stratified institution with classes. Similarly to other temporal logics, the usual presentation of $\underline{\mathrm {CTL}}$ is based on propositional logic. $\underline{\mathrm {CTL}}$ inherits the signatures of propositional logic, and thus, the category of its signatures is $\mathrm {\mathbb {S}et}$.

$\underline{\mathrm {CTL}}$ formulae can express properties of a state or a path (i.e. an infinite sequence of states) of a transition system (defined below), being classified into state and path formulae: $\mathrm {Cls}(\varSigma ) = \{\textit{state}, \textit{path}\}$, for every $\varSigma \in |\mathrm {\mathbb {S}ig} | = |\mathrm {\mathbb {S}et} |$.

We define the functor $\mathrm {Sen}$, and the natural transformation $\kappa$ simultaneously, describing the sentences of a signature and their classes:

• the atomic propositions $a \in \varSigma$ are sentences of class $\textit{state}$,

• $\text {init}$ is a proposition of class $\textit{state}$,

• $\varphi _1 \wedge \varphi _2$ is a sentence of class $\textit{state}$, for every $\varphi _1, \varphi _2$ sentences of class $\textit{state}$,

• $\lnot \varphi$ is a sentence of class $\textit{state}$, for every sentence $\varphi$ of class $\textit{state}$,

• $\exists \pi , \forall \pi$ are sentences of class $\textit{state}$, for every sentence $\pi$ of class $\textit{path}$,

• $\bigcirc \varphi$ is a sentence of class $\textit{path}$, for every sentence $\varphi$ of class $\textit{state}$,

• $\varphi _1 \mathsf {U} \varphi _2$ is a sentence of class $\textit{path}$, for every $\varphi _1, \varphi _2$ sentences of class $\textit{state}$.

The models of a $\underline{\mathrm {CTL}}$ signature $\varSigma$ are transition systems $\mathrm {TS} = (S, \rightarrow , I, L)$, where $S$ is a set of states, ${\rightarrow } \subseteq S \times S$ is a transition relation, $I \subseteq S$ is a set of initial states, and $L :S \rightarrow 2^{\varSigma }$ is a labelling function. We define a transition system morphism $h :(S,\rightarrow ,I,L) \rightarrow (S',\rightarrow ',I',L')$ as a function $h :S \rightarrow S'$ such that $h(I) \subseteq I', \ h({\rightarrow }) \subseteq {\rightarrow '},$ and $L(s) = L'(h(s))$, for every $s \in S$.

The stratification of models is defined as follows:

• $[\![\mathrm {TS} ]\!]_{\varSigma ,\textit{state}}$ is the set $S$ of states of $\mathrm {TS}$,

• $[\![\mathrm {TS} ]\!]_{\varSigma ,\textit{path}}$ is the set of paths of $\mathrm {TS}$, that is sequences $s_0,s_1,\cdots \in S^{\omega },$ such that $s_i \rightarrow s_{i+1}$ for $i \in \omega$.

For every signature morphism $\phi :\varSigma \rightarrow \varSigma '$, the components of the natural transformations $[\![\_ ]\!]_{\phi ,c}$ are identity functions:

$$\begin{aligned}{}[\![\mathrm {TS}' ]\!]_{\phi ,\textit{state}}(s') = s', \quad [\![\mathrm {TS}' ]\!]_{\phi ,\textit{path}}(p') = p', \end{aligned}$$

for every $s' \in [\![\mathrm {TS}' ]\!]_{\varSigma ',\textit{state}}, \ p' \in [\![\mathrm {TS}' ]\!]_{\varSigma ',\textit{path}}, \text { and } \mathrm {TS}' \in |\mathrm {Mod}(\varSigma ') |$.

The satisfaction relation between models and sentences is given by:

• $\mathrm {TS} \models ^{s}_{\varSigma ,\textit{state}} \rho \quad \text { iff }$

  • $\rho \in L(s)$, for $\rho \in \varSigma$

  • $s \in I$, for $\rho = \mathrm {init}$

  • $\mathrm {TS} \not \models ^{s}_{\varSigma ,\textit{state}} \varphi$, for $\rho = \lnot \varphi$

  • $\mathrm {TS} \models ^{s}_{\varSigma ,\textit{state}} \varphi _1$ and $\mathrm {TS} \models ^{s}_{\varSigma ,\textit{state}} \varphi _2$, for $\rho = \varphi _1 \wedge \varphi _2$

  • there is $p = s_0,s_1,\cdots \in [\![\mathrm {TS} ]\!]_{\varSigma ,\textit{path}}$ with $s_0 = s$ such that $\mathrm {TS} \models ^{p}_{\varSigma ,\textit{path}} \pi$, for $\rho = \exists \pi ,$

• $\mathrm {TS} \models ^{p}_{\varSigma ,\textit{path}} \rho \quad \text { iff }$

  • $\mathrm {TS} \models ^{s_1}_{\varSigma ,\textit{state}} \varphi$, for $\rho = \bigcirc \varphi$

  • there exists an index $j$ such that $\mathrm {TS} \models ^{s_j}_{\varSigma ,\textit{state}} \varphi _2$, and for all $i < j$, $\mathrm {TS} \models ^{s_i}_{\varSigma ,\textit{state}} \varphi _1$, for $\rho = \varphi _1 \textsf {U} \varphi _2$,

for every signature $\varSigma$, every state $s \in S$, every path $p = s_0,s_1,\cdots$, every sentence $\rho$ and every model $\mathrm {TS} \in |\mathrm {Mod}(\varSigma ) |$.

3.2 Matching Logic

The original notion of matching logic developed in [18] can be described as a stratified institution with classes $\underline{\mathrm {ML}}$ as follows.

Signatures. The signatures of $\underline{\mathrm {ML}}$ are algebraic signatures.

Example

Let us consider the specification of the IMP programming language exemplified in Listing 1.1. The signature of the $\textsc {IMP-SYNTAX}$ module is obtained by adding to the built-in syntactic categories and their corresponding semantic operations new sorts and operation symbols introduced by the syntax keyword. For example, in the fragment of the syntax module below, the AExp sort is introduced as a supersort of the Int and Id sorts.¹ Addition and division are defined as binary operations with arguments and results of sort AExp, while bracketing is defined as a unary operation of the same sort. We note that only the bracket attribute has an effect on the signature of the specification as it determines the removal of its corresponding symbol of operation from the signature. The left and strict attributes are only used in parsing programs and in refining the evaluation strategy (by sequencing computational tasks), and thus, they do not play a role in defining the signature.

The signature of the fragment above is $\textsc {AExp}^{\mathrm {\mathbb {S}ig}} = (S\cup {S_{\textsc {BUILT-IN}}}, F \cup F_{\textsc {BUILT-IN}}),$ where $S_{\textsc {BUILT-IN}}$ and $F_{\textsc {BUILT-IN}}$ are the built-in sorts and operations, $S = \{ \text {AExp}\}$ and $F_{AExp \, AExp \rightarrow AExp} = \{ \_+\_ , \ \_/\_ \}$. Similarly, the signature of the $\textsc {IMP}$ module is obtained from the signature of the imported module $\textsc {IMP-SYNTAX}$, extending its signature through the addition of the sorts T, K, State and KResult and the operations $\langle k \rangle \_ \langle /k\rangle \in F_{\text {Pgm} \rightarrow \text {K}}$,² $\langle \text {state}\rangle \_ \langle /\text {state}\rangle \in F_{\text {Map} \rightarrow \text {State}}$ and $\langle \text {t}\rangle \_ \langle /\text {t}\rangle \in F_{\text {K} \, \text {State} \rightarrow \text {T}}$ introduced by the keyword configuration.

Classes of a Signature. Every algebraic signature $(S,F)$ determines (through the functor $\mathrm {Cls}$) the set of classes $S$, that is the set of its sorts. Similarly, every morphism $\phi :(S,F) \rightarrow (S',F')$ determines a translation of classes $\phi ^{\mathrm {st}} :S \rightarrow S'$.

Sentences. The sentences (or patterns) in $\underline{\mathrm {ML}}$ of given sorts are defined as follows: for every signature $\varSigma$, $\mathrm {Sen}(\varSigma )$ is the least set that contains basic patterns (terms over $\varSigma$, see [18]) and that is closed under the Boolean connectives $\lnot , \wedge$, and the existential quantifier $\exists$.

• For each $s \in S$, the basic patterns of sort $s$ are first-order $\varSigma$-terms of sort $s$.

• For every pattern $\pi$ of sort s, $\lnot \pi$ is a pattern of sort $s$.

• For every two patterns $\pi _1, \pi _2$ of sort $s$, $\pi _1 \wedge \pi _2$ is a pattern of sort $s$.

• For every variable $x$ of sort $s$ (defined formally as a tuple $\langle x, s, \varSigma \rangle$, where $x$ is the name of the variable, and $s$ is its sort), and every pattern $\pi \in \mathrm {Sen}(S,F \uplus \{x\,\mathord {:}\,{s}\})$, $\exists x \,\mathord {:}\,s. \pi$ is a pattern in $\mathrm {Sen}(\varSigma )$.

The sentence translation along a signature morphism $\phi :\varSigma \rightarrow \varSigma '$ is defined similarly to the translation of first-order sentences. For instance, for basic patterns $\pi$ of sort $s$, $\mathrm {Sen}(\phi )(\pi ) = \phi ^{\mathrm {tm}}_{s}(\pi )$, where $\phi ^{\mathrm {tm}}$ is the extension of $\phi$ to terms that maps $\sigma (t_1,\cdots ,t_n) \,\mathord {:}\,s$ to $\phi ^{\mathrm {op}}(\sigma )(\phi ^{\mathrm {tm}}(t_1), \cdots , \phi ^{\mathrm {tm}}(t_n)) \,\mathord {:}\,\phi ^{\mathrm {st}}(s)$, for every $\sigma \in F_{s_1 \cdots s_n \rightarrow s}$, and term $t_i$ of sort ${s_i}$.

Example

We can give as examples of sentences of an $\underline{\mathrm {ML}}$-signature, the patterns matched in the $\mathbb {K}$ rules corresponding to the IMP programming language specification presented in Listing 1.1: $\text {I}1{:}{Int} + \text {I}2{:}{Int}$, $\text {I}1{:}{Int} / \text {I}2{:}{Int} \wedge \text {I}2 {=}{/}{=} 0$.

Classes of Sentences. The class of a pattern is given by its sort through the natural transformation $\kappa :\mathrm {Sen}\Rightarrow \mathrm {Cls}$ that is defined inductively on the structure of sentences:

• $\kappa _{(S,F)}(\pi ) = s$, for every basic pattern $\pi \in (T_{\varSigma })_{s}$,

• $\kappa _{(S,F)}(\lnot \pi ) = \kappa _{(S,F)}(\pi )$, for every pattern $\pi$,

• $\kappa _{(S,F)}(\pi _1 \wedge \pi _2) = \kappa _{(S,F)}(\pi _1) = \kappa _{(S,F)}(\pi _2)$, for every two patterns $\pi _1,\pi _2$,

• $\kappa _{(S,F)}(\exists x \,\mathord {:}\,s. \pi ) = \kappa _{(S,F \uplus \{x \,\mathord {:}\,s\})}(\pi )$, for every pattern $\pi$.

Models. The models of $\underline{\mathrm {ML}}$ are multialgebras [13]. These are generalisations of algebras having non-deterministic operations that return sets of possible values; that is, multialgebras interpret operation symbols from the carrier set of their arity to the powerset of the carrier set of their sort. For a signature $\varSigma = (S, F)$, a multialgebra homomorphism $h :M \rightarrow N$ is a family of functions indexed by the signature’s sorts $\{h_s :M_s \rightarrow N_s \mid s \in S\}$, such that $h_s(M_\sigma (m_1,\cdots ,m_n)) \subseteq N_\sigma (h_{s_1}(m_1),\cdots ,h_{s_n}(m_n))$, for every $\sigma \in F_{s_1 \cdots s_n \rightarrow s}$ and every $m_i \in M_{s_i}$.

Stratification. The stratification of models is given, for every signature $\varSigma$ and class $s$ of $\varSigma$, by $[\![M ]\!]_{\varSigma ,s} = M_s$, and for every signature morphism $\phi :\varSigma \rightarrow \varSigma '$, class $s$ of $\varSigma$ and model $M'$ of $\varSigma '$, by $[\![M' ]\!]_{\phi ,s}(m') = m'$, where $m' \in M'_{\phi ^{\mathrm {st}(s)}}$.

Satisfaction Relation. The satisfaction relation is based on the interpretation of patterns in models. For any multialgebra $M$, we define $M_{\pi }$, the interpretation of a pattern $\pi$ in $M$, inductively, as follows:

• for every pattern $\pi \in F_{\lambda \rightarrow s}$, $M_\pi$ is the interpretation of the constant $\pi$,

• $M_\pi = \bigcup \{ M_{\sigma }(m_1,\cdots ,m_n) \mid m_i \in M_{t_i}\}$, for every basic pattern $\sigma (t_1,\cdots ,t_n)$,

• $M_\pi = M_s \setminus M_{\pi _1}$, for every pattern $\pi = \lnot \pi _1$, where $\pi _1$ is a pattern of sort $s$,

• $M_\pi = M_{\pi _1} \cap M_{\pi _2}$, for every pattern $\pi = \pi _1 \wedge \pi _2$,

• $M_\pi = \bigcup \{(M,X)_{\pi _1} \mid X \subseteq M_t \}$, for every pattern $\pi = \exists x \,\mathord {:}\,t. \pi _1$, where $\pi _1$ is a pattern of sort $s$, and $(M,X)$ is the expansion of $M$ along the inclusion $(S,F) \subseteq (S,F \uplus \{x\,\mathord {:}\,{t}\})$ given by $(M,X)_{x} = X$.

We now have all the necessary concepts for defining the satisfaction relation:

$$\begin{aligned} M \models _{\varSigma ,s}^{m} \pi \quad \text { iff } \quad m \in M_{\pi }. \end{aligned}$$

Proposition 2

For every signature morphism $\phi :\varSigma \rightarrow \varSigma '$, sort $s \in \mathrm {Cls}(\varSigma )$, multialgebra $M' \in \mathrm {Mod}(\varSigma ')$, state $m' \in [\![M' ]\!]_{\varSigma ', \mathrm {Cls}(\phi )(s)}$, and pattern $\pi$ of sort $s$

$$ \mathrm {Mod}(\phi )(M') \models ^{[\![M' ]\!]_{\phi ,s}(m')}_{\varSigma ,s} \pi \quad \text { iff } \quad M' \models _{\varSigma ',\mathrm {Cls}(\phi )(s)}^{m'} \mathrm {Sen}(\phi )(\pi ). $$

In order to formalise the $\mathbb {K}$ framework we should interpret the variables in a deterministic manner. For example, in the specification of the IMP language, the variables in the patterns matched by the semantic rules have a deterministic interpretation: the variables $\text {I}1, \text {I}2$ and $\text {T}$ of the patterns $\text {I}1:Int + \text {I}2:Int$, $\text {!} \ \text {T}:Bool$ are interpreted as sole elements of sort Int or Bool respectively, as opposed to the interpretation of variables in $\underline{\mathrm {ML}}$ as sets of elements.

Matching Logic with Deterministic Variables $\mathbf ( \underline{\mathrm{ML}}^+\mathbf )$. We refine the above definition of matching logic $\underline{\mathrm {ML}}= (\mathrm {\mathbb {S}ig}, \mathrm {Cls}, \mathrm {Sen}, \kappa , \mathrm {Mod}, [\![\_ ]\!], \models )$, by interpreting the variables in a deterministic way, as presented in [18].

$\underline{\mathrm {ML}}^{+}$ is defined as a stratified institution with classes, whose category of signatures is denoted by $\mathrm {\mathbb {S}ig}^{+}$. Its objects are tuples $(S,F,D)$, where $(S,F)$ and $(S,D)$ are algebraic signatures of $\underline{\mathrm {ML}}$, such that $F_{w \rightarrow s} \cap D_{w \rightarrow s} = \emptyset$ for every $w \in S^{*}$, and $s \in S$. For signatures $\varSigma = (S,F,D) \text { and } \varSigma ' = (S',F',D')$, a signature morphism $\phi :\varSigma \rightarrow \varSigma '$ is a tuple $(\phi ^{\mathrm {st}}, \phi ^{\mathrm {op}}, \phi ^{\mathrm {det}})$, where the pairs $(\phi ^{\mathrm {st}},\phi ^{\mathrm {op}})$ and $(\phi ^{\mathrm {st}},\phi ^{\mathrm {det}})$ are signature morphisms in $\mathrm {\mathbb {S}ig}$.

We define the functor $\mathrm {U}:\mathrm {\mathbb {S}ig}^{+} \rightarrow \mathrm {\mathbb {S}ig}$ by $\mathrm {U}(S,F,D) = (S, F \cup D)$ for signatures, and by $\mathrm {U}(\phi ) = ( \phi ^{\mathrm {st}}, \phi ^{\mathrm {op}} \cup \phi ^{\mathrm {det}})$ for signature morphisms. The classes and the sentences of a signature are given by the functor compositions $\mathrm {Cls}^{+} = \mathrm {U}\mathbin {;}\mathrm {Cls}$, and $\mathrm {Sen}^{+} = \mathrm {U}\mathbin {;}\mathrm {Sen}$³ respectively. The classes of sentences are determined by the composition $\mathrm {U}\cdot \kappa :\mathrm {Sen}^{+} \rightarrow \mathrm {Cls}^{+}$ of the functor $\mathrm {U}$ with the natural transformation $\kappa$, that is, $(U \cdot \kappa )_{\varSigma } = \kappa _{\mathrm {U}(\varSigma )}$, for every signature $\varSigma$.

The models of $\underline{\mathrm {ML}}^{+}$ are determined by the functor $\mathrm {Mod}^{+} :(\mathrm {\mathbb {S}ig}^{+})^{\mathrm {op}} \rightarrow \mathrm {\mathbb {C}at}$, that assigns to each signature $\varSigma = (S,F,D)$ the full subcategory of $\mathrm {Mod}(\mathrm {U}(\varSigma ))$ consisting of the models $M$ in which every operation symbol in $D$ is interpreted in a deterministic way. For every signature morphism $\phi :\varSigma \rightarrow \varSigma '$ and every model $M' \in |\mathrm {Mod}^{+}(\varSigma ') |$, we define $\mathrm {Mod}^{+}(\phi )(M')$ as $\mathrm {Mod}(\mathrm {U}(\phi ))(M')$. Notice that the functor $\mathrm {Mod}^{+}$ is well-defined, as $|\mathrm {Mod}(\mathrm {U}(\phi ))(M')_{\sigma }(m_1,\cdots ,m_n) | = |M'_{\phi ^{\mathrm {det}}(\sigma )}(m_1,\cdots ,m_n) | = 1$ for every operation symbol $\sigma$ of $D$.

The stratification of models is defined just as in the case of $\underline{\mathrm {ML}}$:

• $[\![\_ ]\!]^{+}_{\varSigma ,c} :\mathrm {Mod}^{+}(\varSigma ) \rightarrow \mathrm {\mathbb {S}et}$ maps every model $M$ to $[\![M ]\!]_{\mathrm {U}(\varSigma ), c}$

• $[\![M ]\!]^{+}_{\phi ,c} :[\![M ]\!]^{+}_{\varSigma ',\mathrm {Cls}^{+}(\phi )(c)} \rightarrow \mathrm {Mod}^{+}(\phi ) \mathbin {;}[\![M ]\!]^{+}_{\varSigma ,c}$ maps every state $m$ to the state $[\![M ]\!]_{\mathrm {U}(\phi ),c}(m)$, for every morphism $\phi :\varSigma \rightarrow \varSigma '$ and class $c$ of $\varSigma$.

Finally, the satisfaction relation between models and sentences is defined analogously to the satisfaction relation of $\underline{\mathrm {ML}}$. As a result, it holds for example, that for any basic pattern $\pi$, any signature $\varSigma \in \mathrm {\mathbb {S}ig}^{+}$, any class $c \in \mathrm {Cls}^{+}(\varSigma )$, and any model $M \in |\mathrm {Mod}^{+}(\varSigma ) |$, $M (\models ^{\underline{\mathrm {ML}}^{+}})^{m}_{\varSigma ,c} \pi \quad \text { iff } \quad M (\models ^{\underline{\mathrm {ML}}})^{m}_{\mathrm {U}(\varSigma ),c} \pi .$ We note, however, that the satisfaction relation of $\underline{\mathrm {ML}}^{+}$ is not a restriction of the satisfaction relation of $\underline{\mathrm {ML}}$. For example, if $\pi$ were an existentially quantified pattern $\exists x \,\mathord {:}\,{t}.\pi _1$, then only the converse implication of the above equivalence would be ensured to hold. This follows because in $\underline{\mathrm {ML}}$ every expansion of $M$ may interpret in a non-deterministic manner the variable $x \,\mathord {:}\,{t}$; in order words, there is no guarantee that there exists an expansion of $M$ in $\underline{\mathrm {ML}}$ that satisfies $\pi$ and is also a model of $\underline{\mathrm {ML}}^{+}$.

3.3 Encoding Matching Logic into First-Order Logic

There exists a comorphism of institutions between $\flat \mathbf {ML}^{+}$, the institution obtained from $\underline{\mathrm {ML}}^{+}$ following Proposition 1, and $\mathbf {FOL}$, the institution of first-order logic. In short, the deterministic operations of any given $\flat \mathbf {ML}^{+}$-signature are preserved by the signature-translation component of the comorphism, while each non-deterministic operation is transformed into a new predicate. In this manner, the interpretation of first-order predicates corresponds to the interpretation of non-deterministic operations in multialgebras. Furthermore, the underlying sentence-translation map of the comorphism encodes each matching pattern to a corresponding universally quantified sentence over states having the same class as the pattern. We define $(\varPhi , \alpha , \beta ) :\flat \mathbf {ML}^{+} \rightarrow \mathbf {FOL}$ as follows:

For Signatures: The underlying signature functor $\varPhi :\mathrm {\mathbb {S}ig}^{\flat \mathbf {ML}^{+}} \rightarrow \mathrm {\mathbb {S}ig}^{\mathbf {FOL}}$ maps

• every $\flat \mathbf {ML}^{+}$ signature $\varSigma = (S, F, D)$ to the $\mathbf {FOL}$ signature $\varSigma ' = (S',F',P')$ where $S' = S$, $F'_{w \rightarrow s} = D_{w \rightarrow s}$, $P'_{\lambda } = \emptyset$, and $P'_{ws} = F_{w \rightarrow s}$ for $ws \ne \lambda$.

• every $\flat \mathbf {ML}^{+}$-signature morphism $\phi :\varSigma _1 \rightarrow \varSigma _2$ to the $\mathbf {FOL}$-signature morphism $\phi ' = (\phi '^{\mathrm {st}}, \phi '^{\mathrm {op}}, \phi '^{\mathrm {rel}})$, where $\phi '^{\mathrm {st}} = \phi ^{\mathrm {st}}$, $\phi '^{\mathrm {op}} = \phi ^{\mathrm {det}}$, and $\phi '^{\mathrm {rel}}_{ws} = \phi ^{\mathrm {op}}_{w \rightarrow s}, \text { for } ws \ne \lambda .$

For Models: The model functor $\beta _\varSigma :\mathrm {Mod}^{\mathbf {FOL}}(\varPhi (\varSigma )) \rightarrow \mathrm {Mod}^{\flat \mathbf {ML}^{+}}(\varSigma )$ given by a signature $\varSigma = (S,F,D)$ maps

• every first-order structure $M'$ for $\varPhi (\varSigma )$ to the multialgebra $M$ whose carrier sets $M_s$ are defined as $M'_s$ for every sort $s \in S$, whose interpretations $M_\sigma :M_{s_1} \times \cdots \times M_{s_n} \rightarrow 2^{M_s}$ of function symbols $\sigma \in F_{s_1\cdots s_n \rightarrow s}$ are defined as $M_\sigma (m_1,\cdots ,m_n) = \{m \in M_s \mid (m_1,\cdots ,m_n,m) \in M'_\sigma \}$, and whose interpretations $M_\sigma$ of function symbols $\sigma \in D_{w \rightarrow s}$ are given by the composition of $M'_{\sigma }$ with the singleton-forming map $\{ \_ \} :M_s \rightarrow 2^{M_s}$, and

• every morphism of first-order structures $h' :M' \rightarrow N'$ in $\mathrm {Mod}^{\mathbf {FOL}}(\varPhi (\varSigma ))$ to a multialgebra morphism $h :\beta _{\varSigma }(M') \rightarrow \beta _{\varSigma }(N')$ given by $h_s = h'_s$, for every $s \in S$. We note that the fact that $h'$ commutes with the interpretation of operation symbols suits the deterministic nature of the morphism $h$ for the interpretation of operations in $D$, while its compatibility with the interpretation of predicate symbols guarantees the satisfaction of the morphism condition for multialgebras.

For Sentences: The sentence translation $\alpha _{\varSigma } :\mathrm {Sen}^{\flat \mathbf {ML}^{+}}(\varSigma ) \rightarrow \mathrm {Sen}^{\mathbf {FOL}}(\varPhi (\varSigma ))$ given by a signature $\varSigma = (S, F, D)$ maps every $\varSigma$-pattern $\pi$ to the sentence $\alpha _{\varSigma }(\pi ) = \forall m\,\mathord {:}\,{s}. \mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma }(\pi ),$ where $s = \kappa _{\varSigma }(\pi )$, $m$ is a first-order variable of sort $s$ for the signature $\varPhi (\varSigma )$, and $\mathrm {FOL}^{m \,\mathord {:}\,{s}}_{\varSigma } :\kappa ^{-1}_{\varSigma }(s) \rightarrow \mathrm {Sen}^{\mathbf {FOL}}(\varPhi (\varSigma ) \uplus \{m\,\mathord {:}\,{s}\})$ is the sorted translation of sentences defined as follows:

• We begin with a notation: for every operation symbol $\sigma \in (F \cup D)_{s_1,\cdots ,s_n \rightarrow s}$, and every variables $m_i \,\mathord {:}\,{s_i}$ and $m \,\mathord {:}\,{s}$, we denote by $\sigma ^{=}(m_1,\cdots ,m_n,m)$ either the relational atom $\sigma (m_1,\cdots ,m_n,m)$ if $\sigma \in F$, or the equational atom $\sigma (m_1,\cdots ,m_n) = m$ if $\sigma \in D$.

• for every basic pattern $\pi \in (F \cup D)_{\lambda \rightarrow s}$, $\mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma } (\pi ) = \pi ^{=}(m),$

• for every basic pattern $\pi = \sigma (t_1,\cdots ,t_n)$, with $\sigma \in (F\cup D)_{s_1,\cdots ,s_n \rightarrow s}$,

  $$\begin{aligned} \mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma } (\pi ) = \exists m_1\,\mathord {:}\,{s_1} \cdots \exists m_n\,\mathord {:}\,{s_n}.&\mathrm {FOL}^{m_1\,\mathord {:}\,{s_1}}_{\varSigma }(t_1) \wedge \cdots \wedge \mathrm {FOL}^{m_n\,\mathord {:}\,{s_n}}_{\varSigma }(t_n) \\&\wedge \sigma ^{=}(m_1,\cdots ,m_n,m),\end{aligned}$$

• for every pattern $\pi = \lnot \pi _1$, $\mathrm {FOL}_{\varSigma }^{m\,\mathord {:}\,{s}}(\lnot \pi _1) = \lnot \mathrm {FOL}_{\varSigma }^{m\,\mathord {:}\,{s}}(\pi _1),$

• for every pattern $\pi = \pi _1 \wedge \pi _2$, $\mathrm {FOL}_{\varSigma }^{m\,\mathord {:}\,{s}}(\pi _1 \wedge \pi _2) = \mathrm {FOL}_{\varSigma }^{m\,\mathord {:}\,{s}}(\pi _1) \wedge \mathrm {FOL}_{\varSigma }^{m\,\mathord {:}\,{s}}(\pi _2),$

• for every pattern $\pi = \exists x\,\mathord {:}\,{t}. \pi _1$, where $\pi _1 \in \mathrm {Sen}^{\flat \mathbf {ML}^{+}}(\varSigma \uplus \{x\,\mathord {:}\,{t}\})$, we have $\mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma }(\exists x\,\mathord {:}\,{t}.\pi _1) = \exists x\,\mathord {:}\,{t}.\xi _{\varSigma }(\mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma \uplus \{x\,\mathord {:}\,{t}\}}(\pi _1)),$ where $\xi _{\varSigma }$ is a first-order signature morphism from $\varPhi (\varSigma \uplus \{x\,\mathord {:}\,{t}\}) \uplus \{m \,\mathord {:}\,{s}\}$ to $\varPhi (\varSigma ) \uplus \{m\,\mathord {:}\,{s}\} \uplus \{x\,\mathord {:}\,{t}\}$ defined as the extension of $1_{\varPhi (\varSigma )}$ that maps the matching-logic variable $x\,\mathord {:}\,{t}$ for the signature $\varSigma$ to the first-order variable $x\,\mathord {:}\,{t}$ for the signature $\varPhi (\varSigma ) \uplus \{m\,\mathord {:}\,{s}\}$, and the first-order variable $m\,\mathord {:}\,{s}$ for the signature $\varPhi (\varSigma \uplus \{x\,\mathord {:}\,{t}\})$ to the first-order variable $m\,\mathord {:}\,{s}$ but for the signature $\varPhi (\varSigma )$.⁴

The naturality of $\alpha$ results from an analogous property for $\mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma }$.

Proposition 3

For every two $\flat \mathbf {ML}^{+}$ signatures $\varSigma _1, \ \varSigma _2$, signature morphism $\phi :\varSigma _1 \rightarrow \varSigma _2$, and variable $m \,\mathord {:}\,{s}$ for $\varSigma _1$, the following diagram commutes.

Satisfaction Condition. In order to show that the definitions of the components of the comorphism given above guarantee that the satisfaction condition holds, it suffices to know that Proposition 4 holds.

Proposition 4

For every $\flat \mathbf {ML}^{+}$ signature $\varSigma$, every first-order structure $M$ for $\varPhi (\varSigma )$, and every $\varSigma$-pattern $\pi$ of sort $s$, $M_{\mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma }(\pi )} = {\beta _{\varSigma }(M)}_{\pi }.$

This can be easily shown by induction on the structure of $\pi$, starting with the base case of patterns $\pi \in F_{\lambda \rightarrow s}$, for which $M_{\mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma }(\pi )}$ is the set of states $m \in M_s$ such that $(M, m) \models \pi (m)$, that is $M_{\pi }$, and, by definition, $\beta _{\varSigma }(M)_{\pi } = M_{\pi }$.

4 Reachability Logic

In order to capture reachability logic [21] as an institution, we first define an abstract, parameterised institution over an arbitrary stratified institution with classes, which necessarily has to enjoy properties such as the existence of a quantification space, model amalgamation, and preservation of pushouts by the class functor. We then obtain the concrete version of reachability logic that underlies the $\mathbb {K}$ framework by instantiating the parameter of the abstract version with $\underline{\mathrm {ML}}^{+}$, the stratified institution with classes of matching logic, which we show to satisfy the desired properties.

4.1 Abstract Reachability Logic

We formalise reachability logic in two steps: we begin by describing a sub-institution of reachability logic whose sentences are all atomic (reachability atoms), and we subsequently extend it by adding logical connectives and quantifiers through a general universal-quantification construction.

To define atomic abstract reachability logic we first describe it as a pre-institution [22] whose construction is based upon a stratified institution with classes. This amounts to defining the same elements as those comprised by an institution but without imposing the requirement of the satisfaction condition.

Throughout this section we assume an arbitrary, but fixed stratified institution with classes $\underline{\mathrm {M}}= (\mathrm {\mathbb {S}ig}^{\underline{\mathrm {M}}}, \mathrm {Cls}^{\underline{\mathrm {M}}}, \mathrm {Sen}^{\underline{\mathrm {M}}}, \mathrm {Mod}^{\underline{\mathrm {M}}}, [\![\_ ]\!]^{\underline{\mathrm {M}}}, \models ^{\underline{\mathrm {M}}})$. This serves as a parameter for all the constructions below.

Signatures. The category of signatures of atomic abstract reachability logic, denoted by $\mathrm {\mathbb {S}ig}^{\mathbf {ARL}(\underline{\mathrm {M}})}$, is the same as the category of signatures of $\underline{\mathrm {M}}$.

Sentences. For every signature $\varSigma$, $\mathrm {Sen}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\varSigma )$ is the set of pairs of sentences of the stratified institution with classes, denoted by $\pi _1 \Rightarrow \pi _2$, where $\pi _1, \pi _2 \in \mathrm {Sen}^{\underline{\mathrm {M}}}(\varSigma )$. The translation of such a sentence $\pi _1 \Rightarrow \pi _2$ along a signature morphism $\phi :\varSigma \rightarrow \varSigma '$ is defined as the pair of its translated components according to $\mathrm {Sen}^{\underline{\mathrm {M}}}(\phi )$: $\mathrm {Sen}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\phi )(\pi _1 \Rightarrow \pi _2) = \mathrm {Sen}^{\underline{\mathrm {M}}}(\phi )(\pi _1) \Rightarrow \mathrm {Sen}^{\underline{\mathrm {M}}}(\phi )(\pi _2).$

Example

If we instantiate the parameter $\underline{\mathrm {M}}$ with the stratified institution with classes $\underline{\mathrm {ML}}^{+}$, the sentences of $\mathbf {ARL}(\underline{\mathrm {ML}}^{+})$ will only capture atomic $\mathbb {K}$ semantic rules, i.e. without quantification and side conditions. This means we could only express atomic rules in the specification of the simple imperative programming language IMP, like $\mathbf {rule } \ ! \text { true} => \text {not}_{\text {Bool}} \text { true}$.

Models. The reachability models of a signature $\varSigma$, given by the $\mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}$ functor, are pairs $(M,\leadsto )$ of $\varSigma$-models $M$ of the underlying stratified institution with classes, and families of preorders ${\leadsto _{c}} \subseteq [\![M ]\!]_{\varSigma ,c} \times [\![M ]\!]_{\varSigma ,c}$ indexed by the classes of the signature. The model homomorphisms $h :(M_1, \leadsto _1) \rightarrow (M_2, \leadsto _2)$ are defined as the morphisms between the $\underline{\mathrm {M}}$-models $M_1$ and $M_2$ that preserve the preorders: for every $c \in \mathrm {Cls}(\varSigma )$, the function $[\![h ]\!]_{\varSigma ,c}$ from $([\![M_1 ]\!]_{\varSigma ,c}, \leadsto _1)$ to $([\![M_2 ]\!]_{\varSigma ,c},\leadsto _2)$ is monotone. This allows $\mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\varSigma )$ to inherit the identities and the composition of model homomorphisms of $\mathrm {Mod}^{\underline{\mathrm {M}}}(\varSigma )$.

The model reduct $\mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\phi ) :\mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\varSigma ') \rightarrow \mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\varSigma )$ given by a signature morphism $\phi :\varSigma \rightarrow \varSigma '$ is defined as

• $\mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\phi )(M', \leadsto ') = (\mathrm {Mod}^{\underline{\mathrm {M}}}(\phi )(M'),\leadsto )$ for every $\varSigma '$-model $(M', \leadsto ')$, where $\leadsto _{c} \subseteq [\![M'\mathord {\upharpoonright }_{\phi } ]\!]_{\varSigma ,c} \times [\![M'\mathord {\upharpoonright }_{\phi } ]\!]_{\varSigma ,c}$ is the reflexive and transitive closure of $[\![M' ]\!]_{\phi ,c}(\leadsto '_{\phi (c)})$, which will be further denoted by $\rightarrow _c$,

• $\mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\phi )(h')$ is simply $\mathrm {Mod}^{\underline{\mathrm {M}}}(\phi )(h')$ for every two $\varSigma '$-models $M'_1, M'_2$, and every model homomorphism $h' :(M'_1, \leadsto '_1) \rightarrow (M'_2, \leadsto '_2)$.

Satisfaction Relation. The satisfaction relation between any model $(M,\leadsto )$ and any sentence $\pi _1 \Rightarrow \pi _2$ is defined as follows: $(M,\leadsto ) \models ^{\mathbf {ARL}(\underline{\mathrm {M}})}_{\varSigma } \pi _1 \Rightarrow \pi _2$ if and only if for every $m \in [\![M ]\!]_{\varSigma ,c}$ such that $M (\models ^{\underline{\mathrm {M}}})^{m}_{\varSigma ,c} \pi _1$, there exists $n \in [\![M ]\!]_{\varSigma ,c}$ such that $M (\models ^{\underline{\mathrm {M}}})^{n}_{\varSigma ,c} \pi _2$, and $m \leadsto _c n$.

Corollary 1

$\mathbf {ARL}(\underline{\mathrm {M}}) = (\mathrm {\mathbb {S}ig}^{\mathbf {ARL}(\underline{\mathrm {M}})}, \mathrm {Sen}^{\mathbf {ARL}(\underline{\mathrm {M}})}, \mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}, \models ^{\mathbf {ARL}(\underline{\mathrm {M}})})$ is a pre-institution.

The direct implication of the satisfaction condition holds unconditionally.

Proposition 5

For every signature morphism $\phi :\varSigma \rightarrow \varSigma '$, every class $c \in \mathrm {Cls}(\varSigma )$, every model $(M',\leadsto ') \in |\mathrm {Mod}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\varSigma ') |$, and every sentence $\pi _1 \Rightarrow \pi _2$,

$$\begin{aligned} (M',\leadsto ') \models ^{\mathbf {ARL}(\underline{\mathrm {M}})}_{\varSigma '} \phi (\pi _1 \Rightarrow \pi _2) \text { implies } (M',\leadsto ')\mathord {\upharpoonright }_{\phi } \models ^{\mathbf {ARL}(\underline{\mathrm {M}})}_{\varSigma } \pi _1 \Rightarrow \pi _2. \end{aligned}$$

The converse of Proposition 5 holds if the stratification of the underlying institution of $\mathbf {ARL}(\underline{\mathrm {M}})$ satisfies a property similar to that of lifting relations from [7, Chapter 9].

Proposition 6

If in $\mathbf {ARL}(\underline{\mathrm {M}})$, for every signature morphism $\phi :\varSigma \rightarrow \varSigma '$, every class $c \in \mathrm {Cls}(\varSigma )$, every $\varSigma '$-model $(M',\leadsto ')$, and every states $m' \in [\![M' ]\!]_{\varSigma ',\phi (c)}$ and $n \in [\![M'\mathord {\upharpoonright }_{\phi } ]\!]_{\varSigma ,c}$ such that $[\![M' ]\!]_{\phi , c}(m') \leadsto _c n$, there exists $n' \in [\![M' ]\!]_{\varSigma ',\phi (c)}$ such that $m' \leadsto '_{\phi (c)} n'$ and $[\![M' ]\!]_{\phi , c}(n') = n$, then

$$\begin{aligned} (M',\leadsto ')\mathord {\upharpoonright }_{\phi } \models ^{\mathbf {ARL}(\underline{\mathrm {M}})}_{\varSigma } \pi _1 \Rightarrow \pi _2 \text { implies } (M',\leadsto ') \models ^{\mathbf {ARL}(\underline{\mathrm {M}})}_{\varSigma '} \phi (\pi _1 \Rightarrow \pi _2), \end{aligned}$$

for every sentence $\pi _1 \Rightarrow \pi _2$.

Corollary 2

If the stratified institution with classes $\underline{\mathrm {M}}$ satisfies the hypothesis of Proposition 6, then $\mathbf {ARL}(\underline{\mathrm {M}})$ is an institution.

In most concrete examples of stratified institutions with classes the natural transformations $[\![M' ]\!]_{\phi ,c}$ of the stratification are bijective, or even identities (see for example the definitions of $\underline{\mathrm {ML}}^{+}$ and $\underline{\mathrm {CTL}}$). Therefore, the hypothesis of Proposition 6 is usually satisfied, entailing that $\mathbf {ARL}(\underline{\mathrm {M}})$ is an institution.

We have hitherto defined only an atomic fragment of the desired institution of abstract reachability logic. To describe the construction of the institution with universally quantified Horn-clause sentences over the atomic sentences of $\mathbf {ARL}(\underline{\mathrm {M}})$, we use the notion of quantification space originating from [8].

Definition 7

For any category $\mathrm {\mathbb {S}ig}$ a class of arrows $\mathcal {D} \subseteq \mathrm {\mathbb {S}ig}$ is called a quantification space if, for any $\chi :\varSigma \rightarrow \varSigma ' \in \mathcal {D}$ and $\varphi :\varSigma \rightarrow \varSigma _1$ there exists a designated pushout

with $\chi (\varphi ) \in \mathcal {D}$ and such that the horizontal composition of these designated pushouts is also a designated pushout, i.e. for the pushouts in the diagram below

$\varphi [\chi ] \mathbin {;}\theta [\chi (\varphi )] = (\varphi \mathbin {;}\theta )[\chi ]$ and $\chi (\varphi )(\theta ) = \chi (\varphi \mathbin {;}\theta )$, and such that $\chi (1_{\varSigma }) = \chi$ and $1_{\varSigma }[\chi ] = 1_{\varSigma '}$. A quantification space $\mathcal {D}$ for $\mathrm {\mathbb {S}ig}$ is adequate for a functor $\mathrm {Mod}:\mathrm {\mathbb {S}ig}^{\mathrm {op}} \rightarrow \mathrm {\mathbb {C}at}$ when the aforementioned designated pushouts are weak amalgamation squares for $\mathrm {Mod}$. A quantification space $\mathcal {D}$ for $\mathrm {\mathbb {S}ig}$ is called adequate for an institution if it is adequate for its model functor.

Proposition 7

For any institution $\mathbf {I}$ with an adequate quantification space $\mathcal {D}$, the following data defines an institution, called the institution of universally $\mathcal {D}$-quantified Horn clauses over $\mathbf {I}$, and denoted $\mathbf {HCL}(\mathbf {I})$:

• $\mathrm {\mathbb {S}ig}^{\mathbf {HCL}(\mathbf {I})} = \mathrm {\mathbb {S}ig}^{\mathbf {I}}$,

• $\mathrm {Mod}^{\mathbf {HCL}(\mathbf {I})} = \mathrm {Mod}^{\mathbf {I}}$,

• $\begin{aligned}&\mathrm {Sen}^{\mathbf {HCL}(\mathbf {I})}(\varSigma ) \\&= \{ \forall \chi . \rho '_1 \wedge \cdots \wedge \rho '_n \rightarrow \rho ' \mid (\chi :\varSigma \rightarrow \varSigma ') \in \mathcal {D} \text { and } \rho '_i,\rho ' \in \mathrm {Sen}^{\mathbf {I}}(\varSigma ')\}, \\&\text {for every signature } \varSigma \end{aligned}$

• $\begin{aligned}&\mathrm {Sen}^{\mathbf {HCL}(\mathbf {I})}(\varphi )(\forall \chi . \rho '_1 \wedge \cdots \wedge \rho '_n \rightarrow \rho ') \\&= \forall \chi (\varphi ). \mathrm {Sen}^{\mathbf {I}}(\varphi [\chi ])(\rho '_1) \wedge \cdots \wedge \mathrm {Sen}^{\mathbf {I}}(\varphi [\chi ])(\rho '_n) \rightarrow \mathrm {Sen}^{\mathbf {I}}(\varphi [\chi ])(\rho '), \\&\text {for every signature morphism } \varphi :\varSigma \rightarrow \varSigma _1 \end{aligned}$

• $\begin{aligned}&M \models ^{\mathbf {HCL}(\mathbf {I})}_{\varSigma } \forall \chi . \rho '_1 \wedge \cdots \wedge \rho '_n \rightarrow \rho ' \\&\text { iff for all } \chi \text {-expansions } M' \text { of } M, M' \models ^{\mathbf {I}}_{\varSigma '} \rho ' \text { if } M' \models ^{\mathbf {I}}_{\varSigma '} \rho '_i \text { for } i = \overline{1,n}. \end{aligned}$

To build an institution with universally quantified sentences over $\mathbf {ARL}(\underline{\mathrm {M}})$ as described in Proposition 7, we need to ensure that $\mathbf {ARL}(\underline{\mathrm {M}})$ satisfies its hypothesis. This cannot be guaranteed in general, because $\underline{\mathrm {M}}$ is abstract. Nevertheless, we can obtain an appropriate set of hypotheses for the underlying stratified institution $\underline{\mathrm {M}}$ that allow us to apply Proposition 7:

• the existence of a quantification space for $\mathbf {ARL}(\underline{\mathrm {M}})$ is guaranteed by the existence of a quantification space for $\underline{\mathrm {M}}$, as the categories $\mathrm {\mathbb {S}ig}^{\mathbf {ARL}(\underline{\mathrm {M}})}$ and $\mathrm {\mathbb {S}ig}^{\underline{\mathrm {M}}}$ are equal,

• the fact that $\mathbf {ARL}(\underline{\mathrm {M}})$ has weak model amalgamation follows from the weak model amalgamation property of $\underline{\mathrm {M}}$ (see Definition 8 below) and the preservation of pushouts by the class functor of $\underline{\mathrm {M}}$ (see Proposition 8 below).

Definition 8

A stratified institution with classes $\underline{\mathrm {M}}$ has (weak) model amalgamation whenever its corresponding institution $\flat \mathbf {M}$ has this property.

Proposition 8

For every stratified institution with classes $\underline{\mathrm {M}}$ having (weak) model amalgamation such that its class functor $\mathrm {Cls}$ preserves pushouts, $\mathbf {ARL}(\underline{\mathrm {M}})$ has (weak) model amalgamation.

Corollary 3

If $\underline{\mathrm {M}}$ has an adequate quantification space and a pushout preserving class functor, then $\mathbf {HCL}(\mathbf {ARL}(\underline{\mathrm {M}}))$ is an institution.

4.2 Defining Reachability over Matching Logic

In order to capture reachability logic in its original, concrete form, we must instantiate the parameter of the institution $\mathbf {HCL}(\mathbf {ARL}(\underline{\mathrm {M}}))$ defined above, with the stratified institution $\underline{\mathrm {ML}}^{+}$. To this end, we first point out that by adding variables as deterministic constants to the signatures of $\underline{\mathrm {ML}}^{+}$ we obtain a quantification space. Furthermore, to show that the quantification space is adequate, we use the property of model amalgamation of the comorphism $(\varPhi ,\alpha ,\beta )$ between $\flat \mathbf {ML}^{+}$ and $\mathbf {FOL}$ defined in Sect. 3.3.

Proposition 9

$\underline{\mathrm {ML}}^{+}$ has pushouts of signatures. Moreover, its class functor preserves pushouts.

Example

Let us consider the $\mathbb {K}$ definition of the IMP programming language. By splitting the syntax module into three modules, AExp, BExp and IMP-SYNTAX importing the two expressions modules, we have an immediate and natural example of a pushout of signatures: as both the AExp and BExp modules import the BUILT-IN module containing the built-in sorts and corresponding operations of $\mathbb {K}$, we need to construct the pushout of their signatures in order to obtain the signature of the module IMP-SYNTAX.

Proposition 10

In $\underline{\mathrm {ML}}^{+}$, the family of extensions with deterministic constants forms a quantification space.

The following definition originates from [4].

Definition 9

An institution comorphism $(\varPhi ,\alpha ,\beta ) :\mathbf {I} \rightarrow \mathbf {I}'$ has weak model amalgamation if for every $\mathbf {I}$-signature morphism $\varphi :\varSigma \rightarrow \varSigma '$, every $\varSigma '$-model $M'$, and every $\varPhi (\varSigma )$-model $N$ such that $\beta _{\varSigma }(N) = M'\mathord {\upharpoonright }_{\varphi }$, there exists a $\varPhi (\varSigma ')$-model $N'$ such that $\beta _{\varSigma '}(N') = M'$ and $N'\mathord {\upharpoonright }_{\varPhi (\varphi )} = N$. We say that $(\varPhi ,\alpha ,\beta ) :\mathbf {I} \rightarrow \mathbf {I}'$ has model amalgamation when $N'$ is required to be unique.

Remark 1

$\underline{\mathrm {ML}}^{+}$ has model amalgamation. Let us first note that the comorphism $(\varPhi ,\alpha ,\beta )$ between the institution $\flat \mathbf {ML}^{+}$ and $\mathbf {FOL}$ defined in the previous section has model amalgamation. This property holds trivially since the model reduction functors $\beta _{\varSigma }$ are isomorphisms of categories, for every signature $\varSigma$. As the institution of $\mathbf {FOL}$ also has model amalgamation, we can use a general result of institution theory to deduce that $\flat \mathbf {ML}^{+}$ has model amalgamation.

Corollary 4

$\mathbf {HCL}(\mathbf {ARL}(\underline{\mathrm {ML}}^{+}))$ is an institution.

4.3 Encoding Reachability Logic into First-Order Logic

For any institution $\mathbf {ARL}(\underline{\mathrm {M}})$ defined over a stratified institution with classes $\underline{M}$, there exists a comorphism of institutions between $\mathbf {ARL}(\underline{\mathrm {M}})$ and $\mathbf {FOL}^{\mathrm {pres}}$, the institution of presentations over first-order logic, whenever there exists a comorphism of institutions $(\varPhi , \alpha , \beta )$ between $\flat \mathbf {M}$ and $\mathbf {FOL}$ such that:

• the classes of a signature in $\mathrm {\mathbb {S}ig}^{\flat \mathbf {M}}$ are given by the sorts of its translation to $\mathbf {FOL}$: $\mathrm {Cls}= \varPhi \mathbin {;}\mathrm {St}$, where $\mathrm {St}$ is the forgetful functor $\mathrm {St}:\mathrm {\mathbb {S}ig}^{\mathbf {FOL}} \rightarrow \mathrm {\mathbb {S}et}$,

• for every signature $\varSigma$, $\alpha _{\varSigma }(\pi ) = \forall m \,\mathord {:}\,{s}. \mathrm {FOL}^{m \,\mathord {:}\,{s}}_{\varSigma }(\pi )$, for every $\pi$ of class $s$,⁵

• for every $N \in |\mathrm {Mod}^{\mathbf {FOL}}(\varPhi (\varSigma )) |$, and every $s \in \mathrm {Cls}(\varSigma )$, $N_s = [\![\beta _{\varSigma }(N) ]\!]_{\varSigma ,s}$.

The signature-translation component of the comorphism encodes the reachability relation through the addition of new preorder predicates and corresponding axioms for each class of the signature. The new predicates determine relations on reachable states that define the preorder-family component of a reachability model. The sentence component of the comorphism translates each reachability statement between two patterns to a sentence that expresses the existence of a reachable state for the target pattern for every state of the source pattern. We define the comorphism $(\varPhi ^{R}, \alpha ^{R}, \beta ^{R}) :\mathbf {ARL}(\underline{\mathrm {M}}) \rightarrow \mathbf {FOL}^{\mathrm {pres}}$ as follows:

For Signatures: The signature functor $\varPhi ^{R} :\mathrm {\mathbb {S}ig}^{\mathbf {ARL}(\underline{\mathrm {M}})} \rightarrow \mathrm {\mathbb {S}ig}^{\mathbf {FOL}^{\mathrm {pres}}}$ maps every signature $\varSigma$ of $\mathbf {ARL}(\underline{\mathrm {M}})$ to $\varPhi ^{R}(\varSigma ) = (\mathrm {Reach}(\varSigma ), E),$ where

• $\mathrm {Reach}(\varSigma )$ denotes the first-order signature obtained by adding to $\varPhi (\varSigma ) = (S',F',P')$ a predicate $reach$ of arity $s \, s$ for every sort $s \in S'$, and

• $E$ is a set of axioms that define the predicates $reach$ as preorders: $\{ \forall x \,\mathord {:}\,{s}. reach (x,x), \forall x,y,z \,\mathord {:}\,{s}. reach (x,y) \wedge reach (y,z) \rightarrow reach (x,z) \mid {s \in S'} \}.$

For Sentences: For every signature $\varSigma$ of $\mathbf {ARL}(\underline{\mathrm {M}})$, the sentence translation function $\alpha ^{R}_{\varSigma } :\mathrm {Sen}^{\mathbf {ARL}(\underline{\mathrm {M}})}(\varSigma ) \rightarrow \mathrm {Sen}^{\mathbf {FOL}}(\mathrm {Reach}(\varSigma ))$ maps every $\varSigma$-sentence $\pi _1 \Rightarrow \pi _2$ to $\alpha ^{R}_{\varSigma }(\pi _1 \Rightarrow \pi _2) = \forall m\,\mathord {:}\,{s}.\mathrm {FOL}^{m\,\mathord {:}\,{s}}_{\varSigma }(\pi _1) \rightarrow \exists n\,\mathord {:}\,{s}.\mathrm {FOL}^{n\,\mathord {:}\,{s}}_{\varSigma }(\pi _2) \wedge reach (m,n).$

For Models: For every signature $\varSigma$ of $\mathbf {ARL}(\underline{\mathrm {M}})$, $\beta ^{R}_{\varSigma } :\mathrm {Mod}^{\mathbf {FOL}}(\mathrm {Reach}(\varSigma ),E) \rightarrow \mathrm {Mod}^{\mathbf {ARL}(M)}(\varSigma )$ is the model functor that maps every first-order structure $N \in |\mathrm {Mod}^{\mathbf {FOL}}(\mathrm {Reach}(\varSigma ),E) |$ to the model $(M,\leadsto ) \in |\mathrm {Mod}^{\mathbf {ARL}(M)}(\varSigma ) |$, given by $M = \beta _{\varSigma }(N) \in |\mathrm {Mod}^{\underline{\mathrm {M}}}(\varSigma ) |$ and ${\leadsto _s} = \{ (m,n) \mid (N,m,n) \models reach (x,y) \}$, for every sort $s$. Note that $\leadsto _s$ is well-defined as $\mathrm {Cls}= \varPhi \mathbin {;}\mathrm {St}$ and $N_s = [\![M ]\!]_{\varSigma ,s}$.

To encode the Horn-clause reachability logic of Corollary 4 (defined over $\underline{\mathrm {ML}}^{+}$) into first-order logic, it suffices to notice that the comorphism considered in Sect. 3.3, $(\varPhi , \alpha , \beta ) :\flat \mathbf {ML}^{+} \rightarrow \mathbf {FOL}$, satisfies all of the above requirements, and thus can be extended to a comorphism $(\varPhi ^{R}, \alpha ^{R}, \beta ^{R}) :\mathbf {ARL}(\underline{\mathrm {ML}}^{+}) \rightarrow \mathbf {FOL}^{\mathrm {pres}}$. This can be further extended to an encoding of $\mathbf {HCL}(\mathbf {ARL}(\underline{\mathrm {ML}}^{+}))$ into $\mathbf {FOL}^{\mathrm {pres}}$ through the use of a general result about Horn-clause institutions.

Proposition 11

Let $\mathbf {I}$ and $\mathbf {I}'$ be institutions equipped with quantification spaces. Every comorphism of institutions $(\varPhi , \alpha , \beta ) :\mathbf {I} \rightarrow \mathbf {I}'$ that has weak model amalgamation, and for which $\varPhi$ preserves the quantification space of $\mathbf {I}$, can be extended to a comorphism of institutions between $\mathbf {HCL}(\mathbf {I})$ and $\mathbf {HCL}(\mathbf {I'})$.

5 Conclusions and Future Research

In this work, we proposed an institutional formalisation of the logical systems that underlie the $\mathbb {K}$ semantic framework. These logical systems account for the structural properties of program configurations (through matching logic), and changes of these configurations (through reachability logic).

Our work sets the foundation for integrating the $\mathbb {K}$ semantic framework into heterogeneous institution-based toolsets, allowing us to exploit the combined potential of the $\mathbb {K}$ tool and of other software tools such as the MiniSat solver, the SPASS automated prover or the Isabelle interactive proof assistant. Having both matching and reachability logic defined as institutions allows us to integrate them into the logic graphs of institution-based heterogeneous specification languages such as HetCasl [16]. As an immediate result, the $\mathbb {K}$ framework can inherit the powerful module systems developed for specifications built over arbitrary institutions, with dedicated operators for aggregating, renaming, extending, hiding and parameterising modules. In addition, this will enable us to combine reachability logic and the tool support provided by $\mathbb {K}$ with other logical systems and tools. Towards that end, as a preliminary effort to integrate the $\mathbb {K}$ framework into Hets [17], we described comorphisms from matching and reachability logic to the institution of first-order logic.

Another line of research concerns the development of $\mathbb {K}$ from a purely formal-specification perspective, including for example, studies on modularisation and initial semantics. Within this context, verification can be performed based on the proof systems that have already been defined for $\mathbb {K}$.