Double pushout graph rewriting

Last updated

In computer science, double pushout graph rewriting (or DPO graph rewriting) refers to a mathematical framework for graph rewriting. It was introduced as one of the first algebraic approaches to graph rewriting in the article "Graph-grammars: An algebraic approach" (1973). [1] It has since been generalized to allow rewriting structures which are not graphs, and to handle negative application conditions, [2] among other extensions.

Contents

Definition

A DPO graph transformation system (or graph grammar) consists of a finite graph, which is the starting state, and a finite or countable set of labeled spans in the category of finite graphs and graph homomorphisms, which serve as derivation rules. The rule spans are generally taken to be composed of monomorphisms, but the details can vary. [3]

Rewriting is performed in two steps: deletion and addition.

After a match from the left hand side to is fixed, nodes and edges that are not in the right hand side are deleted. The right hand side is then glued in.

Gluing graphs is in fact a pushout construction in the category of graphs, and the deletion is the same as finding a pushout complement, hence the name.

Uses

Double pushout graph rewriting allows the specification of graph transformations by specifying a pattern of fixed size and composition to be found and replaced, where part of the pattern can be preserved. The application of a rule is potentially non-deterministic: several distinct matches can be possible. These can be non-overlapping, or share only preserved items, thus showing a kind of concurrency known as parallel independence, [4] or they may be incompatible, in which case either the applications can sometimes be executed sequentially, or one can even preclude the other.

It can be used as a language for software design and programming (usually a variant working on richer structures than graphs is chosen). Termination for DPO graph rewriting is undecidable because the Post correspondence problem can be reduced to it. [5]

DPO graph rewriting can be viewed as a generalization of Petri nets. [4]

Generalization

Axioms have been sought to describe categories in which DPO rewriting will work. One possibility is the notion of an adhesive category, which also enjoys many closure properties. Related notions are HLR systems, quasi-adhesive categories and -adhesive categories, adhesive HLR categories. [6]

The concepts of adhesive category and HLR system are related (an adhesive category with coproducts is a HLR system [7] ).

Hypergraph, typed graph and attributed graph rewriting, [8] for example, can be handled because they can be cast as adhesive HLR systems.

