Paper Details

On Congruence Property of Scope Equivalence for Concurrent Programs with Higher-Order Communication

Authors: Murakami, Masaki

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 in extrusion of scopes of names. This paper shows that the equivalence relation is a congruence relation wrt tau-prefix, new-name, replication and composition even if higher-order communication is allowed. And we also show the equivalence relation is not congruent wrt input-prefix though it is congruent wrt input prefix in first-order case.

Proceedings:

Communicating Process Architectures 2009, Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter, 2009, pp 49 - 66 published by IOS Press, Amsterdam

Files: Paper (PDF), Slides (PDF)

This record in other formats:

Web page: BibTEX, Refer
Plain text: BibTEX, Refer

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.