  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.
