X Informatique MP 2013

Thème de l'épreuve Logique temporelle
Principaux outils utilisés logique, arbres, automates

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.