Verification and synthesis of MITL through alternating timed automata
Morgane Estiévenart · ORBi UMONS · 2015
vie d'un chercheur que j'ai découverte à leurs côtés.Votre expérience et vos conseils judicieux ont été d'une grande aide: ils m'ont notamment permis de me familiariser avec la formalisation d'idées clés et la rédaction (en anglais !) de papiers.Merci également pour votre compréhension face à mes dicultés en anglais et mon aversion des longs voyages avec lesquelles il n'a pas toujours été facile de composer.Je remercie ensuite tous les membres de mon jury pour avoir eu le courage d'accepter la relecture de ma thèse et la tâche de la juger.Je me dois aussi de remercier ma famille qui a toujours cru en moi, sûrement plus que je n'en suis moi-même capable.Merci d'avoir toujours été là pour moi et de m'avoir toujours soutenue dans mes choix.Merci de m'aider et de m'épauler dans mes entreprises, même les plus farfelues !Merci pour votre gentillesse et vos attentions, biens rares dont j'ai la chance de pouvoir proter.Je n'oublie pas non plus mes amis, pour les moments de détente nécessaires à la décompression.Je les remercie pour tous ces moments partagés, ces nombreux iii We now dene the satisfaction relation `|ù v ' enabling to express the notion of minimal model.Denition 2.92.Let M P Config pAq be a conguration of an OCATA A, and v P R .We dene the satisfaction relation `| ù v ' on ΓpLq as: