基于Tarski系统执行的分类（以面包店算法为例）
计算机科学中的逻辑
2010-06-02 v2
摘要
我们认为谓词语言及其Tarski结构在并发研究中占有重要地位。本文的论证基于一个例子：我们展示了两个看似不同的算法具有一组共同的高级属性，这揭示了它们的相似性。这两个算法分别是Lamport面包店算法的一个变体和Ricart与Agrawala算法。它们看似不同，因为一个使用共享内存，另一个使用消息传递进行通信。然而，直观上很明显它们在某种意义上是十分相似的，并且属于同一个“面包店算法家族”。本文旨在用形式化的方式表达这种将两个算法归为一类的直觉。为此，我们使用谓词语言及其Tarski结构来表达这两个算法共有的抽象高级属性。我们找到了一组用量化语言表达的属性，这些属性被模拟任一协议运行的每个Tarski系统执行所满足，并且足够强以确保在这些运行中互斥性质成立。
引用
@article{arxiv.0910.4565,
title = {Classification with Tarskian system executions (Bakery Algorithms as an example)},
author = {Uri Abraham},
journal= {arXiv preprint arXiv:0910.4565},
year = {2010}
}
备注
The paper is withdrawn since an improved version is being submitted