SWE 619 Temporal Logic Examples
Fall 2011

Answers
Use the variables listed in typewriter font as your primitive propositions.
  1. For any state, if a request occurs, it will eventually be acknowledged.
  2. A given process is enabled infinitely often on every computation path.
  3. Whatever happens, a certain process will eventually be deadlocked.
  4. If request is called in a rebooting state, then the action will eventually occur in some ready state but not before the system enters the ready state.