Construction du système de transitions probabiliste correspondant à une machine probabiliste

Télécharger le fichier pdf d’un mémoire de fin d’études

Cohérence d’un modèle B évenementiel

La validation d’un modèle B événementiel nécessite de démontrer des obligations de preuve[17]. Les obligations de preuve sont des formules mathématiques qu’il faut démontrer pour prouver qu’un modèle B événementiel est correct.
Une obligation de preuve est construite d’un ensemble d’hypothèses et d’un but. Démontrer une obligation de preuve revient à montrer que le but peut être établi à partir des hypothèses. Plusieurs sortes d’obligations de preuve sont à considérer en B événementiel : celles liées à la preuve de correction des expressions, celles liées à la preuve de correction des machines et celles liées à la preuve de correction de raffinement. Dans un processus de spécification d’un système en B événementiel, les obligations de preuve sont générées d’une façon automatique par l’outil utilisé pour la spécification, et déchargées (en partie ou automatiquement) à l’aide des prouveurs associés à l’outil de spécification. Dans ce qui suit, nous détaillons les types d’obligations de preuve utilisés en B événementiel.

Correction des expressions

L’objectif de ces obligations de preuve est de s’assurer que chaque expression utilisée dans une machine ou un contexte B événementiel est correcte et bien définie. Cette expression peut être un axiome, un variant, une garde, une action, un invariant… Ces expressions peuvent être dépourvues de sens si elles ne sont pas bien définies.
Supposons que nous ayons une expression contenant l’opérateur mathématique card appliqué sur un ensemble S. Nous rappelons que l’opérateur mathématique card retourne le nombre d’élé-ments contenus dans un ensemble fini. Pour assurer que cette expression est bien définie, il faut entre autre s’assurer que l’ensemble S est fini. Nous devons donc vérifier que f inite(S) est satis-fait où f inite est un opérateur mathématique qui s’applique sur un ensemble d’éléments et qui retourne vrai lorsque l’ensemble est fini et faux dans le cas contraire.

Obligations de preuve de machine

Concernant la dynamique d’une machine, nous dirons qu’une machine satisfait une obligation de preuve si tous ses événements satisfont cette obligation de preuve. Nous détaillons dans ce qui suit les différentes obligations de preuve.
Faisabilité des événements L’objectif de cette obligation de preuve est de s’assurer que l’action de chaque événement est applicable. Rappelons que l’action d’un événement est définie par un prédicat avant-après qui décrit la relation entre la valeur des variables avant (v¯) et après (v¯’) l’occurrence de l’action. L’objectif de cette obligation est de s’assurer pour chaque événement qu’il existe au moins une valuation des variables v¯’ obtenue après son exécution telle que le prédicat avant-après est satisfait. Démontrer la faisabilité d’une action d’un événement consiste à démontrer
la faisabilité de toutes les substitutions constituant cette action.

Raffinement

D’une façon générale, le raffinement est un processus qui permet l’enrichissement ou la modifica-tion d’une spécification par l’ajout de nouvelles fonctionnalités ou par l’ajout de nouveaux détails aux fonctionnalités décrites dans la spécification initiale. Comme nous l’avons précisé dans la sec-tion 2.1, le processus de développement en B événementiel est basé sur le raffinement.
Le concept de raffinement a été introduit initialement dans les années 1970 par Dijkstra . Il a été ensuite formalisé par Back[23, 24] dans les années 1980. Depuis ce moment, plusieurs travaux de recherche ont étudié ce concept. Nous citons à titre d’exemples, les travaux de Abadi et Lamport[13], Back[26], Morgan[77], Morris[80] et Abrial[16].

Raffinement en B événementiel

Le raffinement en B événementiel consiste en l’extension des contextes et le raffinement des ma-chines. L’extension du contexte consiste en l’ajout de nouveaux éléments statiques : ensembles, constantes, axiomes… Le raffinement de machine permet de décrire d’une manière progressive le comportement dynamique du système. Il consiste à transformer une machine abstraite en une ma-chine plus concrète par l’ajout de nouveaux éléments, ce qui rapproche d’une implantation par un langage de programmation.
Le raffinement offre plusieurs avantages. D’abord, il permet le partage de la complexité de dé-veloppement formel : au lieu de spécifier un modèle global contenant tous les artefacts du système, le raffinement permet l’introduction progressive du comportement du système. Cela permet la prise en compte de tous les aspects du système et facilite la compréhension du modèle. D’un autre côté, il permet aussi la simplification de la preuve de correction des machines B événementiel et la réutilisation des propriétés déjà prouvées.

