1 Introduction
This note is devoted to liveness and progress properties. They are properties stating intuitively that “something good will eventually happens”. For instance, the absence of starvation for any of the dining philosophers in [1] is a liveness property and so is the possibility of being allowed to copy in the printer and scanner example also presented in [1].
We shall see how progress and liveness properties can be specified in the recursive extension of HML [1], however as it turns out, these kind of properties we must specify using minimal fixed points instead of as for safety properties using the maximal fixed points.
For illustration purposes, we shall use the classical example of readers and writers as our running example.
The examples of models to be run in MWB in this note are presented with emphasis on readability and may thus not compile due to extra line breaks.
References
[1] J.C. Godskesen. Deadlocks and safety properties (version 1.2), 2005. Teaching notes, IT University of Copenhagen.
[2] B. Victor. The mobility workbench user’s guide, polyadic version 3.122. Technical report, SICS, Stockholm, Sweden, 1995.
