> A philosopher can only leave the waiting phase and attempt to pick up the forks again after each of their adjacent philosophers has either started eating or e

> A philosopher can only leave the waiting phase and attempt to pick up the forks again after each of their adjacent philosophers has either started eating or entered and left the waiting phase once. Consider the case of Plato starts eating, and both Hume and Arendt try to eat before he finishes. What happens to the system after that? Exercise: can you express the Dining Philosophers system entirely symbolically in terms of FOL+GFX? From there you can run model checkers on it, which is great for building an intuition for problematic edge cases.