7 Jan 04: Introduction du cours. La vérification automatique. Ses limites. Besoin de considérer des modèles formels des systèmes. Un exemple de vérification formelle : le protocole du bit alterné.
Note : le protocole du bit alterné a été proposé dans [BSW69]. L'analyse présentée en cours est un calcul à la main basé sur des techniques automatisables que nous verrons dans un cours futur.
14 Jan 04: Un modèle formel : les systèmes communicants [BZ83]. Sémantique opérationnelle. Un Théorème de Rice pour les systèmes communicants. Le cas des systèmes non-fiables. Décidabilité de la terminaison basée sur le Lemme de Higman.
21 Jan 04: La terminaison et l'accessibilité sont décidables pour les systèmes communicants non-fiables. L'accessibilité répétée d'un état de contrôle est indécidable [AJ96b].
Note : la décidabilité de la terminaison est due à [Fin94] (preuve dans un cadre moins élégant mais équivalent à ce qui a été vu en cours). La décidabilité de l'accessibilité est due à [AJ96a]. L'indécidabilité de l'accessibilité répétée est due à [AJ96b] (preuve moins élégante que comme vu en cours).
28 Jan 04: La finitude (de l'ensemble des configurations atteignables) est indécidable pour les systèmes communicants non-fiables. Par conséquent, il n'existe pas de méthode permettant de calculer l'ensemble Post*(S) des configurations atteignables, même si on sait que cet ensemble est reconnaissable (= « régulier ») car fermé par sous-mots.
L'équivalence entre deux systèmes communicants non-fiables est indécidable, ceci pour toute notion d'équivalence comprise entre la bisimulation et l'égalité des langages de trace.Note : l'indécidabilité de la finitude est due à [May03]. Attention : sa preuve est plus générale que celle vue en cours. L'indécidabilité des équivalences comportementales est due à [Sch01].
4 Fév 04: Les beaux préordres (ou well-quasi-orders, ou WQO's). Définition. Liens entre WQO et WFO (ordre bien fondé). Lemmes de Dickson, de Higman. Des notes (sans les preuves) et des exos (sans les solutions) sont disponibles ici (en postscript).
11 Fév 04: Les réseaux de Petri, un modèle pour les systèmes concurrents. Définitions, comportement, une propriété de monotonie des transitions. Le modèle n'a pas la puissance des machines de Turing. L'accessibilité est décidable. La construction d'un arbre d'accessibilité fini permet de décider la terminaison, la finitude et l'inévitabilité d'une place.
Note : la décidabilité de l'accessibilité est due à Kosaraju [Kos82] et Mayr [May84]. Le livre [Reu89] est consacrée à une présentation détaillée d'une preuve de ce résultat fondamental.
18 Fév 04: Vacances de février -- pas de cours cette semaine.
25 Fév 04: Techniques de réductions entre problèmes sur les réseaux de Petri. On montre que les quatre problèmes suivants sont équivalents (c.-à-d. inter-réductibles) : l'accessibilité, l'accessibilité d'un sous-marquage (peut-on atteindre un marquage dont le contenu pour un certain ensemble de places soit fixés ?), l'accessibilité du marquage vide (peut-on vider le réseau de ses jetons ?), l'accessibilité d'un marquage où une place donnée est vide. Ils sont donc tous décidables (admis).
Par ailleurs, on montre l'indécidabilité du problème de savoir si deux réseaux donnés ont le même ensemble de marquages atteignables. La preuve enchaîne plusieurs réductions : le 10e problème de Hilbert se réduit au problème de savoir si le graphe G(P1) d'un polynômes P1 à coefficients positifs est inclus dans le graphe G(P2) d'un autre polynôme, sachant que pour un polynôme P à n variables, G(P) = {<x1,...,xn,y> | 0≤x1,...,xn & 0≤y≤P(x1,...,xn)}. Ce problème d'inclusion de graphes se ramène au problème de l'inclusion des ensembles d'accessibilité entre deux réseaux : on construit des réseaux de Petri qui calculent les valeurs y telles que 0≤y≤P(x1,...,xn). Ensuite il reste à réduire le problème d'inclusion d'ensembles d'accessibilité au problème d'égalité de ces ensembles.
Note : la preuve d'indécidabilité est due à M. O. Rabin (pour l'inclusion plutôt que l'égalité entre les ensembles d'accessibilité). Les autres réductions sont dues à M. Hack (cf. [Hac76]). Une preuve lisible de l'indécidabilité du 10e problème de Hilbert est disponible dans [Dav77].
3 Mar 04: Les systèmes de transitions bien-structurés sont des systèmes vérifiant une propriété de monotonie des transitions par rapport à un beau préordre entre les configurations (cf. [FS01]). Pour ces systèmes on peut montrer que la couvrabilité est décidable (si le beau préordre est décidable et si on dispose d'une fonction premin(s) effective pour calculer l'ensemble des configurations minimales permettant de couvrir une configuration s en un coup). On peut montrer que la finitude est décidable pour les systèmes bien-structurés en un sens strict (et si post(s) est effectif).
Ces résultats s'appliquent par exemple à des extensions monotones des réseaux de Petri : réseaux avec transferts, resets et doublements. NB : les réseaux avec resets ne sont pas bien-structurés au sens strict, et de fait leur finitude est indécidable [DJS99].
On notera que l'accessibilité n'est décidable pour aucune de ces extensions.
10 Mar 04: Les systèmes BPP (pour Basic Parallel Processes) sont des réseaux de Petri où les préconditions des transitions sont toujours réduites à un singleton. Ces systèmes ont un comportement à base de parallélisme avec récursivité (création/destruction de jetons) mais il n'y a pas de synchronisation entre des jetons coexistants. Un résultat positif important dans le domaine de la vérification d'équivalences entre systèmes infinis est dû à Christensen, Hirshfeld et Moller : la bisimilarité est décidable entre marquages d'un système BPP [CHM93].
17 Mar 04: Pas de cours cette semaine, profitez-en pour préparer l'examen.
24 Mar 04: Examen. Documents papiers autorisés.