建立服务级别协议的对称协议
摘要：对两方之间的服务水平进行重复协商的对称协议，其中服务水平来自于某个完全有序的有限域。协商确定的服务水平从两方动态提议的水平中选择，并且在协商过程中，双方只能减少期望的服务水平。利用模态公式来陈述协议的正确性，并使用行为外部化简（模弱追踪等效性）和保持发散的分支同步（弱迹等效性）来解释其行为。我们的协议源于一个工业应用案例，并且设计正确的过程非常复杂。
作者：Jan Friso Groote and Tim A. C. Willemse
论文ID：2001.07658
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22