Embeddings and contexts for link graphs.

*(English)*Zbl 1076.68045
Kreowski, Hans-Jörg (ed.) et al., Formal methods in software and systems modeling. Essays dedicated to Hartmut Ehrig on the occasion of his 60th birthday. Berlin: Springer (ISBN 3-540-24936-2/pbk). Lecture Notes in Computer Science 3393, 343-351 (2005).

Introduction: Graph-rewriting has been a growing discipline for over three decades. It grew out of the study of graph grammars, in which – analogously to string and tree grammars – a principal interest was to describe the families of graphs that could be generated from a given set of productions. A fundamental contribution was, of course, the double-pushout construction of H. Ehrig and his colleagues [see Lect. Notes Comput. Sci. 73, 1–69 (1979; Zbl 0407.68072)]; it made precise how the left-hand side of a production, or rewriting rule, could be found to occur in a host graph, and how it should then be replaced by the right-hand side. This break-through led to many theoretical developments and many applications. It relies firmly upon the treatment of graphs as objects in a category whose arrows are embedding maps.

A simultaneous development was Petri nets, with a quite different motivation; it was the first substantial mathematical model of concurrent processes, and gives strong emphasis to the causality relation among events. Although Petri nets are graphical, their study has been largely independent of graph-rewriting; after all, a Petri net does not change its shape – only the tokens placed upon the net actually move.

A little later came the development algebraic calculi, such as CSP and CCS, to represent interactive concurrent processes. The key concept distinguishing them from (Petri) net theory was the emphasis upon modularity. Initially at least, net theory focussed upon complete systems, developing powerful techniques such as linear algebra to analyse them. In contrast, process calculi focussed upon assembling larger systems from smaller ones using a variety of combinators, and upon defining the behaviour of the whole in terms of abstract entities that can be constructed from the behaviours of the parts by algebraic operations corresponding to the combinators. This approach was inspired by the modularity present in all good programming languages, and by the categorical formulation of algebraic theories by F. W. Lawvere [Proc. Natl. Acad. Sci. USA 50, 869–872 (1963; Zbl 0119.25901)]; in contrast with graph-rewriting methodology, here the graphs are the arrows in a category whose objects are interfaces.

A recent development in process calculi by J. J. Leifer and R. Milner [Lect. Notes Comput. Sci. 1877, 243–258 (2000; Zbl 0999.68141)] is the demonstration that labelled transition systems can be derived uniformly for a wide variety of calculi, using the notion of relative pushout (RPO), in a category where the arrows are processes. In the particular case of graphical process calculi, such as mobile ambients or bigraphs, where graph-rewriting is used to model various kinds of mobility among processes, this naturally leads to the need for a rapprochement between graphs-as-objects and graphs-as-arrows.

