中文

异步控制状态编排

计算机科学中的逻辑 2022-12-06 v2

摘要

编排规定了通信有限状态机系统中消息的集合点同步。如果一个规定的通信轨迹与对等体的异步系统(其通信信道使用FIFO队列或多重集邮箱)的轨迹一致,则称该系统是可实现的。在最近的一篇文章中,可实现性由两个必要条件刻画,二者共同构成充分条件。一个简单推论是,在存在编排的情况下的可实现性变为可判定的。本文通过将对编排推广到控制状态编排来扩展该工作,后者支持并行性。我们在控制状态机的基础上重新定义P2P系统,并证明控制状态编排等价于其对等体的集合点组合,且语言可同步性等同于可同步性。这些结果被用于刻画控制状态编排的可实现性。对于基于FSM的编排的情况,我们证明两个必要条件:序列条件和选择条件。然后我们也证明这两个条件共同构成控制状态编排可实现性的充分条件。

关键词

引用

@article{arxiv.2009.03623,
  title  = {Asynchronous Control-State Choreographies},
  author = {Klaus-Dieter Schewe and Yamine Ait-Ameur and Sarah Benyagoub},
  journal= {arXiv preprint arXiv:2009.03623},
  year   = {2022}
}

备注

32 pages, 6 figures, 28 references