Logic-based verification of the distributed dining philosophers protocol