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.
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.