Skip to main content

Timed Multiparty Session Types

Bocchi, Laura, Yang, Weizhen, Yoshida, Nobuko (2014) Timed Multiparty Session Types. In: Baldan, Paolo and Gorla, Daniele, eds. International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science . pp. 419-434. Springer, Berlin, Germany ISBN 978-3-662-44583-9. E-ISBN 978-3-662-44584-6. (doi:10.1007/978-3-662-44584-6_29) (KAR id:43729)

Abstract

We propose a typing theory, based on multiparty session types, for modular verification of real-time choreographic interactions. To model real-time implementations, we introduce a simple calculus with delays and a decidable static proof system. The proof system ensures type safety and time-error freedom, namely processes respect the prescribed timing and causalities between interactions. A decidable condition on timed global types guarantees time-progress for validated processes with delays, and gives a sound and complete characterisation of a new class of CTAs with general topologies that enjoys progress and liveness.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1007/978-3-662-44584-6_29
Projects: From Data Types to Session Types---A Basis for Concurrency and Distribution, Conversation-Based Governance for Distributed Systems by Multiparty Session Types
Subjects: Q Science > QA Mathematics (inc Computing science) > QA299 Analysis, Calculus
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Funders: Organisations -1 not found.
Depositing User: Laura Bocchi
Date Deposited: 05 Nov 2014 10:17 UTC
Last Modified: 08 Dec 2022 18:02 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/43729 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.