# A Logic on Subobjects and Recognizability

H. J. Sander Bruggink, Barbara König

► To cite this version:

H. J. Sander Bruggink, Barbara König. A Logic on Subobjects and Recognizability. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. pp.197-212, 10.1007/978-3-642-15240-5_15. hal-01054459

HAL Id: hal-01054459

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

Submitted on 6 Aug 2014

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
A Logic on Subobjects and Recognizability

H. J. Sander Bruggink and Barbara König

Universität Duisburg-Essen, Germany
{sander.bruggink, barbara_koenig}@uni-due.de

**Abstract.** We introduce a simple logic that allows to quantify over the subobjects of a categorical object. We subsequently show that, for the category of graphs, this logic is equally expressive as second-order monadic graph logic (MSOGL). Furthermore we show that for the more general setting of hereditary pushout categories, a class of categories closely related to adhesive categories, we can recover Courcelle's result that every MSOGL-expressible property is recognizable. This is done by giving an inductive translation of formulas of our logic into so-called automaton functors which accept recognizable languages of cospans.

# 1 Introduction

Regular languages have been studied extensively in computer science and have a large number of applications, such as model checking [3] and termination analysis [10]. The notions of regularity and finite automata can be straightforwardly generalized to trees and tree automata, opening the possibility to define regular tree languages and exploit the convenient closure properties that these languages enjoy. In recent years, the success of regular languages has sparked interest in obtaining a similar notion for other classes of object, in particular graphs. Courcelle has focused on the notion of recognizability – which is equivalent to regularity in the case of word languages – in an algebra of graphs with interfaces. It turns out that recognizable graph languages in this setting can be characterized by locally finite congruences. Bozapalidis and Kalampakas explored a similar characterization based on magmoids [4]. The authors of this paper defined automaton functors to investigate recognizability in a more category theoretic setting [6].

A common disadvantage of the approaches above, is that it is in general not possible to describe a recognizable graph language in a finite way, because the size of the interface of a graph is in principle unbounded. Several solutions for this problem have been developed, such as monadic second-order graph logic [7] and graph automata [5]. In both cases, the class of languages described is a proper subclass of the class of all recognizable graph languages.

In this paper, we develop a logic, similar to monadic second-order graph logic, which describes properties of objects in a category. We show that – under some assumptions on the underlying category – every language describable by the logic is recognizable (the converse does not hold) and that in the category of graphs our logic has the same expressive power as Courcelle's monadic
second-order graph logic. This work extends the work of Courcelle in two aspects: First, we generalize the monadic second-order graph logic of Courcelle to arbitrary categories. Second, we prove, for hereditary pushout categories in which for each composable pair of arrows there exist finitely many pushout complements (up to isomorphism), that each language described by a logic formula is recognizable. We do this by giving an inductive construction (on the structure of the formula), which is more convenient in practice than the construction given by Courcelle in [7]. However, another inductive construction has recently been developed independently from our work [9].

The paper is organized as follows: In §2 we give preliminary definitions and fix notation. In §3 we present the syntax and semantics of the logic on subobjects. We continue in §4 to compare the logic to monadic second-order graph logic, and show that, in the category of hypergraphs, the expressive power of our logic and monadic second-order logic are the same. Finally, in §5, we show, by constructing automaton functors from logic formulas, that all languages definable by the logic on subobjects are recognizable, and in §6 an example of the translation is given.

## 2 Preliminaries

We assume a basic familiarity with category theory. In the following we fix a category **C**. For a morphism $f: A \to B$ we denote by $dom(f) = A$ the domain and by $cod(f) = B$ the codomain of $f$. When $f$ and $g$ are (composable) morphisms, we write $f; g$ for the morphism $f$ postcomposed with $g$, that is $f; g = g \circ f$.

Let $f: A \to T$ and $g: B \to T$ be monos with the same codomain $T$. We write $f \sqsubseteq g$ if there exists an arrow $h: A \to B$ (which is necessarily unique) such that $h; f = g$. The subobject lattice $Sub(T)$ of an object $T$ is formed by isomorphism classes of monos with codomain $T$, where $\sqsubseteq$ forms the inclusion order. (In practice, we will take unique representatives of the isomorphism classes.)

In the second half of this paper, we will restrict our attention to so-called *hereditary pushout categories* (HPCs) [13], which are related to the well-known adhesive categories [15]. Most adhesive categories are also HPC, including all topoi. In particular, the categories **Set** of sets and **Graph** of hypergraphs (see page 4) are HPC. A category **C** is a HPC if

1. **C** has pushouts along monos;

2. **C** has all pullbacks;

3. given a cube diagram as shown on the right, where $a, b$ and $c$ are monos, the bottom face is a pushout and the back faces are pullbacks, we have that the top face is a pushout if and only if the front faces are pullbacks and $d$ is a mono.

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

Different from adhesive categories the vertical arrows in the cube must be mono, instead of one of the arrows in the lower square.

In [6], the authors of the present paper defined recognizable languages of arrows by means of *finite automaton functors*¹ (compare also with a similar
notion introduced by Griffing [11]). Let **Rel** be the category which has sets as objects and relations between sets as arrows.

**Definition 2.1 (Recognizability).** Let $\mathbf{C}$ be a category. An automaton functor is a functor $\mathcal{A}: \mathbf{C} \to \mathbf{Rel}$ which maps each object $X$ of $\mathbf{C}$ to a set $\mathcal{A}(X)$ (called the set of states of $X$) and each arrow $f: X \to Y$ to a relation $\mathcal{A}(f) \subseteq \mathcal{A}(X) \times \mathcal{A}(Y)$. Additionally, each state set $\mathcal{A}(X)$ contains a distinguished set of start states and a distinguished set of final states as subsets.

An automaton functor is finite if every set in the image of $\mathcal{A}$ is finite, and
deterministic if every relation $\mathcal{A}(f)$ is functional and every state set contains
exactly one initial state.

Let $J, K$ be two $\mathbf{C}$-objects. The $(J, K)$-language $L_{J,K}(\mathcal{A})$ (of arrows from $J$ to $K$) is defined as follows: $f: J \to K$ is contained in $L_{J,K}(\mathcal{A})$ if and only if $\mathcal{A}(f)$ relates a start state of $\mathcal{A}(J)$ to a final state of $\mathcal{A}(K)$.

A language $L_{J,K}$ of arrows from $J$ to $K$ is recognizable in $\mathbf{C}$ if it is the $(J, K)$-language of a finite automaton functor $\mathcal{A}: \mathbf{C} \to \mathbf{Rel}$.

