Notes on Model Checking and Abstraction in Rewriting Logic
José Meseguer Guaita, Miguel Palomino, Narciso Martí Oliet · 2003
6 Minimal Structures as Quotients 17 6.1 Example 1: A Communication Protocol . . . . . . . . . . . . . . 21 6.2 Example 2: The Alternating Bit Protocol . . . . . . . . . . . . . 24 6.3 Example 1 Revisited . . . . . . . . . . . . . . . . . . . . . . . . . 29 6.4 Readers and Writers Revisited . . . . . . . . . . . . . . . . . . . 30 6.5 The Bakery Protocol Revisited . . . . . . . . . . . . . . . . . . . 31