面向编排的逻辑
编程语言
2011-10-20 v1 分布式、并行与集群计算
计算机科学中的逻辑
摘要
我们探讨了全局演算（一种基于编排概念的协调模型）的逻辑推理，旨在为结构化通信的规约与验证提供一套方法论。以 Hennessy-Milner 逻辑的扩展为起点，我们提出了全局逻辑（GL），这是一种描述编排中参与者之间可能交互的模态逻辑。我们通过给出服务规约上的属性示例来说明其用途。最后，我们证明尽管 GL 是不可判定的，但存在一个重要的可判定片段，并为其提供了一个可靠且完备的证明系统，用于检验公式的有效性。
引用
@article{arxiv.1110.4159,
title = {A Logic for Choreographies},
author = {Marco Carbone and Davide Grohmann and Thomas T. Hildebrandt and Hugo A. López},
journal= {arXiv preprint arXiv:1110.4159},
year = {2011}
}
备注
In Proceedings PLACES 2010, arXiv:1110.3853