|Final Report of the COST-247 Action|
Verifying mutual exclusion algorithms by reducing state spaces
|Department of Computer Science|
|P.O.Box 26 (Teollisuuskatu 23)|
|FIN-00014 UNIVERSITY OF HELSINKI|
|Tel:+358 9 7084 4175|
|Fax:+358 9 7084 4441|
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.
This presentation has been given during the COST-247 3rd Management Committee Meeting (Evry, France, September 19--20, 1994).
COST-247 Working Group(s): 2