On congruence property of scope equivalence for concurrent programs with higher-order communication

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

Representation of scopes of names is important for analysis and verification of concurrent systems. However, it is difficult to represent the scopes of channel names precisely with models based on process algebra.We introduced a model of concurrent systems with higher-order communication based on graph rewriting in our previous work. A bipartite directed acyclic graph represents a concurrent system that consists of a number of processes and messages in that model. The model can represent the scopes of local names precisely. We defined an equivalence relation such that two systems are equivalent not only in their behavior, but also in extrusion of scopes of names. This paper shows that our equivalence relation is a congruence relation w.r.t. ? -prefix, new-name, replication and composition, even when higher-order communication is allowed. We also show our equivalence relation is not congruent w.r.t. input-prefix though it is congruent w.r.t. input-prefix in the first-order case.

Original languageEnglish
Pages (from-to)49-66
Number of pages18
JournalConcurrent Systems Engineering Series
Volume67
DOIs
Publication statusPublished - Dec 1 2009

Keywords

  • Bisimilarity
  • Graph rewriting
  • Higherorder communication
  • Theory of concurrency
  • π-calculus

ASJC Scopus subject areas

  • Computer Science(all)
  • Engineering(all)

Fingerprint Dive into the research topics of 'On congruence property of scope equivalence for concurrent programs with higher-order communication'. Together they form a unique fingerprint.

  • Cite this