作为并发原语的协商
计算机科学中的逻辑
2016-12-26 v1 形式语言与自动机理论
摘要
本文引入了协商（negotiation），一种接近 Petri 网的并发模型，并以多方协商作为并发原语。我们研究两个基本分析问题。可靠性问题旨在判定无论当前状态如何，协商是否总能成功终止。给定一个可靠的协商，摘要化问题旨在计算一个具有相同输入/输出行为的等价单步协商。可靠性与摘要化问题可以通过作用于协商状态空间的简单算法来解决，然而这些算法面临众所周知的状态爆炸问题。我们研究了避免构建状态空间的替代算法。特别地，我们定义了归约规则，在保持协商的可靠/非可靠特性及其摘要的同时简化协商。在第一个结果中，我们证明了对于弱确定性无环协商类，我们的规则是完备的，这意味着它们将该类中所有的可靠协商（且仅这些协商）归约为等价的单步协商。这为可靠性和摘要化问题提供了避免构建状态空间的算法。随后，我们研究了确定性协商类。我们的第二个主要结果表明，即使协商包含环，该规则对该类也是完备的。此外，我们提出了一种算法，能够在多项式时间内完全归约所有可靠的确定性协商，且仅归约这些协商。
引用
@article{arxiv.1612.07912,
title = {Negotiation as Concurrency Primitive},
author = {Joerg Desel and Javier Esparza and Philipp Hoffmann},
journal= {arXiv preprint arXiv:1612.07912},
year = {2016}
}
备注
Long version encompassing arXiv:1307.2145 [cs.LO] and arXiv:1403.4958 [cs.LO]. It also corrects a mistake of arXiv:1403.4958 [cs.LO]