> First, let’s prove that a certain protocol ensures that no philosopher will starve. Starvation occurs when a philosopher is perpetually denied access to resou

> First, let’s prove that a certain protocol ensures that no philosopher will starve. Starvation occurs when a philosopher is perpetually denied access to resources (in this case, forks), and thus can never eat. We'll use a protocol where a philosopher must pick up both forks at once or put down any fork they've picked up and wait before trying again. This doesn't actually guarantee starvation freedom. Consider a scenario with three philosophers: Plato, Hume, and Arendt. Plato needs forks HA, Hume needs forks PA, etc. 1. Plato picks up forks HA and starts eating. 2. Hume picks up P, fails to pick up A. Hume immediately puts down P and enters the waiting phase. 3. Plato puts down HA. 4. Arendt picks up HP and starts eating. 5. Hume exits waiting phase. 6. Hume picks up A, fails to pick up P. Hume immediately puts down H and enters the waiting phase. 7. GOTO 1 The problem is that there's no guarantee of "strong fairness": that if the system keeps returning to a state where Hume can pick up both forks, he is guaranteed to eventually pick up both forks. Unrelated, but this is formalism is more precisely known as "linear temporal logic". That's because there are many different temporal logics! Temporal logics are "modal" logics, which means it's a logic equipped with the "necessarily" and "possibly" modifiers. The "necessarily" easily maps onto temporal logic: it just means "true at all times". But what does "possibly" mean? If I flip a coin, is it "possibly heads?" In linear temporal logic, the answer is "no", because there are sequences of events where the coin is never heads. In computation tree logic, the answer is "yes", because the timeline has a branch where it lands heads. Lamport wrote an article arguing that LTL is more useful in the context of programming (https://dl.acm.org/doi/pdf/10.1145/567446.567463 https://dl.acm.org/doi/pdf/10.1145/567446.567463). He'd later go on to make TLA, which is a restricted variant of LTL.