Table of Contents
Fetching ...

Global types and event structure semantics for asynchronous multiparty sessions

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini

TL;DR

The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its asynchronous type, namely their domains of configurations are isomorphic.

Abstract

We propose an interpretation of multiparty sessions with asynchronous communication as Flow Event Structures. We introduce a new notion of global type for asynchronous multiparty sessions, ensuring the expected properties for sessions, including progress. Our global types, which reflect asynchrony more directly than standard global types and are more permissive, are themselves interpreted as Prime Event Structures. The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its global type.

Global types and event structure semantics for asynchronous multiparty sessions

TL;DR

The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its asynchronous type, namely their domains of configurations are isomorphic.

Abstract

We propose an interpretation of multiparty sessions with asynchronous communication as Flow Event Structures. We introduce a new notion of global type for asynchronous multiparty sessions, ensuring the expected properties for sessions, including progress. Our global types, which reflect asynchrony more directly than standard global types and are more permissive, are themselves interpreted as Prime Event Structures. The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its global type.

Paper Structure

This paper contains 4 sections, 2 theorems, 1 equation, 2 figures.

Key Result

Lemma 3.5

Figures (2)

  • Figure 1: LTS for networks.
  • Figure 2: Projection of global types onto participants.

Theorems & Definitions (12)

  • Definition 2.1: Processes
  • Definition 2.2: Networks
  • Definition 2.3: Traces
  • Example 2.4
  • Example 2.5
  • Definition 2.6: Players of communications and traces
  • Definition 3.1: Global and asynchronous types
  • Definition 3.2: Depth
  • Definition 3.3: Boundedness
  • Example 3.4
  • ...and 2 more