基于通信自动机的可实现性
Realisability of Pomsets via Communicating Automata
摘要：
Pomsets是Pratt提出的并发计算模型。它们可以提供基于异步消息传递的协调模型（如消息序列图（MSC））的语义的语法无关描述。在本文中，我们研究的条件，确保规范表示为一组pomsets可以忠实地实现通过通信自动机。我们的主要贡献是（一）的可实现性条件的定义占终止健全性，（二）与“多线程”参与者的全球规范的条件，及（iii）可实现性条件的定义，可以直接决定在pomsets。我们方法的一个积极副产品是，在限制以行为类型为特征的特定编排类别时，验证可实现性条件的效率提高。
英文摘要：
Pomsets are a model of concurrent computations introduced by Pratt. They can provide a syntax-oblivious description of semantics of coordination models based on asynchronous message-passing, such as Message Sequence Charts (MSCs). In this paper, we study conditions that ensure a specification expressed as a set of pomsets can be faithfully realised via communicating automata. Our main contributions are (i) the definition of a realisability condition accounting for termination soundness, (ii) conditions for global specifications with "multi-threaded" participants, and (iii) the definition of realisability conditions that can be decided directly over pomsets. A positive by-product of our approach is the efficiency gain in the verification of the realisability conditions obtained when restricting to specific classes of choreographies characterisable in term of behavioural types.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
