Oméga-Algèbre. Théorie et application en vérification de programmes

by Bolduc, Claude

L’algèbre de Kleene est la théorie algébrique des automates finis et des expressions régulières. Récemment, Kozen a proposé un cadre de travail basé sur l’algèbre de Kleene avec tests

(une variante de l’algèbre de Kleene) pour vérifier qu’un programme satisfait une politique

de sécurité spécifiée par un automate de sécurité. Malheureusement, cette approche ne permet

pas de vérifier des propriétés de vivacité pour les programmes réactifs (programmes qui

s’exécutent à l’infini). Le but de ce mémoire est d’étendre la méthode de vérification de programmes

proposée par Kozen pour enlever cette limitation. Pour y arriver, nous développons

la théorie de l’oméga-algèbre (une extension de l’algèbre de Kleene qui prend en compte

les exécutions infinies) qui constitue la majeure partie de ce mémoire. En particulier, nous

présentons des résultats de complétude concernant la théorie de Horn de cette algèbre. Inscrit au Tableau d'honneur de la Faculté des études supérieures