Massimo Bartoletti ; Tiziana Cimoli ; Maurizio Murgia - Timed Session Types

lmcs:4130 - Logical Methods in Computer Science, December 8, 2017, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:25)2017
Timed Session TypesArticle

Authors: Massimo Bartoletti ; Tiziana Cimoli ORCID; Maurizio Murgia ORCID

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.

https://doi.org/10.23638/LMCS-13(4:25)2017
Source: arXiv.org:1710.05388
Volume: Volume 13, Issue 4
Secondary volumes: Selected Papers of the 35th International Conference on Formal Techniques for Distributed Objects, Components and Systems and the 17th International Conference on Coordination Models and Languages (FORTE and COORDINATION 2015)
Published on: December 8, 2017
Accepted on: December 8, 2017
Submitted on: December 7, 2017
Keywords: Computer Science - Logic in Computer Science
Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 20201
Sources:
  • [1] zbMATH Open.

6 Documents citing this article

Share and export

Consultation statistics

This page has been seen 3447 times.
This article's PDF has been downloaded 581 times.