In many previous Colloquium talks, I have presented work on using mCRL2 to verify mutual exclusion algorithms under various models of shared register behaviour. In particular, we have looked at whether read and write operations on a register, which have duration, can overlap in time. If they can, we must consider how the overlapping operations affect each other; if they cannot, then operations may block each other indefinitely. The mCRL2 models of the registers we have used until now, which we have since termed full-read models, closely capture the notion that operations have duration. However, by abstracting away from the duration of reads in particular we can create models that are smaller and thus more suitable to model checking. In this talk, I will present these instant-read models and discuss how we proved that the two modelling approaches give the same verification results.

This is joint work with Rob van Glabbeek and Bas Luttik.