Behavioural equivalence for a graph rewriting model of concurrent programs

Research output: Contribution to journalArticle

Abstract

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 labelled transition system. The model presented here makes it possible to represent local names that their scope is not nested. The author defines the weak bisimulation equivalence relation that two systems are equivalent in their behaviours. The author shows that the equivalence relation is a congruence relation wrt prefix, new-name, replication and composition.

Original languageEnglish
Pages (from-to)169-180
Number of pages12
JournalWorld Review of Science, Technology and Sustainable Development
Volume7
Issue number1-2
DOIs
Publication statusPublished - Mar 2010

Fingerprint

Semantics
Chemical analysis

Keywords

  • π-calculus
  • Bisimilarity
  • Distributed computing
  • Graph rewriting
  • Theory of concurrency

ASJC Scopus subject areas

  • General

Cite this

@article{a727cc52990f4444983a85ff487adbca,
title = "Behavioural equivalence for a graph rewriting model of concurrent programs",
abstract = "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 labelled transition system. The model presented here makes it possible to represent local names that their scope is not nested. The author defines the weak bisimulation equivalence relation that two systems are equivalent in their behaviours. The author shows that the equivalence relation is a congruence relation wrt prefix, new-name, replication and composition.",
keywords = "π-calculus, Bisimilarity, Distributed computing, Graph rewriting, Theory of concurrency",
author = "Masaki Murakami",
year = "2010",
month = "3",
doi = "10.1504/WRSTSD.2010.032352",
language = "English",
volume = "7",
pages = "169--180",
journal = "World Review of Science, Technology and Sustainable Development",
issn = "1741-2242",
publisher = "Inderscience Enterprises Ltd",
number = "1-2",

}

TY - JOUR

T1 - Behavioural equivalence for a graph rewriting model of concurrent programs

AU - Murakami, Masaki

PY - 2010/3

Y1 - 2010/3

N2 - 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 labelled transition system. The model presented here makes it possible to represent local names that their scope is not nested. The author defines the weak bisimulation equivalence relation that two systems are equivalent in their behaviours. The author shows that the equivalence relation is a congruence relation wrt prefix, new-name, replication and composition.

AB - 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 labelled transition system. The model presented here makes it possible to represent local names that their scope is not nested. The author defines the weak bisimulation equivalence relation that two systems are equivalent in their behaviours. The author shows that the equivalence relation is a congruence relation wrt prefix, new-name, replication and composition.

KW - π-calculus

KW - Bisimilarity

KW - Distributed computing

KW - Graph rewriting

KW - Theory of concurrency

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

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

U2 - 10.1504/WRSTSD.2010.032352

DO - 10.1504/WRSTSD.2010.032352

M3 - Article

AN - SCOPUS:77950609225

VL - 7

SP - 169

EP - 180

JO - World Review of Science, Technology and Sustainable Development

JF - World Review of Science, Technology and Sustainable Development

SN - 1741-2242

IS - 1-2

ER -