Specifying Graph Languages with Type Graphs

Andrea Corradini; Barbara K\"onig; Dennis Nolte

arXiv:1704.05263·cs.FL·April 24, 2017

Specifying Graph Languages with Type Graphs

Andrea Corradini, Barbara K\"onig, Dennis Nolte

PDF

Open Access

TL;DR

This paper explores formal methods for defining graph languages using type graphs, including logic and annotations, analyzing their decidability and closure properties to advance graph specification techniques.

Contribution

It introduces three novel formalisms for specifying graph languages with type graphs, extending the basic approach with logic and annotations, and analyzes their theoretical properties.

Findings

01

Decidability results for each formalism

02

Closure properties of the graph language classes

03

Relationships between restriction graphs and type graphs

Abstract

We investigate three formalisms to specify graph languages, i.e. sets of graphs, based on type graphs. First, we are interested in (pure) type graphs, where the corresponding language consists of all graphs that can be mapped homomorphically to a given type graph. In this context, we also study languages specified by restriction graphs and their relation to type graphs. Second, we extend this basic approach to a type graph logic and, third, to type graphs with annotations. We present decidability results and closure properties for each of the formalisms.

Equations92

L (T) = {G ∣ G \to T} .

L (T) = {G ∣ G \to T} .

L_{R} (R) = {G ∣ R ↛ G} .

L_{R} (R) = {G ∣ R ↛ G} .

F := T ∣ F \lor F ∣ F \land F ∣ \neg F, where T is a type graph.

F := T ∣ F \lor F ∣ F \land F ∣ \neg F, where T is a type graph.

L (T)

L (T)

L (F_{1} \land F_{2})

B_{φ}^{n} (a) (y) = φ (x) = y \sum a (x), where x \in (V_{G} \cup E_{G}) and y \in (V_{G^{'}} \cup E_{G^{'}})

B_{φ}^{n} (a) (y) = φ (x) = y \sum a (x), where x \in (V_{G} \cup E_{G}) and y \in (V_{G^{'}} \cup E_{G^{'}})

