Cette étude, qui vise donc à décrire en logique les comportements des programmes, soulève immédiatement deux problèmes : il faut tout d'abord disposer d'un modèle mathématique de la notion de programmes puis comprendre quel modèle de comportements est induit par ce modèle de programmes. Cette distinction est d'autant plus cruciale qu'en général les programmes sont finis alors que les comportements, souvent, ne le sont pas.

Un modèle de programmes, aussi vieux que l'informatique mais dont la pertinence, comme l'illustre Arnold (Système de transitions finis, Etude et Recherche en Informatique, Masson), semble loin d'être épuisée, est le modèle des systèmes de transitions.

Intuitivement, un système de transitions se compose d'un ensemble d' états : représentant les diverses images mémoires possibles du programme, d'un état initial et d'un ensemble d'arcs entre ces états, appelées transitions, représentant les effets possibles de l'exécution d'une action à partir de tel ou tel état du programme.

Théoriquement, il est possible de modéliser tout ordinateur à l'aide d'un système de transitions. En pratique cependant, une telle modélisation est irréalisable. Le nombre d'états nécessaire à une telle modélisation est en effet exponentiel en la taille de la mémoire de l'ordinateur !

Un premier remède face à cette explosion combinatoire consiste à ne conserver que certains aspects de l'image mémoire du programme à modéliser. Autrement dit, on peut faire abstraction d'une partie de l'information contenue dans la mémoire de l'ordinateur à un instant donné.

En général, cette approche introduit du non-déterminisme, c'est-à-dire, à partir d'un certain état du système, la possibilité d'exécuter de plusieurs façons une même action. En effet, même si l'ordinateur sous-jacent est déterministe, l'information partielle que modélise un état peut être insuffisante pour être déterminante.

Ayant donc retenu les systèmes de transitions comme modèles de programmes, la notion, sous-jacente, de comportement reste à définir. Plus précisément : étant donné un système de transitions S, quelle notion de comportement C(S) doit-on associer au programme modélisé par S ?

En premier lieu, on souhaite ne pas tenir compte de l'éventuelle réutilisation de la mémoire. Or dans les systèmes de transitions, chaque circuit modélise précisément une telle réutilisation. La notion de développement d'un système, c'est à dire l' arbre de transitions obtenu en construisant les chemins issus de l'état initial, s'impose ici comme premier modèle de comportements.

En second lieu, la présence de non-déterminisme peut conduire à ne pas faire de différence entre deux états à partir desquels les exécutions des mêmes actions conduisent à des états décrivant les mêmes comportements. Dans cette approche, dupliquer les sous-arbres du développement d'un système de transitions ne doit pas modifier le comportement modélisé. La notion d' a-expansion d'un système, c'est à dire l' arbre de transitions obtenu en dupliquant a fois tout sous-arbres du développement de ce système, s'impose ici comme second modèle de comportements.

Les travaux de Castellani \cite{castellani} montre que cette notion caractérise l'équivalence de bisimulation de Park \cite{park} au sens où, pour tout système de transition S1 et S2 de cardinalité au plus a, l'existence d'une relation de bisimulation entre les états initiaux de S1 et S2 équivaut à l'existence d'une a-expansion commune aux système S1 et S2. Autrement dit, la notion d'a-expansion d'un système permet d'associer à tout système de cardinalité au plus a un représentant canonique et arborescent de sa classe d'équivalence par bisimulation.

On dispose alors d'un modèle de programmes et d'un modèle de comportement associé à ces programmes. La spécification comportementale d'un programme est alors définie comme une propriété logique de comportement.

Un candidat naturel de logique pour ces spécifications comportementales est la logique monadique du second ordre.

Elle est en effet suffisamment expressive pour spécifier des comportements limites, à l'infini, tels que ceux traitant du problème de l'équité. Elle est aussi suffisamment restreinte pour rester décidable : étant donnée une spécification de comportement exprimée en logique monadique du second ordre, on est capable de tester en un temps fini la cohérence de cette spécification, c'est-à-dire savoir si elle admet au moins un modèle.

Cependant les modèles de comportements peuvent être infinis. La construction explicite d'un modèle d'une spécification comportementale est donc exclue. Au mieux, peut-on espérer construire un système de transitions dont le comportement associé soit effectivement un modèle de la spécification.

D'un point de vue logique, cela soulève le problème suivant : étant donnée une spécification comportementale $\phi$, existe-t-il une formule $C^{-1}(\phi)$ telle que, pour tout comportement C(S) de système de transitions S, affirmer que C(S) est un modèle de $\phi$ équivaut à dire que S est un modèle de $C^{-1}(\phi)$ ? Ce problème a été résolue par Courcelle et Walukiewicz \cite{courc:igw:95} lorsque C(S) est définie comme le développement de S.

Nous traitons dans ce mémoire le cas où le comportement d'un système est l'$\omega$-expansion de ce système.

L'outils logique qui s'impose dans ce cas là est le $\mu$-calcul modal, un calcul de point fixe définie par Kozen \cite{kozen:83}.

Du point de vue comportementale, ce calcul a en effet la propriété remarquable que pour toute formule $\phi$, tout système de transitions S, en notant à nouveau C(S) l'$\alpha$-expansion de S, affirmer que C(S) est un modèle de $\phi$ équivaut à affirmer que S est un modèle de $\phi$. Autrement dit, la sémantique de ces formules est closes par équivalence de bisimulation.

Nous démontrons dans ce mémoire non seulement l'existence, pour toute formule $\phi$ de la logique monadique du second ordre, d'une formule $C^{-1}(\phi)$ satisfaisant les propriétés ci-dessus, mais nous démontrons aussi que l'ensemble des formules logiques décrit par $C^{-1}(\phi)$ lorsque $\phi$ décrit l'ensemble des formules de logique monadique du second ordre est équivalent, d'un point de vue sémantique, à l'ensemble des formules du $\m$-calcul modal.