Convergence des nouveaux événements

Comme mentionné précédemment, une opération importante du raffinement des machines en B événementiel consiste en l’ajout de nouveaux événements. Cette opération permet la description de nouveaux comportements. Cependant, afin de préserver certaines propriétés de la machine abstraite dans laquelle nous introduisons les événements, il faut s’assurer que leur introduction ne contredit pas le comportement de la machine abstraite. Pour cela, il faut prouver que les nouveaux événements ajoutés ne prennent pas le contrôle de la machine concrète indéfiniment. Pour cela, une solution est de proposer un variant, et de prouver que l’action de chaque nouvel événement décroît la valeur de ce variant. Ainsi, on montrera bien que les nouveaux événements finiront par terminer. Cela est formalisée par deux obligations de preuve : la première veille à ce que le variant proposé soit bien un entier positif minoré par zéro. La deuxième obligation assure que chaque nouvel événement décroît le variant. Nous présentons dans ce qui suit ces deux obligations de preuve.
Variant minoré L’objectif de cette obligation de preuve est de s’assurer que sous l’invariant et la garde de chaque nouvel événement, le variant est bien un entier naturel strictement positif, c’est-à-dire minoré par 0. Pour un nouvel événement ec , cette obligation de preuve est présentée formellement comme suit.

Étude de cas : Protocole Pair à Pair

Pour illustrer la méthode B événementiel, nous spécifions un protocole pair à pair inspiré de celui de Bittorent [4]. Une description complète de ce protocole est présentée dans [8]. Ce cas d’étude comporte N clients qui essayent de télécharger un fichier partitionné en K blocs. Nous notons que N et K sont strictement supérieurs à zéro. Initialement, aucun client n’a encore téléchargé aucun bloc. Le protocole se termine lorsque tous les clients ont réussi à télécharger tous les blocs du fichier. La figure 2.5 illustre le principe général du protocole.

Stratégie du développement du protocole en B événementiel

Nous rappelons que le processus de développement en B événementiel est basé sur le raffinement. Ainsi, nous utilisons le raffinement pour une description progressive du protocole. Dans cette partie, nous expliquons notre stratégie de raffinement. Dans la figure 2.6, nous présentons la stratégie du développement du protocole en B événementiel. Nous créons un premier contexte protocole1 et une première machine P2P1 qui utilise les éléments de ce contexte. Dans cette machine, nous spé-cifions l’objectif global du protocole sans spécifier le détail. Nous étendons le contexte protocole1 obtenant ainsi le contexte protocole2 et nous raffinons la première machine P2P1 obtenant ainsi la machine P2P2. Dans cette machine, nous détaillons le téléchargement d’un bloc par un client. Nous raffinons la machine P2P2 obtenant ainsi la machine P2P3. Dans cette machine, nous spécifions les cas d’erreurs qui peuvent arriver durant le téléchargement d’un bloc par un client. Nous allons montrer que l’étape de raffinement de P2P2 par P2P3 n’est pas correcte.

La première machine

Le protocole décrit le téléchargement d’un fichier partitionné en K blocs par un ensemble de N clients. Ainsi, nous avons besoin de deux constantes, N pour dénoter le nombre de clients et K pour dénoter le nombre de blocs. De même, nous avons besoin de constantes pour décrire l’état d’un bloc par rapport à un client, c’est-à-dire si ce client a réussi à télécharger ce bloc ou si ce n’est pas encore le cas. Tous les éléments de ce contexte sont stockés dans le contexte protocole présenté dans la figure 2.7.
La première machine présentée dans la figure 2.7 permet de spécifier l’objectif général du pro- tocole d’une manière très abstraite. Dans cette machine, l’état du système est décrit par une seule variable DB. DB est une matrice qui indique pour chaque client c ∈ 1..N et chaque bloc k ∈ 1..K si le client c a réussi à télécharger ce bloc (DB(c 7→k)=finished) ou si ce n’est pas encore le cas (DB(c 7→k)=empty). Initialement, aucun client n’a encore téléchargé aucun bloc. Cette machine contient un seul événement : AIIDL. Cet événement modélise le téléchargement de tous les blocs
par tous les clients, il agit sur la variable DB, cette dernière prend une nouvelle valeur telle que pour tous les clients c ∈ 1..N et pour tous les blocs k ∈ 1..K nous avons DB(c 7→k)=finished.