Connections between these two approaches have recently been surveyed by H. Ehrig [Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 78, 72–85 (2002)]. In one of these connections, previously explored for example by F. Gadducci, R. Heckel and M. Llabrés [Electronic Notes in Theoretical Computer Science 29, 21 p. (1999; Zbl 0967.68089)], graphs-as-arrows are obtained as cospans \(I\to G\leftarrow J\) of graphs-as-objects, where the interfaces \(I\) and \(J\) are graphs of some simple form (e.g. discrete). A second connection goes the other way; graphs-are-objects arise in a coslice category of a category, or s-category, of graphs-as-arrows. This connection was first proposed by Cattani, and was exploited technically in the theory of action calculi [G. L. Cattani, J. J. Leifer and R. Milner, \`\` Contexts and embeddings for closed shallow action graphs”, University of Cambridge Computer Laboratory, Technical Report 496 (2000) (submitted for publication), available at http://pauillac.inria.fr/\(\sim\)leifer].

The purpose of the present paper is to examine this latter connection more closely, in the context of link graphs [J. J. Leifer and R. Milner, \`\` Transition systems, link graphs and Petri nets” (2004), University of Cambridge Computer Laboratory, Technical Report (forthcoming)], which are a constituent of bigraphs. It is shown that, for link graphs, the coslice category is isomorphic to the natural category of embeddings (as arrows) between so-called ground link graphs. The connection almost certainly extends to full bigraphs. More generally, it is an open challenge to characterise the classes of graphs (or other entities) and interfaces for which this elegant isomorphism exists. I suggest that the existence of the isomorphism is a valuable test of probity for any proposed class of graphs.

For the entire collection see [Zbl 1069.68009].

A simultaneous development was Petri nets, with a quite different motivation; it was the first substantial mathematical model of concurrent processes, and gives strong emphasis to the causality relation among events. Although Petri nets are graphical, their study has been largely independent of graph-rewriting; after all, a Petri net does not change its shape – only the tokens placed upon the net actually move.

A little later came the development algebraic calculi, such as CSP and CCS, to represent interactive concurrent processes. The key concept distinguishing them from (Petri) net theory was the emphasis upon modularity. Initially at least, net theory focussed upon complete systems, developing powerful techniques such as linear algebra to analyse them. In contrast, process calculi focussed upon assembling larger systems from smaller ones using a variety of combinators, and upon defining the behaviour of the whole in terms of abstract entities that can be constructed from the behaviours of the parts by algebraic operations corresponding to the combinators. This approach was inspired by the modularity present in all good programming languages, and by the categorical formulation of algebraic theories by F. W. Lawvere [Proc. Natl. Acad. Sci. USA 50, 869–872 (1963; Zbl 0119.25901)]; in contrast with graph-rewriting methodology, here the graphs are the arrows in a category whose objects are interfaces.

A recent development in process calculi by J. J. Leifer and R. Milner [Lect. Notes Comput. Sci. 1877, 243–258 (2000; Zbl 0999.68141)] is the demonstration that labelled transition systems can be derived uniformly for a wide variety of calculi, using the notion of relative pushout (RPO), in a category where the arrows are processes. In the particular case of graphical process calculi, such as mobile ambients or bigraphs, where graph-rewriting is used to model various kinds of mobility among processes, this naturally leads to the need for a rapprochement between graphs-as-objects and graphs-as-arrows.

Connections between these two approaches have recently been surveyed by H. Ehrig [Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 78, 72–85 (2002)]. In one of these connections, previously explored for example by F. Gadducci, R. Heckel and M. Llabrés [Electronic Notes in Theoretical Computer Science 29, 21 p. (1999; Zbl 0967.68089)], graphs-as-arrows are obtained as cospans \(I\to G\leftarrow J\) of graphs-as-objects, where the interfaces \(I\) and \(J\) are graphs of some simple form (e.g. discrete). A second connection goes the other way; graphs-are-objects arise in a coslice category of a category, or s-category, of graphs-as-arrows. This connection was first proposed by Cattani, and was exploited technically in the theory of action calculi [G. L. Cattani, J. J. Leifer and R. Milner, \`\` Contexts and embeddings for closed shallow action graphs”, University of Cambridge Computer Laboratory, Technical Report 496 (2000) (submitted for publication), available at http://pauillac.inria.fr/\(\sim\)leifer].

The purpose of the present paper is to examine this latter connection more closely, in the context of link graphs [J. J. Leifer and R. Milner, \`\` Transition systems, link graphs and Petri nets” (2004), University of Cambridge Computer Laboratory, Technical Report (forthcoming)], which are a constituent of bigraphs. It is shown that, for link graphs, the coslice category is isomorphic to the natural category of embeddings (as arrows) between so-called ground link graphs. The connection almost certainly extends to full bigraphs. More generally, it is an open challenge to characterise the classes of graphs (or other entities) and interfaces for which this elegant isomorphism exists. I suggest that the existence of the isomorphism is a valuable test of probity for any proposed class of graphs.

For the entire collection see [Zbl 1069.68009].