Skip to main content.
[an error occurred while processing this directive]

Traffic Dilema

Suppose we need to travel to Sidney from Aalborg as soon as possible but we are not sure which mode of transport is the fastest: a bike, a car or a train. Each of them have different speeds and risks depending on traffic conditions. Below is a stochastic timed automaton capturing trip possibilities:

We start in the location Aalborg on the left, pack our things and leave within 2 minutes. Then we can choose/control our prefered mode of travel:

Given our model, we can inspect sample trip trajectories via SMC simulate query where the locations are encoded as different levels:

simulate 1 [<=100] { 
     Kim.Aalborg +  2*Kim.Bike +  4*Kim.Easy +  6*Kim.Heavy + 
     8*Kim.Train + 10*Kim.Go +   12*Kim.Wait + 14*Kim.Sydney }

Below are two sample trajectories computed by Uppaal Stratego:

Normal train trip in 20 minutes:Train and then bike in 50 minutes:

The following queries and resulting plot show where and when the time is being spent:

simulate 100 [<=100] {
     14+Kim.Aalborg, 12+Kim.Bike, 10+Kim.Easy, 8+Kim.Heavy,
      6+Kim.Train,    4+Kim.Go,    2+Kim.Wait, Kim.Sydney 
}

Pr[<=60](<> Kim.Sydney) // probability of reaching Sydney within 60 minutes is about 0.97 (not certain, thus not safe)

E[<=200 ; 500] (max: trip) // mean trip is about 28 minutes

Generate and evaluate a safe strategy to get to Sydney within 60 minutes:

strategy GoSafe = control: A<> Kim.Sydney && time<=60

simulate 100 [<=100] {
     14+Kim.Aalborg, 12+Kim.Bike, 10+Kim.Easy, 8+Kim.Heavy,
      6+Kim.Train,    4+Kim.Go,    2+Kim.Wait, Kim.Sydney
} under GoSafe

A<> (Kim.Sydney && time<=60) under GoSafe // satisfied: using GoSafe we certainly reach Sydney within 60 minutes

E[<=200; 500] (max: trip) under GoSafe // mean trip time of GoSafe is about 33 minutes

The plot shows that most of the time is spent in Bike and Sydney and some in Train, therefore Bike is the sure way to reach Sydney but we can also risk catching a train within 10 minutes (if train does not come, we go back to Bike option).


Learn fast strategy by minimizing the time to get to Sydney:

strategy GoFast = minE (trip) [<=200] : <> Kim.Sydney

simulate 100 [<=100] {
     14+Kim.Aalborg, 12+Kim.Bike, 10+Kim.Easy, 8+Kim.Heavy,
      6+Kim.Train,    4+Kim.Go,    2+Kim.Wait, Kim.Sydney 
} under GoFast

Pr[<=60](<> Kim.Sydney) under GoFast // probability is about 0.94 (rushing is risky!)

E[<=200; 500] (max: trip) under GoFast // mean trip time is 15.4 minutes (almost 2x faster than no strategy)

The plot shows that most of the time is spent in Easy and Heavy and then Sydney, therefore Car is the fastest choice on average but we can get stuck in Heavy traffic and be late.


In order to get safe and fast strategy we optimize the GoSafe by minimizing the trip time to get to Sydney:

strategy GoFastSafe = minE (trip) [<=200] : <> Kim.Sydney under GoSafe

simulate 100 [<=100] {
     14+Kim.Aalborg, 12+Kim.Bike, 10+Kim.Easy, 8+Kim.Heavy,
      6+Kim.Train,    4+Kim.Go,    2+Kim.Wait, Kim.Sydney
} under GoFastSafe

Pr[<=60](<> Kim.Sydney) under GoFastSafe // probability is >0.99 (we could not find a counter-example)

E[<=200 ; 500] (max: trip) under GoFastSafe // mean trip time is 22.4 minutes (faster than GoSafe but not as fast than GoFast)

The result shows that Train is the safe and fast option, but a few times one may need to go back and pick a bike.

The model and queries can be downloaded here: traffic.xml.

A walkthrough video presented at ATVA 2014: ATVA14-walkthrough.wmv.