Stark has been introduced for the specification, analysis and verification of cyber-physical systems operating under uncertainty. In this paper, we apply it to the modelling and safety analysis of several instances of a highway environment with autonomous vehicles: One vehicle will be controlled by a Stark agent, while the others are modelled as part of a Stark environment. Given the unpredictable behaviour of the environment, we analyse some safety guarantees on the behaviour of the agent in terms of its robustness against perturbations by means of the temporal logic RobTL and statistical model checking. We then discuss the use of Stark for the validation of the behaviour of reinforcement learning agents in the highway environment with the temporal logic DisTL.