Consider a three bit binary counter. This has three spaces for digits which can be 0 or 1. Initially all the bits are set to 0 (i.e. the counter reads 000).
Incrementing the counter leads to the following sequence of readings 001, 010,011, 100, 101, 110, 111, returning again then to 000 and so on. Let x, y and z stand for each of the bits where z represents the most signi cant bit (at the left hand side), y is the bit in the middle and x the least signi cant (at the right hand side) where x represents 1 in the right hand column and :x represents 0 in the right hand column (and similarly for y and z). For example z = T, y = F and x = F would represent 100 on the counter. Specify the three bit counter using LTL.
The following are properties we may wish to try and prove are valid given the speci cation of the three bit counter.
(a) Eventually the counter reaches 111.
(b) It is not possible to reach a state where the counter reads 010 and in the next moment the counter reads 100.
Formulate these properties in LTL. Construct a model that satis es the spec-i cation and both the above properties.