# 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:

**Bike**is relatively slow but it is the most predictable option which takes to**Sydney**in between 42 and 45 minutes and thus depends very little on uncontrollable traffic conditions.**Car**has a possibility of an**Easy**and fast trip in 20 minutes if traffic permits (probability weight 10 yields likelyhood of 10/11), but there is a risk of 1 in 11 to get stuck in**Heavy**traffic and thus the trip could be prolonged up to 140 minutes.**Train**have periodic schedules and thus may have a waiting time up to 6 minutes and it is quite likely (10 out of 11) that we will board the train successfully and spend up to 35 minutes in location**Go**before reaching**Sydney**. There is also a small risk (1 out of 11) that the train is canceled and we end up in**Wait**, where we would have to decide either to switch to another train or**GoBack**home and in**Aalborg**make a decision again.

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.