Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

Søren Debois, Thomas Hildebrandt, Tijs Slaats, Nobuko Yoshida

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Abstract

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.
Original languageEnglish
JournalLogical Methods in Computer Science
Volume12
Issue number1
Pages (from-to)1-38
Number of pages38
ISSN1860-5974
DOIs
Publication statusPublished - 11 Feb 2016

Keywords

  • Session types
  • Business processes
  • Liveness
  • Bounded recursion
  • Process algebra
  • Typing system

Fingerprint

Dive into the research topics of 'Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion'. Together they form a unique fingerprint.

Cite this