Model-checking Edinburgh buses

prism3d3smallOne of the case studies in the QUANTICOL project is concerned with modelling and analysing the public transport system in the city of Edinburgh, with a specific focus on the bus network. Buses in Edinburgh are thoroughly instrumented with GPS positioning instrumentation, and report their latitude and longitude every thirty seconds back to a central server which uses a predictive model to estimate arrival times at bus stops. These predictions are relayed back to passengers of the bus service using on-street signage, made accessible via a web site, and delivered by smartphone apps.

The Traffic Commissioner for Scotland sets standards for bus operators mandating the percentage of buses which should be on-time for services (that is, they depart from their stop no more than one minute early and no more than five minutes late for specific timing points along the route). The gravity and seriousness of these definitions was made clear when the Traffic Commissioner for Scotland held a public enquiry into the operation of Edinburgh’s Lothian Buses in response to a complaint about buses running too early. The public enquiry and the subsequent decision of the Traffic Commissioner were reported in national newspapers.

Using measurement data from the city’s automatic vehicle location service, the QUANTICOL project has been able to build accurate stochastic models of Edinburgh’s bus services. Using this it is possible to determine whether potential changes to their service would expose a bus company to liability in the future.

The first step was to find an appropriate stochastic model which would capture the variability in the bus service due to delays which occur for operational reasons such as traffic conditions, passenger boarding and alighting, and road congestion. Empirical distributions of journey times were used as an input for the HyperStar tool for fitting phase-type distributions to data sets, producing a phase-type stochastic process as the result.

Phase-type distributions have the desirable property that they can approximate any distribution with non-negative support arbitrarily closely and can also be represented as continuous-time Markov chains. This allowed the QUANTICOL researchers to reformulate the problem as a model- checking problem and verify probabilistic logic formulae against this model.

This efficient modelling method meant that the researchers on the project can compute the probability of completing a journey within a specified window of tolerance on arrival times. Varying the upper and lower bounds on the time of arrival allows the modellers to see whether the bus service could operate under stricter terms of operation or whether there is no potential for this because they are already near to failing to meet their targets for on-time arrivals.