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é

 : 👈 gratuite pour tous les corrigés si tu crées un compte
👈 l'accès aux indications de tous les corrigés ne coûte que 5 € ⬅ clique ici
👈 gratuite pour tous les corrigés si tu crées un compte
- - - - - - - - - - - - - - - - - - - -

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