Notes

  1. Hartmut Ehrig; Michael Pfender; Hans-Jürgen Schneider (Oct 1973). "Graph-Grammars: An Algebraic Approach". IEEE Conference Record of 14th Annual Symposium on Switching and Automata Theory (SWAT'08). IEEE. pp. 167–180. doi:10.1109/SWAT.1973.11.
  2. Hartmut Ehrig; Karsten Ehrig; Annegret Habel; Karl-Heinz Pennemann (2004). "Constraints and Application Conditions: From Graphs to High-Level Structures". In Ehrig H.; Engels G.; Parisi-Presicce F.; Rozenberg G. (eds.). Graph Transformations. Lecture Notes in Computer Science. Vol. 3256. Springer. pp. 287–303. doi:10.1007/978-3-540-30203-2_21. ISBN   978-3-540-23207-0.
  3. "Double-pushout graph transformation revisited", Habel, Annegret and Müller, Jürgen and Plump, Detlef, Mathematical Structures in Computer Science, vol. 11, no. 05., pp. 637--688, 2001, Cambridge University Press
  4. 1 2 "Concurrent computing: from Petri nets to graph grammars", Corradini, Andrea, ENTCS, vol. 2, pp. 56--70, 1995, Elsevier
  5. , "Termination of graph rewriting is undecidable", Detlef Plump, Fundamenta Informaticae, vol. 33, no. 2, pp. 201--209, 1998, IOS Press
  6. Hartmut Ehrig and Annegret Habel and Julia Padberg and Ulrike Prange, "Adhesive high-level replacement categories and systems", 2004, Springer
  7. "Adhesive categories", Stephen Lack and Paweł Sobociński, in Foundations of software science and computation structures, pp. 273--288, Springer 2004
  8. "Fundamentals of Algebraic Graph Transformation", Hartmut Ehrig, Karsten Ehrig, Ulrike Prange and Gabriele Taentzer

Related Research Articles

<span class="mw-page-title-main">Context-free grammar</span> Type of formal grammar

In formal language theory, a context-free grammar (CFG) is a formal grammar whose production rules can be applied to a nonterminal symbol regardless of its context. In particular, in a context-free grammar, each production rule is of the form

<span class="mw-page-title-main">Automata theory</span> Study of abstract machines and automata

Automata theory is the study of abstract machines and automata, as well as the computational problems that can be solved using them. It is a theory in theoretical computer science with close connections to mathematical logic. The word automata comes from the Greek word αὐτόματος, which means "self-acting, self-willed, self-moving". An automaton is an abstract self-propelled computing device which follows a predetermined sequence of operations automatically. An automaton with a finite number of states is called a Finite Automaton (FA) or Finite-State Machine (FSM). The figure on the right illustrates a finite-state machine, which is a well-known type of automaton. This automaton consists of states and transitions. As the automaton sees a symbol of input, it makes a transition to another state, according to its transition function, which takes the previous state and current input symbol as its arguments.

In graph theory, a quiver is a directed graph where loops and multiple arrows between two vertices are allowed, in other words a multidigraph. They are commonly used in representation theory: a representation V of a quiver assigns a vector space V(x) to each vertex x of the quiver and a linear map V(a) to each arrow a.

In computer science, an abstract semantic graph (ASG) or term graph is a form of abstract syntax in which an expression of a formal or programming language is represented by a graph whose vertices are the expression's subterms. An ASG is at a higher level of abstraction than an abstract syntax tree, which is used to express the syntactic structure of an expression or program.

In computer science, graph transformation, or graph rewriting, concerns the technique of creating a new graph out of an original graph algorithmically. It has numerous applications, ranging from software engineering to layout algorithms and picture generation.

In theoretical computer science and mathematical logic a string rewriting system (SRS), historically called a semi-Thue system, is a rewriting system over strings from a alphabet. Given a binary relation between fixed strings over the alphabet, called rewrite rules, denoted by , an SRS extends the rewriting relation to all strings in which the left- and right-hand side of the rules appear as substrings, that is , where , , , and are strings.

A bigraph can be modelled as the superposition of a graph and a set of trees.

In computational mathematics, a word problem is the problem of deciding whether two given expressions are equivalent with respect to a set of rewriting identities. A prototypical example is the word problem for groups, but there are many other instances as well. A deep result of computational theory is that answering this question is in many important cases undecidable.

In computer science, the expressive power of a language is the breadth of ideas that can be represented and communicated in that language. The more expressive a language is, the greater the variety and quantity of ideas it can be used to represent.

In theoretical computer science and formal language theory, a regular tree grammar is a formal grammar that describes a set of directed trees, or terms. A regular word grammar can be seen as a special kind of regular tree grammar, describing a set of single-path trees.

Combinatorics on words is a fairly new field of mathematics, branching from combinatorics, which focuses on the study of words and formal languages. The subject looks at letters or symbols, and the sequences they form. Combinatorics on words affects various areas of mathematical study, including algebra and computer science. There have been a wide range of contributions to the field. Some of the first work was on square-free words by Axel Thue in the early 1900s. He and colleagues observed patterns within words and tried to explain them. As time went on, combinatorics on words became useful in the study of algorithms and coding. It led to developments in abstract algebra and answering open questions.

In mathematics, directed algebraic topology is a refinement of algebraic topology for directed spaces, topological spaces and their combinatorial counterparts equipped with some notion of direction. Some common examples of directed spaces are spacetimes and simplicial sets. The basic goal is to find algebraic invariants that classify directed spaces up to directed analogues of homotopy equivalence. For example, homotopy groups and fundamental n-groupoids of spaces generalize to homotopy monoids and fundamental n-categories of directed spaces. Directed algebraic topology, like algebraic topology, is motivated by the need to describe qualitative properties of complex systems in terms of algebraic properties of state spaces, which are often directed by time. Thus directed algebraic topology finds applications in concurrency, network traffic control, general relativity, noncommutative geometry, rewriting theory, and biological systems.

<span class="mw-page-title-main">Grzegorz Rozenberg</span> Polish and Dutch computer scientist

Grzegorz Rozenberg is a Polish and Dutch computer scientist.

In mathematics, an adhesive category is a category where pushouts of monomorphisms exist and work more or less as they do in the category of sets. An example of an adhesive category is the category of directed multigraphs, or quivers, and the theory of adhesive categories is important in the theory of graph rewriting.

A term graph is a representation of an expression in a formal language as a generalized graph whose vertices are terms. Term graphs are a more powerful form of representation than expression trees because they can represent not only common subexpressions but also cyclic/recursive subexpressions.

Hans-Jörg Kreowski is a professor for computer science at the University of Bremen in North West Germany. His primary research area is theoretical computer science with an emphasis on graph transformation, algebraic specification, and syntactic picture processing. He is also a member of the Forum of Computer Scientists for Peace and Social Responsibility (FIfF).

In computer science, a single pushout graph rewriting or SPO graph rewriting refers to a mathematical framework for graph rewriting, and is used in contrast to the double-pushout approach of graph rewriting.

In computer science, an attributed graph grammar is a class of graph grammar that associates vertices with a set of attributes and rewrites with functions on attributes. In the algebraic approach to graph grammars, they are usually formulated using the double-pushout approach or the single-pushout approach.

Hartmut Ehrig was a German computer scientist and professor of theoretical computer science and formal specification. He was a pioneer in algebraic specification of abstract data types, and in graph grammars.

Zdeněk Hedrlín was a Czech mathematician, specializing in universal algebra and combinatorial theory, both in pure and applied mathematics.