TVT Examples

This page will eventually hold many examples of systems modelled as LSTSs.


The Dining Philosophers

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

    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

  • Henri Hansen,
    Maintained by Timo Erkkilä,
    Last modifications to this page: Tue Feb 18 19:57:03 EET 2003.