From Hyperedge Replacement to Separation Logic and Back

  • Hyperedge-replacement grammars and separation-logic formulas both define classes of graph-like structures. In this paper, we relate the different formalisms by effectively translating restricted hyperedge-replacement grammars into formulas of a fragment of separation-logic with recursive predicates, and vice versa. The translations preserve the classes of specified graphs, and hence the two approaches are of equivalent power. It follows that our fragment of separation-logic inherits properties oHyperedge-replacement grammars and separation-logic formulas both define classes of graph-like structures. In this paper, we relate the different formalisms by effectively translating restricted hyperedge-replacement grammars into formulas of a fragment of separation-logic with recursive predicates, and vice versa. The translations preserve the classes of specified graphs, and hence the two approaches are of equivalent power. It follows that our fragment of separation-logic inherits properties of hyperedge-replacement grammars, such as inexpressibility results. We also show that several operators of full separation logic cannot be expressed using hyperedge replacement.show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author: Mike Dodds, Detlef Plump
URN:urn:nbn:de:kobv:83-opus-31269
ISBN:1863-2122
Series (Serial Number):Electronic Communications of the EASST- ECEASST (16/02)
Document Type:Arbeitspapier/Research Paper
Language:English
Date of Publication (online):2011/08/10
Publishing Institution:Technische Universität Berlin
Release Date:2011/08/10
Tag:graph grammars; graph transformation; hyperedge replacement; program verification; separation logic
Note:
http://journal.ub.tu-berlin.de/eceasst/article/view/237
Institutes:Institut für Softwaretechnik und Theoretische Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Collection:Volume 16 (2009): International Conference on Graph Transformation 2008 - Doctoral Symposium
Licence (German):License LogoCC BY-NC-SA 2.0 DE: Creative Commons-Lizenz: Namensnennung, nicht kommerziell, Weitergabe unter gleichen Bedingungen 2.0 Deutschland