11 June 2015
Title: Formal analysis of Edinburgh buses using GPS data
We present recent work on the development of stochastic performance models of a public transportation network using real-world data. The data is provided to us by Lothian Buses, which operates an extensive bus network in Edinburgh. In particular, we use datasets of GPS measurements with about 30-40 seconds between subsequent observations. Some quantities of interest that can be analysed using this data are the times needed to complete specific route segments, and the 'headway': the distance (in terms of journey completion) between subsequent buses. Both can be modelled using established formalisms, namely Markov chains and time series respectively. We briefly discuss several applications, including a 'what-if' scenario involving the introduction of trams to the Edinburgh city centre, and the evaluation of the punctuality of frequent services in terms of criteria set by the Scottish government.