X Informatique MP 2013

Thème de l'épreuve Logique temporelle
Principaux outils utilisés logique, arbres, automates
Mots clefs logique temporelle, logique LTL, parcours de graphe

Corrigé

(c'est payant, sauf le début): - - - - - - - - - - - - - - - - - - - - - - -

Extrait gratuit du corrigé

(télécharger le PDF)
           

Énoncé complet

(télécharger le PDF)
                          

Rapport du jury

(télécharger le PDF)
              

Énoncé obtenu par reconnaissance optique des caractères


ÉCOLE POLYTECHNIQUE -- ÉCOLES NORMALES SUPÉRIEURES CONCOURS D'ADMISSION 2013 FILIÈRE MP SPÉCIALITÉ INFO COMPOSITION D'INFORMATIQUE -- A -- (XULC) (Durée : 4 heures) L'utilisation des calculatrices n'est pas autorisée pour cette épreuve. Le langage de programmation choisi par le candidat doit être spécifié en tête de la copie. *** Logique temporelle On étudie dans ce problème un formalisme logique, la logique temporelle, permettant de définir des formules auxquelles sont associés des langages de mots. Ainsi, pour toute formule go de la logique temporelle et pour tout mot u on définira la propriété que le mot u satisfait la formule go, et a toute formule go on associera l'ensemble LSD des mots qui satisfont g0. L'objet principal de ce probléme est de s'intéresser aux propriétés de ces langages LSD. La partie I introduit la logique temporelle et donne des exemples de formules La partie Il introduit une forme normale pour les formules La partie III est consacrée a montrer que pour toute formule l'ensemble de mots associés est un langage rationnel. Enfin, la partie IV étudie d'une part probléme de la satisfiabilité d'une formule (étant donnée une formule g0, existe--t--il un mot satisfaisant g0 ?) et d'autre part l'expressivité des formules Les parties peuvent être traitées indépendamment. Néanmoins, chaque partie utilise des nota-- tions et des fonctions introduites dans les parties précédentes. La complexité, ou le coût, d'un programme P (fonction ou procédure) est le nombre d'opérations élémentaires (addition, soustraction, multiplication, division, affectation, etc...) nécessaires a l'exécution de P. Lorsque cette complexité dépend d'un paramètre n, on dira que P a une complexité en (9( f (n)), s'il existe K > 0 tel que la complexité de P est au plus K f (n), pour tout n. Lorsqu'il est demandé de garantir une certaine complexité, le candidat devra justifier cette dernière si elle ne se déduit pas directement de la lecture du code. Partie I. Préliminaires Un alphabet est un ensemble fini A dont les éléments sont appelés lettres. Un mot sur un alphabet A est une suite finie d'éléments de A; on notera e le mot vide (c'est--à--dire la suite de longueur nulle) et on définira la longueur lul d'un mot non vide u : ao - - - CLg_1 comme valant Æ. Si A est un alphabet, on notera A* l'ensemble des mots sur A et A+ : A* \ {EUR} l'ensemble des mots non vides sur A. Dans la suite, les lettres d'un mot de longueur Æ sont indicées de 0 a Æ -- 1. En Caml, nous représenterons les mots a l'aide du type string. Les fonctions suivantes pour-- ront être utilisées dans la suite. -- Si mot est de type string et i est de type int alors mot. [i] est de type char et donne la lettre d'indice i de mot. Par exemple : "bonj our". [3] renvoie 'j '. -- string_length: string --> int renvoie la longueur d'un mot. En Pascal, nous représenterons les mots a l'aide du type string. Les fonctions suivantes pourront être utilisées dans la suite. -- Si mot est de type string et i est de type integer alors mot [i] est de type char et donne la lettre d'indice i de mot avec la convention que la première lettre est d'indice 1. Par exemple : mot:='bonj our' ;mot [4] renvoie 'j '. -- Si mot est de type string, length (mot) donne la longueur de mot. Dans tout le problème on se fixe un alphabet fini A (on pourra imaginer qu'il s'agit des lettres minuscules de l'alphabet usuel). On souhaite définir des ensembles de mots sur l'alphabet A a l'aide de formules logiques. Pour cela, on définit, pour chaque lettre a E A, un prédicat p... qui permettra de tester si la lettre a une position donnée est un a. Pour construire des formules a partir de ces prédicats, on utilise les connecteurs Booléeens \/ (ou), /\ (et) et fi (non) ainsi que les connecteurs temporels X (juste après), G (désormais), F (un jour) et U (jusqu'à). Les formules de la logique temporelle sont alors construites par induction comme suit. Si pa est un prédicat, et si g0, rt sont des formules de la logique temporelle, toutes les formules seront construites selon la syntaxe suivante : 1. VRAI ÇOEN@P"ÈP°N Toutes les formules seront construites de la facon précédente, en omettant les parenthèses si celles--ci sont inutiles. Par exemple, Xpb, pa Upg, et F(Gpa) sont des formules. Nous allons maintenant définir le sens (ou la sémantique) des formules. Soit un mot u et soit une formule de la logique temporelle g0. On définit, pour tout i 2 0, la propriété " le mot u satisfait la formule cv à la position i", ce qui sera noté (u, i) ): g0, comme suit. Si i 2 lul, on n'a pas (u,i) \: g0 : une formule ne peut être vraie qu'à une position du mot; en particulier le mot vide ne satisfait aucune formule (pas même la formule VRAI). Si i S lul -- 1, on note u : ao - - - a|u|_1 et on raisonne alors par induction sur la structure de go. % Pa si et seulement si a,- = a. % (agp) si et seulement si l'on n'a pas (u, i) % 90. % (go \/ rfi) si et seulement si (u, i) % g0 ou (U, 2) l= @- % (go /\ rfi) si et seulement si (u, i) % go et (U, 2) l= @- % (Xg0) si et seulement si (u,z' + 1) % g0. Notez que si z' : lul -- 1, alors on ne peut (u l: l: }: .© P" H; ." !° !" A A A A A A È @. \./ \./ \./ \./ \./ \./ J) % (X90)- Gg0) si et seulement si (u,j) % gr) pour tout z' £j £ lul -- 1. ."' A È @ Fra) si et seulement si 3j tel que i £j £ lul -- 1 et (u,j) % g0. (g0Urÿ) si et seulement si 3j tel que i £j £ lul -- 1, (u,j) % w et (u,k) % gr) pour tout ktel que i S k  char --> ensemble { Pascal } maj(phi: ensemble; c: Char) : ensemble; Question 15 Écrire une fonction sousFormulesVraies qui prend en argument une formule (0 et un mot et renvoie un ensemble décrivant les sous--formules @ de (& telles que u \= @. Votre fonction devra avoir une complexité polynomiale dans la taille de la formule et dans la taille du mot. Justifier la terminaison et préciser la complexité (dans la taille de la formule et la taille du mot). (* Caml *) sousFormulesVraies: formule --> string --> ensemble { Pascal } sousFormulesVraies(phi: formule; v: string) : ensemble; Question 16 En déduire une fonction veriteBis qui teste si une formule donnée est vraie a la première position d'un mot donné. (* Caml *) veriteBis: formule --> string --> bool { Pascal } veriteBis(phi: formule; v: String) : Boolean; Soit (0 une formule. On associe a (0 un langage de mots LSD Ç A+ en posant Loe={UEA+lUl=SÛ} Soit un mot u : ao - - - ag_1. On note & le mot miroir de u : ü : CLg_1CLg_2 - - - CLO. Soit un langage L Ç A+, on notera L : {Ü \ U E L}. Question 17 En vous inspirant de la fonction maj de la question 14, montrer que pour toute formule (0, le langage LSD est reconnu par un automate déterministe complet. Donner un majorant du nombre d'états d'un tel automate. Question 18 En déduire que pour toute formule (0, le langage LSD est reconnu par un automate fini. Donner un majorant du nombre d'états d'un tel automate (automate qui pourra être pris non--déterministe) . Partie IV. Satisfiabi1îté et expressivité On rappelle que désormais les formules considérées sont normalisées (elles n'utilisent donc ni le F ni le G). Dans toute cette partie, on considérera que A = {a, 19} sauf mention explicite. Le but de cette partie est dans un premier temps d'écrire un programme qui prend en entrée une formule (0 et renvoie true si et seulement s'il existe U E A+ tel que u \= (0. Dans un second temps, on montre qu'il existe un langage accepté par un automate fini qui ne peut être décrit par aucune formule de la logique temporelle. Question 19 Soit A un automate fini déterministe sur l'alphabet A. Décrire informellement un algorithme qui calcule la liste des états atteignables depuis l'état initial (c'est--à--dire l'ensemble des états (] tels qu'il existe un mot qui lu depuis l'état initial termine dans q). Question 20 Soit g0 une formule satisfiable, c'est--à--dire pour laquelle existe un mot U E A+ tel que u \: g0. Soit u...... un plus court u tel que u \: g0. Majorer la longueur de u...... en fonction de la taille de go. Pour la question suivante, on pourra utiliser des listes de couples formés d'un ensemble et d'une chaîne de caractères. En Caml, une telle liste aura le type (ensemble*string) list. En Pascal, une telle liste aura le type listeEnsembles donné par : listeEnsembles = "rlisteEnsembles; rlisteEnsembles = Record Mot : string; Element : ensemble; Suivant : listeEnsembles; End; En Pascal, on pourra utiliser sans la programmer une fonction cons (mot : string; ens ensemble; L : listeEnsembles): listeEnsembles qui renvoie la liste obtenue en ajoutant le couple (mot , ens) en tête de la liste L. L'appel a cette fonction a un coût constant. Question 21 Écrire une fonction satisfiable qui prend en argument une formule go et renvoie soit la chaine "Formule non satisfiable" (Caml) ou la chaine 'Formule non satisfiable' (Pascal) s'il n'existe pas de U E A+ tel que u \: go et sinon renvoie un U E A+ tel que u \: g0. La complexité de votre fonction devra être en O(2OElfilfi) où oz et [3 sont deux constantes que vous préciserez. Il est permis de décomposer la réponse en quelques fonctions auxiliaires. On rappelle ici que l'on suppose que A = {a, 19}. Donner dans un premier temps les idées clés de l'algorithme avant d'écrire le code. (* Caml *) satisfiable : formule --> string { Pascal } satisfiable(phiz formule) : string; Question 22 Pour cette question, on pose A = {a} et on note a' le mot formé de z' lettres a, par exemple a4 : aaaa. Montrer qu'il n'existe pas de formule g0 telle que LSD : {a2' \ z' 2 1}. On pourra montrer que pour toute formule g0, il existe N 2 0 tel que l'on ait l'une des deux situations suivantes : -- pour tout n 2 N, a" \: gp. -- pour tout n 2 N, a" l7£ gp.

Extrait du corrigé obtenu par reconnaissance optique des caractères


 X Informatique MP 2013 -- Corrigé Ce corrigé est proposé par Guillaume Batog (Professeur en CPGE) ; il a été relu par Benjamin Monmege (ENS Cachan) et Vincent Puyhaubert (Professeur en CPGE). En logique propositionnelle, on décrit la syntaxe des formules construites à partir d'un ensemble de variables et à l'aide des connecteurs logiques ¬, , . Puis on définit la sémantique de ces formules à l'aide d'une relation de satisfiabilité d'une valuation des variables sur une formule. Dans la logique temporelle présentée dans ce problème, on ajoute des connecteurs temporels X (juste après), G (désormais), F (un jour) et U (jusqu'à) dont la sémantique est précisée par une relation de satisfiabilité d'un mot u sur une formule . Ce sujet a pour objectif d'étudier les langages de mots reconnus par une formule de cette logique. Il est composé de 4 parties, qu'il est préférable de traiter dans l'ordre. · La première partie, préliminaire, permet de se familiariser avec la logique temporelle. Elle doit être traitée assez rapidement mais avec rigueur car les questions, faciles en apparence, recèlent des cas particuliers cachés. · Dans la deuxième partie, on transforme toute formule en une formule normalisée (sans connecteurs F et G) qui lui est logiquement équivalente (c'est-à-dire ayant le même langage de mots). Puis on écrit une fonction vérifiant si un mot satisfait une formule normalisée. L'algorithmique sous-jacente consiste simplement à parcourir des arbres représentant les formules. La dernière question, portant sur une étude de complexité, est la plus ardue du problème. · La troisième partie présente une méthode plus efficace pour vérifier si un mot satisfait une formule. On montre en fin de partie qu'elle peut être vue comme l'exécution d'un mot sur un automate, qui peut être construit à partir de la formule. · La quatrième partie débute par deux questions classiques sur les automates. Elles apportent une aide précieuse pour écrire ensuite une fonction décidant si une formule est satisfiable (c'est-à-dire si son langage de mots est non vide). Pour traiter cette question, il est nécessaire d'avoir bien compris les ressorts de la troisième partie. Enfin, la dernière question, indépendante de tout le reste, propose un exemple de langage rationnel qui n'est pas un langage de mots satisfaisant une formule de la logique temporelle. Outre que les notions abordées sont nouvelles aux concours, la difficulté de ce sujet tient au fait qu'il est impossible de traiter les questions de programmation sans avoir réussi à répondre aux questions théoriques qui les précèdent, excepté pour les fonctions faciles qui ne rapportaient que peu de points. L'intrication (naturelle) entre logique et automates en fait un sujet intéressant pour qui souhaite avoir un aperçu d'un domaine d'étude de l'informatique théorique appliquée à la vérification de programmes. Indications Partie I 3 Rappelons que la formule VRAI n'est vraie que pour les positions de mot. 5 Une lettre b d'un tel mot est toujours suivie de la lettre a sauf s'il s'agit de la dernière lettre du mot. 7 Écrire la sémantique de u |= U et distinguer les cas j = 0 et j 6= 0 puis i = 0 et i 6= 0 dans la définition donnée par l'énoncé. Le but est de faire apparaître (u, 1) |= U. Partie II 9 Utiliser l'opérateur U. 10 Trouver un lien entre F et G 11 La fonction veriteN s'appuie sur les règles sémantiques de l'énoncé et sur l'équivalence logique de la question 7. Montrer la terminaison de la fonction par récurrence forte sur (n, k), élément de N × N muni de l'ordre lexicographique, où n désigne la taille de la formule en argument et k le nombre de lettres du mot à partir de la position donnée. Pour obtenir la complexité de la fonction, poser T(, k) le nombre d'appels récursifs pour une formule , un mot u et une position |u| - k puis établir l'inégalité de récurrence i k h P T(, k) 6 2 + T(1 , j) + T(2 , j) j=1 où 1 et 2 sont les sous-formules (éventuellement vides) du connecteur à la k racine de . Enfin, montrer que T(, k) 6 k || avec k indépendant de à déterminer. Partie III 13 Démontrer la propriété par induction structurelle sur la formule . 14 Effectuer la mise à jour de bas en haut en suivant les règles obtenues au cours de la question 13. 17 Considérer maj comme la fonction de transition d'un automate. Partie IV 20 Montrer que le plus petit mot reconnu par un automate à n états (reconnaissant un langage non vide) est de taille au plus n - 1. 21 Implémenter l'algorithme de la question 19 en utilisant l'automate décrit à la question 17. 22 Démontrer par induction structurelle sur que toute formule appartient à un ensemble V(N) ou F(N) avec N N où V(N) = { | n > N an |= } et F(N) = { | n > N an 6|= } I. Préliminaires 1 Notons P(x) la propriété de la question (x). · P(a) est vraie car le mot u n'est constitué que des lettres a et b à partir de la position 4. · P(b) est fausse car elle équivaut à la propriété (u, 3) |= G(pa pc ) qui est fausse puisque a4 = b / {a, c}. · P(c) est vraie car P(a) est vraie. · P(d) est vraie car a3 = c et toutes les lettres précédant a3 sont a ou b. 2 Un mot u possède une lettre x si et seulement si u |= Fpx . Ainsi, Le mot u contient un a suivi plus tard d'un b si et seulement si u |= F(pa Fpb ). D'autres formules peuvent être trouvées pour cette question et les suivantes. Elles sont « logiquement équivalentes » entre elles (cf. question 7). Celle proposée ici a l'avantage de la concision. 3 Excepté dans le cas où l'entier i ne correspond pas à une position du mot u, la formule VRAI est toujours satisfaite par (u, i), d'où i = |u| - 1 i = |u| - 1 Ainsi, et i + 1 > |u| i 6 |u| - 1 (u, i) |= VRAI et (u, i + 1) 6|= VRAI (u, i) |= VRAI ¬X(VRAI) Fin = VRAI ¬X(VRAI) 4 Puisque le mot u satisfait la formule Fin uniquement à la dernière position, u se termine par un a si et seulement si u |= F(pa Fin). 5 Décrivons un mot u de (ab)+ : · la première lettre est un a, soit u |= pa ; · la dernière lettre est un b, soit u |= F(pb Fin) (question 4) ; · pour tout i tel que 0 6 i 6 |u| - 1, ai vaut a ou b, soit (u, i) |= pa pb ; si ai = a alors ai+1 = b, soit (u, i) |= (¬pa ) Xpb ; si ai = b et ai n'est pas la dernière lettre de u, alors ai+1 = a, soit (u, i) |= ¬(pb ¬Fin) Xpa . Finalement, u (ab)+ si et seulement si u |= avec = pa F(pb Fin) G (pa pb ) (¬pa ) Xpb (¬pb ) Fin Xpa 6 Un mot u satisfait la formule si, et seulement si, il existe j 6 |u|-1 (opérateur F) tel que : · la lettre aj est un a (formule pa ) ; · le suffixe aj+1 . . . a|u|-1 ne contient pas la lettre a (formule X(G(¬pa ))) ; · le suffixe aj . . . a|u|-1 contient le motif bc (formule F(pb Xpc )). L'automate suivant reconnaît le langage L : a, b, c b, c a b, c b c 7 Soit u un mot de longueur n N. Montrons la propriété u |= U u |= (X(U)) Puisque le mot vide ne satisfait aucune formule, cette propriété est vraie pour le mot vide. Considérons un mot u non vide (n > 1). Par définition, u |= U j 6 n (u, j) |= et i < j (u, i) |= Distinguons les cas j = 0 et j > 1 : u |= U (u, 0) |= ou 1 6 j 6 n (u, j) |= et i < j Distinguons les cas i = 0 et i > 1 : i < j d'où (u, i) |= u |= U (u, i) |= (u, 0) |= et 1 6 i < j (u, i) |= u |= ou u |= et 1 6 j 6 n (u, j) |= et 1 6 i < j (u, i) |= On reconnaît la sémantique de U à partir de la position 1 du mot u : u |= U u |= ou u |= et (u, 1) |= U soit u |= U u |= (X(U)) pour tout mot u. Autrement dit, U (X(U)) Une paraphrase du type « un mot u satisfait U si, et seulement si, il satisfait ou s'il satisfait et si le suffixe de u obtenu en supprimant sa première lettre satisfait U » est une justification sans doute insuffisante à un concours comme l'X.