Timed Session Types

TL;DR

This paper introduces timed session types to formalize timed communication protocols, providing a decidable compliance relation and methods to determine and construct compliant session types, including subtyping.

Contribution

It presents a sound and complete technique for deciding compliance and constructing the most precise compliant session type, extending untimed session type concepts to the timed setting.

Findings

Decidability of compliance between timed session types.

Method to construct the most precise compliant session type.

Decidability of subtyping based on compliance.

Abstract

Timed session types formalise timed communication protocols between two participants at the endpoints of a session. They feature a decidable compliance relation, which generalises to the timed setting the progress-based compliance between untimed session types. We show a sound and complete technique to decide when a timed session type admits a compliant one. Then, we show how to construct the most precise session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results.