Skip to main content

Timed Multiparty Session Types

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

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: Book section
DOI/Identification number: 10.1007/978-3-662-44584-6_29
Projects: Projects 0 not found.
Projects 0 not found.
Subjects: Q Science > QA Mathematics (inc Computing science) > QA299 Analysis, Calculus
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Laura Bocchi
Date Deposited: 05 Nov 2014 10:17 UTC
Last Modified: 29 May 2019 13:17 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/43729 (The current URI for this page, for reference purposes)
Bocchi, Laura: https://orcid.org/0000-0002-7177-9395
  • Depositors only (login required):

Downloads

Downloads per month over past year