Publications

BibTex format

@article{Debois:2016:10.2168/LMCS-12(1:1)2016,
author = {Debois, S and Hildebrandt, T and Slaats, T and Yoshida, N},
doi = {10.2168/LMCS-12(1:1)2016},
journal = {Logical Methods in Computer Science},
pages = {1--38},
title = {Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion},
url = {http://dx.doi.org/10.2168/LMCS-12(1:1)2016},
volume = {12},
year = {2016}
}

Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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.
AU  - Debois,S
AU  - Hildebrandt,T
AU  - Slaats,T
AU  - Yoshida,N
DO  - 10.2168/LMCS-12(1:1)2016
EP  - 38
PY  - 2016///
SN  - 1860-5974
SP  - 1
TI  - Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
T2  - Logical Methods in Computer Science
UR  - http://dx.doi.org/10.2168/LMCS-12(1:1)2016
UR  - http://hdl.handle.net/10044/1/26934
VL  - 12
ER  -

Download

ProfessorNobukoYoshida

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)