A Chart Semantics for the Pi-Calculus

10 years 6 months ago
A Chart Semantics for the Pi-Calculus
We present a graphical semantics for the pi-calculus, that is easier to visualize and better suited to expressing causality and temporal properties than conventional relational semantics. A pi-chart is a finite directed acyclic graph recording a computation in the pi-calculus. Each node represents a process, and each edge either represents a computation step, or a message-passing interaction. Pi-charts enjoy a natural pictorial representation, akin to message sequence charts, in which vertical edges represent control flow and horizontal edges represent data flow based on message passing. A pi-chart represents a single computation starting from its top (the nodes with no ancestors) to its bottom (the nodes with no descendants). Unlike conventional reductions or transitions, the edges in a pi-chart induce ancestry and other causal relations on processes. We give both compositional and operational definitions of pi-charts, and illustrate the additional expressivity afforded by the chart ...
Johannes Borgström, Andrew D. Gordon, Andrew
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Authors Johannes Borgström, Andrew D. Gordon, Andrew Phillips
Comments (0)