有界与无界递归协作过程的活性类型检查

我们提出了第一个会话类型系统，能够保证可能不终止的通信过程的请求-响应活性。这些类型通过一组必需的响应来扩展标准二元会话类型的分支和选择类型，表明每当选择特定标签时，一组其他标签（即其响应）最终也必须被选择。我们证明了这些扩展类型在表达能力上严格强于标准会话类型。我们为一个进程演算提供了类型系统，该演算类似于协作式BPMN过程的子集，具有内部（基于数据）和外部（基于事件）分支、消息传递、有界和无界循环。我们证明了该类型系统是可靠的，即它保证了无死锁进程的请求-响应活性。我们通过一个无限状态系统的具体示例，展示了该演算和类型系统的使用。