This notion of recognizable language is a generalization of finite automata for
word languages. If we take $\mathbf{C}$ as a one-object category with all words as arrows
(the free monoid of the alphabet), then a finite automaton is isomorphic to an
automaton functor (mapping the single object to the state set of the automaton
and each arrow to its respective transition relation).

The intuition behind the definition is to have a mapping into a (finite) domain
that respects compositionality and identities, that is, which is a functor. The
functor property ensures that decomposing the arrow in different ways does not
affect acceptance in any way. This is different from the case of words where there
is essentially only one way to decompose a word into atomic components.

Let $\mathbf{C}$ be a category with pushouts. A cospan $c: D \to^{c_L} E \to^{c_R} F$ is a pair of $\mathbf{C}$-arrows with the same codomain. Here, $D$ and $F$ are the domain (or *inner interface*) and codomain (or *outer interface*) of the cospan $c$, respectively. The identity cospan for an object $E$ is the cospan consisting of twice the identity arrow of $E$. Let $c: D \to^{c_L} E \to^{c_R} F$ and $d: F \to^{d_L} G \to^{d_R} H$ be cospans (where the codomain of $c$ equals the domain of $d$). The composition of $c$ and $d$ is obtained by taking the pushout of $c_R$ and $d_L$.

A *semi-abstract cospan* is an equivalence class of cospans, where we take the
middle object of the cospan up to isomorphism. (In practice, we will choose
unique representatives from each isomorphism class.)

Now, the category Cospan($\mathbf{C}$) is defined as the category which has the objects of $\mathbf{C}$ as objects, and semi-abstract cospans as arrows. In [6] we have shown that Courcelle's notion of recognizable graph language [7, 8] coincides with our notion of recognizability in the category of cospans of graphs when we consider cospans of the form $\emptyset \to G \leftarrow \emptyset$.

<footnote n="1">¹ What we call *finite automaton functor* here, is simply called *automaton functor* in [6].</footnote>
For the comparison with the monadic second-order logic of Courcelle, and for most examples, we introduce a category of hypergraphs (just called *graphs* in the following). Fix a signature $\Sigma$ of labels, each element $A$ of which has an arity $ar(A)$. A graph is a tuple $G = (V_G, E_G, att_G, lab_G)$, consisting of a set $V_G$ of vertices (or nodes), a set $E_G$ of edges, an attachment function $att_G: E_G \to V_G^*$ and a labeling function $lab_G: E_G \to \Sigma$, such that for each $e \in E_G$ it holds that $|att_G(e)| = ar(lab(e))$. (Here, $A^*$ is the set of finite sequences over $A$, and $|a|$ denotes the length of a sequence $a$.) A graph is *discrete* if it has no edges. A graph morphism is a structure preserving map between graphs. The category **Graph** is the category of finite graphs and graph morphisms.

We define the following “special” graphs and morphisms: The graph $Dis_k$ is the discrete graph with node set $\{1, \dots, k\}$. Furthermore, for each $A \in \Sigma$, we define the graph $E_A$, consisting of a single A-labelled edge and adjacent (pairwise unequal) nodes, and the morphisms $e_A^i: Dis_1 \to E_A$ mapping the single node in $Dis_1$ to the node connected to the $i$-th port of the single edge $e \in E_A$ (that is, to the $i$th node of $att_{E_A}(e)$). Furthermore, we define $Epi_A$ to be the set of epimorphisms with domain $E_A$, up to isomorphism (in the case of **Graph** this set is finite).

For the examples, we will usually consider unlabeled, directed (multi)graphs, i.e. we take $\Sigma = \{\star\}$, with $ar(\star) = 2$. We define $E = E_\star$ to be the graph consisting of a single (directed) edge connecting two nodes, and morphisms $src = e_\star^0$ and $tgt = e_\star^1$, mapping the node of $Dis_1$ to the source and the target of the edge in $E$, respectively.

## 3 A Logic on Subobjects

In this section we introduce the syntax and semantics of the logic for a fixed category **C**. The logic will be used to describe properties of objects of **C**.

**Syntax.** Let $Var$ be a (countably infinite) set of variables. A variable typing is a partial map $\tau: Var \to Obj(C) \cup \{\Omega\}$. There are two kinds of variables: *first-order variables* of sort $T$ (where $T$ is an arbitrary object of **C**), representing subobjects of fixed structure, and *second-order variables* of sort $\Omega$, representing arbitrary subobjects.<fnref n="2" /> Unless otherwise indicated, first-order variables are denoted by lowercase letters $(x, y, z)$ and second-order variables by capitals $(X, Y, Z)$.

