Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
File(s)
Accepted version
Author(s)
Debois, S
Hildebrandt, T
Slaats, T
Yoshida, N
Type
Journal Article
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.
Date Issued
2016-02-11
Date Acceptance
2016-02-11
Citation
Logical Methods in Computer Science, 2016, 12 (1)
ISSN
1860-5974
Publisher
Logical Methods in Computer Science
Journal / Book Title
Logical Methods in Computer Science
Volume
12
Issue
1
Copyright Statement
© S. Debois, T. Hildebrandt, T. Slaats, and N. Yoshida. Made available under a CC BY ND licence.
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
Subjects
Science & Technology
Technology
Computer Science, Theory & Methods
Logic
Computer Science
Science & Technology - Other Topics
Session types
Business processes
Liveness
Bounded recursion
Process algebra
Typing system
OBJECT-ORIENTED LANGUAGES
SESSION TYPES
SEQUENCE CHARTS
PI-CALCULUS
PROGRESS
VERIFICATION
Artificial Intelligence & Image Processing
08 Information And Computing Sciences
0101 Pure Mathematics
0803 Computer Software
0802 Computation Theory And Mathematics
Publication Status
Published
Article Number
1