Proving LQG controller global optimality