Congruence results of weak equivalence for a graph rewriting model of concurrent programs with higher-order communication

Abstract

This paper presents congruence results of a weak equivalence on a graph rewriting model of concurrent processes with higher-order communication. A bipartite directed acyclic graph represents a concurrent system that consists of a number of processes and messages in our model. The model presented here makes it possible to represent local names that their scopes are not nested. We show that weak bisimulation equivalence is a congruence relation w.r.t. operations that correspond to τ-prefix, input prefix, new-name, replication, composition and application respectively. © 2011 Springer-Verlag Berlin Heidelberg.