Subobject expressions are generated by the grammar $e := X \mid f \;_\Omega x$, where $X$ is of sort $\Omega$, $x$ is of sort $T$ and $f: T' \to T$ is a mono. We then say that the expression $f \;_\Omega x$ is of sort $T'$. (Intuitively $f$ restricts the graph denoted by $x$ to a subgraph $T'$.) Variables of sort $\Omega$ cannot be precomposed with monos.

The set $Form(\tau)$ of formulas typed by $\tau$ is specified by the following grammar:

$$ Form(\tau) := e_1 \sqsubseteq e_2 \mid Form(\tau) \wedge Form(\tau) \mid \neg Form(\tau) \mid (\exists X: \Omega) Form(\tau[X \mapsto \Omega]) \mid (\exists x: T) Form(\tau[x \mapsto T]).^3 $$

<footnote n="2">² Later, in the comparison with `MSOGL`, it will become clearer why these types of variables are called first-order and second-order, respectively.</footnote>
Note that in a formula of the form $e_1 \sqsubseteq e_2$ the two expressions can have arbitrary sorts. The set of free variables of a formula $\varphi$, denoted $FV(\varphi)$ is defined as usual. We also define the abbreviation $(x = y) \equiv (x \sqsubseteq y \land y \sqsubseteq x)$. Furthermore, we use the usual abbreviations for falsity ($\bot$), disjunction ($\vee$), implication ($\rightarrow$) and universal quantification ($\forall$).

Note that we do not define syntax for defining the morphism $f$ and the object $T$ in expressions and formulas of the form $f \circled{x}$ and $(\exists \varphi : T)$. The exact syntax needed for this depends on the category, and falls outside the scope of this paper.

**Semantics.** Let $\varphi$ be formula typed by variable typing $\tau$ and $B$ a C-object. A $B$-valuation $\eta$ for $\varphi$ is a function which assigns:

- to each $x \in FV(\varphi)$, with $\tau(x) = T$ (where $T \neq \Omega$), a mono $v_x : T \to B$; and

- to each $X \in FV(\varphi)$, with $\tau(X) = \Omega$, a mono $v_X : V \to B$ (where $V$ is arbitrary).

Now we can define the semantics of formulas of the logic. Let $\varphi$ be a subobject formula typed by $\tau$ and let $B$ be a C-object. We say that $B, \eta \models \varphi$, for some $B$-valuation $\eta$, whenever:

- $B, \eta \models X \sqsubseteq Y$ if $\eta(X) \sqsubseteq \eta(Y)$.

- $B, \eta \models f \circled{x} \sqsubseteq g \circled{y}$ if $f : \eta(x) \sqsubseteq g : \eta(y)$.

- $B, \eta \models f \circled{x} \sqsubseteq Y$ if $f : \eta(x) \sqsubseteq \eta(Y)$.

- $B, \eta \models X \sqsubseteq g \circled{y}$ if $\eta(X) \sqsubseteq g : \eta(y)$.

- $B, \eta \models \varphi_1 \land \varphi_2$ if $B, \eta \models \varphi_1$ and $B, \eta \models \varphi_2$.

- $B, \eta \models \neg \varphi$ if $B, \eta \not\models \varphi$.

- $B, \eta \models (\exists x : T) \varphi$ if there is a mono $v : T \to D$ such that $B, \eta[x \mapsto v] \models \varphi$.

- $B, \eta \models (\exists X : \Omega) \varphi$ if there is a mono $v : V \to D$ such that $B, \eta[X \mapsto v] \models \varphi$.

Furthermore, for a closed formula $\varphi$, we write $B \models \varphi$ whenever $B, \eta \models \varphi$ for the empty valuation $\eta$. Note that this definition works for any category. However the results of §5 (translation of formulas into automaton functors) will only be valid for hereditary pushout categories (which satisfy some additional conditions).

**Examples.** In an arbitrary category C we can define the following formula:

- The join of two expressions:

$$ (e = e_1 \sqcup e_2) := e_1 \sqsubseteq e \land e_2 \sqsubseteq e \land (\forall X : \Omega) ((e_1 \sqsubseteq X \land e_2 \sqsubseteq X) \to e \sqsubseteq X). $$

In the next examples we will use the category of unlabeled directed graphs, as presented on page 4.

$$ f[a \mapsto b](a') = \begin{cases} b & \text{if } a' = a \\ f(a') & \text{otherwise} \end{cases} $$

<footnote n="3">³ Let $f: A \to B$ be a function and let $a, b$ be two elements, which are not necessarily contained in $A$ or $B$. Then $f[a \mapsto b]: A \cup \{a\} \to B \cup \{b\}$ denotes the function defined as follows:</footnote>
- The subgraph $X$ is closed under reachability:

$$RC(X: \Omega) := (\forall y: E) (src \; \ddot{s} \; y \sqsubseteq X \rightarrow tgt \; \ddot{s} \; y \sqsubseteq X)$$

- There exists a path from node $x$ to node $y$ (every reachability closed subgraph containing $x$ also contains $y$):

$$Path(x, y: Dis_1) := (\forall Z: \Omega) ((id \; \ddot{s} \; x \sqsubseteq Z \land RC(Z)) \rightarrow id \; \ddot{s} \; y \sqsubseteq Z)$$

# 4 Comparison to Monadic Second-Order Graph Logic

Consider the category **Graph** as presented on page 4. We show that for this category the logic on subobjects has the same expressive power as monadic second-order graph logic [8, 7]. We do this by defining translations from monadic second-order logic to the logic on subobjects and vice versa, and proving that a graph satisfies a formula if and only if it satisfies the translation of the formula.

## 4.1 Monadic Second-Order Graph Logic

First we define monadic second-order graph logic (MSOGL), mainly in order to fix notation and terminology. This logic is one of the most important specification logics for graphs. Especially, Courcelle's theorem says that every graph property definable in MSOGL is decidable in linear time on (finite) graphs of bounded tree-width.

The MSOGL is a sorted second-order logic with four kinds of variables: first-order node variables (range over nodes), first-order edge variables (range over edges), second-order node variables (range over sets of nodes) and second-order edge variables (range over sets of edges). As a notational convention, first-order variables will be denoted by lowercase letters ($x, y, z$) and second-order variables by capitals ($X, Y, Z$). The syntax of MSOGL is given by the following grammar:

$$\begin{array}{l}
\varphi := \varphi_1 \land \varphi_2 | \neg \varphi | (\exists X: V) \varphi | (\exists X: E) \varphi | (\exists x: v) \varphi | (\exists x: e) \varphi \\
x = y | x \in X | edge_A(x, y_1, \dots, y_{ar(A)}),
\end{array}$$

where typing must be respected, that is, in formulas of the form $x = y$ both variables have the same type and in formulas of the form $x \in X$ it holds that $x$ is a first-order node (edge) variable and $X$ a second-order node (edge) variable. Formulas of the form $edge_A(x, y_1, \dots, y_{ar(A)})$ denote that the edge $x$ has label $A$ and is adjacent to the nodes $y_1, \dots, y_n$.

A graph $G = (V_G, E_G, att_G, lab_G)$ satisfies a formula $\varphi$, written $G \models \varphi$, if there exists a valuation $\theta$, mapping first-order variables to nodes and edges of $G$ and second-order variables to sets of nodes and sets of edges of $G$, such that $G, \theta \models \varphi$, where:

- $G, \theta \models x = y$ if $\theta(x) = \theta(y)$ and $G, \theta \models x \in X$ if $\theta(x) \in \theta(X)$.

- $G, \theta \models edge_A(x, y_1, \dots, y_n)$ if $lab_G(\theta(x)) = A$ and $att_G(\theta(x)) = \theta(y_1) \dots \theta(y_n)$.

- $G, \theta \models \varphi_1 \land \varphi_2$ if $G, \theta \models \varphi_1$ and $G, \theta \models \varphi_2$.

- $G, \theta \models \neg \varphi$ if $G, \theta \nvDash \varphi$.

- $G, \theta \models (\exists x: v) \varphi$ if there is a $v' \in V_G$ such that $G, \theta[x \mapsto v'] \models \varphi$.
- $G, \theta \models (\exists x: e) \varphi$ if there is a $e' \in E_G$ such that $G, \theta[x \mapsto e'] \models \varphi$.

- $G, \theta \models (\exists X: V) \varphi$ if there is a $V \subseteq V_G$ such that $G, \theta[X \mapsto V] \models \varphi$.

- $G, \theta \models (\exists X: E) \varphi$ if there is a $E \subseteq E_G$ such that $G, \theta[X \mapsto E] \models \varphi$.

In [7] an extension to monadic second-order logic is presented which also considers cardinality constraints of the form $card_{n,p}(X)$, expressing that the set represented by $X$ contains $n$ elements modulo $p$, which are omitted here for simplicity. It is currently not entirely clear to us how to integrate a similar predicate into the logic on subobjects in a natural way.

## 4.2 From Monadic Second-Order Logic to the Logic on Subobjects

We define a translation $[\cdot]_S$ from formulas of MSOGL to formulas of the logic on subobjects. For this, we define an edge typing as a map $\zeta$ from first-order edge variables (labelled with $A$) to epimorphisms (with domain $E_A$). We define the translation function $[[\varphi]]_S = [[\varphi]]_S^0$ where, for an edge typing $\zeta$, $[[\varphi]]_S^\zeta$ is inductively defined as follows:

$$ 
\begin{align*}
[[\neg \varphi]]_S^\zeta &:= [[\varphi]]_S^\zeta & [[x = y]]_S^\zeta &:= x = y \\
[[\varphi \wedge \psi]]_S^\zeta &:= [[\varphi]]_S^\zeta \wedge [[\psi]]_S^\zeta & [[x \in X]]_S^\zeta &:= x \subseteq X \\
[(\exists X: V) \varphi]_S^\zeta &:= (\exists X: \Omega) [[\varphi]]_S^\zeta & [(\exists x: v) \varphi]_S^\zeta &:= (\exists x: \mathrm{Dis}_1) [[\varphi]]_S^\zeta \\
[(\exists X: E) \varphi]_S^\zeta &:= (\exists X: \Omega) [[\varphi]]_S^\zeta & [(\exists x: e) \varphi]_S^\zeta &:= \bigvee_{A \in \zeta} \bigvee_{f \in E_{pi_A}} (\exists x: \mathrm{cod}(f)) [[\varphi]]_S^{\zeta[x \mapsto f]}
\end{align*}
$$

$$ [[\mathrm{edge}_A(x, y_1, \dots, y_n)]_S^\zeta := \begin{cases} \bigwedge_{1 \le i \le ar(A)} (e_i^A; \zeta(x)) & ; x = y_i \text{ if } \mathrm{dom}(\zeta(x)) = E_A \\ \bot & \text{otherwise.} \end{cases} $$

**Proposition 4.1.** Let $G$ be a graph, and $\varphi$ a closed formula of monadic second order logic. Then $G \models_M \varphi$ if and only if $G \models [[\varphi]]_S$.

## 4.3 From the Logic on Subobjects to Monadic Second-Order Logic

We define a translation $[\cdot]_M$ from formulas of our logic to formulas of MSOGL. The main difference between the two logics is that in our logic, we can quantify over arbitrary subobjects, while in MSOGL we can only quantify over nodes, edges, sets of nodes and sets of edges. Thus, a single quantification in the logic on subobjects will in general correspond to more than one quantification in MSOGL. In order to make sure that the multiple variables in an MSOGL-formula evaluate to a possible subobject, we need to express the following two “consistency properties” as MSOGL-formulas (the exact definitions of both formulas is left as an exercise to the reader):

- Let $T$ be a graph and $f: X \to (V_T \cup E_T)$ a bijection between first-order variables and nodes and edges of $T$. The formula $\mathrm{struct}_f(T)$ expresses that the nodes and edges assigned to the variables in the codomain of $f$ build a graph isomorphic to $T$.
- Let $X_V$ be a second-order node variable and $X_E$ a second-order edge variable. The formula $\text{cons}(X_E, X_V)$ expresses that all nodes adjacent to an edge in $X_E$ must be in $X_V$.

A variable mapping $\xi$ is a function which maps:

- each free first-order variable $x$ of type $T$ in the formula over subobjects to a bijection from a subset of first-order node and edge variables in the MSOGL-formula to the nodes and edges of $T$, and

- each free second-order variable $X$ of the source formula to a pair of a second-order node and a second-order edge variable in the target formula.

Now, we define $[[\varphi]]_M = [[\varphi]]_M^0$, where $[[\varphi]]_M^\xi$, parametrized by a variable mapping $\xi$, is inductively defined as follows:

$$[[\neg\varphi]]_M^\xi := \neg[[\varphi]]_M^\xi$$

$$[[\varphi \wedge \psi]]_M^\xi := [[\varphi]]_M^\xi \wedge [[\psi]]_M^\xi$$

$$[[ (\exists X: \Omega) \varphi ]]_M^\xi := (\exists X_E: E) (\exists X_V: V) \text{ cons}(X_E, X_V) \wedge [[\varphi]]_M^{\xi[X \mapsto (X_E, X_V)]}$$
where $X_E$ and $X_V$ are fresh variables.

$$[[ (\exists x: T) \varphi ]]_M^\xi := (\exists x_1, \dots, x_m : e) (\exists y_1, \dots, y_n : v) \text{ struct}_{\xi'(x)}(T) \wedge [[\varphi]]_M^{\xi'}$$
where $T$ is a graph with $m$ edges $(e_1, \dots, e_m)$ and $n$ nodes $(v_1, \dots, v_n)$, the $x_i$ and $y_i$ are fresh variables, and

$$\xi' := \xi[x \mapsto \{x_1 \mapsto e_1, \dots, x_m \mapsto e_m, y_1 \mapsto v_1, \dots, y_n \mapsto v_n\}].$$

$$[[X \sqsubseteq Y]]_M^\xi := (\forall x: e) (x \in X_E \rightarrow x \in Y_E) \wedge (\forall x: v) (x \in X_V \rightarrow x \in Y_V)$$
where $(X_E, X_V) := \xi(X)$ and $(Y_E, Y_V) := \xi(Y)$.

$$[[f \circled{x} \sqsubseteq X]]_M^\xi := x_1 \in X_E \wedge \dots \wedge x_m \in X_E \wedge y_1 \in X_V \wedge \dots \wedge y_n \in X_V$$
where $(X_E, X_V) := \xi(X)$,
$$\{x_1, \dots, x_m\} := \{u \mid \exists e: \langle u, f(e) \rangle \in \xi(x)\} \text{ and}$$
$$\{y_1, \dots, y_n\} := \{w \mid \exists v: \langle w, f(v) \rangle \in \xi(x)\}.$$

$$[[X \sqsubseteq f \circled{x}]_M^\xi := (\forall x': e) (x' \in X_E \rightarrow (x' = x_1 \vee \dots \vee x' = x_m)) \wedge$$
$$(\forall y': v) (y' \in X_V \rightarrow (y' = y_1 \vee \dots \vee y' = y_n))$$
where $(X_E, X_V) := \xi(X)$,
$$\{x_1, \dots, x_m\} := \{u \mid \exists e: \langle u, f(e) \rangle \in \xi(x)\} \text{ and}$$
$$\{y_1, \dots, y_n\} := \{w \mid \exists v: \langle w, f(v) \rangle \in \xi(x)\}.$$

$$[[f \circled{x} \sqsubseteq g \circled{x'}]]_M^\xi := (x_1 = x'_1 \vee \dots \vee x_1 = x'_p) \wedge \dots \wedge (x_m = x'_1 \vee \dots \vee x_m = x'_p) \wedge$$
$$(y_1 = y'_1 \vee \dots \vee y_1 = y'_q) \wedge \dots \wedge (y_n = y'_1 \vee \dots \vee y_n = y'_q)$$
where $\{x_1, \dots, x_m\} := \{u \mid \exists e: \langle u, f(e) \rangle \in \xi(x)\}$,
$$\{y_1, \dots, y_n\} := \{w \mid \exists v: \langle w, f(v) \rangle \in \xi(x)\},$$
$$\{x'_1, \dots, x'_p\} := \{u \mid \exists e: \langle u, f(e) \rangle \in \xi(x')\} \text{ and}$$
$$\{y'_1, \dots, y'_q\} := \{w \mid \exists v: \langle w, f(v) \rangle \in \xi(x')\}.$$

**Proposition 4.2.** Let $G$ be a graph, and $\varphi$ a closed formula of the logic on subobjects. Then $G \models \varphi$ if and only if $G \models_M [[\varphi]]_M^\xi$.
# 5 Logic and Recognizability

In this section we prove a generalization of Courcelle’s result which says that every language definable in monadic second-order graph logic is recognizable [7, 8]: we show that every language of objects of a hereditary pushout category definable by our logic is recognizable in the sense described in [6], by giving an encoding of a formula into an automaton functor. The resulting automaton functor is finite if the category enjoys the property that each composable pair of arrows has finitely many pushout complements (up to isomorphism). In order to be able to use structural induction on the logical formula, we need objects which keep track of the free variables. To this end we introduce a category of objects with valuations.

We fix a hereditary pushout category $\mathbf{C}$ with an initial object $0$.<fnref n="4" />

**Definition 5.1 (Object with valuation).** Let $\tau$ be a variable typing. An object with valuation (short: V-object) of type $\tau$ is a triple $D = (\mathbf{B}^D, \eta^D, \sigma^D)$, where

- $\mathbf{B}^D$ (the base object) is a $\mathbf{C}$-object;

- $\eta^D$ maps each variable $x$ for which $\tau(x)$ is defined to a mono $\eta^D(x): V_x^D \to \mathbf{B}^D$ (the valuation morphism); and

- $\sigma^D$ maps each variable $x$ for which $\tau(x)$ is defined and $\tau(x) \neq \Omega$ to an arrow $\sigma^D(x): V_x^D \to \tau(x)$ (the typing morphism).

We say that $D$ is well-typed whenever all arrows $\sigma^D(x)$ are identities.

Let $\tau$ be defined only on the variables $x_1, \dots, x_n$ and $Y_1, \dots, Y_m$, with $\tau(x_i) = T_i$ and $\tau(Y_j) = \Omega$ (for $1 \le i \le n$ and $1 \le j \le m$). Then a V-object of type $\tau$ is a diagram as shown on the right (where $t_i = \sigma^D(x_i)$, $v_i = \eta^D(x_i)$ and $w_j = \eta^D(Y_j)$). Note that if $D$ is well-typed (all typing morphisms are identities), $\eta^D$ corresponds exactly to a valuation (see §3). For the translation we need to allow typing morphisms which are not identities, however, because some objects of the category may not contain the type in its entirety.

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

We introduce the following operators for diagram extension and restriction. Let $D = (\mathbf{B}^D, \eta^D, \sigma^D)$ be a V-object of type $\tau$. By $\text{drop}_x(D)$ we denote the V-object of type $\tau|_{\text{Var}\setminus\{x\}}$ from which the morphisms and objects associated to $x$ have been dropped. Furthermore, let $v: V \to \mathbf{B}^D$ and $t: V \to T$ be given. Then $\text{add}_y^v(D) = (\mathbf{B}^D, \eta^D[y \mapsto v], \sigma^D)$ denotes the V-object of type $\tau[y \mapsto \Omega]$, which is obtained by adding the arrow $v$ (indexed by $y$) to $D$. Similarly, $\text{add}_y^{v,t}(D) = (\mathbf{B}^D, \eta^D[y \mapsto v], \sigma^D[y \mapsto t])$ denotes the V-object of type $\tau[y \mapsto T]$ which is obtained by adding the arrows $v$ and $t$ (indexed by $y$).

<footnote n="4">⁴ We require an initial object since we want to convert an arbitrary object $A$ into the corresponding cospan $0 \to A \leftarrow 0$. Then the automaton functor recognizes such cospans by “starting” and “ending” with the initial object.</footnote>
We consider the following category of objects with vertical interfaces, some of which might be typed.

**Definition 5.2 (Category of objects with valuations).** Let $\tau$ be a variable typing. We define the category $V_{\tau}^{C}$ (or simply $V_{\tau}$) as follows.

The objects of $V_{\tau}^{C}$ are the objects with valuation of type $\tau$ (see Def. 5.1). An arrow $p: D \to E$ of $V_{\tau}^{C}$ consists of $\mathbf{C}$-arrows $\alpha^p: B^D \to B^E$ and $\nu_x^p: \eta^D(x) \to \eta^E(x)$ (for each $x \in \text{Var}$ such that $\tau(x)$ is defined) such that the square below is a pullback and the triangle commutes (whenever $\tau(x) \neq \Omega$):

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

The two diagrams above specify the following: the valuation morphisms of $D$ can be obtained from the valuation morphisms of $E$ by taking a pullback (if $\alpha^p$ is mono this is simply some form of restriction). Furthermore the typing morphisms must be consistent.

We will consider (semi-abstract) cospans over $V_{\tau}^{C}$, i.e., we will work with the category $\mathit{Cospan}(V_{\tau}^{C})$. Note that due to Property 3 on page 2 pushouts in $V_{\tau}^{C}$ – and hence cospan composition in $\mathit{Cospan}(V_{\tau}^{C})$ – can be computed component- wise by taking pushouts of all the component morphisms and obtaining the morphisms of the resulting diagram as mediating morphisms. In the initial object 0 all objects (apart from the $\tau(x)$) are the initial objects of $\mathbf{C}$. We extend the operation $\mathit{drop}_x$ to $V_{\tau}^{C}$-cospans in the straightforward way.

Given a $V_{\tau}$-object $D = (B^D, \eta^D, \sigma^D)$ and a variable $x$ such that $\tau(x)$ is defined, we define the selection morphism $sel_x^D$ (in the case that $\tau(x) \neq \Omega$ parametrized by a morphism $f: V_x^D \to \tau(x)$) as follows:

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

- Suppose $\tau(x) \neq \Omega$. Let $f: S \to \tau(x)$. We take the pullback of $\sigma^D(x)$ and $f$, and obtain an object $U$ and arrows $U \to S$ and $g: U \to V_x^D$ (see the diagram on the right). Now we take $sel_{f,x}^D := g; v_x^D$.

- Suppose $\tau(x) = \Omega$. Then we simply take $sel_x^D := \eta^D(x)$.

We extend the definition of selection morphism to expressions of subobject logic in the obvious way, i.e. $sel_{f \otimes x}^D := sel_{f,x}^D$.

We will now present an inductive encoding that takes a formula $\varphi \in \mathit{Form}(\tau)$ and translates it into an automaton functor $A_{\varphi}^{\mathcal{A}}$ (or simply $\mathcal{A}$) for the category $\mathit{Cospan}(V_{\tau}^{C})$. The definition is divided into four subcases: *atomic formulas*, *boolean operations*, *first-order quantification* and *second-order quantification*.

**Atomic formulas:** Suppose $\varphi \equiv e_1 \sqsubseteq e_2$. Since the variables contained in $e_1, e_2$ are free and hence the corresponding vertical interfaces are present, it is enough to just check inclusion of those interfaces. This information is recorded in just one state $\star$ and we produce the empty relation whenever inclusion fails.
Formally, we define the automaton functor $\mathcal{A}_{\tau}^{\varphi}$ as follows. To each object $D$, $\mathcal{A}_{\tau}^{\varphi}$ assigns the one-element set $\{\star\}$ if $sel_{e_1}^{D} \subseteq sel_{e_2}^{D}$ (where $\star$ is the initial as well as the final state), and the empty set otherwise.

For a cospan $c: D \to E \leftarrow r \to F$ we define $\mathcal{A}_{\tau}^{\varphi}(c) = C(l); C(r)^{-1}$, where, for a $V_{\tau}$-arrow $p: D_1 \to D_2$, we define

$$C(p) := \begin{cases} id_{\{\star\}} & \text{if } sel_{e_1}^{D_2} \subseteq sel_{e_2}^{D_2} \\ \emptyset & \text{otherwise.} \end{cases}$$

Here, $id_{\{\star\}}$ refers to the identity relation on $\{\star\}$ and $\emptyset$ to the empty relation. Note that the empty relation is the identity relation on the empty set, i.e. $id_{\emptyset} = \emptyset$.

**Boolean operations:** Suppose $\varphi \equiv \varphi_1 \land \varphi_2$ or $\varphi \equiv \neg \varphi$. In this case compute the automaton functors for the subformulas and apply the standard techniques for intersection or complement to the automaton functors (due to a result of [6] these operations can be performed on all automaton functors, independent of the category). In the latter case (negation/complement) it is necessary to first construct the equivalent deterministic automaton functor.

**Second-order quantification:** Since the second-order quantification case is much simpler than the first-order case, we present it first. Suppose $\varphi \equiv (\exists X: \Omega) \varphi'$. Let $\mathcal{A}' := \mathcal{A}_{\tau'}^{\varphi'}$, where $\tau' = \tau[X \mapsto \Omega]$, be the automaton functor constructed for $\varphi'$.

The domain of the automaton functor for the subformula $\varphi'$ is a category of objects with an additional vertical interface. The automaton functor for $\varphi$ works in the following way: non-deterministically, a satisfying assignment for $X$ is chosen and then it behaves like the automaton functor for $\varphi'$.

The automaton functor $\mathcal{A}$ for $\varphi$ is formally defined as follows:

$$\mathcal{A}(D) = \bigcup_{v \in \text{Sub}(B^D)} \mathcal{A}'(\text{add}_X^v(D)) \times \{v\},$$

where $v \in \text{Sub}(B^D)$ means that $v$ ranges over representatives of isomorphism classes of monos into $B^D$. To a cospan $c: D \to E \leftarrow r \to F$ we assign the following relation $\mathcal{A}(c) \subseteq \mathcal{A}(D) \times \mathcal{A}(F)$: $\langle q, v^D \rangle$ is in relation with $\langle q', v^F \rangle$ whenever there exists a cospan

$$c': \text{add}_X^{v^D}(D) \to E' \leftarrow \text{add}_X^{v^F}(F)$$

of type $\tau'$ such that $\text{drop}_X(c') = c$ and $\langle q, q' \rangle \in \mathcal{A}'(c')$.

Finally, a state $\langle q, v \rangle$ is initial (final) if and only if $q$ is initial (final).

**First-order quantification:** Suppose $\varphi \equiv (\exists x: T) \varphi'$. Let $\mathcal{A}' := \mathcal{A}_{\tau'}^{\varphi'}$, where $\tau' = \tau[x \mapsto T]$, be the automaton functor constructed for $\varphi'$.

As in the case of second-order quantification, we non-deterministically choose a satisfying assignment for $x$. This time, however, we have to track how much
of the sought after subobject (T) has already been recognized (see explanation below).

We define the new automaton functor $\mathcal{A}_{\tau}^{\varphi}$ as follows:

$$ \mathcal{A}_{\tau}^{\varphi}(D) = \bigcup_{\substack{(v: V \to B^D) \in \mathrm{Sub}(B^D), \\ (t: V \to T)}} \mathcal{A}'(\mathrm{add}_x^{v,t}(D)) \times \{\langle v, t_1, t_2 \rangle \mid t = t_1; t_2, \mathrm{POC} \text{ exists}\}, $$

where, by “POC exists” we mean that there exists arrows $s_1, s_2$ such that $t_1; t_2 = s_1; s_2$ and the four arrows form a pushout. In the cases of $v$ and the decomposition $t_1; t_2$ we actually take representatives of the respective isomorphism classes.

To a cospan $c: D -l \to E \leftarrow r - F$ we assign the following relation $\mathcal{A}_{\tau}^{\varphi}(c) \subseteq \mathcal{A}_{\tau}^{\varphi}(D) \times \mathcal{A}_{\tau}^{\varphi}(F)$: $\langle q, v^D, t_1^D, t_2^D \rangle$ is in relation with $\langle q', v^F, t_1^F, t_2^F \rangle$ whenever $c$ can be extended to a cospan

$$ c': \mathrm{add}_x^{v^D, (t_1^D; t_2^D)}(D) \xrightarrow{l'} \mathrm{add}_x^{v^E, t^E}(E) \xleftarrow{r'} \mathrm{add}_x^{v^F, (t_1^F; t_2^F)}(F), $$

satisfying the following conditions:

$$ - \langle q, q' \rangle \in \mathcal{A}'(c') \text{ and} $$

- we have the commuting diagram below (on the left), where $\overline{V}^F$ is the pushout object of $t_1^D$ and $\nu^{l'}$.

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

A state $\langle q, v, t_1, t_2 \rangle$ is initial if and only if $q$ is initial and $t_1$ is an identity. It is final if and only if $q$ is final and the arrow $t_2$ is an identity.

The intuition behind the diagram above is the following: we are tracking an object of type $T$, while we are reading the “complete” object step by step. The vertical interface $V^F$ (with mono $v^F$) denotes the part of the outer interface that corresponds to this object. On the other hand $\overline{V}^F$ (with mapping $t_2^F$ into the type $T$) tells which part of the object we have already seen. Finally $t_1^F$ relates the part which is currently in the (outer) interface to the part we have already seen (see image above, on the right). Similar explanations can be given for $v^D$, $t_1^D$ and $t_2^D$. Finally, $\overline{V}^F$ is obtained from $\overline{V}^D$ by gluing those (new) parts of the tracked object that have been seen in the current cospan, namely $V^E$. (Additional intuition is provided by the example in §6).

**Proposition 5.3.** $\mathcal{A}_{\tau}^{\varphi}$, constructed for a formula $\varphi$ and a typing $\tau$ as described above, is a functor, that is, it preserves identities and composition.
**Theorem 5.4.** Let $\varphi$ be a formula, let $\tau$ be a typing and let $D = \langle B^D, \eta^D, \sigma^D \rangle$ be a well-typed V-object of type $\tau$. Then $B^D, \eta^D \models \varphi$ if and only if $D$ is contained in the $(0,0)$-language of $A_{\tau}^{\varphi}$, that is, if there exists an initial state $i_0$ and a final state $f_0$ with $\langle i_0, f_0 \rangle \in A_{\tau}^{\varphi}(c)$, where $c$ is the unique cospan of the form $0 \to D \leftarrow 0$.

*Finiteness.* Note that so far we did not impose any restrictions on the finiteness of the state sets. For this we first require that the objects in our category are finite in the sense that they contain only finitely many subobjects. In the case of graphs that would be the finite graphs and in the case of sets the finite sets.

However, in addition we need another requirement: in the encoding of first-order quantification we split a given arrow $t$ into $t = t_1; t_2$ such that all pushout complements for this split exist. In order to guarantee finiteness it is hence also necessary that a given arrow $t$ only admits finitely many such splits up to isomorphism.

It is currently not clear to us how subobject finiteness is related to the condition of having finitely many pushout complement splits. Clearly the latter property implies the former, but the other direction is unclear. In any case, the category **Graph** satisfies both requirements.

# 6 Detailed example

As an example, we consider (in the category of cospans of unlabeled directed graphs) the translation into an automaton functor of the formula

$$ \neg RC(X) \equiv (\exists y: E) (src \; ; \; y \sqsubseteq X \wedge \neg (tgt \; ; \; y \sqsubseteq X)), $$

which expresses that the subgraph $X$ is not closed under reachability.

The automaton functor for the atomic formula $\varphi_2 := \text{tgt} \; ; \; y \sqsubseteq X$ maps each graph, in which the target of edge $y$ does not lie in $X$, to the empty set, and all other graphs to the state set $\{\star\}$. It maps a cospan to $\text{id}_{\{\star\}}$ if the above also holds for the middle object of the cospan. The automaton functor of the other atomic formula, $\varphi_1 := src \; ; \; y \sqsubseteq X$, is built analogously.

To calculate the negation of $\varphi_2$, we must first make its automaton functor deterministic by means of the powerset construction (see [6]). Graphs are now mapped to either the state set $\{\emptyset, \{\star\}\}$ (where $\{\star\}$ is initial as well as final) or the state set $\{\emptyset\}$ (no initial or final states), and cospans are mapped accordingly. After the negation, final and non-final states are swapped.

To construct the automaton functor for $\varphi_1 \wedge \neg \varphi_2$, we use a Cartesian product construction. In the rest of the example, we will restrict our attention to an object $D'$ with $A^{\varphi_1}(D') = \{\star\}$ and $A^{\neg \varphi_2}(D') = \{\emptyset, \{\star\}\}$. For this object $D'$ we have that $A^{\varphi_1 \wedge \neg \varphi_2}(D') = \{\langle\{\star\}, \emptyset\rangle, \langle\{\star\}, \{\star\}\rangle\}$ where $\langle\{\star\}, \{\star\}\rangle$ is the initial and $\langle\{\star\}, \emptyset\rangle$ the final state. By reaching the final state we record that both the source node of the edge assigned to $y$ is contained in $X$ and the target node is not contained in $X$.
Finally, we build an automaton functor $\mathcal{A}$ for $\varphi \equiv (\exists y : E) (\varphi_1 \wedge \neg\varphi_2)$. Recall that $E = \circ\to\circ$. We obtain a V-object $D = \text{drop}_y(D')$. Assume it has base object $B^D = \text{Dis}_2 = \circ\circ$, a two-node discrete graph. States of the new automaton functor consist of arbitrary monos $v: V \to B^D$, allowed decompositions $t_1, t_2$ of arbitrary typing morphisms $t: V \to E$, and the states of $D$ extended with $v, t_1, t_2$. Let us list the possible decompositions of the typing morphism for all $2^2 = 4$ possible $v$ into $B^D$:

- For $v: \emptyset \to B^D$, there is a single typing morphism, and two possible decompositions, given by the two legs of the pushout diagram on the right. The top leg expresses the situation where no part of the sought after subobject has been encountered yet, whereas the bottom leg expresses the situation that the entire sought after subobject was already encountered.

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

- For $v = 1\circ \to 1\circ\circ$, there are two possible typing morphisms (mapping the node to the source and the target of the edge, respectively), with two decompositions each. For $v = \circ\circ \to \circ\circ\circ$, four decompositions are obtained analogously.<fnref n="5" />

- Let $v = \text{id}_{B^D}$. There are four possible typing morphisms. For $t = 1\circ\circ \to 1\circ\circ\circ$ there are two allowed decompositions, which can be read from the diagram on the right. For $t = 1\circ\circ \to 1,2\circ\circ\to\circ$ the allowed decompositions can be read from the pushout diagrams below. Since two decompositions occur twice, there are four decompositions in total.

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

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

For $t = 1\circ\circ \to 2\circ\circ\to 1$ and $t = 1\circ\circ \to \circ\circ\to 1,2$ we symmetrically obtain five decompositions.

As an example, consider the decomposition $1\circ\circ \to 1\circ\circ\circ \circ\circ \to 1,2\circ\circ\to\circ$ (the top right in the three diagrams above). This decomposition expresses that both nodes of $B^D$ are part of the sought after graph (as source node), but still need to be merged.

Suppose that for all possible $v, t$, the object $D$ extended with $v, t$ has the state set above (2 states). The new automaton functor then has $2 \cdot 20 = 40$ states. Accepting states are the ones which contain an accepting state of the automaton functor for the subterm, and in which the second part of the decomposition ($t_2$) is an isomorphism (that is, a subgraph isomorphic to $E$ was found).

The automaton functor works as follows: given a cospan $c: D \to c_L \to E \to c_R \to F$, it non-deterministically chooses what parts of the new information (the parts of $E$ not in the range of $c_L$) belong to the sought-after type $E$, and then works the same as the automaton functor constructed for the subformula.

<footnote n="5">⁵ The numbers beside the nodes indicate which nodes are mapped to which.</footnote>
# 7 Conclusion and Further Research

We have introduced a logic on subobjects and shown how it is related to monadic second-order graph logic. Although we are working in a categorical setting our choice was to focus on a classical logic, quantifying over sets of subobjects, and not a categorical logic where the universe is replaced by an object [14, 16]. With our current understanding it is not clear to us how to obtain a similar correspondence of MSOGL with a categorical logic. For instance, our predicates on subobjects can not directly be interpreted as subobjects of a product object, as would be customary for subobject logic. Although our logic falls out of scope of known categorical logics, we still believe that its intimate connection to MSOGL and recognizability makes it an interesting logic to study.

Furthermore it would be interesting to study which kind of equivalences on objects are induced by the logics in various categories (also in Set). Another interesting question is to consider in greater detail the relation to the graph predicates of [17] which are equivalent to first-order graph logic.

Note that although here we focused exclusively on graphs as examples, the greater generality of the logic allows us to easily talk about all kinds of “graph-like” structures, such as hierarchical graphs, graphs with scopes, attributed graphs or graphs with higher-order edges.

We also introduced a procedure for translating formulas of our logic induc-
tively into automaton functors, which are automata for accepting cospans in
hereditary pushout categories, a class of categories which includes all topoi. That
is, we have shown how to convert specifications into algorithms, albeit in a fairly
abstract setting. Other methods for converting MSOGL-formulas into recognizable
languages which are known to us [7, 12] do not follow such an inductive strategy,
but directly specify state sets by forming equivalence classes of logical formulas.
We hope that such an inductive method can help in practice in order to generate
and use automaton functors. In implementations, we can construct the automa-
ton functor only for a restricted set of “atomic” cospans from which all cospans
can be generated by composition. We are especially interested in applications
in verification such as invariant checking [1, 2] and termination analysis. Despite
the inductive approach the state sets of automata can still become fairly large, as
is already evident from the detailed example in §6. Our current approach to solve
this problem is to represent automaton functors (which are basically relations)
via binary decision diagrams. Initial experiments have been quite encouraging.

Finally, decomposing a graph into atomic cospans is basically equivalent to
the path decomposition of a graph and checking whether a graph is contained in
the language is hence linear-time for graphs of bounded pathwidth. For efficiency
reasons it would be more suitable to consider generalizations of tree automata
that can handle tree decompositions of graphs, as it is similarly done in the
work by Courcelle. While we think that this should be feasible in principle, we
did not choose to follow this path here since it would have added additional
complexity to the encoding into automaton functors. In the implementation we
will restrict ourselves to discrete interfaces and, out of necessity, to graphs of
bounded pathwidth or treewidth in order to work with finitely many state sets.
*Acknowledgements:* We are grateful to Tobias Heindel for his suggestions and his help with the categorical foundations. Furthermore we would like to thank Paolo Baldan and Andrea Corradini for stimulating discussions on this research topic.

## References

1. C. Blume. Graphsprachen für die Spezifikation von Invarianten bei verteilten und dynamischen Systemen. Master's thesis, Universität Duisburg-Essen, Nov. 2008.

2. Christoph Blume, H.J. Sander Bruggink, and Barbara König. Recognizable graph languages for checking invariants. In *Proc. of GT-VMT '10 (Workshop on Graph Transformation and Visual Modeling Techniques)*, Electronic Communications of the EASST, 2010.

3. A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In *Proc. of CAV '00*, pages 403–418. Springer, 2000. LNCS 1855.

4. S. Bozapalidis and A. Kalampakas. Recognizability of graph and pattern languages. *Acta Informatica*, 42(8/9):553–581, 2006.

5. S. Bozapalidis and A. Kalampakas. Graph automata. *Theoretical Computer Science*, 393:147–165, 2008.

6. H.J.S. Bruggink and B. König. On the recognizability of arrow and graph languages. In *Proc. of ICGT '08*, pages 336–350. Springer, 2008. LNCS 5214.

7. B. Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. *Information and Computation*, 85:12–75, 1990.

8. B. Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In G. Rozenberg, editor, *Handbook of Graph Grammars and Computing by Graph Transformation, Vol.1: Foundations*, chapter 5. World Scientific, 1997.

9. Bruno Courcelle and Irène Durand. Verifying monadic second order graph properties with tree automata. In *European Lisp Symposium*, May 2010.

10. A. Geser, D. Hofbauer, and J. Waldmann. Match-bounded string rewriting systems. *Applicable Algebra in Engineering, Communication and Computing*, 15(3–4):149–171, 2004.

11. G. Griffing. Composition-representative subsets. *Theory and Applications of Categories*, 11(19):420–437, 2003.

12. M. Grohe. Logic, graphs and algorithms. In J.Frum, E.Grädel, and T.Wilke, editors, *Logic and Automata – History and Perspectives*. Amsterdam University Press, 2007.

13. T. Heindel. *A category theoretical approach to the concurrent semantics of rewriting*. PhD thesis, Universität Duisburg-Essen, September 2009. http://www.ti.inf.uni-due.de/people/heindel/diss.pdf.

14. Bart Jacobs. *Categorical Logic and Type Theory*, volume 141 of *Studies in Logic and the Foundation of Mathematics*. Elsevier, 1999.

15. S. Lack and P. Sobociński. Adhesive and quasiadhesive categories. *RAIRO – Theoretical Informatics and Applications*, 39(3), 2005.

16. A.M. Pitts. Categorical logic. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, *Handbook of Logic in Computer Science V*. Oxford University Press, 2001.

17. A. Rensink. Representing first-order logic using graphs. In *Proc. of ICGT '04*, pages 319–335. Springer, 2004. LNCS 3256.