论文标题
正式编舞语言的理论
A Theory of Formal Choreographic Languages
论文作者
论文摘要
我们介绍了一种基于正式语言的元模型，以形式编排语言，以研究通信系统。我们的框架使我们能够从文献中概括标准结构并比较它们。特别是，我们考虑了诸如全球观点，本地观点以及从前者到后者的预测之类的概念。从全球视图预测的本地观点的正确性是根据封闭属性的特征。我们考虑了许多通信属性（例如（死）锁定式 - 封闭式），并提供有关正式编排语言的条件以保证它们。最后，我们展示了形式的编排语言如何捕捉现有的形式主义。具体而言，我们考虑传达有限状态机器，编排自动机和多方会话类型。值得注意的是，与文献中大多数方法不同的形式编排语言自然可以模拟表现出非规范行为的系统。
We introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our framework allows us to generalise standard constructions from the literature and to compare them. In particular, we consider notions such as global view, local view, and projections from the former to the latter. The correctness of local views projected from global views is characterised in terms of a closure property. We consider a number of communication properties -- such as (dead)lock-freedom -- and give conditions on formal choreographic languages to guarantee them. Finally, we show how formal choreographic languages can capture existing formalisms; specifically we consider communicating finite-state machines, choreography automata, and multiparty session types. Notably, formal choreographic languages, differently from most approaches in the literature, can naturally model systems exhibiting non-regular behaviour.
