Excommunication: transforming π-calculus specifications to remove internal communication

Geoff W. Hamilton, Benjamin Aziz

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this paper, we present a new automatic transformation algorithm called excommunication that transforms π-calculus processes to remove parallelism, and hence internal communication. We prove that the transformation is correct and that it always terminates for any specification in which the named processes are in a particular syntactic form we call serial form. We argue that this transformation facilitates the proving of properties of mobile processes, and demonstrate this by showing how it can be used to simplify a leakage analysis.
Original languageEnglish
Title of host publicationProceedings of the 25th Brazilian Symposium on Formal Methods
PublisherSpringer
Pages109-123
Number of pages15
ISBN (Electronic)9783031224768
ISBN (Print)9783031224751
DOIs
Publication statusPublished - 1 Dec 2022
Event25th Brazilian Symposium on Formal Methods - Online
Duration: 5 Dec 20229 Dec 2022
https://sites.google.com/dcomp.ufs.br/sbmf2022/home

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume13768
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th Brazilian Symposium on Formal Methods
Abbreviated titleSBMF 2022
Period5/12/229/12/22
Internet address

Keywords

  • Formal Methods
  • Pi Calculus
  • Process Algebra
  • Program Transformation
  • Security

Fingerprint

Dive into the research topics of 'Excommunication: transforming π-calculus specifications to remove internal communication'. Together they form a unique fingerprint.

Cite this