Formal Modelling and Analysis of Real-Time Systems: Lab 3

Part of the ARTES++ course Formella analysmetoder för realtidssystem (5p) VT'04.

Exercise: Vector Rally

In this exercise you are asked to model and analyse an optimisation problem, proposed by Kåre J. Kristoffersen in 2003.

The purpose of Vector Rally is to simulate the challenges met when driving a vehicle as fast as possible through a course with many turns and obstacles. It is natural in the sense that it involves acceleration, and captures nicely the fact that one needs to slow down before taking a turn. The purpose of the challenge is to use a model-checker to find the optimal path (i.e. the fastest/shortest path) on a rally course.

An example of a rally course is shown in this figure:

The vehicle is represented by the two integer pairs position = (x, y) and speed = (dx,dy). In each step the vehicle changes position by adding speed to position (i.e. the next position is (dx+x,dy+y)) possibly by first adjusting speed by +/- 1 horizontally and/or vertically.

The vehicle starts in position (0,0) with speed (0,0). It should reach the goal (represented by a vertical or horizontal line), but without going out of bound as well as hitting or crossing any of the obstacles. In the figure above, a vector from (5,6) to (8,6) is illegal (the vector from (5,6) to (8,8) or (7,8) are also illegal).