MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
Søren DEBOIS , Thomas HILDEBRANDT , Tijs SLAATS , Nobuko YOSHIDA
34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE 2014) p. 1 - 16

We present the first session typing system guaranteeing 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.

@inproceedings{DHSY2014,
  author = {Søren Debois and Thomas Hildebrandt and Tijs Slaats and Nobuko Yoshida},
  title = {{Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion}},
  series = {LNCS},
  volume = {8461},
  pages = {1--16},
  publisher = {Springer},
  year = 2014
}
@inproceedings{DHSY2014,
  author = {Søren Debois and Thomas Hildebrandt and Tijs Slaats and Nobuko Yoshida},
  title = {{Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion}},
  booktitle = {34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems},
  series = {LNCS},
  volume = {8461},
  pages = {1--16},
  publisher = {Springer},
  doi = "10.1007/978-3-662-43613-4_1",
  year = 2014
}