This page will eventually hold many examples of systems modelled as
The Dining Philosophers problem is a classic problem. The problem consists of
N philosophers sitting at a table who do nothing but think and eat.
Between each philosopher, there is a single fork. In order to eat,
a philosopher must have both forks. A problem can arise if each philosopher
grabs the fork on the right, then waits for the fork on the left. In this
case a deadlock has occurred, and all philosophers will starve.
This example is presented also in the TVT tutorial.
A philosopher as an LSTS
A fork as an LSTS
Rules for making the generic system
The Bankteller machine is a more extensive and practical example that captures
some essential problems in two-way communication where messages may be lost.
The Bankteller machine
Maintained by Timo Erkkilä, firstname.lastname@example.org.
Last modifications to this page: Tue Feb 18 19:57:03 EET 2003.