Add to ORKGDate de soutenance: 13 mars 2012 i ii Acknowledgments The work presented in this manuscript has been carried out in the group of Tom Henzinger at École Polytechnique Fédérale de Lausanne (Oct. 2006- Dec. 2008), in the group of Jean-François Raskin at Universite ́ Libre de Bruxelles (Jan. 2009-Sep. 2009), and in the Laboratoire Spécification et Vérification at ENS Cachan under the auspices of Alain Finkel (since Oct. 2009). Great collaboration with Krishnendu Chatterjee has also been possible through several visits to IST Austria. I would like to warmly thank Tom, Jean-François, Alain, and Krishnendu, as well as all my other co-authors
