Projects per year
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 language | English |
---|---|
Journal | Logical Methods in Computer Science |
Volume | 12 |
Issue number | 1 |
Pages (from-to) | 1-38 |
Number of pages | 38 |
ISSN | 1860-5974 |
DOIs | |
Publication status | Published - 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.Projects
- 2 Finished
-
CompArt: Towards a design-oriented theory of computational artifacts in cooperative work practices
Hildebrandt, T. (PI), Normann, H. (CoI) & Slaats, T. (CoI)
01/01/2014 → 31/05/2019
Project: Research
-
Technologies for Declarative Model-driven Development of Cross-organizational Process Aware
Hildebrandt, T. (PI)
01/08/2011 → 30/07/2014
Project: Research