Søren Debois ; Thomas Hildebrandt ; Tijs Slaats ; Nobuko Yoshida - Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

lmcs:1624 - Logical Methods in Computer Science, January 6, 2016, Volume 12, Issue 1 - https://doi.org/10.2168/LMCS-12(1:1)2016
Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

Authors: Søren Debois ORCID-iD; Thomas Hildebrandt ; Tijs Slaats ; Nobuko Yoshida ORCID-iD

    We present the first session typing system guaranteeing request-response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.


    Volume: Volume 12, Issue 1
    Published on: January 6, 2016
    Submitted on: November 30, 2014
    Keywords: Computer Science - Logic in Computer Science
    Fundings :
      Source : OpenAIRE Research Graph
    • Conversation-Based Governance for Distributed Systems by Multiparty Session Types; Funder: UK Research and Innovation; Code: EP/K011715/1
    • From Inherent Concurrency to Massive Parallelism through Type-based Optimizations; Funder: European Commission; Code: 612985
    • Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems; Funder: UK Research and Innovation; Code: EP/L00058X/1

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1145/3009837.3009847
    Source : ScholeXplorer IsReferencedBy DOI 10.1145/3093333.3009847
    • 10.1145/3093333.3009847
    • 10.1145/3093333.3009847
    • 10.1145/3093333.3009847
    • 10.1145/3009837.3009847
    • 10.1145/3009837.3009847
    Fencing off go: liveness and safety for channel-based programming
    Nicholas Ng ; Nobuko Yoshida ; Julien Lange ; Bernardo Toninho ;

    3 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 537 times.
    This article's PDF has been downloaded 264 times.