Let a three bit binary counter. This has three spaces for the digits which may be 0 or 1. Initially all bits are set to 0 (i.e. the counter reads 000). Incrementing the counter leads to following sequence of readings 001, 010, 011, 100, 101, 110, 111, returning again then to 000 and so on. Consider x, y and z stand for each of the bits in which z represents the most significant bit (at the left hand side), y refers to the bit in the middle and x the least significant (at the right hand side) in which 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. State the three bit counter utilizing the LTL. The following are the properties we may wish to try and prove are valid given the specification of the three bit counter.

a) Eventually the counter reaches 111.

b) It is not possible to achieve a state where the counter reads 010 and in the next moment the counter reads 100.

Formulate these properties in the LTL. Construct a model that satisfies the specification and both the above given properties.