On Urgency in Asynchronous Timed Session Types

TL;DR

This paper introduces an urgent semantics for asynchronous timed session types, demonstrating that deadlock-freedom is preserved when transitioning from synchronous to asynchronous communication, which enhances the reliability of timed communication protocols.

Contribution

It proposes a novel urgent semantics for asynchronous timed session types that maintains deadlock-freedom, bridging a gap between untimed and timed session type properties.

Findings

Deadlock-freedom is preserved under the urgent semantics.

The semantics allows input actions to occur as soon as possible.

The approach extends untimed session type properties to timed settings.

Abstract

We study an urgent semantics of asynchronous timed session types, where input actions happen as soon as possible. We show that with this semantics we can recover to the timed setting an appealing property of untimed session types: namely, deadlock-freedom is preserved when passing from synchronous to asynchronous communication.