next up previous

Final Report of the COST-247 Action

Verifying mutual exclusion algorithms by reducing state spaces

Martti Tienari

Department of Computer Science
P.O.Box 26 (Teollisuuskatu 23)
Tel:+358 9 7084 4175
Fax:+358 9 7084 4441
Email: tienari@cs.Helsinki.FI


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

Web links:

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page