The pi-calculus with polyadic synchronization
Author
Martinho, Joana
Term
10. Term
Education
Publication year
2004
Abstract
Denne afhandling undersøger pi-kalkylen med polyadisk synkronisering, en udvidelse af pi-kalkylen hvor kanaler er sekvenser af navne (flereleddet kanaler). Vi tilføjer kryptografiske primitiver (grundlæggende kryptografiske operationer) til denne ramme og viser, at den udvidede kalkyle kan kodes i den oprindelige pi-kalkyle med polyadisk synkronisering. Kodningen er en oversættelse, der bevarer og afspejler den observerbare adfærd. Vi beviser dette ved at vise, at kodningen er korrekt og fuldstændig i forhold til barbed congruence, en adfærdslig ækvivalens baseret på, hvad der kan observeres på kanaler. Vi viser også, at barbed congruence i denne sammenhæng falder sammen med early congruence.
This thesis studies the pi-calculus with polyadic synchronization, an extension of the pi-calculus in which channels are sequences of names (multi-part channels). We add cryptographic primitives (basic cryptographic operations) to this setting, and then show that the resulting calculus can be encoded in the original pi-calculus with polyadic synchronization. The encoding is a translation that preserves and reflects observable behavior. We prove this by showing the encoding is sound and complete with respect to barbed congruence, a behavioral equivalence based on what can be observed at channels. We also show that, in this setting, barbed congruence coincides with early congruence.
[This abstract was generated with the help of AI]
Documents