Jan Friso Groote: A symmetric protocol to establish service level agreements

Event Details

We present a protocol designed using mCRL2 to negotiate the optimal service level by two parties. The problem is inspired by a similar problem at ASML where software had to be written to decide whether a “chuck swap” should be executed. For some time I believed that a symmetric solution was fundamentally impossible, but out of the impossibility proof a solution emerged. The correctness is shown using modal formulas.