tokens: Furthermore , we illustrate the application of SSTL , and the verification methods we have developed , on a larger case study concerning issues of the spatio - temporal distribution of bikes in a bike - sharing system , modelled as a Continuous Time Markov Chain ( CTMC ) .