b^{'} (x) = b (x) + ∣ {y \in (G ∖ ψ_{R} (K)) ∣ h (y) = x} ∣

b^{'} (x) = b (x) + ∣ {y \in (G ∖ ψ_{R} (K)) ∣ h (y) = x} ∣

L \ignorespaces \ignorespaces \ignorespaces \ignorespaces

L \ignorespaces \ignorespaces \ignorespaces \ignorespaces

L (T_{0} \land \neg T_{1} \land \dots \land \neg T_{n}) = \emptyset

L (T_{0} \land \neg T_{1} \land \dots \land \neg T_{n}) = \emptyset

L (F_{1}) \subseteq L (F_{2}) ⟺ L (F_{1} \land \neg F_{2}) = \emptyset

L (F_{1}) \subseteq L (F_{2}) ⟺ L (F_{1} \land \neg F_{2}) = \emptyset

ℓ_{2}

ℓ_{2}

\Rightarrow

\Rightarrow

\Rightarrow

A_{φ_{1}} (u_{1})

A_{φ_{1}} (u_{1})

\Rightarrow

\Rightarrow

\Rightarrow

b_{2} (x)

b_{2} (x)

= b_{1} (x) + ∣ {y \in \emptyset ∣ h (y) = x} ∣ = b_{1} (x) + 0 = b_{1} (x)

C_{T [M]} (i d_{G})

C_{T [M]} (i d_{G})

= i d_{C_{T [M]} (G)}

(i,k)\in\mathcal{C}_{T[M]}(c_{1})\left\{\begin{array}[]{ll}(1)&g_{1};h_{1}=f_{1}\\ (2)&g_{2};h_{1}=f_{2}\\ (3)&\forall x\in T\quad b_{2}(x)=b_{1}(x)+|\{y\in(G\setminus g_{2}(K))\mid h_{1}(y)=x\}|\end{array}\right.

(i,k)\in\mathcal{C}_{T[M]}(c_{1})\left\{\begin{array}[]{ll}(1)&g_{1};h_{1}=f_{1}\\ (2)&g_{2};h_{1}=f_{2}\\ (3)&\forall x\in T\quad b_{2}(x)=b_{1}(x)+|\{y\in(G\setminus g_{2}(K))\mid h_{1}(y)=x\}|\end{array}\right.

(k,j)\in\mathcal{C}_{T[M]}(c_{2})\left\{\begin{array}[]{ll}(4)&g_{1}^{\prime};h_{2}=f_{2}\\ (5)&g_{2}^{\prime};h_{2}=f_{3}\\ (6)&\forall x\in T\quad b_{3}(x)=b_{2}(x)+|\{y\in(H\setminus g_{2}^{\prime}(L))\mid h_{2}(y)=x\}|\end{array}\right.

(k,j)\in\mathcal{C}_{T[M]}(c_{2})\left\{\begin{array}[]{ll}(4)&g_{1}^{\prime};h_{2}=f_{2}\\ (5)&g_{2}^{\prime};h_{2}=f_{3}\\ (6)&\forall x\in T\quad b_{3}(x)=b_{2}(x)+|\{y\in(H\setminus g_{2}^{\prime}(L))\mid h_{2}(y)=x\}|\end{array}\right.

(1)

(1)

(2)

b_{3} (x) = b_{1} (x) + ∣ {y \in (G ∖ g_{2} (K)) ∣ h_{1} (y) = x} ∣ + ∣ {y \in (H ∖ g_{2}^{'} (L)) ∣ h_{2} (y) = x} ∣

b_{3} (x) = b_{1} (x) + ∣ {y \in (G ∖ g_{2} (K)) ∣ h_{1} (y) = x} ∣ + ∣ {y \in (H ∖ g_{2}^{'} (L)) ∣ h_{2} (y) = x} ∣

∣ {y \in (G ∖ g_{2} (K)) ∣ h_{1} (y) = x} ∣ + ∣ {y \in (H ∖ g_{2}^{'} (L)) ∣ h_{2} (y) = x} ∣

∣ {y \in (G ∖ g_{2} (K)) ∣ h_{1} (y) = x} ∣ + ∣ {y \in (H ∖ g_{2}^{'} (L)) ∣ h_{2} (y) = x} ∣

=

∣ {y \in (G^{'} ∖ g_{2}^{'}; j_{2} (L)) ∣ h (y) = x} ∣

∣ {y \in (G^{'} ∖ g_{2}^{'}; j_{2} (L)) ∣ h (y) = x} ∣

=

=

=

=

=

b_{3} (x)

b_{3} (x)

= b_{1} (x) + ∣ {y \in (G ∖ g_{2} (K)) ∣ h_{1} (y) = x} ∣ + ∣ {y \in (H ∖ g_{2}^{'} (L)) ∣ h_{2} (y) = x} ∣

= b_{2} (x) + ∣ {y \in (H ∖ g_{2}^{'} (L)) ∣ h_{2} (y) = x} ∣

b_{3} (x) = b_{1} (x) + ∣ {y \in (G ∖ g_{2} (K)) ∣ h_{1} (y) = x} ∣ + ∣ {y \in (H ∖ g_{2}^{'} (L)) ∣ h_{2} (y) = x} ∣

b_{3} (x) = b_{1} (x) + ∣ {y \in (G ∖ g_{2} (K)) ∣ h_{1} (y) = x} ∣ + ∣ {y \in (H ∖ g_{2}^{'} (L)) ∣ h_{2} (y) = x} ∣

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsLogic, programming, and type systems · Formal Methods in Verification · Model-Driven Software Engineering Techniques

Full text

References

[1]

Parosh Aziz Abdulla, Lukás Holík, Bengt Jonsson, Ondrej Lengál, Cong Quy Trinh, and Tomás Vojnar.

Verification of heap manipulating programs with ordered data by extended forest automata.

In Proc. of ATVA ’13, pages 224–239, 2013.

LNCS 8172.

[2]

Christoph Blume, H.J. Sander Bruggink, Dominik Engelke, and Barbara König.

Efficient symbolic implementation of graph automata with applications to invariant checking.

In Proc. of ICGT ’12, pages 264–278. Springer, 2012.

LNCS 7562.

[3]

Christoph Blume, H.J. Sander Bruggink, Martin Friedrich, and Barbara König.

Treewidth, pathwidth and cospan decompositions with applications to graph-accepting tree automata.

Journal of Visual Languages & Computing, 24(3):192–206, 2013.

[4]

H.J. Sander Bruggink and Barbara König.

On the recognizability of arrow and graph languages.

In Proc. of ICGT ’08, pages 336–350. Springer, 2008.

LNCS 5214.

[5]

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.

Counterexample-guided abstraction refinement for symbolic model checking.

Journal of the ACM, 50(5):752–794, 2003.

[6]

Andrea Corradini, Ugo Montanari, and Francesca Rossi.

Graph processes.

Fundamenta Informaticae, 26(3/4):241–265, 1996.

[7]

Bruno Courcelle.

The monadic second-order logic of graphs I. Recognizable sets of finite graphs.

Information and Computation, 85:12–75, 1990.

[8]

Bruno Courcelle and Joost Engelfriet.

Graph Structure and Monadic Second-Order Logic, A Language-Theoretic Approach.

Cambridge University Press, June 2012.

[9]

Dino Distefano, Peter W. O’Hearn, and Hongseok Yang.

A local shape analysis based on separation logic.

In Proc. of TACAS ’06, pages 287–302. Springer, 2006.

LNCS 3920.

[10]

Jörg Endrullis and Hans Zantema.

Proving non-termination by finite automata.

In RTA ’15, volume 36 of LIPIcs, pages 160–176. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015.

[11]

Annegret Habel.

Hyperedge Replacement: Grammars and Languages.

Springer-Verlag, 1992.

LNCS 643.

[12]

Annegret Habel and Karl-Heinz Pennemann.

Nested constraints and application conditions for high-level structures.

In Formal Methods in Software and Systems Modeling. Essays Dedicated to Hartmut Ehrig, on the Occasion of His 60th Birthday, pages 294–308. Springer, 2005.

LNCS 3393.

[13]

Reiko Heckel and Annika Wagner.

Ensuring consistency of conditional graph rewriting – a constructive approach.

In Proc. of the Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation, volume 2 of ENTCS, 1995.

[14]

Stephen Lack and Paweł Sobociński.

Adhesive and quasiadhesive categories.

RAIRO – Theoretical Informatics and Applications, 39(3), 2005.

[15]

Jaroslav Nešetřil and Claude Tardif.

Duality theorems for finite structures (characterising gaps and good characterisations).

Journal of Combinatorial Theory, Series B, 80:80–97, 2000.

[16]

Peter W. O’Hearn.

Resources, concurrency and local reasoning.

Theoretical Computer Science, 375(1–3):271–307, May 2007.

Reynolds Festschrift.

[17]

Fernando Orejas, Hartmut Ehrig, and Ulrike Prange.

A logic of graph constraints.

In Proc. of FASE ’08, pages 179–198. Springer, 2008.

LNCS 4961.

[18]

Karl-Heinz Pennemann.

Development of Correct Graph Transformation Systems.

PhD thesis, Universität Oldenburg, May 2009.

[19]

Arend Rensink.

Canonical graph shapes.

In Proc. of ESOP ’04, pages 401–415. Springer, 2004.

LNCS 2986.

[20]

Arend Rensink.

Representing first-order logic using graphs.

In Proc. of ICGT ’04, pages 319–335. Springer, 2004.

LNCS 3256.

[21]

Grzegorz Rozenberg, editor.

Handbook of Graph Grammars and Computing by Graph Transformation, Vol.1: Foundations.

World Scientific, 1997.

[22]

Adrian Rutle, Alessandro Rossini, Yngve Lamo, and Uwe Wolter.

A diagrammatic formalisation of MOF-based modelling languages.

In Proc. of TOOLS EUROPE ’09, pages 37–56. Springer, 2009.

LNBIP 33.

[23]

Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.

Parametric shape analysis via 3-valued logic.

TOPLAS (ACM Transactions on Programming Languages and Systems), 24(3):217–298, 2002.

[24]

Dominik Steenken, Heike Wehrheim, and Daniel Wonisch.

Sound and complete abstract graph transformation.

In Proc. of SBMF ’11, pages 92–107. Springer, 2011.

LNCS 7021.

11institutetext: Università di Pisa, Italy

11email: [email protected] 22institutetext: Universität Duisburg-Essen, Germany

22email: {barbara_koenig,dennis.nolte}@uni-due.de

Specifying Graph Languages with Type Graphs

Andrea Corradini 11

Barbara König 22

Dennis Nolte 22

Abstract

We investigate three formalisms to specify graph languages, i.e. sets of graphs, based on type graphs. First, we are interested in (pure) type graphs, where the corresponding language consists of all graphs that can be mapped homomorphically to a given type graph. In this context, we also study languages specified by restriction graphs and their relation to type graphs. Second, we extend this basic approach to a type graph logic and, third, to type graphs with annotations. We present decidability results and closure properties for each of the formalisms.

1 Introduction

Formal languages in general and regular languages in particular play an important role in computer science. They can be used for pattern matching, parsing, verification and in many other domains. For instance, verification approaches such as reachability checking, counterexample-guided abstraction refinement [5] and non-termination analysis [10] could be directly adapted to graph transformation systems if one had a graph specification formalism with suitable closure properties, computable pre- and postconditions and inclusion checks. Inclusion checks are also important for checking when a fixpoint iteration sequence stabilizes.

While regular languages for words and trees are well-understood and can be used efficiently and successfully in applications, the situation is less satisfactory when it comes to graphs. Although the work of Courcelle [8] presents an accepted notion of recognizable graph languages, equivalent to regular languages, this is often not useful in practice, due to the sheer size of the resulting graph automata. Other formalisms, such as application conditions [20, 12] and first-order or second-order logics, feature more compact descriptions, but there are problems with expressiveness, undecidability issues or unsatisfactory closure properties.111A more detailed overview over related formalisms is given in the conclusion (Section 6).

Hence, we believe that it is important to study and compare specification formalisms (i.e., automata, grammars and logics) that allow to specify potentially infinite sets of graphs. In our opinion there is no one-fits-all solution, but we believe that specification mechanisms should be studied and compared more extensively.

In this paper we study specification formalisms based on type graphs, where a type graph $T$ represents all graphs that can be mapped homomorphically to $T$ , potentially taking into account some extra constraints. Type graphs are common in graph rewriting [6, 21]. Usually, one assumes that all items, i.e., rules and graphs to be rewritten, are typed, introducing constraints on the applicability of rules. Hence, type graphs are in a way seen as a form of labelling. This is different from our point of view, where graphs (and rules) are – a priori – untyped (but labeled) and type graphs are simply a means to represent sets of graphs.

There are various reasons for studying type graphs: first, they are reasonably simple with many positive decidability results and they have not yet been extensively studied from the perspective of specification formalisms. Second, other specification mechanisms – especially those used in connection with verification and abstract graph transformation [19, 23, 24] – are based on type graphs: abstract graphs are basically type graphs with extra annotations. Third, while not being as expressive as recognizable graph languages, they retain a nice intuition from regular languages: given a finite state automaton $M$ one can think of the language of $M$ as the set of all string graphs that can be mapped homomorphically to $M$ (respecting initial and final states).

We in fact study three different formalisms based on type graphs: first, pure type graphs $T$ , where the language consists simply of all graphs that can be mapped to $T$ . We also discuss the connection between type graph and restriction graph languages. Then, in order to obtain a language with better boolean closure properties, we study type graph logic, which consists of type graphs enriched with boolean connectives (negation, conjunction, disjunction). Finally, we consider annotated type graphs, where the annotations constrain the number of items mapped to a specific node or edge, somewhat similar to the proposals from abstract graph rewriting mentioned above.

In all three cases we are interested in closure properties and in decidability issues (such decidability of the membership, emptiness and inclusion problems) and in expressiveness. Proofs for all the results can be found in Appendix 0.A.

2 Preliminaries

We first introduce graphs and graph morphisms. In the context of this paper we use edge-labeled, directed graphs.

Definition 1 (Graph)

Let $\Lambda$ be a fixed set of edge labels. A $\Lambda$ -labeled graph is a tuple $G=\langle V,E,\mathit{src},\mathit{tgt},\mathit{lab}\rangle$ , where $V$ is a finite set of nodes, $E$ is a finite set of edges, $\mathit{src},\mathit{tgt}\colon E\to V$ assign to each edge a source and a target node, and $\mathit{lab}\colon E\to\Lambda$ is a labeling function.

We will denote, for a given graph $G$ , its components by $V_{G}$ , $E_{G}$ , $\mathit{src}_{G}$ , $\mathit{tgt}_{G}$ and $\mathit{lab}_{G}$ , unless otherwise indicated.

Definition 2 (Graph morphism)

Let $G,G^{\prime}$ be two $\Lambda$ -labeled graphs. A graph morphism $\varphi\colon G\to G^{\prime}$ consists of two functions $\varphi_{V}\colon V_{G}\to V_{G^{\prime}}$ and $\varphi_{E}\colon E_{G}\to E_{G^{\prime}}$ , such that for each edge $e\in E_{G}$ it holds that $\mathit{src}_{G^{\prime}}(\varphi_{E}(e))=\varphi_{V}(\mathit{src}_{G}(e))$ , $\mathit{tgt}_{G^{\prime}}(\varphi_{E}(e))=\varphi_{V}(\mathit{tgt}_{G}(e))$ and $\mathit{lab}_{G^{\prime}}(\varphi_{E}(e))=\mathit{lab}_{G}(e)$ . If $\varphi$ is both injective and surjective it is called an isomorphism.

We will often drop the subscripts $V,E$ and write $\varphi$ instead of $\varphi_{V}$ , $\varphi_{E}$ . We will consider the category ${\mathbf{Graph}}$ having $\Lambda$ -labeled graphs as objects and graph morphisms as arrows. The set of its objects will be denoted by ${\mathbf{Gr_{\Lambda}}}$ . The categorical structure induces an obvious preorder on graphs, defined as follows.

Definition 3 (Homomorphism preorder)

Given graphs $G$ and $H$ , we write $G\to H$ if there is a graph morphism from $G$ to $H$ in ${\mathbf{Graph}}$ . The relation $\to$ is obviously a preorder (i.e. it is reflexive and transitive) and we call it the homomorphism preorder on graphs. We write $G\nrightarrow H$ if $G\to H$ does not hold. Graphs $G$ and $H$ are homomorphically equivalent, written $G\sim H$ , if both $G\to H$ and $H\to G$ hold.

We will revisit the concept of retracts and cores from [15]. Cores are a convenient way to minimize type graphs, as, according to [15], all graphs $G,H$ with $G\sim H$ have isomorphic cores.

Definition 4 (Retract and core)

A graph $H$ is called a retract of a graph $G$ if $H$ is a subgraph of $G$ and in addition there exists a morphism $\varphi\colon G\to H$ . A graph $H$ is called a core of $G$ , written $H=\mathit{core}(G)$ , if it is a retract of $G$ and has itself no proper retracts.

Example 1

The graph $H$ is a retract of $G$ , where the morphism $\varphi$ is indicated by the node numbering:

[TABLE]

Since the graph $H$ does not have a proper retract itself it is also the core of $G$ .

3 Languages Specified by Type or Restriction Graphs

In this section we introduce two classes of graph languages that are characterized by two somewhat dual properties. A type graph language contains all graphs that can be mapped homomorphically to a given type graph, while a restriction graph language includes all graphs that do not contain an homomorphic image of a given restriction graph. Next, we discuss for these two classes of languages some properties such as closure under set operators, decidability of emptiness and inclusion, and decidability of closure under rewriting via double-pushout rules. Finally we discuss the relationship between these two classes of graph languages.

Definition 5 (Type graph language)

A type graph $T$ is just a $\Lambda$ -labeled graph. The language $\mathcal{L}(T)$ is defined as:

[TABLE]

Example 2

The following type graph $T$ over the edge label set $\Lambda=\{A,B\}$ specifies a type graph language $\mathcal{L}(T)$ consisting of infinitely many graphs:

[TABLE]

The category ${\mathbf{Graph}}$ has a final object, that we denote $T^{\Lambda}_{\mbox{\char 82}}$ , consisting of one node (called flower node ✲) and one loop for each label in $\Lambda$ . Therefore $\mathcal{L}(T^{\Lambda}_{\mbox{\char 82}})={\mathbf{Gr_{\Lambda}}}$ . The graph $T^{\Lambda}_{\mbox{\char 82}}$ for $\Lambda=\{A,B,C\}$ is depicted to the right.

Specifying graph languages using type graphs gives us the possibility to forbid certain graph structures by not including them into the type graph. For example, no graph in the language of Example 2 can contain a $B$ -loop or an $A$ -edge incident to the target of a $B$ -edge. However, it is not possible to force some structures to exist in all graphs of the language, since the morphism to the type graph need not be surjective. This point will be addressed with the notion of annotated type graph in Section 5.

Another way (possibly more explicit) to specify languages of graphs not including certain structures, is the following one.

Definition 6 (Restriction graph language)

A restriction graph $R$ is just a $\Lambda$ -labeled graph. The language $\mathcal{L}_{R}(R)$ is defined as:

[TABLE]

We will consider the relationship between the class of languages introduced in Definitions 5 and 6 in Section 3.3.

3.1 Closure and Decidability Properties

The type graph and restriction graph languages enjoy the following complementary closure properties with respect to set operators.

Proposition 1

Type graph languages are closed under intersection (by taking the product of type graphs) but not under union or complementation, while restriction graph languages are closed under union (by taking the coproduct of restriction graphs) but not under intersection or complementation.

Instead the two classes of languages enjoy similar decidability properties.

Proposition 2

For a graph language $\mathcal{L}$ characterized by a type graph $T$ (i.e. $\mathcal{L}=\mathcal{L}(T)$ ) or by a restriction graph $R$ (i.e. $\mathcal{L}=\mathcal{L}_{R}(R)$ ) the following problems are decidable:

Membership, i.e. for each graph $G$ it is decidable if $G\in\mathcal{L}$ holds. 2. 2.

Emptiness, i.e. it is decidable if $\mathcal{L}=\varnothing$ holds.

*Furthermore, language inclusion is decidable for both classes of languages: *

Given type graphs $T_{1}$ and $T_{2}$ it is decidable if $\mathcal{L}(T_{1})\subseteq\mathcal{L}(T_{2})$ holds. 2. 4.

Given restriction graphs $R_{1}$ and $R_{2}$ it is decidable if $\mathcal{L}_{R}(R_{1})\subseteq\mathcal{L}_{R}(R_{2})$ holds.

3.2 Closure under Double-Pushout Rewriting

In this subsection we are using the DPO approach with general, not necessarily injective, rules and matches. We discuss how we can show that a graph language $\mathcal{L}$ is a closed under a given graph transformation rule $\rho=(L\mathchoice{\xleftarrow{\varphi_{L}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}I\mathbin{\mathchoice{\xrightarrow{\varphi_{R}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}}R)$ , i.e., $\mathcal{L}$ is an invariant for $\rho$ . This means that for all graphs $G,H$ , where $G$ can be rewritten to $H$ via $\rho$ , it holds that $G\in\mathcal{L}$ implies $H\in\mathcal{L}$ .

For both type graph languages and restriction graph languages, separately, we characterize a sufficient and necessary condition which shows that closure under rule application is decidable. The condition for restriction graph languages is related to a condition already discussed in [13].

Proposition 3 (Closure under DPO rewriting for restriction graphs)

A restriction graph language $\mathcal{L}_{R}(S)$ is closed under a rule $\rho=(L\mathchoice{\xleftarrow{\varphi_{L}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}I\mathbin{\mathchoice{\xrightarrow{\varphi_{R}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}}R)$ if and only if the following condition holds: for every pair of morphisms $\alpha\colon R\to F$ , $\beta\colon S\to F$ which are jointly surjective, applying the rule $\rho$ with (co-)match $\alpha$ backwards to $F$ yields a graph $E$ with a homomorphic image of $S$ , i.e., $E\not\in\mathcal{L}_{R}(S)$ .

Proposition 4 (Closure under DPO rewriting for type graphs)

A type graph language $\mathcal{L}(T)$ is closed under a rule $\rho=(L\mathchoice{\xleftarrow{\varphi_{L}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}I\mathbin{\mathchoice{\xrightarrow{\varphi_{R}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}}R)$ if and only if for each morphism $t_{L}\colon L\to\mathit{core}(T)$ , there exists a morphism $t_{R}\colon R\to\mathit{core}(T)$ such that $t_{L}\circ\varphi_{L}=t_{R}\circ\varphi_{R}$ .

$L$$I$$R$$\mathit{core}(T)$$\Leftrightarrow$$\mathcal{L}(T)$ * is closed under application of $\rho$ * $\rho$$\forall t_{L}$$\varphi_{L}$$\varphi_{R}$$\exists t_{R}$

We show that the only if part ( $\Rightarrow$ ) of Proposition 4 cannot be weakened by considering morphisms to the type graph $T$ , instead of to $\mathit{core}(T)$ . In fact, consider the following type graph $T$ and the rule $\rho$ :

[TABLE]

The type graph $T$ contains the flower node, i.e., it has $T^{\{A,B\}}_{\mbox{\char 82}}$ as subgraph. This ensures that each graph $G$ , edge-labeled over $\Lambda=\{A,B\}$ , is in the language $\mathcal{L}(T)$ , and thus by rewriting any graph $G\in\mathcal{L}(T)$ into a graph $H$ using $\rho$ it is guaranteed that $H\in\mathcal{L}(T)$ . However there is a morphism $t_{L}\colon L\to T$ , the one mapping the $A$ -labeled edge of $L$ to the left $A$ -labeled edge of $T$ , such that there exists no morphism $t_{R}\colon R\to T$ satisfying $t_{L}\circ\varphi_{L}=t_{R}\circ\varphi_{R}$ .

3.3 Relating Type graph and Restriction Graph Languages

Both type graph and restriction graph languages specify collections of graphs by forbidding the presence of certain structures. This is more explicit with the use of restriction graphs, though. A natural question is how the two classes of languages are related. A partial answer to this is provided by the notion of duality pairs and by an important result concerning their existence, presented in [15].222Note that in [15] graphs are simple, but it can be easily seen that for our purposes the results can be transferred straightforwardly.

Definition 7 (Duality pair)

Given two graphs $R$ and $T$ , we call $T$ the dual of $R$ if for every graph $G$ it holds that $G\to T$ if and only if $R\nrightarrow G$ . In this case the pair $(R,T)$ is called duality pair.

Clearly, we have that $(R,T)$ is a duality pair if and only if the restriction graph language $\mathcal{L}_{R}(R)$ coincides with the type graph language $\mathcal{L}(T)$ .

Example 3

Let $\Lambda=\{A,B\}$ be given. The following is a duality pair:

[TABLE]

Since node 1 of $T$ is not the source of a $B$ -labeled edge and node 2 is not the target of an $A$ -labeled edge, for every graph $G$ we have $G\to T$ iff it does not contain a node which is both the target of an $A$ -labeled edge and the source of a $B$ -labeled edge. But it contains such a node if and only if $R\to G$ .

One can identify the class of restriction graphs for which a corresponding type graph exists which defines the same graph language. Results from [15] state333We refer to Lemma 2.3, Lemma 2.5 and Theorem 3.1 in [15]. that given a core graph $R$ , a graph $T$ can be constructed such that $(R,T)$ is a duality pair if and only if $R$ is a tree.

Thus we have a precise characterisation of the intersection of the classes of type and restriction graph languages: $\mathcal{L}$ belongs to the intersection if and only if it is of the form $\mathcal{L}=\mathcal{L}_{R}(R)$ and $\mathit{core}(R)$ is a tree. It is worth mentioning that the construction of $T$ from $R$ using the results from [15] contains two exponential blow-ups. This can be interpreted by saying that type graphs have limited expressiveness if used to forbid the presence of certain structures.

4 Type Graph Logic

In this section we investigate the possibility to define a language of graphs using a logical formula over type graphs. We start by defining the syntax and semantics of a type graph logic ( ${\mathit{TGL}}$ ).

Definition 8 (Syntax and semantics of ${\mathit{TGL}}$ )

A ${\mathit{TGL}}$ formula $F$ over a fixed set of edge labels $\Lambda$ is formed according to the following grammar:

[TABLE]

Each ${\mathit{TGL}}$ formula $F$ denotes a graph language $\mathcal{L}(F)\subseteq{\mathbf{Gr_{\Lambda}}}$ defined by structural induction as follows:

[TABLE]

Clearly, due to the presence of boolean connectives, boolean closure properties come for free.

Example 4

Let the following ${\mathit{TGL}}$ formula $F$ over $\Lambda=\{A,B\}$ be given:

[TABLE]

The graph language $\mathcal{L}(F)$ consists of all graphs which do not consist exclusively of $A$ -edges or of $B$ -edges, i.e., which contain at least one $A$ -labeled edge and at least one $B$ -labeled edge, something that can not be expressed by pure type graphs.

We now present some positive results for graph languages $\mathcal{L}(F)$ over ${\mathit{TGL}}$ formulas $F$ with respect to decidability problems. Due to the conjunction and negation operator, the emptiness (or unsatisfiability) check is not as trivial as it is for pure type graphs. Note that thanks to the presence of boolean connectives, inclusion can be reduced to emptiness.

Proposition 5

For a graph language $\mathcal{L}(F)$ characterized by a ${\mathit{TGL}}$ formula $F$ , the following problems are decidable:

•

Membership, i.e. for all graphs $G$ it is decidable if $G\in\mathcal{L}(F)$ holds.

•

Emptiness, i.e. it is decidable if $\mathcal{L}(F)=\varnothing$ holds.

•

Language inclusion, i.e. given two ${\mathit{TGL}}$ formulas $F_{1}$ and $F_{2}$ it is decidable if $\mathcal{L}(F_{1})\subseteq\mathcal{L}(F_{2})$ holds.

Such a logic could alternatively also be defined based on restriction graphs. A related logic, for injective occurrences of restriction graphs, is studied in [17], where the authors also give a decidability result via inference rules.

5 Annotated Type Graphs

In this section we will improve the expressiveness of the type graphs themselves, rather than using an additional logic to do so. We will equip graphs with additional annotations. As explained in the introduction, this idea was already used similarly in abstract graph rewriting. In contrast to most other approaches, we will investigate the problem from a categorical point of view.

The idea we follow is to annotate each element of a type graph with pairs of multiplicities, denoting upper and lower bounds. We will define a category of multiply annotated graphs, where we consider elements of a lattice-ordered monoid (short $\ell$ -monoid) as multiplicities.

Definition 9 (Lattice-ordered monoid)

A lattice-ordered monoid ( $\ell$ -monoid) $(\mathcal{M},+,\leq)$ consists of a set $\mathcal{M}$ , a partial order $\leq$ and a binary operation $+$ such that

•

$(\mathcal{M},\leq)$ is a lattice.

•

$(\mathcal{M},+)$ is a monoid; we denote its unit by [math].

•

It holds that $a+(b\lor c)=(a+b)\lor(a+c)$ and $a+(b\land c)=(a+b)\land(a+c)$ , where $\land,\lor$ are the meet and join of $\leq$ .

We denote by ${\mathbf{{\ell}Mon}}$ the category having $\ell$ -monoids as objects and as arrows monoid homomorphisms which are monotone.

Example 5

Let $n\in\mathbb{N}\backslash\{0\}$ and take $\mathcal{M}_{n}=\{0,1,\dots,n,m\}$ (zero, one, $\dots$ , $n$ , many) with $0\leq 1\leq\dots\leq n\leq m$ and addition as monoid operation with the proviso that $\ell_{1}+\ell_{2}=m$ if the sum is larger than $n$ . Clearly, for all $a,b,c\in\mathcal{M}_{n}$ $a\lor b=\text{max}\{a,b\}$ and $a\land b=\text{min}\{a,b\}$ . From this we can infer distributivity and therefore $(\mathcal{M}_{n},+,\leq)$ forms an $\ell$ -monoid.

Furthermore, given a set $S$ and an $\ell$ -monoid $(\mathcal{M},+,\leq)$ , it is easy to check that also $(\{a\colon S\to\mathcal{M}\},+,\leq)$ is an $\ell$ -monoid, where the elements are functions from $S$ to $\mathcal{M}$ and the partial order and the monoidal operation are taken pointwise.

In the following we will sometimes denote an $\ell$ -monoid by its underlying set.

Definition 10 (Annotations and multiplicities for graphs)

Given a functor $\mathcal{A}\colon{\mathbf{Graph}}\to{\mathbf{{\ell}Mon}}$ , an annotation based on $\mathcal{A}$ for a graph $G$ is an element $a\in\mathcal{A}(G)$ . We write $\mathcal{A}_{\varphi}$ , instead of $\mathcal{A}(\varphi)$ , for the action of functor $\mathcal{A}$ on a graph morphism $\varphi$ . We assume that for each graph $G$ there is a standard annotation based on $\mathcal{A}$ that we denote by $s_{G}$ , thus $s_{G}\in\mathcal{A}(G)$ .

Given an $\ell$ -monoid $\mathcal{M}_{n}=\{0,1,\dots,n,m\}$ we define the functor $\mathcal{B}^{n}:{\mathbf{Graph}}\to{\mathbf{{\ell}Mon}}$ as follows:

•

for every graph $G$ , $\mathcal{B}^{n}(G)=\{a\colon(V_{G}\cup E_{G})\to\mathcal{M}_{n}\}$ ;

•

for every graph morphism $\varphi\colon G\to G^{\prime}$ and $a\in\mathcal{B}^{n}(G)$ , we have

$\mathcal{B}^{n}_{\varphi}(a)\colon V_{G^{\prime}}\cup E_{G^{\prime}}\to\mathcal{M}_{n}$ with:

[TABLE]

Therefore an annotation based on a functor $\mathcal{B}^{n}$ associates every item of a graph with a number (or the top value $m$ ). We will call such kind of annotations multiplicities. Furthermore, the action of the functor on a morphism transforms a multiplicity by summing up (in $\mathcal{M}_{n}$ ) the values of all items of the source graph that are mapped to the same item of the target graph.

For a graph $G$ , its standard multiplicity $s_{G}\in\mathcal{B}^{n}(G)$ is defined as the function which maps every node and edge of $G$ to 1.

Some of the results that we will present in the rest of the paper will hold for annotations based on a generic functor $\mathcal{A}$ , some only for annotations based on functors $\mathcal{B}^{n}$ , i.e. for multiplicities.

The type graphs which we are going to consider are enriched with a set of pairs of annotations. The motivation for considering multiple annotations rather than a single one is mainly to ensure closure under union. Each pair can be interpreted as establishing a lower and an upper bound to what a graph morphism can map to the graph.

Definition 11 (Multiply annotated graphs)

Given a functor $\mathcal{A}\colon{\mathbf{Graph}}\to{\mathbf{{\ell}Mon}}$ , a multiply annotated graph $G[M]$ (over $\mathcal{A}$ ) is a graph $G$ equipped with a finite set of pairs of annotations $M\subseteq\mathcal{A}(G)\times\mathcal{A}(G)$ , such that $\ell\leq u$ for all $(\ell,u)\in M$ .

An arrow $\varphi\colon G[M]\to G^{\prime}[M^{\prime}]$ , also called a legal morphism, is a graph morphism $\varphi\colon G\to G^{\prime}$ such that for all $(\ell,u)\in M$ there exists $(\ell^{\prime},u^{\prime})\in M^{\prime}$ with $\mathcal{A}_{\varphi}(\ell)\geq\ell^{\prime}$ and $\mathcal{A}_{\varphi}(u)\leq u^{\prime}$ . We will write $G[\ell,u]$ as an abbreviation of $G[\{(\ell,u)\}]$ . In case of annotations based on $\mathcal{B}^{n}$ , we will often call a pair $(\ell,u)$ a double multiplicity.

Multiply annotated graphs and legal morphisms form a category.

Lemma 1

The composition of two legal morphisms is a legal morphism.

Example 6

Consider the following multiply annotated graphs (over $\mathcal{B}^{2}$ ) $G[\ell,u]$ and $H[\ell^{\prime},u^{\prime}]$ , both having one double multiplicity.

[TABLE]

As evident from the picture, multiplicities are represented by writing the lower and upper bounds next to the corresponding graph elements. Note that there is a unique, obvious graph morphism $\varphi\colon G\to H$ , mapping both nodes of $G$ to the only node of $H$ . Concerning multiplicities, by adding the lower and upper bounds of the two nodes of $G$ , one gets the interval $[2,m]$ which is included in the interval of the node of $H$ , $[1,m]$ . Similarly, the double multiplicity $[0,1]$ of the edge of $G$ is included in $[0,m]$ . Therefore, since both $\mathcal{B}^{2}_{\varphi}(\ell)\geq\ell^{\prime}$ and $\mathcal{B}^{2}_{\varphi}(u)\leq u^{\prime}$ hold, we can conclude that $\varphi\colon G[\ell,u]\to H[\ell^{\prime},u^{\prime}]$ is a legal morphism.

We are now ready to define how a graph language $\mathcal{L}(T[M])$ looks like.

Definition 12 (Graph languages of multiply annotated type graphs)

We say that a graph $G$ is represented by a multiply annotated type graph $T[M]$ whenever there exists a legal morphism $\varphi\colon G[s_{G},s_{G}]\to T[M]$ , i.e., there exists $(\ell,u)\in M$ such that $\ell\leq\mathcal{A}_{\varphi}(s_{G})\leq u$ . We will write $G\in\mathcal{L}(T[M])$ in this case. Whenever $M=\varnothing$ for a multiply annotated type graph $T[M]$ we get $\mathcal{L}(T[M])=\varnothing$ .

An extended example can be found in Appendix 0.B.

5.1 Decidability Properties for Multiply Annotated Graphs

We now address some decidability problems for languages defined by multiply annotated graphs. We get positive results with respect to the membership and emptiness problems. However, for decidability of language inclusion we only get partial results.

For the membership problem we can simply enumerate all graph morphisms $\varphi\colon G\to T$ and check if there exists a legal morphism $\varphi\colon G[s_{G},s_{G}]\to T[M]$ .

The emptiness check is somewhat more involved, since we have to take care of “illegal” annotations.

Proposition 6

For a graph language $\mathcal{L}(T[M])$ characterized by a multiply annotated type graph $T[M]$ over $\mathcal{B}^{n}$ the emptiness problem is decidable: $\mathcal{L}(T[M])=\varnothing$ iff $M=\varnothing$ or for each $(\ell,u)\in M$ there exists an edge $e\in E_{T}$ such that $\ell(e)\geq 1$ and $(u(\mathit{src}(e))=0$ or $u(\mathit{tgt}(e))=0)$ .

Language inclusion can be deduced from the existence of a legal morphism between the two multiply annotated type graphs.

Proposition 7

The existence of a legal morphism $\varphi\colon T_{1}[M]\to T_{2}[N]$ implies $\mathcal{L}(T_{1}[M])\subseteq\mathcal{L}(T_{2}[N])$ .

We would like to remark that this condition is sufficient but not necessary, and we present the following counterexample. Let the following two multiply annotated type graphs $T_{1}[M_{1}]$ and $T_{2}[M_{2}]$ over $\mathcal{B}^{1}$ be given where $|M_{1}|=|M_{2}|=1$ :

[TABLE]

Clearly we have that the languages $\mathcal{L}(T_{1}[M_{1}])$ and $\mathcal{L}(T_{2}[M_{2}])$ are equal as both contain all discrete non-empty graphs. Thus $\mathcal{L}(T_{1}[M_{1}])\subseteq\mathcal{L}(T_{2}[M_{2}])$ , but there exists no legal morphism $\varphi\colon T_{1}[M_{1}]\to T_{2}[M_{2}]$ . In fact, the upper bound of the first node of $T_{2}$ would be violated if the node of $T_{1}$ is mapped by $\varphi$ to it, while the lower bound would be violated if the node of $T_{1}$ is mapped to the other node.

5.2 Deciding Language Inclusion for Annotated Type Graphs

In this section we show that if we allow only bounded graph languages consisting of graphs up to a fixed pathwidth, the language inclusion problem becomes decidable for annotations based on $\mathcal{B}^{n}$ . Pathwidth is a well-known concept from graph theory that intuitively measures how much a graph resembles a path.

The proof is based on the notion of recognizability, which will be described via automaton functors that were introduced in [4]. We start with the main result and explain step by step the arguments that will lead to decidability.

Proposition 8

The language inclusion problem is decidable for graph languages of bounded pathwidth characterized by multiply annotated type graphs over $\mathcal{B}^{n}$ . That is, given $k\in\mathbb{N}$ and two multiply annotated type graphs $T_{1}[M_{1}]$ and $T_{2}[M_{2}]$ over $\mathcal{B}^{n}$ , it is decidable whether $\mathcal{L}(T_{1}[M_{1}])^{\leq k}\subseteq\mathcal{L}(T_{2}[M_{2}])^{\leq k}$ , where $\mathcal{L}(T[M])^{\leq k}=\{G\in\mathcal{L}(T[M])\mid G$ has pathwidth $\leq k\}$ .

Our automaton model, given by automaton functors, reads cospans (i.e., graphs with interfaces) instead of single graphs. Therefore in the following, the category under consideration will be $\emph{Cospan}_{m}({\mathbf{Graph}})$ , i.e. the category of cospans of graphs where the objects are discrete graphs $J,K$ and the arrows are cospans $c\colon J\to G\leftarrow K$ where both graph morphisms are injective. We will refer to the graph $J$ as the inner interface and to the graph $K$ as the outer interface of the graph $G$ . In addition we will sometimes abbreviate the cospan $c\colon J\to G\leftarrow K$ to the short representation $c\colon J\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}K$ .

According to [3] a graph has pathwidth $k$ iff it can be decomposed into cospans where each middle graph of a cospan has at most $k+1$ nodes. Hence it is easy to check that a path has pathwidth $1$ , while a clique of order $k$ has pathwidth $k-1$ .

Our main goal is to build an automaton which can read all graphs of our language step by step, similar to the idea of finite automata reading words in formal languages. Such an automaton can be constructed for an unbounded language, where the pathwidth is not restricted. However, we obtain a finite automaton only if we restrict the pathwidth. Then we can use well-known algorithms for finite automata to solve the language inclusion problem. Note that, if we would use tree automata instead of finite automata, our result could be generalized to graphs of bounded treewidth.

We will first introduce the notion of automaton functor (which is a categorical automaton model for so-called recognizable arrow languages) and which is inspired by Courcelle’s theory of recognizable graph languages [8].

Definition 13 (Automaton functor [4])

An automaton functor $\mathcal{C}\colon\emph{Cospan}_{m}({\mathbf{Graph}})\to\mathbf{Rel}$ is a functor that maps every object $J$ (i.e., every discrete graph) to a finite set $\mathcal{C}(J)$ (the set of states of $J$ ) and every cospan $c\colon J\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}K$ to a relation $\mathcal{C}(c)\subseteq\mathcal{C}(J)\times\mathcal{C}(K)$ (the transition relation of $c$ ). In addition there is a distinguished set of initial states $I\subseteq\mathcal{C}(\varnothing)$ and a distinguished set of final states $F\subseteq\mathcal{C}(\varnothing)$ . The language $\mathcal{L}_{\mathcal{C}}$ of $\mathcal{C}$ is defined as follows:

A graph $G$ is contained in $\mathcal{L}_{\mathcal{C}}$ if and only if there exist states $q\in I$ and $q^{\prime}\in F$ which are related by $\mathcal{C}(c)$ , i.e. $(q,q^{\prime})\in\mathcal{C}(c)$ , where $c\colon\varnothing\to G\leftarrow\varnothing$ is the unique cospan with empty interfaces and middle graph $G$ .

Languages accepted by automaton functors are called recognizable.

We will now define an automaton functor for a type graph $T[M]$ over $\mathcal{B}^{n}$ .

Definition 14 (Counting cospan automaton)

Let $T[M]$ be a multiply annotated type graph over $\mathcal{B}^{n}$ . We define an automaton functor $\mathcal{C}_{T[M]}\colon\emph{Cospan}_{m}({\mathbf{Graph}})\linebreak\to\mathbf{Rel}$ as follows:

•

For each object $J$ of $\emph{Cospan}_{m}({\mathbf{Graph}})$ (thus $J$ is a finite discrete graph), $\mathcal{C}_{T[M]}(J)=\{(f,b)\mid f\colon J\to T,b\in\mathcal{B}^{n}(T)\}$ is its finite set of states

•

$I\subseteq\mathcal{C}_{T[M]}(\varnothing)$ is the set of initial states with $I=\{(f\colon\varnothing\to T,0)\}$ , where [math] is the constant [math]-function

•

$F\subseteq\mathcal{C}_{T[M]}(\varnothing)$ is the set of final states with $F=\{(f\colon\varnothing\to T,b)\mid\exists(\ell,u)\in M:\ell\leq b\leq u\}$

– Let $c\colon J\mathbin{\mathchoice{\xrightarrow{\psi_{L}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle\psi_{L} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\psi_{L} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\psi_{L} $}}{\shortrightarrow}}}G\mathchoice{\xleftarrow{\psi_{R}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle\psi_{R} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\psi_{R} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\psi_{R} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}K$ be an arrow in the category $\emph{Cospan}_{m}({\mathbf{Graph}})$ with discrete interface graphs $J$ and $K$ where both graph morphisms $\psi_{L}\colon J\to G$ and $\psi_{R}\colon K\to G$ are injective. Two states $(f\colon J\to T,b)$ and $(f^{\prime}\colon K\to T,b^{\prime})$ are in the relation $\mathcal{C}_{T[M]}(c)$ if and only if there exists a morphism $h\colon G\to T$ such that the diagram to the right commutes and for all $x\in V_{T}\cup E_{T}$ the following equation holds:

$J$$G$$K$$T$$c\colon J\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}K$$f$$\psi_{L}$$\exists h$$\psi_{R}$$f^{\prime}$

[TABLE]

The set $G\setminus\psi_{R}(K)$ consists of all elements of $G$ which are not targeted by the morphism $\psi_{R}$ , e.g. $G\setminus\psi_{R}(K)=(V_{G}\setminus\psi_{R}(V_{K}))\cup(E_{G}\setminus\psi_{R}(E_{K}))$ . Instead of $\mathcal{L}_{\mathcal{C}_{T[M]}}$ and $\mathcal{C}_{T[M]}$ we just write $\mathcal{L}_{\mathcal{C}}$ and $\mathcal{C}$ if $T[M]$ is clear from the context.

The intuition behind this construction is to count for each item $x$ of $T$ , step by step, the number of elements that are being mapped from a graph $G$ (which is in the form of a cospan decomposition) to $x$ , and then check if the bounds of a pair of annotations $(\ell,u)\in M$ of the multiply annotated type graph $T[M]$ are satisfied. We give a short example before moving on to the results.

Example 7

Let the following multiply annotated type graph (over $\mathcal{B}^{2}$ ) $T[\ell,u]$ and the cospan $(c\colon\varnothing\to G\leftarrow\varnothing)$ with $G\in\mathcal{L}(T[\ell,u])$ be given:

[TABLE]

We will now decompose the cospan $c$ into two cospans $c_{1},c_{2}$ with $c=c_{1};c_{2}$ in the following way:

$\varnothing$$\mathit{A}$$\mathit{B}$$\varnothing$$c_{1}$$c_{2}$$c$

We let our counting cospan automaton parse the cospan decomposition $c_{1};c_{2}$ step by step now to show how the annotations for the type graph $T$ evolve during the process. According to our construction, every element in $T$ has multiplicity [math] in the initial state of the automaton. We then sum up the number of elements within the middle graphs of the cospans which are not part of the right interface. Therefore we get the following parsing process:

$\varnothing$$\mathit{A}$$\mathit{B}$$\varnothing$ [0][0]A[0]B[0][1][0]A[1]B[0][1][2]A[1]B[1] $f_{1}$$f_{2}$$f_{3}$$q_{1}$$q_{2}$$q_{3}$

We visited three states $q_{1},q_{2}$ and $q_{3}$ in the automaton with $(q_{1},q_{2})\in\mathcal{C}(c_{1})$ and $(q_{2},q_{3})\in\mathcal{C}(c_{2})$ . Since $\mathcal{C}$ is supposed to be a functor we get that $\mathcal{C}(c_{1});\mathcal{C}(c_{2})=\mathcal{C}(c)$ and therefore $(q_{1},q_{3})\in\mathcal{C}(c)$ also holds. In addition we have $q_{1}\in I$ and since the annotation function $b\in\mathcal{B}^{2}(T)$ in $q_{3}=(f_{3},b)$ satisfies $\ell\leq b\leq u$ we can infer that $q_{3}\in F$ . Therefore we can conclude that $G\in\mathcal{L}_{\mathcal{C}}$ holds as well.

We still need to prove that $\mathcal{C}$ is indeed a functor. Intuitively this shows that acceptance of a graph by the automaton is not dependent on its specific decomposition.

Proposition 9

Let $c_{1}\colon J\to G\leftarrow K$ and $c_{2}\colon K\to H\leftarrow L$ be two arrows and let $id_{G}\colon G\to G\leftarrow G$ be the identity cospan.

The mapping $\mathcal{C}_{T[M]}\colon\emph{Cospan}_{m}({\mathbf{Graph}})\to\mathbf{Rel}$ is a functor:

$\mathcal{C}_{T[M]}(id_{G})=id_{C_{T[M]}(G)}$ ** 2. 2.

$\mathcal{C}_{T[M]}(c_{1};c_{2})=\mathcal{C}_{T[M]}(c_{1});\mathcal{C}_{T[M]}(c_{2})$ **

The language accepted by the automaton $\mathcal{L}_{\mathcal{C}}$ is exactly the graph language $\mathcal{L}(T[M])$ .

Proposition 10

Let the multiply annotated type graph $T[M]$ (over $\mathcal{B}^{n}$ ) and the corresponding automaton functor $\mathcal{C}\colon\emph{Cospan}_{m}({\mathbf{Graph}})\to\mathbf{Rel}$ for $T[M]$ be given. Then $\mathcal{L}_{\mathcal{C}}=\mathcal{L}(T[M])$ holds, i.e. for a graph $G$ we have $G\in\mathcal{L}(T[M])$ if and only if there exist states $i\in I\subseteq\mathcal{C}(\varnothing)$ and $f\in F\subseteq\mathcal{C}(\varnothing)$ such that $(i,f)\in\mathcal{C}(c)$ , where $c\colon\varnothing\to G\leftarrow\varnothing$ .

Therefore we can construct an automaton for each graph language specified by a multiply annotated type graph $T[M]$ , which accepts exactly the same language. In case of a bounded graph language this automaton will have only finitely many states. Furthermore we can restrict the label alphabet, i.e., the cospans by using only atomic cospans, adding a single node or edges (see [2]). Once these steps are performed, we obtain conventional non-deterministic finite automata over a finite alphabet and we can use standard techniques from automata theory to solve the language inclusion problem directly on the finite automata.

5.3 Closure Properties for Multiply Annotated Graphs

Extending the expressiveness of the type graphs by adding multiplicities gives us positive results in case of closure under union and intersection. Here we use constructions that rely on products and coproducts in the category of graphs.

Closure under intersection holds for the most general form of annotations. From $T_{1}[M_{1}]$ , $T_{2}[M_{2}]$ we can construct an annotated type graph $(T_{1}\times T_{2})[N]$ , where $N$ contains all annotations which make both projections $\pi_{i}\colon T_{1}\times T_{2}\to T_{i}$ legal.

Proposition 11

The category of multiply annotated graphs is closed under intersection.

We can prove closure under union for the case of annotations based on the functor $\mathcal{B}^{n}$ . Here we take the coproduct $(T_{1}\oplus T_{2})[N]$ , where $N$ contains all annotations of $M_{1}$ , $M_{2}$ , transferred to $T_{1}\oplus T_{2}$ via the injections $i_{j}\colon T_{j}\to T_{1}\oplus T_{2}$ . Intuitively, graph items not in the original domain of the annotations receive annotation $[0,0]$ . This can be generalized under some mild assumptions(see proof in the appendix).

Proposition 12

The category of multiply annotated graphs over functor $\mathcal{B}^{n}$ is closed under union.

Closure under complement is still an open issue. If we restrict to graphs of bounded pathwidth, we have a (non-deterministic) automaton (functor), as described in Section 5.1, which could be determinized and complemented. However, this does not provide us with an annotated type graph for the complement. We conjecture that closure under complement does not hold.

6 Conclusion

Our results on decidability and closure properties for specification languages are summarized in the following table. In the case where the results hold only for bounded pathwidth, the checkmark is in brackets.

[TABLE]

One open question that remains is whether language inclusion for annotated type graphs is decidable if we do not restrict to bounded treewidth. Similarly, closure under complement is still open.

Furthermore, in order to be able to use these formalisms extensively in applications, it is necessary to provide a mechanism to compute weakest preconditions and strongest postconditions. This does not seem feasible for pure type graphs or the type graph logic. Hence, we are currently working on characterizing weakest preconditions and strongest postconditions in the setting of annotated type graphs. This requires a materialisation construction, similar to [23], which we plan to characterize abstractly, exploiting universal properties in category theory.

Note that our annotations are global, i.e., we count all items that are mapped to a specific item in the type graph. This holds also for edges, as opposed to UML multiplicities, which are local wrt. the classes which are related by an edge (i.e., an association). We plan to study the possibility to integrate this into our framework and investigate the corresponding decidability and closure properties.

Related work: As already mentioned there are many approaches for specifying graph languages. One can not say that one is superior to the other, usually there is a tradeoff between expressiveness and decidability properties, furthermore they differ in terms of closure properties.

Recognizable graph languages [7, 8], which are the counterpart to regular word languages, are closely related with monadic second-order graph logic. If one restricts recognizable graph languages to bounded treewidth (or pathwidth as we did), one obtains satisfactory decidability properties. On the other hand, the size of the resulting graph automata is often quite intimidating [2] and hence they are difficult to work with in practical applications. The use of nested application conditions [12], equivalent to first-order logic [20], has a long tradition in graph rewriting and they can be used to compute pre- and postconditions for rules [18]. However, satisfiability and implication are undecidable for first-order logic.

A notion of grammars that is equivalent to context-free (word) grammars are hyperedge replacement grammars [11]. Many aspects of the theory of context-free languages can be transferred to the graph setting.

In heap analysis the representation of pointer structures to be analyzed requires methods to specify sets of graphs. Hence both the TVLA approach by Sagiv, Reps and Wilhelm [23], as well as separation logic [16, 9] face this problem. In [23] heaps are represented by graphs, annotated with predicates from a three-valued logics (with truth values yes, no and maybe).

A further interesting approach are forest automata [1] that have many interesting properties, but are somewhat complex to handle.

In [22] the authors study an approach called Diagram Predicate Framework (DPF), in which type graphs have annotations based on generalized sketches. This formalism is intended for MOF-based modelling languages and allows more complex annotations than our framework.

Appendix 0.A Proofs

0.A.1 Languages Specified by Type or Restriction Graphs

Proposition 1.* Type graph languages are closed under intersection (by taking the product of type graphs) but not under union or complementation, while restriction graph languages are closed under union (by taking the coproduct of restriction graphs) but not under intersection or complementation. *

Proof

The product $T_{1}\times T_{2}$ has the property that for any graph $G$ we have $G\to T_{1}\times T_{2}$ if and only if $G\to T_{1}$ and $G\to T_{2}$ . Hence, given two type graphs $T_{1}$ and $T_{2}$ , by the universal property of the product graph we get immediately the following equality: $\mathcal{L}(T_{1})\cap\mathcal{L}(T_{2})=\mathcal{L}(T_{1}\times T_{2})$ .

Dually, given two restriction graphs $R_{1}$ and $R_{2}$ , we show that $\mathcal{L}_{R}(R_{1})\cup\mathcal{L}_{R}(R_{2})=\mathcal{L}_{R}(R_{1}\oplus R_{2})$ . In fact, $G\not\in\mathcal{L}_{R}(R_{1}\oplus R_{2})$ iff $R_{1}\oplus R_{2}\to G$ , iff (by the universal property of coproducts) $R_{1}\to G$ and $R_{2}\to G$ , iff $G\not\in\mathcal{L}_{R}(R_{1})$ and $G\not\in\mathcal{L}_{R}(R_{2})$ , iff $G\not\in(\mathcal{L}_{R}(R_{1})\cup\mathcal{L}_{R}(R_{2}))$ .

For the negative results, we will show counterexamples using the following graphs over $\Lambda=\{A,B\}$ :

[TABLE]

We first show by contradiction that there is no type graph $T$ such that $\mathcal{L}(T)=\mathcal{L}(G_{A})\cup\mathcal{L}(G_{B})$ . In fact, the type graph language $\mathcal{L}(G_{A})$ contains all graphs which do not have any $B$ -labeled edge, and $\mathcal{L}(G_{B})$ contains all graphs which do not have any $A$ -labeled edge. Since $G_{A},G_{B}\in\mathcal{L}(G_{A})\cup\mathcal{L}(G_{B})$ , we would have $G_{A}\to T$ and $G_{B}\to T$ , which implies that $T$ contains at least one $A$ -labeled loop (thus $T\nrightarrow G_{B}$ ) and one $B$ -labeled loop (thus $T\nrightarrow G_{A}$ ). It follows that $T\not\in\mathcal{L}(G_{A})\cup\mathcal{L}(G_{B})$ , but instead $T\in\mathcal{L}(T)$ yielding a contradiction.

Now we show by contradiction that there is no restriction graph $R$ such that $\mathcal{L}_{R}(R)=\mathcal{L}_{R}(G_{A})\cap\mathcal{L}_{R}(G_{B})$ . In fact, if such an $R$ exists we would have $\mathcal{L}_{R}(R)\subseteq\mathcal{L}_{R}(G_{A})$ , and thus $R\to G_{A}$ by Proposition 2.4, and $\mathcal{L}_{R}(R)\subseteq\mathcal{L}_{R}(G_{B})$ , and thus $R\to G_{B}$ . But $R\to G_{A}$ means that $R$ has no $B$ -edges, and $R\to G_{B}$ that it has no $A$ -edges, thus $R$ must be discrete. This yields a contradiction, because any graph $G$ with no loops but with at least one edge belongs to $\mathcal{L}_{R}(G_{A})\cap\mathcal{L}_{R}(G_{B})$ but not to $\mathcal{L}_{R}(R)$ , because $R\to G$ .

The lack of closure under complementation immediately follows from these negative results and the fact that union can be expressed using intersection and complementation, and dually. ∎

Proposition 2.*

For a graph language $\mathcal{L}$ characterized by a type graph $T$ (i.e. $\mathcal{L}=\mathcal{L}(T)$ ) or by a restriction graph $R$ (i.e. $\mathcal{L}=\mathcal{L}_{R}(R)$ ) the following problems are decidable:*

Membership, i.e. for each graph $G$ it is decidable if $G\in\mathcal{L}$ holds. 2. 2.

Emptiness, i.e. it is decidable if $\mathcal{L}=\varnothing$ holds.

*Furthermore, language inclusion is decidable for both classes of languages: *

Given type graphs $T_{1}$ and $T_{2}$ it is decidable if $\mathcal{L}(T_{1})\subseteq\mathcal{L}(T_{2})$ holds. 2. 4.

Given restriction graphs $R_{1}$ and $R_{2}$ it is decidable if $\mathcal{L}_{R}(R_{1})\subseteq\mathcal{L}_{R}(R_{2})$ holds.

Proof

To decide whether $G\in\mathcal{L}(T)$ (or $G\in\mathcal{L}_{R}(R)$ ) holds, we need to check for the existence of a morphism $\varphi\colon G\to T$ (or for the non-existence of a morphism $\varphi\colon R\to G$ ), which is obviously possible because graphs are finite. Nevertheless, note that this problem is NP-complete. For instance, searching for a morphism from any graph into the 3-clique is the same as deciding if the graph is 3-colorable. 2. 2.

The emptiness problem is pretty trivial. If $\mathcal{L}=\mathcal{L}(T)$ for a type graph $T$ , then $\mathcal{L}(T)\neq\varnothing$ because it holds $\varnothing\in\mathcal{L}(T)$ (recall that $\varnothing$ is the initial object of ${\mathbf{Graph}}$ ).

If instead $\mathcal{L}=\mathcal{L}_{R}(R)$ for a restriction graph $R$ , then $\mathcal{L}=\varnothing$ if and only if $R=\varnothing$ . In fact, if $R=\varnothing$ then $R\to G$ for all $G\in{\mathbf{Graph}}$ , and thus $\mathcal{L}_{R}(R)=\varnothing$ . Instead if $R\not=\varnothing$ then clearly $R\nrightarrow\varnothing$ , thus $\varnothing\in\mathcal{L}_{R}(R)\not=\varnothing$ . 3. 3.

We show that $\mathcal{L}(T_{1})\subseteq\mathcal{L}(T_{2})$ iff $T_{1}\to T_{2}$ , which is decidable.

$\Rightarrow$ : Assume $\mathcal{L}(T_{1})\subseteq\mathcal{L}(T_{2})$ holds. Since $T_{1}\in\mathcal{L}(T_{1})$ holds then $T_{1}\in\mathcal{L}(T_{2})$ also holds and therefore $T_{1}\to T_{2}$ .

$\Leftarrow$ : Assume $T_{1}\to T_{2}$ holds, and let $G\in\mathcal{L}(T_{1})$ . Therefore $G\to T_{1}$ , and by transitivity $G\to T_{2}$ , thus $G\in\mathcal{L}(T_{2})$ . 4. 4.

We show that $\mathcal{L}_{R}(R_{1})\subseteq\mathcal{L}_{R}(R_{2})$ iff $R_{1}\to R_{2}$ .

$\Rightarrow$ : Assume that $\mathcal{L}_{R}(R_{1})\subseteq\mathcal{L}_{R}(R_{2})$ holds. Equivalently, $\{G\mid R_{2}\to G\}=\overline{\mathcal{L}_{R}(R_{2})}\subseteq\overline{\mathcal{L}_{R}(R_{1})}=\{G\mid R_{1}\to G\}$ , where we wrote $\overline{\mathcal{L}}$ for the complement language $({\mathbf{Gr_{\Lambda}}}\setminus\mathcal{L})$ . Thus, since obviously $R_{2}\to R_{2}$ , we obtain $R_{1}\to R_{2}$ .

$\Leftarrow$ : Assume that $R_{1}\to R_{2}$ holds and that $G\in{\mathcal{L}_{R}(R_{1})}$ , which means $R_{1}\nrightarrow G$ . If, by contradiction, $G\not\in{\mathcal{L}_{R}(R_{2})}$ , then we have $R_{2}\to G$ and, by transitivity, $R_{1}\to G$ , which is a contradiction.∎

Proposition 3.* A restriction graph language $\mathcal{L}_{R}(S)$ is closed under a rule $\rho=(L\mathchoice{\xleftarrow{\varphi_{L}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}I\mathbin{\mathchoice{\xrightarrow{\varphi_{R}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}}R)$ if and only if the following condition holds: for every pair of morphisms $\alpha\colon R\to F$ , $\beta\colon S\to F$ which are jointly surjective, applying the rule $\rho$ with (co-)match $\alpha$ backwards to $F$ yields a graph $E$ with a homomorphic image of $S$ , i.e., $E\not\in\mathcal{L}_{R}(S)$ . *

Proof

$\Leftarrow$ : Assume that the condition holds. Now let $G,H$ with $G\Rightarrow_{\rho}H$ . Instead of showing that $G\in\mathcal{L}_{R}(S)$ implies $H\in\mathcal{L}_{R}(S)$ , we show that $H\not\in\mathcal{L}_{R}(S)$ implies $G\not\in\mathcal{L}_{R}(S)$ .

Since $G\Rightarrow_{\rho}H$ we have the following DPO diagram (below, on the left) for a rule $\rho=(L\mathchoice{\xleftarrow{\varphi_{L}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}I\mathbin{\mathchoice{\xrightarrow{\varphi_{R}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}}R)\in\mathcal{R}$ . Furthermore, since $H\not\in\mathcal{L}_{R}(S)$ , there exists a morphism $S\to H$ .

[TABLE]

Now take the joint image $F$ of $R$ and $S$ in $H$ , i.e., factor the morphisms $\alpha$ , $\beta$ into $R\to F\rightarrowtail H$ and $S\to F\rightarrowtail H$ , where the arrows $R\to F$ , $S\to F$ are jointly epi. Since we are working in an adhesive category, the pushouts split into pushouts according to [14] (see diagram above, on the right). Now, $E$ is obtained from $F$ by applying rule $\rho$ backwards. Hence, the condition implies that there exists a morphism $S\to E$ and this means that there is a morphism $S\to G$ , which implies $G\not\in\mathcal{L}_{R}(S)$ .

$\Rightarrow$ : Assume that $\mathcal{L}_{R}(S)$ is closed under rewriting via a rule $\rho$ . We show that the condition holds. Let $\alpha\colon R\to F$ , $\beta\colon S\to F$ be a pair of morphisms which are jointly epi and assume that $E$ is obtained from $F$ by applying $\rho$ backwards.

Now, since $E\Rightarrow_{\rho}F$ and $H\not\in\mathcal{L}_{R}(S)$ , we infer that $G\not\in\mathcal{L}_{R}(S)$ , otherwise we would have a counterexample to closure under rewriting. Hence there exists a morphism $S\to E$ . ∎

For the next result we need to recall the following lemma presented in [15].

Lemma 2 (Lemma 2.1 of [15])

Let $T$ be a graph and $\mathit{core}(T)$ be its core. Then for each morphism $f:T\to\mathit{core}(T)$ there exists a morphism $f^{\prime}:\mathit{core}(T)\to T$ such that $f\circ f^{\prime}=id_{\mathit{core}(T)}$ . Vice versa, for each morphism $g^{\prime}:\mathit{core}(T)\to T$ there exists a morphism $g:T\to\mathit{core}(T)$ such that $g\circ g^{\prime}=id_{\mathit{core}(T)}$ .

Proposition 4.* A type graph language $\mathcal{L}(T)$ is closed under a rule $\rho=(L\mathchoice{\xleftarrow{\varphi_{L}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}I\mathbin{\mathchoice{\xrightarrow{\varphi_{R}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}}R)$ if and only if for each morphism $t_{L}\colon L\to\mathit{core}(T)$ , there exists a morphism $t_{R}\colon R\to\mathit{core}(T)$ such that $t_{L}\circ\varphi_{L}=t_{R}\circ\varphi_{R}$ .*

$L$$I$$R$$\mathit{core}(T)$$\Leftrightarrow$$\mathcal{L}(T)$ is closed under application of $\rho$$\rho$$\forall t_{L}$$\varphi_{L}$$\varphi_{R}$$\exists t_{R}$

Proof

$\Rightarrow$ : Notice that if $L\not\in\mathcal{L}(T)$ then there is no morphism $t_{L}\colon L\to\mathit{core}(T)$ and we are done. Otherwise, let $t_{L}\colon L\to\mathit{core}(T)$ , and let $n:I\to\mathit{core}(T)$ be defined as $n=t_{L}\circ\varphi_{L}$ . Consider the following diagram, where the top span is the rule, and the two squares are built as pushouts ( $A$ is the pushout of $\varphi_{L},n$ ; $B$ is the pushout of $\varphi_{R},n$ ).

[TABLE] $\textstyle{L\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t_{L}}$$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varphi_{L}}$$\scriptstyle{\varphi_{R}}$$\scriptstyle{n}$$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\@ensuremath{\mathit{core}(T)}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{id}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g^{\prime}}$$\textstyle{\@ensuremath{\mathit{core}(T)}}$

Arrow $A\to\mathit{core}(T)$ is uniquely determined because the left square is a pushout and $id\circ n=t_{L}\circ\varphi_{L}$ . This arrow witnesses that $A\in\mathcal{L}(T)$ (because $\mathit{core}(T)\to T$ ), and thus by assumption $B\in\mathcal{L}(T)$ , because obviously $A\Rightarrow_{\rho}B$ . Therefore we know that $B\to T$ , and thus that there is an arrow $g:B\to\mathit{core}(T)$ . In general, this arrow does not make the lower right triangle commute, but given that we also have arrow $f:\mathit{core}(T)\to B$ as the base of the right pushout, it follows that $B\sim T$ and hence $\mathit{core}(B)\cong\mathit{core}(T)$ . Therefore by Lemma 2, we know that there is an arrow $g^{\prime}:B\to\mathit{core}(T)$ such that $g^{\prime}\circ f=id_{\mathit{core}(T)}$ (in particular, $g^{\prime}=(g\circ f)^{-1}\circ g$ ). Therefore in the above diagram also the lower right triangle commutes, and arrow $t_{R}=g^{\prime}\circ m:R\to\mathit{core}(T)$ satisfies $t_{L}\circ\varphi_{L}=t_{R}\circ\varphi_{R}$ , as desired.

$\Leftarrow$ : Assume that $G\in\mathcal{L}(T)$ by morphism $t_{G}:G\to T$ , and that $G$ is rewritten to $H$ via rule $\rho=(L\mathchoice{\xleftarrow{\varphi_{L}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{L} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}I\mathbin{\mathchoice{\xrightarrow{\varphi_{R}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle\varphi_{R} $}}{\shortrightarrow}}}R)\in\mathcal{R}$ . Also, let $t$ be any arrow from $T$ to $\mathit{core}(T)$ . This gives us the diagram below, where the two squares are pushouts, and the left triangle commutes by taking for $C\to\mathit{core}(T)$ the composition $t\circ t_{G}\circ\psi_{L}$ .

$L$$I$$R$$G$$C$$H$$\mathit{core}(T)$$m$$\varphi_{L}$$n$$\varphi_{R}$$m^{\prime}$$\psi_{L}$$\psi_{R}$$t\circ t_{G}$$t_{R}$$t_{H}$

By assumption, since $t\circ t_{G}\circ m\colon L\to\mathit{core}(T)$ , there exists a morphism $t_{R}\colon R\to\mathit{core}(T)$ such that $t\circ t_{G}\circ m\circ\varphi_{L}=t_{R}\circ\varphi_{R}$ . This means that the square consisting of $I,C,R,\mathit{core}(T)$ commutes, that is $t\circ t_{G}\circ\psi_{L}\circ n=t\circ t_{G}\circ m\circ\varphi_{L}=t_{R}\circ\varphi_{R}$ . Hence there exists a mediating morphism $t_{H}\colon H\to\mathit{core}(T)$ , which implies $H\in\mathcal{L}(T)$ because $\mathit{core}(T)\to T$ . ∎

0.A.2 Type Graph Logic

Proposition 5.*

For a graph language $\mathcal{L}(F)$ characterized by a ${\mathit{TGL}}$ formula $F$ , the following problems are decidable:*

•

Membership, i.e. for all graphs $G$ it is decidable if $G\in\mathcal{L}(F)$ holds.

•

Emptiness, i.e. it is decidable if $\mathcal{L}(F)=\varnothing$ holds.

•

Language inclusion, i.e. given two ${\mathit{TGL}}$ formulas $F_{1}$ and $F_{2}$ it is decidable if $\mathcal{L}(F_{1})\subseteq\mathcal{L}(F_{2})$ holds.

Proof

Membership: The membership problem for graph languages over ${\mathit{TGL}}$ formulae is decidable since it is decidable for every type graph language $\mathcal{L}(T)$ . We simply build the syntax tree of the formula $F$ and search for morphisms $\varphi_{i}\colon G\to T_{i}$ at the leafs of the tree. Afterwards we pass the boolean results up to the root to decide whether $G\in\mathcal{L}(F)$ holds.

Emptiness: In order to show whether $\mathcal{L}(F)=\varnothing$ holds, we transform $F$ into disjunctive normal form (DNF). It is sufficient to check whether all conjunctions of the form $(T_{0}\land\lnot T_{1}\land\dots\land\lnot T_{n})$ are unsatisfiable. We can assume that there is at most one positive type graph in every conjunction, since type graphs are closed under conjunction/intersection. Furthermore we can even assume that there is exactly one positive type graph, since we always add $T_{\text{\char 92}}$ (the flower graph).

Now we have:

[TABLE]

Therefore, we need to check whether for each of the conjunctions $(T_{0}\land\lnot T_{1}\land\dots\land\lnot T_{n})$ in the DNF of $F$ , there exists a morphism $\varphi\colon T_{0}\to T_{k}$ for some $1\leq k\leq n$ .

Inclusion: The language inclusion problem can be reduced to the aforementioned emptiness problem. To solve the language inclusion we use the following equivalence:

[TABLE]

Since the emptiness problem is decidable we can conclude that the language inclusion problem is decidable as well. ∎

0.A.3 Annotated Type Graphs

Lemma 1.* The composition of two legal morphisms is a legal morphism. *

Proof

Let $\varphi_{1}\colon T_{1}[M_{1}]\to T_{2}[M_{2}]$ and $\varphi_{2}\colon T_{2}[M_{2}]\to T_{3}[M_{3}]$ be two legal morphisms in the category of multiply annotated graphs. Since $\varphi_{1}$ is legal we get that for all $(\ell_{1},u_{1})\in M_{1}$ there exists $(\ell_{2},u_{2})\in M_{2}$ such that $\ell_{2}\leq\mathcal{A}_{\varphi_{1}}(\ell_{1})$ and $\mathcal{A}_{\varphi_{1}}(u_{1})\leq u_{2}$ hold. Furthermore $\varphi_{2}$ is legal and therefore we get that for all $(\ell_{2},u_{2})\in M_{2}$ there exists $(\ell_{3},u_{3})\in M_{3}$ such that $\ell_{3}\leq\mathcal{A}_{\varphi_{2}}(\ell_{2})$ and $\mathcal{A}_{\varphi_{2}}(u_{2})\leq u_{3}$ hold as well. We define $\varphi\colon T_{1}[M_{1}]\to T_{3}[M_{3}]$ to be the composed morphism with $\varphi=\varphi_{2}\circ\varphi_{1}$ and due to the fact that $\mathcal{A}$ is a functor which preserves monotonicity, we get the following two inequalities:

[TABLE]

$\displaystyle\mathcal{A}_{\varphi_{1}}(u_{1})$ $\displaystyle\leq u_{2}$

$\displaystyle\Rightarrow$ $\displaystyle\mathcal{A}_{\varphi_{2}}(\mathcal{A}_{\varphi_{1}}(u_{1}))$ $\displaystyle\leq\mathcal{A}_{\varphi_{2}}(u_{2})$

$\displaystyle\Rightarrow$ $\displaystyle\mathcal{A}_{\varphi_{2}\circ\varphi 1}(u_{1})$ $\displaystyle\leq\mathcal{A}_{\varphi_{2}}(u_{2})\leq u_{3}$

$\displaystyle\Rightarrow$ $\displaystyle\mathcal{A}_{\varphi}(u_{1})$ $\displaystyle\leq u_{3}$

Since both $\ell_{3}\leq\mathcal{A}_{\varphi}(\ell_{1})$ and $\mathcal{A}_{\varphi}(u_{1})\leq u_{3}$ hold, the morphism $\varphi$ is legal. ∎

Proposition 6.*

For a graph language $\mathcal{L}(T[M])$ characterized by a multiply annotated type graph $T[M]$ over $\mathcal{B}^{n}$ the emptiness problem is decidable: $\mathcal{L}(T[M])=\varnothing$ iff $M=\varnothing$ or for each $(\ell,u)\in M$ there exists an edge $e\in E_{T}$ such that $\ell(e)\geq 1$ and $(u(\mathit{src}(e))=0$ or $u(\mathit{tgt}(e))=0)$ . *

Proof

$\Leftarrow$ : Assume that $M=\varnothing$ , in this case $\mathcal{L}(T[M])$ is clearly empty as well. Assume that there is an annotation $(\ell,u)\in M$ such that $\ell(e)\geq 1$ and ( $u(\mathit{src}(e))=0$ or $u(\mathit{tgt}(e))=0$ ) for some edge $e\in E_{T}$ . Then no graph can satisfy these lower and upper bounds, since we are forced to map at least one edge to $e$ , but are not allowed to map any node to the source respectively target node. If this is true for all annotations, the language of the type graph must be empty.

$\Rightarrow$ : Now assume that $M\neq\varnothing$ and there exists one annotation $(\ell,u)\in M$ such that for every edge $e\in E_{T}$ with $\ell(e)\geq 1$ we have $u(\mathit{src}(e))\geq 1$ and $u(\mathit{tgt}(e))\geq 1$ ).

Now take $T[\ell,u]$ and remove from $T$ all edges and nodes $x$ with $u(x)=0$ , resulting in a graph $T^{\prime}$ . If a node is removed all incident edges are removed as well. Note that in such a case only edges $e$ with $\ell(e)=0$ will be removed (due to the condition above).

Now define $\ell^{\prime}=\ell|_{T^{\prime}}$ and $u^{\prime}=u|_{T^{\prime}}$ . Due to the considerations above there exists a legal morphisms (embedding) $T^{\prime}[\ell^{\prime},u^{\prime}]\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}T[\ell,u]$ , since the removed items had a lower bound of [math]. Furthermore each remaining item has an upper bound of at least $1$ , i.e., it represents at least one node or edge.

Now construct a graph $G$ from $T^{\prime}$ by proceeding as follows: for every node $v$ with $\ell^{\prime}(v)=k$ add $k-1$ isolated nodes (zero isolated nodes if $k=0$ ). For every edge $e$ with $\ell^{\prime}(e)=k$ put $k$ parallel edges between $\mathit{src}(e),\mathit{tgt}(e)$ . There is a morphism $\varphi\colon G\to T^{\prime}$ obtained by mapping every item to the item from which it orginated.

Mapping $G[s_{G},s_{G}]$ to $T^{\prime}$ via $\varphi$ will give us an annotation $\mathcal{B}^{n}_{\varphi}(s_{G})$ . This annotation will coincide will the lower bound $\ell$ in all cases, apart from the case where there is a node $v$ with $\ell(v)=1$ . In this case $\mathcal{B}^{n}_{\varphi}(s_{G})(v)=1$ , but this is covered by the upper bound which is at least $1$ .

Hence there is a legal graph morphism from $G[s_{G},s_{G}]$ to $T^{\prime}[\ell^{\prime},u^{\prime}]$ and – by composition – to $T[\ell,u]$ . Hence $G\in\mathcal{L}(T[M])$ and hence $\mathcal{L}(T[M])\neq\varnothing$ . ∎

Proposition 7.* The existence of a legal morphism $\varphi\colon T_{1}[M]\to T_{2}[N]$ implies $\mathcal{L}(T_{1}[M])\subseteq\mathcal{L}(T_{2}[N])$ . *

Proof

Every graph $G\in\mathcal{L}(T_{1}[M])$ has a legal morphism $\varphi^{\prime}\colon G[s_{G},s_{G}]\to T_{1}[M]$ . Whenever there exists a legal morphism $\varphi\colon T_{1}[M]\to T_{2}[N]$ between the two multiply annotated type graphs, we obtain the morphism $\eta\colon G[s_{G},s_{G}]\to T_{2}[N]$ with $\eta=\varphi\circ\varphi^{\prime}$ which is legal due to Lemma 1. Therefore $G\in T_{2}[N]$ holds and we can conclude that $\mathcal{L}(T_{1}[M])\subseteq\mathcal{L}(T_{2}[N])$ also holds. ∎

Proposition 9.* Let $c_{1}\colon J\to G\leftarrow K$ and $c_{2}\colon K\to H\leftarrow L$ be two arrows and let $id_{G}\colon G\to G\leftarrow G$ be the identity cospan.*

The mapping $\mathcal{C}_{T[M]}\colon\emph{Cospan}_{m}({\mathbf{Graph}})\to\mathbf{Rel}$ is a functor:

$\mathcal{C}_{T[M]}(id_{G})=id_{C_{T[M]}(G)}$ ** 2. 2.

$\mathcal{C}_{T[M]}(c_{1};c_{2})=\mathcal{C}_{T[M]}(c_{1});\mathcal{C}_{T[M]}(c_{2})$ **

Proof

$1.$ The identity relation $id_{C_{T[M]}(G)}$ consists of all pairs $(i,i)$ with $i\in C_{T[M]}(G)$ . Let the two states $i,j\in\mathcal{C}_{T[M]}(G)$ be given with $i=(f_{1}\colon G\to T,b_{1})$ and $j=(f_{2}\colon G\to T,b_{2})$ . The pair $(i,j)$ is in the relation $\mathcal{C}_{T[M]}(id_{G})$ if and only if there exists a morphism $h\colon G\to T$ such that, for all444We write $x\in T$ as an abbreviation for $x\in V_{T}\cup E_{T}$ . $x\in T$ the equation $b_{2}(x)=b_{1}(x)+|\{y\in(G\setminus id(G))\mid h(y)=x\}|$ holds and the following diagram commutes:

$G$$G$$G$$T$$id_{G}\colon G\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}G$$f_{1}$$id$$\exists h$$id$$f_{2}$

Since the diagram commutes we obtain that $f_{1}=f_{2}$ since $f_{1}=id;h=h;id=f_{2}$ holds and for all $x\in T$ the annotation functions $b_{1}$ and $b_{2}$ are equal due to the following equation:

[TABLE]

This is equivalent to $i=j$ and therefore for all $i\in C_{T[M]}(G)$ the following equation holds:

[TABLE]

Therefore $\mathcal{C}_{T[M]}(id_{G})=id_{C_{T[M]}(G)}$ holds.

In the following part let $c_{1}\colon J\mathbin{\mathchoice{\xrightarrow{g_{1}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle g_{1} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{1} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{1} $}}{\shortrightarrow}}}G\mathchoice{\xleftarrow{g_{2}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle g_{2} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{2} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{2} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}K$ and $c_{2}\colon K\mathbin{\mathchoice{\xrightarrow{g_{1}^{\prime}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle g_{1}^{\prime} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{1}^{\prime} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{1}^{\prime} $}}{\shortrightarrow}}}H\mathchoice{\xleftarrow{g_{2}^{\prime}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle g_{2}^{\prime} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{2}^{\prime} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{2}^{\prime} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}L$ be given and let $c=c_{1};c_{2}$ with $c\colon J\mathbin{\mathchoice{\xrightarrow{g_{1};j_{1}}}{\scalebox{0.8}[1.0]{$ \textstyle\relbar $}{\raisebox{0.99025pt}{$ \scriptstyle g_{1};j_{1} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{1};j_{1} $}}{\shortrightarrow}}{\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{1};j_{1} $}}{\shortrightarrow}}}G^{\prime}\mathchoice{\xleftarrow{g_{2}^{\prime};j_{2}}}{\mathbin{{\textstyle\shortleftarrow}{\raisebox{0.99025pt}{$ \scriptstyle g_{2}^{\prime};j_{2} $}}\scalebox{0.8}[1.0]{$ \textstyle\relbar $}}}{\mathbin{{\scriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{2}^{\prime};j_{2} $}}\scalebox{0.8}[1.0]{$ \scriptstyle\relbar $}}}{\mathbin{{\scriptscriptstyle\shortleftarrow}{\raisebox{0.6458pt}{$ \scriptscriptstyle g_{2}^{\prime};j_{2} $}}\scalebox{0.8}[1.0]{$ \scriptscriptstyle\relbar $}}}L$ be the composed morphism of $c_{1}$ and $c_{2}$ .

$2.\subseteq:$ Let $(i,j)\in\mathcal{C}_{T[M]}(c_{1};c_{2})$ be given with $i\in\mathcal{C}_{T[M]}(J)$ and $j\in\mathcal{C}_{T[M]}(L)$ such that $i=(f_{1}\colon J\to T,b_{1})$ and $j=(f_{3}\colon L\to T,b_{3})$ . Then there exists a morphism $h\colon G^{\prime}\to T$ such that $b_{3}(x)=b_{1}(x)+|\{y\in(G^{\prime}\setminus g_{2}^{\prime};j_{2}(L))\mid h(y)=x\}|$ holds for all $x\in T$ and the following diagram commutes:

$J$$G$$K$$H$$L$$G^{\prime}$$T$$c_{1}\colon J\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}K$$c_{2}\colon K\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}L$$f_{1}$$g_{1}$$g_{1}^{\prime}$$g_{2}^{\prime}$$j_{1}$$j_{2}$$\exists h$$g_{2}$$f_{3}$

To prove that $(i,j)\in\mathcal{C}_{T[M]}(c_{1});\mathcal{C}_{T[M]}(c_{2})$ is satisfied from the above properties, we need to show that there exists a $k\in\mathcal{C}_{T[M]}(K)$ where $k=(f_{2}\colon K\to T,b_{2})$ such that $(i,k)\in\mathcal{C}_{T[M]}(c_{1})$ and $(k,j)\in\mathcal{C}_{T[M]}(c_{2})$ . Let $f_{2}=g_{2};j_{1};h=g_{1}^{\prime};j_{2};h$ . Then there must exist two morphisms $h_{1}\colon G\to T$ , $h_{2}\colon H\to T$ such that the following six properties hold:

[TABLE]

We define $h_{1},h_{2}$ to be $h_{1}=j_{1};h$ and $h_{2}=j_{2};h$ which already satisfy the following four properties:

[TABLE]

We define $b_{2}$ with respect to property $(3)$ , such that for all $x\in T$ the equation $b_{2}(x)=b_{1}(x)+|\{y\in(G\setminus g_{2}(K))\mid h_{1}(y)=x\}|$ holds. Due to property $(6)$ we get the following equation for $b_{3}$ , for which we need to prove that it holds for all elements $x\in T$ :

[TABLE]

We prove the following equation $(7)$ instead for all $x\in T$ , from which we can easily derive afterwards that also $(6)$ holds:

[TABLE]

Since the morphisms $j_{1}$ and $j_{2}$ are both injective and $G^{\prime}$ is the pushout object of $G$ and $H$ over the common graph $K$ we get that $G^{\prime}=j_{1}(G\setminus g_{2}(K))\uplus j_{2}(H)$ . Subtracting all elements $x\in L$ that are being mapped into $H$ on both sides of the equation, we get that $G^{\prime}\setminus g_{2}^{\prime};j_{2}(L)=j_{1}(G\setminus g_{2}(K))\uplus j_{2}(H\setminus g_{2}^{\prime}(L))$ holds as well. Using this fact we can prove equation $(7)$ which holds for all $x\in T$ :

[TABLE]

Using equation $(7)$ we conclude that property $(6)$ always holds for all $x\in T$ :

[TABLE]

Therefore $(i,j)\in\mathcal{C}_{T[M]}(c_{1});\mathcal{C}_{T[M]}(c_{2})$ holds as well.

$2."\supseteq":$ Let two pairs $(i,k)\in\mathcal{C}_{T[M]}(c_{1})$ and $(k,j)\in\mathcal{C}_{T[M]}(c_{2})$ be given with $i\in\mathcal{C}_{T[M]}(J)$ , $k\in\mathcal{C}_{T[M]}(K)$ and $j\in\mathcal{C}_{T[M]}(L)$ such that $i=(f_{1}\colon J\to T,b_{1})$ , $k=(f_{2}\colon K\to T,b_{2})$ and $j=(f_{3}\colon L\to T,b_{3})$ . Then in addition there exist two morphisms $h_{1}\colon G\to T$ and $h_{2}\colon H\to T$ such that for all $x\in T$ the two equations $b_{2}(x)=b_{1}(x)+|\{y\in(G\setminus g_{2}(K))\mid h_{1}(y)=x\}|$ and

$b_{3}(x)=b_{2}(x)+|\{y\in(H\setminus g_{2}^{\prime}(L))\mid h_{2}(y)=x\}|$ both hold and the following diagram commutes:

$J$$G$$K$$H$$L$$T$$c_{1}\colon J\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}K$$c_{2}\colon K\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}L$$f_{1}$$g_{1}$$g_{1}^{\prime}$$f_{2}$$g_{2}^{\prime}$$\exists h_{1}$$\exists h_{2}$$g_{2}$$f_{3}$

To prove that $(i,j)\in\mathcal{C}_{T[M]}(c_{1};c_{2})$ is satisfied from the properties gained so far, we need to show that $b_{3}(x)=b_{1}(x)+|\{y\in(G^{\prime}\setminus g_{2}^{\prime};j_{2}(L))\mid h(y)=x\}|$ holds and that there exists a morphism $h\colon G^{\prime}\to T$ such that the following diagram commutes:

$J$$G$$K$$H$$L$$G^{\prime}$$T$$(PO)$$c_{1}\colon J\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}K$$c_{2}\colon K\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}L$$f_{1}$$g_{1}$$g_{1}^{\prime}$$j_{1}$$j_{2}$$g_{2}^{\prime}$$h_{1}$$\exists h$$h_{2}$$g_{2}$$f_{3}$

The morphism $h\colon G^{\prime}\to T$ exists and is unique due to the universal property of pushouts. From the two equations $b_{2}(x)=b_{1}(x)+|\{y\in(G\setminus g_{2}(K))\mid h_{1}(y)=x\}|$ and $b_{3}(x)=b_{2}(x)+|\{y\in(H\setminus g_{2}^{\prime}(L))\mid h_{2}(y)=x\}|$ we can derive the following equation which holds for all $x\in T$ :

[TABLE]

Using the results of equation $(7)$ from the previous proof direction, we directly can conclude that $b_{3}(x)=b_{1}(x)+|\{y\in(G^{\prime}\setminus g_{2}^{\prime};j_{2}(L))\mid h(y)=x\}|$ also holds and therefore $(i,j)\in\mathcal{C}_{T[M]}(c_{1};c_{2})$ holds, which completes this proof. ∎

Proposition 10.* Let the multiply annotated type graph $T[M]$ (over $\mathcal{B}^{n}$ ) and the corresponding automaton functor $\mathcal{C}\colon\emph{Cospan}_{m}({\mathbf{Graph}})\to\mathbf{Rel}$ for $T[M]$ be given. Then $\mathcal{L}_{\mathcal{C}}=\mathcal{L}(T[M])$ holds, i.e. for a graph $G$ we have $G\in\mathcal{L}(T[M])$ if and only if there exist states $i\in I\subseteq\mathcal{C}(\varnothing)$ and $f\in F\subseteq\mathcal{C}(\varnothing)$ such that $(i,f)\in\mathcal{C}(c)$ , where $c\colon\varnothing\to G\leftarrow\varnothing$ . *

Proof

We will prove the following equality:

[TABLE]

” $\Rightarrow$ ”: Since $(c\colon\varnothing\to G\leftarrow\varnothing)\in\mathcal{L}(T[M])$ holds, there exists a legal morphism $\varphi\colon G\to T$ and a pair of multiplicities $(\ell,u)\in M$ such that $\ell\leq\mathcal{B}^{n}_{\varphi}(s_{G})\leq u$ holds. Let $(i,j)$ be $i=(f_{1}\colon\varnothing\to T,0)\in I$ and $j=(f_{2}\colon\varnothing\to T,\mathcal{B}^{n}_{\varphi}(s_{G}))\in F$ which are clearly in the relation $\mathcal{C}(c)$ , i.e. $(i,j)\in\mathcal{C}(c)$ since for all $x\in T$ the equation $\mathcal{B}^{n}_{\varphi}(s_{G})(x)=0+|\{y\in(G\setminus g_{2}(\varnothing))\mid\varphi(y)=x\}|=|\{y\in G\mid\varphi(y)=x\}|$ holds by definition and the following diagram commutes:

$\varnothing$$G$$\varnothing$$T$$c\colon\varnothing\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}\varnothing$$f_{1}$$g_{1}$$\varphi$$g_{2}$$f_{2}$

” $\Leftarrow$ ”: There exists $i\in I\subseteq\mathcal{C}(\varnothing)$ and $j\in F\subseteq\mathcal{C}(\varnothing)$ with $i=(f_{1}\colon\varnothing\to T,0)$ and $j=(f_{2}\colon\varnothing\to T,b)$ such that $(i,j)\in\mathcal{C}(c)$ holds. Therefore, there exists a pair of multiplicities $(\ell,u)\in M$ with $\ell\leq b\leq u$ and we get that there exists a morphism $\varphi\colon G\to T$ such that the following diagram commutes:

$\varnothing$$G$$\varnothing$$T$$c\colon\varnothing\mathrel{\raisebox{5.59721pt}{\scalebox{1.0}[-1.0]{\mbox{$ \looparrowright $}}}}\varnothing$$f_{1}$$g_{1}$$\exists\varphi$$g_{2}$$f_{2}$

For all $x\in T$ the following equation holds:

[TABLE]

From $\ell\leq b\leq u$ we can infer that $\varphi\colon G\to T$ is a legal morphism due to the fact that $\ell\leq\mathcal{B}^{n}_{\varphi}(s_{G})\leq u$ holds as well, and therefore $G\in\mathcal{L}(T[M])$ . ∎

Proposition 11.*

The category of multiply annotated graphs is closed under intersection. *

Proof

Let two multiply annotated type graphs $T_{1}[M_{1}]$ and $T_{2}[M_{2}]$ be given. Let $T_{1}\times T_{2}$ be the usual product graph in the underlying category ${\mathbf{Graph}}$ .

We now consider the multiply annotated type graph $(T_{1}\times T_{2})[N]$ where the set of annotations $N$ is defined as follows:

[TABLE]

Therefore for each $(\ell,u)\in N$ there exist $(\ell_{1},u_{1})\in M_{1}$ and $(\ell_{2},u_{2})\in M_{2}$ such that the following four properties hold:

[TABLE]

$\textstyle{(T_{1}\times T_{2})[N]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{1}}$$\scriptstyle{\pi_{2}}$$\textstyle{T_{1}[M_{1}]}$$\textstyle{T_{2}[M_{2}]}$

We will now prove the following equality:

[TABLE]

$\subseteq$ : Let $G\in\mathcal{L}(T_{1}[M_{1}])\cap\mathcal{L}(T_{2}[M_{2}])$ . Then there exist two legal morphisms $\varphi_{1}\colon G[s_{G},s_{G}]\to T_{1}[M_{1}]$ and $\varphi_{2}\colon G[s_{G},s_{G}]\to T_{2}[M_{2}]$ . Due to the universal property of pullbacks in the underlying category ${\mathbf{Graph}}$ , there exists a unique graph morphism $\eta\colon G\to T_{1}\times T_{2}$ such that the following diagram commutes:

$\textstyle{G[s_{G},s_{G}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varphi_{1}}$$\scriptstyle{\varphi_{2}}$$\scriptstyle{\eta}$$\textstyle{(T_{1}\times T_{2})[N]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{1}}$$\scriptstyle{\pi_{2}}$$\textstyle{T_{1}[M_{1}]}$$\textstyle{T_{2}[M_{2}]}$

Since $\varphi_{i}=\pi_{i}\circ\eta$ with $i\in\{1,2\}$ is a legal morphism, there exist annotations $(\ell_{1},u_{1})\in M_{1}$ and $(\ell_{2},u_{2})\in M_{2}$ such that the following inequalities hold:

[TABLE]

Therefore the pair $(\mathcal{A}_{\eta}(s_{G}),\mathcal{A}_{\eta}(s_{G}))$ is one of the annotations in $N$ and we can conclude that $G\in\mathcal{L}((T_{1}\times T_{2})[N])$ holds.

$\supseteq$ : We now assume $G\in\mathcal{L}((T_{1}\times T_{2})[N])$ . Then there exists a legal morphism $\eta\colon G[s_{G},s_{G}]\to(T_{1}\times T_{2})[N]$ with an annotation pair $(\ell,u)\in N$ such that $\ell\leq\mathcal{A}_{\eta}(s_{G})\leq u$ . For each such pair $(\ell,u)\in N$ we have two legal morphisms $\pi_{1}\colon(T_{1}\times T_{2})[\ell,u]\to T_{1}[M_{1}]$ and $\pi_{2}\colon(T_{1}\times T_{2})[\ell,u]\to T_{2}[M_{2}]$ , by construction. We obtain two morphisms $\varphi_{1}\colon G[s_{G},s_{G}]\to T_{1}[M_{1}]$ with $\varphi_{1}=\pi_{1}\circ\eta$ and $\varphi_{2}\colon G[s_{G},s_{G}]\to T_{2}[M_{2}]$ with $\varphi_{2}=\pi_{2}\circ\eta$ , which are legal due to Lemma 1. Therefore we can conclude that $G\in(\mathcal{L}(T_{1}[M_{1}])\cap\mathcal{L}(T_{2}[M_{2}]))$ . ∎

In order to show closure under union for annotated type graphs over $\mathcal{B}^{n}$ , we first have a look at the following lemma.

Lemma 3

*Assume that we are working with annotations over $\mathcal{B}^{n}$ .

Let $i\colon A[M]\to T[N]$ and $\varphi\colon G[s_{G},s_{G}]\to T[N]$ be two legal graph morphisms where $i$ is injective. Let $(\ell,u)\in M$ be one of the double multiplicities of the graph $A$ . Whenever $\mathcal{B}^{n}_{\varphi}(s_{G})\leq\mathcal{B}^{n}_{i}(u)$ , we can deduce that there exists a graph morphism $\zeta\colon G\to A$ with $i\circ\zeta=\varphi$ , i.e. the diagram commutes.

$\textstyle{G[s_{G},s_{G}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varphi}$$\scriptstyle{\zeta}$$\textstyle{A[M]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{T[N]}$

Proof

The morphisms $\zeta$ exists if all elements of the form $\varphi(x)$ with $x\in G$ are in the range of $i$ . For such an $x$ we have $1=s_{G}(x)\leq\mathcal{B}^{n}_{\varphi}(s_{G})(\varphi(x))$ , since $\mathcal{B}^{n}_{\varphi}(s_{G})(\varphi(x))$ is the sum of the $s_{G}$ -annotations of all preimages of $x$ . Furthermore $\mathcal{B}^{n}_{\varphi}(s_{G})(\varphi(x))\leq\mathcal{B}^{n}_{i}(u)(\varphi(x))$ . But $\mathcal{B}^{n}_{i}(u)(y)=0$ for all $y\in T$ that are not in the range of $i$ , since the empty sum evaluates to [math]. But since $\mathcal{B}^{n}_{i}(u)(\varphi(x))\geq 1$ , we can conclude that $\varphi(x)$ has a preimage under $i$ . ∎

In addition, we need the concept of reduction: the reduction operation shifts annotations over morphisms in the reverse direction.

Definition 15 (Reduction)

Let $\mathcal{A}$ be an (annotation) functor. For a morphism $\varphi\colon G\to G^{\prime}$ and a monoid element $a^{\prime}\in\mathcal{A}(G^{\prime})$ we define the reduction of $a^{\prime}$ to $G$ as follows:

[TABLE]

In the case of concrete annotations, the reduction operator satisfies the following properties:

Lemma 4

Assume that we are working with annotations over $\mathcal{B}^{n}$ . If $\varphi\colon G\to H$ is injective, we obtain the following equality for all $x\in G$ :

[TABLE]

Furthermore, if $\varphi\colon G\to G^{\prime}$ is injective, it holds that $\mathit{red}_{\varphi}(\mathcal{B}^{n}_{\varphi}(a))=a$ for every $a\in\mathcal{B}^{n}(G)$ .

Proof

Straightforward from the definition of concrete annotations. ∎

We are now ready to prove closure under union for the concrete case. Since we do work with abstract annotations in the proof, but need the results of the lemmas, one could generalize this result to a setting where the properties stated in Lemma 3 and Lemma 4 hold.

Proposition 12.* The category of multiply annotated graphs over functor $\mathcal{B}^{n}$ is closed under union.*

Proof

Let two multiply annotated type graphs $T_{1}[M_{1}]$ and $T_{2}[M_{2}]$ be given. Let $T_{1}\oplus T_{2}$ be the usual coproduct graph in the underlying category ${\mathbf{Graph}}$ , together with the embedding morphisms $i_{1}\colon T_{1}\to T_{1}\oplus T_{2}$ and $i_{2}\colon T_{2}\to T_{1}\oplus T_{2}$ :

$\textstyle{T_{1}[M_{1}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i_{1}}$$\textstyle{T_{2}[M_{2}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i_{2}}$$\textstyle{T_{1}\oplus T_{2}[N]}$

We define the set of annotations $N$ for the multiply annotated type graph $(T_{1}\oplus T_{2})[N]$ using the following two sets:

[TABLE]

Finally we define $N=N_{1}\cup N_{2}$ .

By this definition, we get that for all elements $x\in T_{1}$ and for all $(\ell,u)\in M$ there exists $(\ell_{1},u_{1})\in N_{T_{1}(M)}$ such that $\mathcal{B}^{n}_{i_{1}}(\ell)(i_{1}(x))=\ell_{1}(i_{1}(x))$ and $\mathcal{B}^{n}_{i_{1}}(u)(i_{1}(x))=u_{1}(i_{1}(x))$ . This makes $i_{1}$ a legal morphism since $N_{1}\subseteq N$ . The same holds for $i_{2}$ analogously. We will now prove the following equality:

[TABLE]

$\subseteq$ : Let $G\in(\mathcal{L}(T_{1}[M_{1}])\cup\mathcal{L}(T_{2}[M_{2}]))$ . Then there exists at least one legal morphism $\varphi_{1}\colon G[s_{G},s_{G}]\to T_{1}[M_{1}]$ or $\varphi_{2}\colon G[s_{G},s_{G}]\to T_{2}[M_{2}]$ . We assume that $G\in\mathcal{L}(T_{1}[M_{1}])$ . Let $\eta\colon G[s_{G},s_{G}]\to(T_{1}\oplus T_{2})[N]$ be the composed morphism of $i_{1}$ and $\varphi_{1}$ with $\eta=i_{1}\circ\varphi_{1}$ . Then $\eta$ is legal due to Lemma 1 and therefore $G\in\mathcal{L}((T_{1}\oplus T_{2})[N])$ holds. The proof for the case where $G\in\mathcal{L}(T_{2}[M_{2}])$ works in the same way.

$\supseteq$ : We now assume $G\in\mathcal{L}((T_{1}\oplus T_{2})[N])$ . Then, there exists a legal morphism $\eta\colon G[s_{G},s_{G}]\to(T_{1}\oplus T_{2})[N]$ with an annotation $(\ell,u)\in N$ such that $\ell\leq\mathcal{B}^{n}_{\eta}(s_{G})\leq u$ . For each $(\ell,u)\in N$ , we know that the pair belongs to $N_{1}$ or $N_{2}$ . Assume that $(\ell,u)\in N_{1}$ . Then we know that there exists $(\ell_{1},u_{1})\in M_{1}$ such that $\ell=\mathcal{B}^{n}_{i_{1}}(\ell_{1})$ , $u=\mathcal{B}^{n}_{i_{1}}(u_{1})$ . Hence $\mathcal{B}^{n}_{\eta}(S_{G})\leq u=\mathcal{B}^{n}_{i_{1}}(u_{1})$ . From Lemma 3 it follows that there exists a graph morphism $\zeta_{1}\colon G\to T_{1}$ with $\eta=i_{1}\circ\zeta_{1}$ such that the following diagram commutes in the underlying category ${\mathbf{Graph}}$ :

$\textstyle{G[s_{G},s_{G}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\zeta_{1}}$$\scriptstyle{\eta}$$\textstyle{T_{1}[M_{1}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i_{1}}$$\textstyle{T_{2}[M_{2}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i_{2}}$$\textstyle{(T_{1}\oplus T_{2})[N]}$

We need to prove that $\zeta_{1}$ is a legal graph morphism in the category of multiply annotated graphs. We get that $\mathcal{B}^{n}_{\eta}(s_{G})=\mathcal{B}^{n}_{i_{1}\circ\zeta_{1}}(s_{G})=\mathcal{B}^{n}_{i_{1}}(\mathcal{B}^{n}_{\zeta_{1}}(s_{G}))$ and since $i_{1}$ is injective, the following inequality holds due to the fact that $\mathit{red}_{\varphi}$ is monotone and $\mathit{red}_{\varphi}(\mathcal{B}^{n}_{\varphi}(a))=a$ holds for every $a\in\mathcal{B}^{n}(G)$ , whenever $\varphi$ is injective (cf. Lemma 4):

[TABLE]

Therefore $\zeta_{1}\colon G[s_{G},s_{G}]\to T_{1}[M_{1}]$ is a legal morphism and we can conclude that $G\in\mathcal{L}(T_{1}[M_{1}])$ . For a legal morphism $\eta\colon G[s_{G},s_{G}]\to(T_{1}\oplus T_{2})[N]$ with a pair $(\ell,u)\in N_{2}$ we get a similar proof which shows that $G\in\mathcal{L}(T_{2}[M_{2}])$ . Summarizing, in all cases $G\in(\mathcal{L}(T_{1}[M_{1}])\cup\mathcal{L}(T_{2}[M_{2}]))$ holds.

Appendix 0.B Extended Example: Annotated Type Graphs

In order to illustrate the use of annotated type graphs in applications, we model a client-server scenario with the following specification:

•

There exists exactly one server.

•

An arbitrary number of users can connect to the server, even using multiple connection sessions at the same time.

•

There exists one user with special administrative rights.

•

At least one user is always connected to the server.

•

The server can host an arbitrary number of files from which at most one can be edited at the same time.

The above scenario can be modelled using an annotated type graph $T_{1}[\ell,u]$ (see below). We will use the following edge labels: $A$ -labeled loops for administrative rights, $C$ -labeled edges for connections between users and the server and $E$ -labeled edges which are pointing to the file that is currently edited. We now extend the requirements of our specification:

•

The user with the administrative rights is always connected to the server.

•

There has to be at least one file on the server.

We use the annotated type graph $T_{2}[\ell^{\prime},u^{\prime}]$ , depicted below to model the extended scenario.

[TABLE]

Since the second scenario is more restrictive than the first, there exist graphs in $\mathcal{L}(T_{1}[\ell,u])$ , which do not fulfil the additional requirements of the extended specification.

For instance the graph $G$ shown to the right is such a model, which describes that there exists a user with administrative rights but he is not connected to the server. Instead there is another user which is currently connected. However, it holds that that $\mathcal{L}(T_{2}[\ell^{\prime},u^{\prime}])\subseteq\mathcal{L}(T_{1}[\ell,u])$ , since we can easily find a legal graph morphism $\varphi\colon T_{2}[\ell^{\prime},u^{\prime}]\to T_{1}[\ell,u]$ .

Bibliography48

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1] Parosh Aziz Abdulla, Lukás Holík, Bengt Jonsson, Ondrej Lengál, Cong Quy Trinh, and Tomás Vojnar. Verification of heap manipulating programs with ordered data by extended forest automata. In Proc. of ATVA ’13 , pages 224–239, 2013. LNCS 8172.
2[2] Christoph Blume, H.J. Sander Bruggink, Dominik Engelke, and Barbara König. Efficient symbolic implementation of graph automata with applications to invariant checking. In Proc. of ICGT ’12 , pages 264–278. Springer, 2012. LNCS 7562.
3[3] Christoph Blume, H.J. Sander Bruggink, Martin Friedrich, and Barbara König. Treewidth, pathwidth and cospan decompositions with applications to graph-accepting tree automata. Journal of Visual Languages & Computing , 24(3):192–206, 2013.
4[4] H.J. Sander Bruggink and Barbara König. On the recognizability of arrow and graph languages. In Proc. of ICGT ’08 , pages 336–350. Springer, 2008. LNCS 5214.
5[5] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM , 50(5):752–794, 2003.
6[6] Andrea Corradini, Ugo Montanari, and Francesca Rossi. Graph processes. Fundamenta Informaticae , 26(3/4):241–265, 1996.
7[7] Bruno Courcelle. The monadic second-order logic of graphs I. Recognizable sets of finite graphs. Information and Computation , 85:12–75, 1990.
8[8] Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic, A Language-Theoretic Approach . Cambridge University Press, June 2012.

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Taxonomy

References

Specifying Graph Languages with Type Graphs

Abstract

1 Introduction

2 Preliminaries

Definition 1 (Graph)

Definition 2 (Graph morphism)

Definition 3 (Homomorphism preorder)

Definition 4 (Retract and core)

Example 1

3 Languages Specified by Type or Restriction Graphs

Definition 5 (Type graph language)

Example 2

Definition 6 (Restriction graph language)

3.1 Closure and Decidability Properties

Proposition 1

Proposition 2

3.2 Closure under Double-Pushout Rewriting

Proposition 3 (Closure under DPO rewriting for restriction graphs)

Proposition 4 (Closure under DPO rewriting for type graphs)

3.3 Relating Type graph and Restriction Graph Languages

Definition 7 (Duality pair)

Example 3

4 Type Graph Logic

Definition 8 (Syntax and semantics of TGL{\mathit{TGL}}TGL)

Example 4

Proposition 5

5 Annotated Type Graphs

Definition 9 (Lattice-ordered monoid)

Example 5

Definition 10 (Annotations and multiplicities for graphs)

Definition 11 (Multiply annotated graphs)

Lemma 1

Example 6

Definition 12 (Graph languages of multiply annotated type graphs)

5.1 Decidability Properties for Multiply Annotated Graphs

Proposition 6

Proposition 7

5.2 Deciding Language Inclusion for Annotated Type Graphs

Proposition 8

Definition 13 (Automaton functor [4])

Definition 14 (Counting cospan automaton)

Example 7

Proposition 9

Proposition 10

5.3 Closure Properties for Multiply Annotated Graphs

Proposition 11

Proposition 12

6 Conclusion

Appendix 0.A Proofs

0.A.1 Languages Specified by Type or Restriction Graphs

Proof

Proof

Proof

Lemma 2 (Lemma 2.1 of [15])

Proof

0.A.2 Type Graph Logic

Proof

0.A.3 Annotated Type Graphs

Proof

Proof

Proof

Proof

Proof

Proof

Lemma 3

Proof

Definition 15 (Reduction)

Lemma 4

Proof

Proof

Appendix 0.B Extended Example: Annotated Type Graphs

Definition 8 (Syntax and semantics of ${\mathit{TGL}}$ )