Descriptif
Les logiques sont des langages universels qui permettent de spécifier de manière mathématiquement précise le comportement de systèmes, mais aussi de guider le développement d'algorithmes complexes pour garantir leur sûreté et leur contrôle. La richesse de ces logiques est d'autant plus cruciale pour des systèmes complexes, pour lesquels de nombreux phénomènes différents doivent être pris en compte (temporalité, incertitudes, connaissances, concurrence).
Dans ce cours, nous nous intéresserons particulièrement aux logiques utiles à l'analyse de systèmes hybrides, c’est-à-dire de systèmes soumis à la fois à des dynamiques physiques continues et à du contrôle numérique de systèmes informatiques, comme par exemple les véhicules autonomes. Nous explorerons la richesse des logiques et des langages de modélisation dans ce contexte, et nous ferons un tour d'horizon des méthodes formelles basées ou guidées par ces logiques.
Objectifs pédagogiques
Les objectifs sont multiples :
- Apprendre à modéliser des systèmes et à spécifier des problèmes dans des langages riches (logiques, langages de modélisation)
- Développer un socle solide pour des algorithmes de base mais essentiels en méthodes formelles logiques (ex. : théories décidables, tableaux, automates et jeux)
- Découvrir une variété de méthodes formelles pour l'analyse, la vérification et le contrôle de systèmes hybrides basées sur la logique (satisfaction, vérification de modèles, monitorat, synthèse de contrôle)
- Se faire la main sur quelques outils informatiques du domaine (principalement KeYmaera X, un assistant à la preuve pour la logique de programmes hybrides)
Diplôme(s) concerné(s)
Pour les étudiants du diplôme Programmes d'échange internationaux
Aucun.
Suivre les cours CSC_51075_EP et CSC_51051_EP en P1 est un plus.
Pour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique
Aucun.
Suivre les cours CSC_51075_EP et CSC_51051_EP en P1 est un plus.
Format des notes
Numérique sur 20Littérale/grade réduitPour les étudiants du diplôme M1 MPRI - Fondements de l'Informatique
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 5 ECTS
Pour les étudiants du diplôme Programmes d'échange internationaux
Vos modalités d'acquisition :
Contrôle continu (quiz, rendus de TD)
Final (présentation orale d'un projet)
Pour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique
Vos modalités d'acquisition :
Contrôle continu (quiz, rendus de TD)
Final (présentation orale d'un projet)
- Crédits ECTS acquis : 5 ECTS
La note obtenue rentre dans le calcul de votre GPA.
Programme détaillé
- Langages de modélisation pour les systèmes hybrides
- Logique de programme pour systèmes hybrides
- Théories décidables (ou non)
- Logique Temporelle Linéaire: expressivité et satisfaction
- Logique Temporelle Métrique: automate des régions et vérification de modèle
- Logique Temporelle de Signal: sémantique quantitative, monitorat et falsification
- Éléments de théorie des jeux pour la synthèse de contrôle