Connected cruise control design using probabilistic model checking

In this paper, we synthesize a connected cruise controller with performance guarantee using probabilistic model checking, for a vehicle that receives motion information from several vehicles ahead through wireless vehicle-to-vehicle communication. We model the car-following dynamics of the preceding vehicles as Markov chains and synthesize the connected cruise controller as a Markov decision process. We show through simulations that such a design is robust against imperfections in communication