Qais Hamarneh

The abstract urban traffic model represents a network of roads, lanes,  and intersections as well as the cars driving on them. Traffic  controllers, timed automata using Urban Multi-Lane Spatial Logic, allow  the cars to execute manoeuvres like crossing an intersection safely  (without collision) assuming all cars follow their respective controllers. The aim of this thesis is to use the controllers' safety guarantees to  synthesize driving strategies that ensure safety and if possible let  each car reach its destination within a time constraint. To achieve  this, the abstract urban traffic model will be translated into an  instance of Hybrid Game with Triggers, a framework that can model the  cars' continuous movement, the controllers' actions, and conditions  called triggers that prompt a car to act.