É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.