Troisième machine

À ce niveau de raffinement, nous prenons en compte certaines erreurs qui peuvent arriver durant le téléchargement d’un bloc par un client :
• l’interruption du téléchargement ;
• l’impossibilité du téléchargement du bloc à un instant donné.
Afin de formaliser ces deux erreurs, nous introduisons par raffinement un nouvel événement FailureDL. Cet événement est présenté dans la figure 2.10. Cet événement choisit un client c et un bloc b tel que le client c a commencé le téléchargement du bloc b (DBin(c 7→b)=incoming). L’action de cet événement choisit d’une façon non-déterministe empty ou incoming pour être affecté à DBin(c7→b). empty est choisi dans le cas où l’erreur interrompt le processus de téléchargement du bloc alors que incoming est choisi dans le cas où l’erreur bloque le téléchargement.
Cet événement a la même garde que l’événement Finish1DL. Ils peuvent etre activés en même temps, le choix entre ces deux événements est non-déterministe. Puisque FailureDL est un nouvel événement introduit par raffinement, nous devons prouver sa convergence. Autrement, nous de-vons prouver que son action décroît la valeur du variant. Nous rappelons que le variant de cette machine P2P3 est donné par : 2 × N × K − 2 × card({c7→b | c ∈ 1..N ∧ b ∈ 1..K ∧ DBin(c7→b) = finished}) − card({c7→b | c ∈ 1..N ∧ b ∈ 1..K ∧ DBin(c7→b) = incoming})
Pour un client c et un bloc b telle que c est train de télécharger b (DBin(c7→b) = incoming), l’ac-tion de cet événement choisit d’une façon non-déterministe empty ou incoming pour être affecté à DBin(c7→b). Si empty est choisi, le nombre d’éléments de l’ensemble {c7→b |n∈1..N ∧ b ∈ 1..K ∧ DBin(c7→b) = incoming} va diminuer, ce qui augmente la valeur du va-riant. Si incoming est choisi, le nombre d’éléments de l’ensemble {c7→b |c ∈ 1..N ∧ b ∈ 1..K ∧ DBin(c 7→b) = incoming} reste intacte, et ainsi la valeur du variant n’est pas modifiée. Nous déduisons ainsi que l’événement FailureDL ne converge pas, et ainsi, le protocole ne termine pas dans cette version. Nous montrons dans la suite de ce manuscrit com-ment nous procédons pour faciliter la preuve de convergence de nouveaux événements introduits par raffinement.

Systèmes de transitions

Les systèmes de transitions constituent un formalisme classique permettant de modéliser le com-portement d’un système. Ce formalisme se base sur la notion d’états et de transitions. Les états sont typiquement les valeurs des variables du système et les transitions sont les actions permettant de modifier ces valeurs. Ce formalisme étant bien étudié, il est commun d’exprimer la sémantique d’autres modèles dans le cadre des sytèmes de transitions, c’est le cas par exemple pour le B événe-mentiel. Nous introduisons donc ci-après les définitions nécessaires dans ce cadre pour exprimer la sémantique opérationnelle de nos modèles en termes de systèmes de transitions (probabilistes).

Systèmes de transitions

Nous commençons par donner la définition d’un système de transitions.
Définition 1 (Système de transitions [28])
Un système de transitions est un tuple M = (S, S0, Acts, T ) avec :
• S un ensemble d’états,
• S0 ⊆ S un ensemble d’états initiaux,
• Acts un ensemble d’actions permettant d’étiqueter les transitions,
• T ⊆ S × Acts × S est une relation de transition.
Étant donnés deux états s, t et une action α, une transition (s, α, t) ∈ T qui permet de mener le système de l’état s vers l’état t et qui est effectuée par l’intermediaire de l’action α est notée α s → t. Un système de transitions peut être fini ou infini. On dira qu’il est fini s’il est à nombre d’états et de transitions finis, c’est-à-dire si les ensembles S et Acts sont finis. Autrement, on dira que le système est infini.
Un sytème de transitions peut être déterministe ou non-déterministe. Il est déterministe si la relation de transition est une fonction et non-déterministe dans le cas contraire, c’est-à-dire, pour un état donné, plusieurs transitions sortantes sont présentes. Le choix de la transition à exécuter au moment de l’exécution se fait d’une manière non-déterministe.

