基于通信自动机的偏序集可实现性
计算机科学中的逻辑
2018-10-08 v1 软件工程
摘要
偏序集是由 Pratt 引入的并发计算模型。它们可以为基于异步消息传递的协调模型（如消息序列图 MSCs）提供与语法无关的语义描述。在本文中，我们研究了确保以偏序集集合表达的规范能够通过通信自动机忠实实现的条件。我们的主要贡献是：(i) 考虑终止健全性的可实现性条件的定义；(ii) 具有“多线程”参与者的全局规范的条件；以及 (iii) 可直接在偏序集上判定的可实现性条件的定义。我们方法的一个积极副产品是，在限制于可用行为类型表征的特定编排类时，验证可实现性条件所获得的效率提升。
引用
@article{arxiv.1810.02469,
title = {Realisability of Pomsets via Communicating Automata},
author = {Roberto Guanciale Dr and Emilio Tuosto Dr},
journal= {arXiv preprint arXiv:1810.02469},
year = {2018}
}
备注
In Proceedings ICE 2018, arXiv:1810.02053