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 - 2009

Fingerprint

Communication
Algebra
Extrusion
Chemical analysis

Keywords

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

ASJC Scopus subject areas

  • Engineering(all)
  • Computer Science(all)

Cite this

@article{d064e269bfe34489a734b43aec19929a,
title = "On congruence property of scope equivalence for concurrent programs with higher-order communication",
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.",
keywords = "π-calculus, Bisimilarity, Graph rewriting, Higherorder communication, Theory of concurrency",
author = "Masaki Murakami",
year = "2009",
doi = "10.3233/978-1-60750-065-0-49",
language = "English",
volume = "67",
pages = "49--66",
journal = "Concurrent Systems Engineering Series",
issn = "1383-7575",
publisher = "IOS Press",

}

TY - JOUR

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

AU - Murakami, Masaki

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - π-calculus

KW - Bisimilarity

KW - Graph rewriting

KW - Higherorder communication

KW - Theory of concurrency

UR - http://www.scopus.com/inward/record.url?scp=78649582825&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=78649582825&partnerID=8YFLogxK

U2 - 10.3233/978-1-60750-065-0-49

DO - 10.3233/978-1-60750-065-0-49

M3 - Article

AN - SCOPUS:78649582825

VL - 67

SP - 49

EP - 66

JO - Concurrent Systems Engineering Series

JF - Concurrent Systems Engineering Series

SN - 1383-7575

ER -