Abstract:

This is a case study of verifying safety properties in some concurrent systems using state transition system reduction methods. Reductions have been made with respect to trace-, cffd-equivalences as well as various bisimilarities. A set of mutual exclusion algorithms were considered. By suitable hiding of labels reduced systems, suitable for verification purposes, were of the size of 7.. 20 states, typically. Thus the verification could be done visually based on the pictures of the reduced systems.