摘要：We present a symmetrical protocol to repeatedly negotiate a desired servicelevel between two parties, where the service levels are taken from some totallyordered finite domain. The agreed service level is selected from levelsdynamically proposed by both parties and parties can only decrease the desiredservice level during a negotiation. The correctness of the protocol is statedusing modal formulas and its behaviour is explained using behaviouralreductions of the external behaviour modulo weak trace equivalence anddivergence-preserving branching bisimulation. Our protocol originates from anindustrial use case and it turned out to be remarkably tricky to designcorrectly.
