Congruence results of behavioral equivalence for a graph rewriting model of concurrent programs

This paper presents a formal model of concurrent systems based on graph rewriting to represent scopes of communication channel names precisely. A bipartite directed acyclic graph represents a concurrent system consists of a number of processes and messages. Each process or message corresponds to a source node of the graph. Names of communication channel in the system are sink nodes. The edges of the graph represent the scopes of the names in the system. The operational semantics of the system is given as a labeled transition system. The model presented here makes it possible to represent local names that their scope are not nested. We define the weak bisimulation equivalence relation that two systems are equivalent in their behavior. We show that the equivalence relation is a congruence relation wrt prefix, new-name, replication and composition.