×

Checking bisimilarity for attributed graph transformation. (English) Zbl 1260.68275

Pfenning, Frank (ed.), Foundations of software science and computation structures. 16th international conference, FOSSACS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-37074-8/pbk). Lecture Notes in Computer Science 7794, 113-128 (2013).
Summary: Borrowed context graph transformation is a technique developed by Ehrig and Koenig to define bisimilarity congruences from reduction semantics defined by graph transformation. This means that, for instance, this technique can be used for defining bisimilarity congruences for process calculi whose operational semantics can be defined by graph transformation. Moreover, given a set of graph transformation rules, the technique can be used for checking bisimilarity of two given graphs. Unfortunately, we can not use this ideas to check if attributed graphs are bisimilar, i.e. graphs whose nodes or edges are labelled with values from some given data algebra and where graph transformation involves computation on that algebra. The problem is that, in the case of attributed graphs, borrowed context transformation may be infinitely branching. In this paper, based on borrowed context transformation of what we call symbolic graphs, we present a sound and relatively complete inference system for checking bisimilarity of attributed graphs. In particular, this means that, if using our inference system we are able to prove that two graphs are bisimilar then they are indeed bisimilar. Conversely, two graphs are not bisimilar if and only if we can find a proof saying so, provided that we are able to prove some formulas over the given data algebra. Moreover, since the proof system is complex to use, we also present a tableau method based on the inference system that is also sound and relatively complete.
For the entire collection see [Zbl 1258.68013].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI