Timed Multiparty Session Types

Bocchi, Laura and Yang, Weizhen and Yoshida, Nobuko (2014) Timed Multiparty Session Types. In: International Conference on Concurrency Theory (CONCUR). (doi:https://doi.org/10.1007/978-3-662-44584-6_29) (Full text available)

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)
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 Nov 2016 18:08 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