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 de la logique temporelle et pour tout mot on définira la propriété que le mot satisfait la formule , et à toute formule on associera l'ensemble des mots qui satisfont . L'objet principal de ce problème est de s'intéresser aux propriétés de ces langages .
La partie I introduit la logique temporelle et donne des exemples de formules. La partie II introduit une forme normale pour les formules. La partie III est consacrée à 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 , existe-t-il un mot satisfaisant ?) et d'autre part l'expressivité des formules.
Les parties peuvent être traitées indépendamment. Néanmoins, chaque partie utilise des notations et des fonctions introduites dans les parties précédentes.
La complexité, ou le coût, d'un programme (fonction ou procédure) est le nombre d'opérations élémentaires (addition, soustraction, multiplication, division, affectation, etc...) nécessaires à l'exécution de . Lorsque cette complexité dépend d'un paramètre , on dira que a une complexité en , s'il existe tel que la complexité de est au plus , pour tout . 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 dont les éléments sont appelés lettres. Un mot sur un alphabet est une suite finie d'éléments de ; on notera le mot vide (c'est-à-dire la suite de longueur nulle) et on définira la longueur d'un mot non vide comme valant .
Si est un alphabet, on notera l'ensemble des mots sur et l'ensemble des mots non vides sur .
Dans la suite, les lettres d'un mot de longueur sont indicées de 0 à .
En Caml, nous représenterons les mots à l'aide du type string. Les fonctions suivantes pourront être utilisées dans la suite.
Si mot est de type string et est de type int alors mot. [i] est de type char et donne la lettre d'indice i de mot. Par exemple : "bonjour". [3] renvoie 'j'.
string_length: string -> int renvoie la longueur d'un mot.
En Pascal, nous représenterons les mots à l'aide du type string. Les fonctions suivantes pourront être utilisées dans la suite.
Si mot est de type string et 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:='bonjour';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 (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 à l'aide de formules logiques. Pour cela, on définit, pour chaque lettre , un prédicat , qui permettra de tester si la lettre à une position donnée est un . Pour construire des formules à partir de ces prédicats, on utilise les connecteurs Booléeens (ou), (et) et (non) ainsi que les connecteurs temporels (juste après), (désormais), (un jour) et (jusqu'à).
Les formules de la logique temporelle sont alors construites par induction comme suit. Si est un prédicat, et si sont des formules de la logique temporelle, toutes les formules seront construites selon la syntaxe suivante :
VRAI
Toutes les formules seront construites de la façon précédente, en omettant les parenthèses si celles-ci sont inutiles. Par exemple, et sont des formules.
Nous allons maintenant définir le sens (ou la sémantique) des formules.
Soit un mot et soit une formule de la logique temporelle . On définit, pour tout , la propriété "le mot u satisfait la formule à la position ", ce qui sera noté , comme suit. Si , on n'a pas : 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 , on note et on raisonne alors par induction sur la structure de .
VRAI.
si et seulement si .
si et seulement si l'on n'a pas .
si et seulement si ou .
si et seulement si et .
si et seulement si . Notez que si , alors on ne peut avoir .
si et seulement si pour tout .
si et seulement si tel que et .
si et seulement si tel que et pour tout tel que .
On notera si et seulement si l'on n'a pas . On notera (et on dira alors que est vraie pour ) le fait que ( ) , et on notera le fait que ( ) .
Par exemple :
car la lettre d'indice 3 de est un .
aaabcbab car la lettre d'indice 3 est un et toutes les lettres qui la précèdent sont des .
aaabcbab car il n'existe pas d'indice tel qu'à partir de cet indice il n'y ait plus que des (en effet, la dernière lettre est un ).
Question 1 On pose . Pour chacun des énoncés ci-dessous dire s'il est vrai en justifiant brièvement votre réponse.
(a)
(b)
(c)
(d)
Question 2 Écrire une formule telle que si et seulement si contient un suivi plus tard d'un . Par exemple on aura ccacccba tandis que ccacccaa .
Question 3 Écrire une formule Fin telle que Fin si et seulement si (c'est-à-dire si et seulement si est l'indice de la dernière lettre de ).
Dans la suite, on pourra utiliser Fin comme une boîte noire.
Question 4 Écrire une formule telle que si et seulement si se termine par un .
Question 5 Écrire une formule telle que si et seulement si , c'est-à-dire si et seulement s'il existe tel que et, pour tout tel que on a si est pair et si est impair.
Question 6 Pour cette question, on pose . Soit . Décrire un automate fini (pouvant être non-déterministe) reconnaissant le langage .
Deux formules et sont équivalentes, ce que l'on note , si pour tout mot , on a si et seulement si . Autrement dit, les formules et sont vraies pour les mêmes mots.
Question 7 Soient et deux formules quelconques. Montrer que l'on a .
Partie II. Normalisation de formules
Afin de manipuler des formules de la logique temporelle, on va représenter ces dernières par des arbres. Outre les prédicats et la formule VRAI nous avons des connecteurs unaires , G et ) et des connecteurs binaires ( et ). À la manière des expressions arithmétiques, on représente une formule de la logique temporelle par un arbre dont les feuilles sont étiquetées soit par un prédicat soit par VRAI, et dont les nœuds internes sont étiquetés par un connecteurs unaire (un tel nœud aura alors un seul fils) ou par un connecteur binaire (un tel nœud aura alors deux fils). Dans la suite, on confondra fréquemment une formule avec sa représentation par un arbre.
Par exemple, la formule sera représentée par l'arbre ci-dessous :
Le type des formules est défini comme suit :
(* Caml *)
type formule =
|VRAI
|Predicat of char
|NON of formule
|ET of formule * formule
|OU of formule * formule
|X of formule
|G of formule
|F of formule
|U of formule * formule;;
{ Pascal }
Type
typeFormule = (VRAI,Predicat,NON,ET,OU,X,G,F,U);
formule = `rformule;
rformule = Record
case t : typeFormule of
VRAI : ();
Predicat : (c : char);
NON,X,G,F : (h : formule);
U,ET,OU : (d,g : formule);
End;
En Pascal, on pourra utiliser sans les programmer les fonctions suivantes :
Function FVrai() : formule;
Function FP(c: Char) : formule;
Function FUn(t: typeFormule; h: formule) : formule;
Function FBin(t: typeFormule; g,d: formule) : formule;
La fonction FVrai renvoie la formule VRAI. La fonction FP appelée avec une lettre 'c' renvoie la formule . La fonction FUn appelée avec NON (resp. X,G et F) et une formule renvoie la formule (resp. et ). La fonction FBin appelée avec U (resp. ET et OU) et deux formules et renvoie la formule (resp. et ). Par exemple, ) renvoie la formule .
On définit la taille d'une formule par le nombre de nœuds de l'arbre qui la représente. En particulier, la formule VRAI et les formules réduites à un prédicat sont de taille 1 .
Question 8 Écrire une fonction taille qui prend en argument une formule et renvoie sa taille.
(* Caml *) taille: formule -> int
{ Pascal } taille(phi: formule) : integer;
Question 9 Donner, pour toute formule n'utilisant pas le connecteur , une formule équivalente à qui n'utilise pas le connecteur temporel . En déduire une fonction normaliseF qui prend en entrée une formule quelconque et renvoie une formule équivalente qui n'utilise pas le connecteur F. Quelle est la complexité de votre algorithme?
(* Caml *) normaliseF: formule -> formule
{ Pascal } normaliseF(phi: formule) : formule;
Une formule qui utilise comme seuls connecteurs temporels le et le sera qualifiée de normalisée.
Question 10 Montrer que toute formule est équivalente à une formule normalisée. Donner une fonction normalise de complexité linéaire qui prend en entrée une formule quelconque et renvoie une formule équivalente normalisée.
(* Caml *) normalise: formule -> formule
{ Pascal } normalise(phi: formule) : formule;
Dans toute la suite du problème, on supposera que l'on travaille avec des formules normalisées.
Question 11 Écrire une fonction récursive veriteN qui prend en argument un mot , un indice et une formule (normalisée) et détermine si . Justifier que votre fonction termine et indiquer si elle est exponentielle ou polynomiale en la taille de ses arguments.
Partie III. Rationalité des langages décrits par des formules
Le but de cette partie est de montrer qu'étant donnée une formule , l'ensemble des mots pour lesquels est vraie est un langage rationnel.
Soit une formule représentée par un arbre . Une sous-formule de est une formule représentée par un sous-arbre de . Par exemple si l'on considère la formule , représentée par l'arbre ci-dessous,
l'ensemble de ses sous-formules est :
On souhaite représenter des ensembles de sous-formules d'une formule donnée. Pour cela, on va utiliser des arbres dont les nœuds sont étiquetés (en plus des symboles de la logique) par des booléens. Par exemple pour la formule représentée ci-dessus, l'ensemble de sous-formules sera représenté par l'arbre ci-dessous.
Une sous-formule appartient à l'ensemble représenté par un arbre de type ensemble s'il existe un nœud de l'arbre étiqueté par True et dont le sous-arbre "correspond" à la formule (c'est-à-dire qu'après suppression des booléens, le sous-arbre est égal à l'arbre codant ). Le type ensemble est défini comme suit.
(* Caml *)
type ensemble == eformule * bool
and eformule =
| AVRAI
| APredicat of char
| ANON of ensemble
| AET of ensemble * ensemble
| AOU of ensemble * ensemble
| AX of ensemble
| AU of ensemble * ensemble;;
{ Pascal }
ensemble = `rensemble;
rensemble =
Record
b : Boolean;
case t : typeFormule of
VRAI : ();
Predicat : (c : Char);
NON,X,G,F : (h : ensemble);
U,ET,OU : (d,g : ensemble);
End;
On rappelle que l'on ne travaille plus qu'avec des formules normalisées.
Question 12 Écrire une fonction initialise qui prend en argument une formule et renvoie un ensemble représentant l'ensemble vide de sous-formules de .
Question 13 Soient un mot, une formule et l'ensemble des sous-formules de vraies pour . Soit une lettre. Montrer que l'ensemble des sous-formules de vraies pour peut être déterminé uniquement en fonction de et de (en particulier indépendamment de ).
Question 14 En vous basant sur la question 13, écrire une fonction maj qui prend en argument un ensemble (représentant un ensemble de sous-formules d'une formule ) et une lettre et renvoie un ensemble tel que : pour tout mot si représente l'ensemble et sous-formule de des sous-formules de vraies pour alors représente l'ensemble et sous-formule de des sous-formules de vraies pour . Justifier la terminaison et préciser la complexité (dans la taille de la formule) de votre fonction.
Par exemple si l'on reprend l'exemple de la formule arbre à gauche ci-dessous) et de l'ensemble (au centre ci-dessous), alors maj 'b' devra renvoyer l'ensemble (à droite ci-dessous).
Question 15 Écrire une fonction sousFormulesVraies qui prend en argument une formule et un mot et renvoie un ensemble décrivant les sous-formules de telles que . 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).
Soit une formule. On associe à un langage de mots en posant
Soit un mot . On note le mot miroir de . Soit un langage , on notera .
Question 17 En vous inspirant de la fonction maj de la question 14, montrer que pour toute formule , le langage 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 , le langage 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. Satisfiabilité et expressivité
On rappelle que désormais les formules considérées sont normalisées (elles n'utilisent donc ni le ni le ). Dans toute cette partie, on considérera que sauf mention explicite.
Le but de cette partie est dans un premier temps d'écrire un programme qui prend en entrée une formule et renvoie true si et seulement s'il existe tel que . 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 un automate fini déterministe sur l'alphabet . 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 ).
Question 20 Soit une formule satisfiable, c'est-à-dire pour laquelle existe un mot tel que . Soit un plus court tel que . Majorer la longueur de en fonction de la taille de .
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'appel à cette fonction a un coût constant.
Question 21 Écrire une fonction satisfiable qui prend en argument une formule et renvoie soit la chaîne "Formule non satisfiable" (Caml) ou la chaîne 'Formule non satisfiable' (Pascal) s'il n'existe pas de tel que et sinon renvoie un tel que . La complexité de votre fonction devra être en où et 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 . Donner dans un premier temps les idées clés de l'algorithme avant d'écrire le code.
Question 22 Pour cette question, on pose et on note le mot formé de lettres , par exemple aaaa. Montrer qu'il n'existe pas de formule telle que . On pourra montrer que pour toute formule , il existe tel que l'on ait l'une des deux situations suivantes :
pour tout .
pour tout .
X ENS Option Informatique MP 2013 - Version Web LaTeX | WikiPrépa | WikiPrépa