Systèmes de transitions et probabilités

Comme mentionné précédemment, certains systèmes de transitions permettent la présence du non-déterminisme.
Dans certains types de systèmes de transitions, les transitions sont pondérées par des proba-bilités. Ce type de système ne contient alors pas de non-déterminisme, puisque la distribution de probabilités est entièrement déterminée par l’état actuel du système. Ce type de systèmes de tran-sitions correspond au modèle de Larsen et Skou pour modéliser les systèmes probabilistes ayant un espace d’états fini. Ce modèle est appelé initialement “système probabiliste réactif” [95], puis “fully probabilistic” [27]. Récemment, il est nommé “chaîne de Markov à temps discret” [70].
D’autres modèles ont été proposés. Contrairement aux modèles initialement proposés par Lar-sen et Skou, ces modèles admettent plusieurs distributions de probabilités pour un même état de départ. À partir de cet état, un choix non-déterministe est effectué pour choisir une distribution de probabilité, une fois choisie, il y aura un choix probabiliste entre les états issus de cette distribu-tion. Dans la littérature, ces modèles sont appelés initialement “génératifs” [95], puis “probabilistes concurrents” [27] et récémment processus de décision Markovien ou Automates probabilistes [70]. Nous présentons dans ce qui suit les définitions de ces modèles en commençant par la notion la plus générale de systèmes de transitions probabilistes. Pour un ensemble donné S, nous déno-tons par Dist(S) l’ensemble des distributions de probabilité sur l’ensemble S, i.e. l’ensemble des fonctions δ : S → [0, 1] telles que Ps0∈S δ(s0) = 1. Nous dénotons aussi par Card(S) le cardinal de l’ensemble S, c’est-à-dire, le nombre d’éléments qui apparaissent dans cet ensemble.
Nous présentons maintenant la définition d’un système de transitions probabiliste.
Définition 2 (Système de transitions probabiliste [28])
Un système de transitions probabiliste est un tuple M = (S, s0, Acts, T ) avec :
• S un ensemble d’états,
• s0 ∈ S l’état initial,
• Acts l’ensemble des noms d’actions, et
• T ⊆ S × Acts × (S → [0, 1]) une relation de transition probabiliste.

Sémantique opérationnelle d’une machine B événementiel

La sémantique opérationnelle d’une machine M=(v¯,I(v¯),Evts, Init ) est donnée en termes de système de transitions M = (S, s0, Acts, T ) (adaptée de [32]). L’obtention de la sémantique est comme suit :
• Les états S correspondent aux valuations des variables de la machine. Considérons le cas où nous avons une machine M contenant n variables vi chacune ayant un domaine Di. S est alors formé par les valuations du n-uplet (v1,v2,…,vn) qui sont dans D1 × D2 × … × Dn ;
• L’état s0 correspond aux valuations des variables obtenues après l’exécution de l’événement d’initialisation Init ;
• Acts correspond à l’ensemble des noms des événements Evts de la machine M ;
• T ⊆ S × Acts × S est l’ensemble de transitions. Il correspond à l’ensemble des exécutions possibles des différentes événements de la machine M.
Afin de bien expliquer la construction de la sémantique d’une machine B événementiel, nous présentons dans ce qui suit la sémantique opérationnelle de la machine P2P2 présentée dans la section 2.5.
Sémantique opérationnelle de la machine P2P2 La figure 2.14 donne un extrait du système de transitions correspondant à la machine P2P2 pour N=2 et K=2. Dans cet extrait, les états représentent le contenu des variables de la machine. Pour les variables DBin et DB, les clients sont représentées en ligne et les blocs sont représentés en colonne. Le contenu des matrices est représenté par les symboles (.), (◦), (•) où (.) signifie que le client n’a pas encore commencé le téléchargement du bloc, (◦) signifie que le client a commencé le téléchargement du bloc et (•) signifie que le client a terminé le téléchargement du bloc.
Dans cette figure, v correspond à la valeur du variant dans chaque état du système. On pourra remarquer que la valeur de v décroît à chaque exécution d’un nouvel événement.

