On applying Petri nets to determine optimal offsets for coordinated traffic light timings