Exploring spatio-temporal properties of bike-sharing systems

In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.