Checking a Mutex Algorithm in a Process Algebra with Fairness