一句话：提出一种双方动态协商服务等级的对称协议，并用模态公式与行为归约验证其正确性。
本文提出一种对称协议，用于两方在完全有序的有限服务等级域上反复协商目标服务等级。协商中双方动态提出等级，且任一方在单次协商中只能降低所期望的服务等级，最终从双方提议中选取达成一致的等级。协议源自工业用例，正确设计颇具挑战。作者用模态公式陈述协议应满足的性质，并借助外部行为在弱迹等价和保持发散的分支双模拟下的行为归约来解释协议行为，从而给出正确性论证。
We present a symmetrical protocol to repeatedly negotiate a desired service level between two parties, where the service levels are taken from some totally ordered finite domain. The agreed service level is selected from levels dynamically proposed by both parties and parties can only decrease the desired service level during a negotiation. The correctness of the protocol is stated using modal formulas and its behaviour is explained using behavioural reductions of the external behaviour modulo weak trace equivalence and divergence-preserving branching bisimulation. Our protocol originates from an industrial use case and it turned out to be remarkably tricky to design correctly.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2001-07658,
title = {A symmetric protocol to establish service level agreements},
author = {Jan Friso Groote and Tim A. C. Willemse},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:19)2020}
}