Seminar Room, ground floor (Building IMAG)
15 janvier 2018 - 14h00
Filtrage par Motif Temporisé: Théorie et Applications (Phd Defense)
par Dogan Ulus de Verimag / UGA
Résumé : Les systèmes dynamiques présentent des comportements temporels qui peuvent être exprimés sous diverses formes séquentielles telles que des signaux, des ondes, des séries chronologiques et des suites d’événements. Détecter des motifs sur de tels comportements temporels est une tâche fondamentale pour comprendre et évaluer ces systèmes. Étant donné que de nombreux comportements du système impliquent certaines caractéristiques temporelles, le besoin de spécifier et de détecter des motifs de comportements qui implique des exigences de synchronisation, appelées motifs temporisés, est évidente. Cependant, il s’agit d’une tâche non triviale due à un certain nombre de raisons, notamment la concomitance des sous-systèmes et la densité de temps.
La contribution principale de cette thèse est l’introduction et le développement du filtrage par motif temporisé, c’est-à-dire l’identification des segments d’un comportement donné qui satisfont un motif temporisé. Nous proposons des expressions rationnelles temporisées (TRE) et la logique de la boussole métrique (MCL) comme langages de spécification pour motifs temporisés. Nous développons d’abord un nouveau cadre qui abstraite le calcul des aspects liés au temps appelé l’algèbre des relations temporisées. Ensuite, nous fournissons des algorithmes du filtrage hors ligne pour TRE et MCL sur des comportements à temps dense à valeurs discrètes en utilisant ce cadre et étudions quelques extensions pratiques.
Il est nécessaire pour certains domaines d’application tels que la verification dynamique que le filtrage par motif doit être effectué pendant l’exécution réelle du système. Pour cela, nous fournissons un algorithme du filtrage en ligne pour tres basé sur la technique classique des dérivées d’expressions rationnelles. Nous croyons que la technique sous-jacente qui combine les dérivées et les relations temporisées constitue une autre contribution conceptuelle majeure pour la
recherche sur les systèmes temporisés.
Nous présentons un logiciel libre Montre qui implémente nos idées et algorithmes. Nous explorons diverses applications du filtrage par motif temporisé par l’intermédiaire de plusieurs études de cas. Enfin, nous discutons des orientations futures et plusieurs questions ouvertes qui ont émergé à la suite de cette thèse.
Composition of the Jury:
- Oded Maler, Verimag (Thesis Supervisor)
- Rajeev Alur, University of Pennsylvania, USA (Reviewer)
- Kim G. Larsen, University of Aalborg, Denmark (Reviewer)
- Radu Grosu, Technical University of Vienna, Austria (Reviewer)
- Patricia Bouyer-Decitre, LSV Cachan (Examiner)
- Ahmed Bouajjani, Irif, Universite Paris 7 (Examiner)
- Saddek Bensalem, Verimag (Examiner)
- Eugene Asarin, Irif, Universite Paris 7 (Invited)
- Dejan Nickovic, AIT, Austria (Invited)
