Abstract
We define a finite-state message-passing model using guarded commands. This model is particularly appropriate for defining and reasoning about self-stabilizing protocols, due to the well-known result that self-stabilizing protocols on unbounded-channel models must have infinitely many legitimate states. We argue that our model is more realistic than other models, and demonstrate its use with two simple examples. We then give a translation from this model to a lower-level model that uses a notion of time. We argue that this latter model is very close to a real network. We conclude by discussing how this translation might be used to implement self-stabilizing protocols on actual networks.