B Événementiel et probabilités

Comme présenté dès le début de ce manuscrit, le B événementiel n’introduit pas de concepts particuliers pour traiter les aspects probabilistes des systèmes. Ainsi, plusieurs travaux de recherche visant à marier B événementiel et probabilités ont été menés pour permettre la prise en compte des aspects probabilistes des systèmes en B événementiel.
À notre connaissance, le premier travail traitant de la problématique de l’ajout de probabilités au sein de B événementiel a été mené par Abrial et ses co-auteurs dans [78]. Dans cet article, les auteurs traitent les différentes possibilités pour intégrer des probabilités au sein de B événe-mentiel. Ils suggèrent d’introduire les probabilités comme raffinement du non-déterminisme en B événementiel. Nous rappelons que le non-déterminisme en B événementiel peut avoir lieu à dif-férents niveaux, comme dans le choix entre les événements activables dans le même état, dans le choix des valuations des paramètres d’un événement et dans les substitutions. Ce travail peut être considéré comme un ensemble de consignes ou de bonnes pratiques pour intégrer le raison-nement probabiliste en B événementiel. Les auteurs indiquent de plus que chaque extension de B événementiel pour supporter le raisonnement probabiliste doit respecter certaines exigences :
• Le B événementiel étendu doit rester simple et compréhensible ;
• Le B événementiel doit être générique, permettant ainsi la description d’une large classe de systèmes ;
• L’extension doit être facilement intégrable à la plateforme Rodin.
À notre connaissance, tous les travaux traitant l’intégration de probabilités dans le B événe-mentiel se sont contentés de remplacer les substitutions non-déterministes par des substitutions probabilistes. Les extensions probabilistes au B événementiel existantes gardent ainsi du non-déterminisme qui apparaît alors au niveau du choix de l’événement qui sera exécuté parmi les événements activables et au niveau du choix des valuations des paramètres d’un événement.
Extension qualitative Le deuxième travail visant à intégrer le raisonnement probabiliste en B événementiel a été proposé par Hallerstede et Hoang dans [54]. Dans cet article, les auteurs in-troduisent un nouveau type de raisonnement en B événementiel appelé Raisonnement probabiliste qualitatif.
Ils proposent une extension qualitative du B événementiel dans laquelle les substitutions non-déterministes sous forme de prédicat sont remplacées par des substitutions probabilistes dite qua-litatives. Les nouvelles substitutions s’écrivent de la façon suivante : ¯ 0 ) x :⊕ Qx(t,v,¯x,x.
Dans cette substitution, une variable x prend une nouvelle valeur x’ avec une valeur de proba-bilité qui n’est pas précisée mais qui doit être strictement positive.
Dans ce contexte, les auteurs étudient la convergence presque certaine d’un ensemble d’événe-ments contenant des substitutions probabilistes qualitatives. Ils formalisent des conditions néces-saires pour prouver la convergence presque certaine de cet ensemble par des obligations de preuve. Pour cela, ils adaptent les obligations de preuve de convergence classique du B événementiel et introduisent de nouvelles obligations de preuve. Nous rappelons qu’en B événementiel, prouver qu’un ensemble d’événements converge revient à prouver que chaque événement de cet ensemble remplit les obligations de preuve evt/var/NAT et event/VAR présentées dans la section 2.4.3.
En particulier, l’obligation de preuve event/VAR assure pour chaque événement convergent que toutes les valuations des variables qui sont obtenues après l’exécution de son action décroissent la valeur du variant. Hoang et Hallerstede allègent cette contrainte formalisée par event/VAR : pour chaque événement contenant des substitutions probabilistes, ils imposent qu’au moins une valuation des variables obtenue après l’exécution de son action décroît la valeur du variant. Ainsi, il n’est plus nécessaire de prouver que toutes les valuations des variables obtenues après l’exécu-tion de l’action de l’événement décroissent la valeur du variant, mais il suffit de trouver une seule valuation qui le fait décroitre. Cette condition est en effet suffisante à prouver que la probabilité de décroitre le variant est strictement positive. Pour un événement ei , l’adaptation de cette obligation de preuve est alors donnée par : evt/pVAR.

Table des matières

1 Introduction 
2 B événementiel et systèmes de transitions 
2.1 Introduction
2.2 Modèle B événementiel
2.2.1 Contexte
2.2.2 Machine
2.2.3 Événement
2.2.4 Substitution généralisée
2.3 Cohérence d’un modèle B évenementiel
2.3.1 Correction des expressions
2.3.2 Obligations de preuve de machine
2.4 Raffinement
2.4.1 Raffinement en B événementiel
2.4.2 Exactitude du raffinement
2.4.3 Convergence des nouveaux événements
2.5 Étude de cas : Protocole Pair à Pair
2.5.1 Stratégie du développement du protocole en B événementiel
2.5.2 La première machine
2.5.3 Deuxième machine
2.5.4 Troisième machine
2.6 Systèmes de transitions
2.6.1 Systèmes de transitions
2.6.2 Systèmes de transitions et probabilités
2.6.3 Sémantique opérationnelle d’une machine B événementiel
2.7 B Événementiel et probabilités
3 B événementiel probabiliste 
3.1 Introduction
3.2 Introduction des probabilités en B événementiel
3.2.1 Non-déterminisme en B événementiel : Exemple
3.2.2 Introduction des probabilités dans la machine Mch
3.3 B événementiel probabiliste
3.3.1 Choix de l’événement à exécuter
3.3.2 Choix uniforme des valeurs des paramètres
3.3.3 Les substitutions probabilistes
3.3.4 Machine B événementiel probabiliste
3.3.5 Étude de cas : protocole pair à pair en B événementiel probabiliste
3.4 Cohérence d’une machine B évenementiel probabiliste
3.4.1 Nouvelles obligations de preuve
3.4.2 Adaptation des obligations de preuve standard
3.4.3 Étude de cas : obligations de preuve appliquées au protocole pair à pair
3.5 Sémantique opérationnelle d’une machine B événementiel probabiliste
3.5.1 Notations
3.5.2 Construction du système de transitions probabiliste correspondant à une machine probabiliste
3.5.3 Sémantique opérationnelle exprimée en termes de chaîne de Markov discrète
3.5.4 Étude de cas : sémantique opérationnelle de la machine P2Pp du protocole pair à pair
4 B Événementiel mixte 
4.1 Introduction
4.2 Machine B événementiel mixte
4.2.1 Description
4.3 Cohérence d’une machine B événementiel mixte
4.3.1 Cas général
4.3.2 Cas des machines mixtes partielles
4.4 Sémantique opérationnelle d’une machine B événementiel mixte
4.4.1 Construction de la sémantique opérationnelle d’une machine B événementiel mixte
4.4.2 Exemples d’illustration
4.4.3 Sémantique opérationnelle
4.5 Etude de cas : protocole pair à pair
5 Raffinements probabilistes 
5.1 Introduction
5.2 Probabilisation
5.2.1 Obligations de preuve de faisabilité de la probabilisation
5.2.2 Automatisation du processus de probabilisation
5.2.3 Étude de cas
5.3 Introduction de nouveaux événements par raffinement
5.3.1 Convergence presque certaine en B événementiel dans la littérature
5.3.2 Convergence presque certaine dans notre proposition de B événementiel probabiliste
5.3.3 Étude de cas : convergence presque certaine dans le protocole P2P
5.4 Généralisation de l’introduction d’événements par raffinement
5.4.1 Ajout de nouveaux événements probabilistes au sein d’une machine B évé- nementiel standard ou mixte
5.4.2 Ajout d’événements standard dans une machine B événementiel mixte ou probabiliste
5.4.3 Ajout simultané d’événements standard et probabilistes
6 Études de cas 
6.1 Système d’atterrissage d’un avion
6.2 Stratégie de développement du train d’atterrissage en B événementiel
6.2.1 La première machine
6.2.2 La deuxième machine
6.3 Système de freinage
6.3.1 Stratégie du développement du système de freinage en B événementiel
6.3.2 La première machine
6.3.3 La deuxième machine
6.3.4 La troisième machine : version probabiliste
6.3.5 La quatrième machine
6.3.6 La cinquième machine
7 Extension de la plateforme Rodin 
7.1 Introduction
7.2 La plateforme Rodin
7.2.1 Architecture de Rodin
7.2.2 Processus de développement d’un modèle B événementiel dans Rodin
7.3 Intégration de notre extension probabiliste dans Rodin
7.3.1 Description de l’extension
8 Conclusion 

Télécharger le rapport complet