Racetrack
Racetrack
Racetrack evolved from a pen and paper game and is a well known benchmark in AI autonomous decision making contexts. In Racetrack, a vehicle needs to drive on a 2D-track (gray) from start cells (green) to goal cells (blue), the track being delimited by walls (red) as depicted below. The vehicle can change acceleration in unit steps in nine directions spanned by the x- and y-dimensions [-1, 0, 1].
The natural abstraction of the autonomous driving challenge in this simplified setting is the task of finding a policy that manages to reach the goal with a probability as high as possible and crashes as rarely as possible. Probabilities enter the picture by imperfect acceleration modelling slippery road conditions. If noise occurs in the model with a certain probability, the action suggested by the policy is not applied but the car continues driving with the previous velocity.
Over the last years several different versions of Racetrack benchmarks with different features were developed for different projects. In the following we will describe all of them and highlight their benefits for specific use cases.
All of these benchmarks have in common that they are defined as networks of MDPs in JANI, a modelling language supported by most state-of-the-art model checkers.
The first version of Racetrack, which has been used for the evaluation in Deep Statistical Model Checking, is a quite simple one. The scripts allow to generate models with a certain noise probability, a specific definition for collision calculation, a certain start point or individual model files for a list of start points, a certain start velocity, if the car has to park on the goal line, and other small modifications to the model.
For Components in Probabilistic Systems: Suitable by Construction and Momba: JANI meets Python a featured version of Racetrack was in use. In this version models with different car and underground variants were generated. The car variants differ in their tank size which has an impact on the amount of fuel which can be consumed and they differ in the engine of the car which defines the minimal and maximal speed as well as the acceleration bounds. In addition, different undergrounds are implemented, like ice, tarmac and sand, with different noise values.
Models of this variant can be generated using Momba, a flexible Python framework for dealing with formal models covering the whole process from model construction to analysis. With the help of model.py, which is part of the python racetrack package, a family of Racetrack models with several feature variants can be constructed. For more information about how to interact with the python racetrack package and Momba itself we refer to the Readme of Momba, the package documentation and the artifact describing how to interact with the model.