Considérations algorithmiques
Il n’existe à l’heure actuelle aucune standardisation de la notion d’algorithme qui soit complètement définie est standardisée. Les notations que nous avons introduites jusqu’à présent permettent d’utiliser certaines structures de données mathématiques comme des objets, mais en utilisant des fonctions qui ressemblent plus aux fonctions mathématiques habituelles.
La différence principale entre les notations mathématiques et les notations algorithmiques est qu’en mathématiques, les objets sont supposés pré-existants au discours, et que le mathématician ne fait que référencer ces objets par des représentations diverses, alors qu’en algorithmique, les objets considérés sont construits et modifiés au cours du temps. Ceci pose un problème de notation, car il est parfois beaucoup plus naturel de modifier un objet que d’en effectuer une copie. Cependant, le support notationnel est pratiquement insexistant, ce qui fait qu’il est souvent laissé au lecteur la nécessité de devenu quels objets sont modifiés par certaines fonctions, comme si cela allait de soit. Nous utiliserons le point d’exclamation (‘!’) pour dénoter les objets qui seront modifiés par une fonction. En général, un unique objet est modifié, en utilisant les informations fournies par les autres paramètres de la fonction.
Programmation logique par contraintes
La programmation logique par contraintes s’appuie sur la programmation logique pour résoudre des problèmes de satisfaction de contraintes. Le problème de satisfaction de contraintes conjonctives est un cas particulier en programmation logique, car le langage est capable de gérer aussi la disjonction et la négation de contraintes. Cependant, le support algorithmique pour ces deux opérateurs logiques est pour le moment loin d’être optimal ou satisfaisant dans un contexte général, bien qu’il soit utile pour des applications particulières.
Disjonction de contraintes Le problème de la disjonction de contraintes est que tant que les deux contraintes peuvent être vraies, il est impossible de propager quoi que ce soit. Le mécanisme de disjonction constructive consiste à effectuer indépendamment la propagation de chaque contrainte. Si une valeur est un support dans aucune des contraintes après propagation, alors elle peut être retirée. Bien que cette approche soit simple à mettre en œuvre, le coût d’exécution des propagateurs est en général trop élevé, ce qui rend le mécanisme inadéquat en pratique. Une méthode plus efficace consiste à calculer un support pour chaque valeur de chaque variable, mais ceci impose d’être capable de calculer des supports spécifiques. Les propagateurs de contraintes dans Gecode sont spécifiés par des algorithmes dédiés qui effectuent seulement de la propagation, et ne proposent aucun moyen de répondre simplement à une telle question.
De plus, pour des variables tels que les entiers, dont le domaine peut être vaste, et qui sont représentées par des intervalles, il serait préférable que le propagateur soit capable de déterminer des intervalles de supports valides afin de rendre l’approche viable.
Une autre approche pour gérer la disjonction consiste à utiliser des contraintes réifiées. Cette approche introduit un niveau d’indirection en reliant le fait qu’une contrainte est satisfaite à une variable booléenne b. Si la contrainte est satisfaite, alors b doit être positionnée à vrai. Si elle n’est pas satisfaite, alors b doit être positionnée à faux. Inversement, si b est positionnée à vrai, alors la contrainte doit être satisfaite, ce qui consiste à simplement propager la contrainte. En revanche, si b est positionnée à faux, la négation de la contrainte doit être propagée. Ce niveau d’indirection offre une flexibilité, car il permet d’utiliser des propagateurs dédiés pour les contraintes réifiées, et un propagateur générique pour propager la disjonction.
Logiques temporelles
L’utilisation actuelle des logiques temporelles fait appel à de nombreuses notions, qu’il est aussi simple d’introduire sous la forme d’une chronologie. La présentation que nous donnons ici est une version condensée de la chronologie.
Les logiques temporelles ont longtemps été considérées comme un domaine distinct de la logique classique. Les concepts utilisés dans les logiques temporelles actuelles sont en particulier déjà présents dans (1952), mais le lien avec la logique classique ne sera établi que dans la thèse (1968), où il y est en particulier fait état que la logique temporelle linéaire est équivalente à la logique du premier ordre sur la structure N =< , avec une transformation linéaire de la première vers la seconde, mais une transformation exponentielle de la seconde vers la première.
Parallèlement, le lien entre logique sur les entiers naturels et automates a été établi dans (1960) pour les mots finis, puis étendu aux mots infinis (1962), ainsi que dans un foisonnement de publications contemporaines de celles-ci, dont les références se trouvent dans. L’équivalence entre logique sur les entiers naturels et automates nécessite l’introduction de la notion de structure de mot.
Programmation par contraintes sur horizon borné
La résolution de problèmes de planification par les techniques de satisfaction propositionnelle ou de programmation par contraintes est connue . Le principe consiste à encoder le problème sur un horizon fini puis utiliser un solveur pour rechercher un chemin satisfaisant les contraintes de transition et menant à un état but. Le procédé est réitéré sur des horizons de plus en plus grands jusqu’à ce qu’une solution soit trouvée ou que la taille du problème dépasse les capacités du solveur. Cette approche permet d’inclure facilement des contraintes temporelles diverses ainsi que des contraintes d’optimisation, tout en s’améliorant naturellement via l’amélioration des techniques de satisfaction et de programmation par contraintes.
Un problème comportant des contraintes temporelles est généralement représentable par un système de transitions dont les séquences d’états doivent satisfaire des conditions spécifiées. Un état correspond à un ensemble de variables, qui sont dupliquées pour chaque instant considéré dans le problème. La longueur de la séquence est l’horizon du problème. Nous distinguons les horizons finis/bornés, les horizons non bornés, et les horizons infinis.
Dans le cas d’un horizon fini ou borné, l’approche de résolution par CSP est complète. Un exemple de CSP à horizon fini est celui qui permet la génération d’un emploi du temps. Les problèmes d’ordonnancement avec capacités sont généralement des problèmes d’optimisation dans lesquels la borne supérieure de l’horizon est la somme de la durée maximale de chaque tâche, et pour lesquels l’objectif consiste à minimiser la durée nécessaire à la réalisation de toutes les tâches. Les problèmes de planification sont des problèmes à horizon non borné, dans le sens où la longueur maximale de la séquence est tellement grande qu’il est équivalent de considérer qu’elle est finie mais inconnue. En conséquence, l’absence de solution sur un horizon donné n’implique pas que le problème n’admet pas de solution.
Synthèse de contrôleur
La problématique principale de la théorie du contrôle discret est la conception de contrôleur pour des systèmes à évènements discrets, pour lesquels le contrôleur doit garantir qu’un système se comporte en respectant des propriétés spécifiées. Le problème est par conséquent très apparenté au problème du modèle checking, mais la différence principale est que le problème de décision est ici remplacé par le problème de synthèse d’une restriction d’un système qui satisfait des propriétés données. Une approche consiste à spécifier séparément le système, le contrôleur et les propriétés qui doivent être satisfaites, puis à vérifier que le système contrôlé satisfait bien les propriétés. Le problème de synthèse de contrôleur consiste à considérer les propriétés à vérifier directement comme une spécification du contrôleur, et de s’en servir pour générer un contrôleur valide par construction. Ceci permet de garantir que les propriétés spécifiées seront vérifiées par construction, ou de détecter que le système donné n’est pas contrôlable. Dans le second cas, il est alors facile de modifier les spécifications ou le système pour obtenir rapidement le système contrôlé correspondant. Comme ils existe plusieurs contrôleurs pour un même système, le problème de la synthèse de contrôleur correspond à un problème d’optimisation si l’on souhaite par exemple minimiser la taille du contrôleur produit.
Table des matières
1 Introduction
I État de l’art
2 Notations et définitions préliminaires
2.1 Ensembles, tuples, séquences
2.1.1 Ensembles
2.1.2 Tuple
2.1.3 Séquence
2.2 Graphes orientés
2.2.1 Composantes fortement connexes
2.2.2 Opérations de modification sur les graphes
2.3 Automates
2.4 Formules logiques
2.5 Considérations algorithmiques
3 Programmation par contraintes
3.1 Introduction
3.2 Définitions
3.3 Recherche en profondeur
3.3.1 Arbre de recherche
3.3.2 Modification de domaines
3.3.3 Algorithme
3.4 Consistences locales et propagateurs
3.4.1 Consistance d’arc
3.4.2 Consistances aux bornes
3.4.3 Algorithme
3.5 Optimisation
3.6 Exemple
3.6.1 Formulation
3.6.2 Modélisation
3.7 Formalismes apparentés
3.7.1 Programmation linéaire
3.7.2 Programmation entière
3.7.3 Programmation logique par contraintes
3.8 Conclusion
4 Logiques temporelles
4.1 Introduction
4.2 Logiques classiques
4.2.1 Logique propositionnelle
4.2.2 Problème de vérification et problème de satisfaction
4.2.3 Problème de synthèse
4.2.4 Logiques du premier ordre
4.2.5 Logique propositionnelle quantifiée
4.2.6 Logique du second ordre
4.3 Logiques temporelles
4.4 Logique temporelle linéaire
4.4.1 Syntaxe et sémantique
4.4.2 Automate de Büchi généralisé arborescent
4.4.3 Algorithme
4.4.4 Exemple
4.5 Autres logiques
4.6 Conclusion
5 Formalismes apparentés
5.1 Planification
5.2 Programmation par contraintes sur horizon borné
5.3 Logiques temporelles concrètes
5.4 Optimisation
5.5 Equations sur les séquences infinies
5.6 Synthèse de contrôleur
5.7 Conclusion
II Contributions
6 StCSPs
6.1 Hypothèses de travail
6.2 StCSPs
6.3 Représentation de solutions
6.4 Contraintes de voisinages
7 Résolution
7.1 Première méthode
7.1.1 Réduction de temporalité
7.1.2 Système de transitions associé à un StCSP de temporalité1
7.1.3 Algorithme
7.2 Deuxième méthode
7.3 Discussion
8 Exemples
8.1 Feux de signalisation
8.1.1 Modélisation
8.1.2 Résolution
8.1.3 Discussion
8.2 Problème d’ordonnancement d’une chaîne de production automobile
8.2.1 Modélisation
8.2.2 Comparaison avec la version PPC du problème
8.2.3 Adapation de la contrainte de cardinalité
8.3 Sudoku glissant
9 StCSPs et logiques temporelles
9.1 Transformation d’un StCSP en spécification LTL
9.1.1 Exemple
9.2 Pistes pour la généralisation
10 Conclusion
Bibliographie
