ABSTRACT
In the previous chapter we have defined internal and external semantics of protocols, but we did not explain how to use this definition to verify them—which is the aim of our chapter. We shall use an example to illustrate how to prove properties of protocols (the mutual-exclusion protocol of Peterson, described in Chapter 1).
