Systèmes probabilistes : modèles, vérification et simulation
41
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
41
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
Syst`emes probabilistes Syst`emes temporis´es Propri´et´es V´erification Statistique
Syst`emes probabilistes :
mod`eles, v´erification et simulation
Marie Duflot-Kremer
pr´esentation bas´ee sur un travail en collaboration avec
Paolo Ballarini, Hilal Djafri, Serge Haddad et Nihal Pekergin
Travail partiellement financ´e par le projet ANR Checkbound
18 octobre 2010
Marie Duflot-Kremer Syst`emes probabilistes : mod`eles, v´erification et simulation 1 / 31 Syst`emes probabilistes Syst`emes temporis´es Propri´et´es V´erification Statistique
Syst`emes probabilistes
Syst`emes temporis´es
Propri´et´es
V´erification Statistique
Marie Duflot-Kremer Syst`emes probabilistes : mod`eles, v´erification et simulation 2 / 31 Syst`emes probabilistes Syst`emes temporis´es Propri´et´es V´erification Statistique
Pourquoi utiliser des probabilit´es?
• Certains syst`emes sont probabilistes.
• Environnement probabiliste.
• Syst`eme bas´e sur un algorithme probabiliste
• Approximation probabiliste d’un syst`eme.
• On ne connait pas pr´ecis´ement l’environnement - on
l’approxime par un comportement probabiliste.
• Abstractions probabilistes pour des syst`emes d´eterministes.
[LLM+02]
• Apporter une solution aux probl`emes n’ayant pas de solution
d´eterministe. [DFP02,DKNP04]
Marie Duflot-Kremer Syst`emes probabilistes : mod`eles, v´erification et simulation 3 / 31 1/4
1
Syst`emes probabilistes Syst`emes temporis´es Propri´et´es V´erification Statistique
Syst`emes probabilistes par nature
• Lancer de d´e, de ...
Voir
Syst`emes probabilistes :
mod`eles, v´erification et simulation
Marie Duflot-Kremer
pr´esentation bas´ee sur un travail en collaboration avec
Paolo Ballarini, Hilal Djafri, Serge Haddad et Nihal Pekergin
Travail partiellement financ´e par le projet ANR Checkbound
18 octobre 2010
Marie Duflot-Kremer Syst`emes probabilistes : mod`eles, v´erification et simulation 1 / 31 Syst`emes probabilistes Syst`emes temporis´es Propri´et´es V´erification Statistique
Syst`emes probabilistes
Syst`emes temporis´es
Propri´et´es
V´erification Statistique
Marie Duflot-Kremer Syst`emes probabilistes : mod`eles, v´erification et simulation 2 / 31 Syst`emes probabilistes Syst`emes temporis´es Propri´et´es V´erification Statistique
Pourquoi utiliser des probabilit´es?
• Certains syst`emes sont probabilistes.
• Environnement probabiliste.
• Syst`eme bas´e sur un algorithme probabiliste
• Approximation probabiliste d’un syst`eme.
• On ne connait pas pr´ecis´ement l’environnement - on
l’approxime par un comportement probabiliste.
• Abstractions probabilistes pour des syst`emes d´eterministes.
[LLM+02]
• Apporter une solution aux probl`emes n’ayant pas de solution
d´eterministe. [DFP02,DKNP04]
Marie Duflot-Kremer Syst`emes probabilistes : mod`eles, v´erification et simulation 3 / 31 1/4
1
Syst`emes probabilistes Syst`emes temporis´es Propri´et´es V´erification Statistique
Syst`emes probabilistes par nature
• Lancer de d´e, de ...
Syst`emesprobabilistes
Marie Duflot-Kremer
Syst`emestemporis´es
Proprie´te´s
Syste`mesprobabilistes: mod`eles,v´erificationetsimulation
Marie
Duflot-Kremer
p´tationbase´esuruntravailencollaborationavec resen Paolo Ballarini, Hilal Djafri, Serge Haddad et Nihal Pekergin Travailpartiellementfinanc´eparleprojetANRCheckbound
18
octobre
Syst` probabilistes : emes
2010
mod`eles,ve´rificationetsimulation
Ve´rificationStatistique
1 / 31
temporise´s
Syste`mes
Propri´etes ´
2 / 31
Marie Duflot-Kremer
Syste`mestemporise´s
probabilistes
Syst`emes
V´erificationStatistique
Proprie´tes ´
Statistique
Verification ´
Syste`mesprobabilistes:
mod`ele´ificationetsimulation s, ver
Syst`emesprobabilistes
Syste`mesprobabilistes
•
•
•
Syst`estemporise´s em
Propri´et´es
Pourquoiutiliserdesprobabilit´es?
Certainssyst`emessontprobabilistes. •Environnement probabiliste.
•lligsotreithme´persoubraubnia`tmebesaSsy
Approximationprobabilisted’unsyst`eme. •mentis´er´ecpaspne-tnnmeivor’lneonnocetiannnO l’approxime par un comportement probabiliste.
V´erificationStatistique
•et.sbAtsractionsprobabiletsiuopssedrtsysme`e´esdrmteisin [LLM+02]
Apporterunesolutionauxproble`mesn’ayantpasdesolution d´eterministe.40PN]0PFDKD,2[
Marie Duflot-Kremer
Syste`mesprobabilistes:
mod`eles,ve´rificationetsimulation
3 / 31
Syste`mesprobabilistes
•
•
Init
Syst`emestemporise´s
Proprie´te´s
Systemes probabilistes par nature `
Lancerdede´,depi`,tirageale´atoire. ece
V´erificationStatistique
Pourchaqueexpe´rience,onpeutd´eterminerlaprobabilit´e d’un´eve´nement.
Marie Duflot-Kremer
1/2
PP
PF
FF
Jeudepi`ece: •tuevtuotelse`ipsesec`aOn pile •enclareonpAetaa´qecuhe les “f ” ace Calculerlaprobabilit´e •de gagner en deux coups •de finir par gagner •ou d’autres choses beaucoup plu pliq ´ s com uees
Syst`emesprobabilistes:mode`les,ve´rificationetsimulation
4 / 31
Syste`mesprobabilistes
Syste`mestemporis´es
Proprie´t´ es
Approximations probabilistes
Canaux avec pertes
Un canal de communication qui peut perdre des messages Mode´lisationprobabilistedespertes
Ve´rificationStatistique
Etudedecommunicationssurunre´seau On veut savoir le temps moyen de transmission d’un message Onabesoinderepr´esenterlefluxdemessagescirculantsurle ´ reseau Utilisationd’unmod`eleprobabilistepourrepr´esenterlalongueuret lafr´equencedesmessages.
Marie Duflot-Kremer
Syst` es probabilistes : em
mod`eles,ve´rificationetsimulation
5 / 31
Syste`mesprobabilistes
Syste`mestemporises ´
Probabilit´es
pour
Propri´t´s e e
acc´l´erer e
V´erificationStatistique
Un exemple : le Quicksort •iniste:eVoisre´dnmret •Prendreldereinree´´lmene)tovip=(t •lpsulssetiuo)sullusesppts(rpetiertteM`epr.aspret(anav grands) •tnuadxueruisevembleauxxsous-tailppreuqAmethecr´all’rigo formes. ´ •En moyenne :O(n!log(n)) •Pri:)eaulei´trasecab(tO(n2) •Version probabiliste : •otri´laeegarlenaM´gla’lreuqilppasipuauleabettlenemo ci-dessus •ranceEpse´O(n!log(nr´ntee))leuquqeliosee’lt
Marie Duflot-Kremer
Syste`mesprobabilistes:
mode`les,ve´rificationetsimulation
6 / 31
Systemes probabilistes `
• • •
Syst`emestemporis´es
Propri´ete´s
Cas probabiliste plus simple
Ve´rificationStatistique
Automates communicants Onconsid`eredescanauxavecperte Nombreusesquestionsinde´cidables(accessibilite´re´pe´te´e...)
Avecprobabilite´s: •tilie´essageauneprobabCahuqme!urdhaacequdteˆ’eper ` ´t e e ap •”t´e1bilirobapreselifierv´Onpceva“se´te´irpo •Laedivitnofiiac´vrebldaetdenci´e[BS03].
Marie Duflot-Kremer
Syst`emesprobabilistes:
modeles,ve´rificationetsimulation `
7 / 31
Syste`mesprobabilistes
•
•
•
Syste`mestemporise´s
Propri´et´es
Solutions probabilistes
Certainsproble`mesn’ontpasdesolutiond´eterministe
V´erificationStatistique
Silaconfigurationded´epartestsyme´trique,onnepeut romprelasyme´trie
Besoind’unalgorithmeprobabilistepourromprelasyme´trie.
Exemple : Protocole CSMA/CD
[DFH+05]
mm n reseau • ´Co unicatio •Collision de messages possible •tentediialeta’drisi´dnundoihoecesB!drerue´ivet´erentpo nouvelles collisions •Choix probabiliste du temps d’attente.
Marie Duflot-Kremer
Syste`mesprobabilistes:mod`eles,ve´rificationetsimulation
8 / 31
Syst`emesprobabilistes
• • •
Syste`mestemporis´es
Sy t`mes probabilistes s e
en
Proprie´t´ es
temps
Ve´rificationStatistique
continu
Temps discret : limitation Besoind’unemode´lisationplusfine Exemple : distribution exponentielles •Un taux"ahcruop´seeopirntemitioransquet •satate`rp´ett´el’oiavuirqab’dPortnue´ti:1sdetemps"e!!t •Le temps moyen avant de prendre cette transition est 1/" •noitpmoctsidubirunechaecibatavlekrvoedaMıˆen
Marie Duflot-Kremer
Syste`mesprobabilistes:
mod`l ´rification et simulation e es, ve
9 / 31
Syste`mesprobabilistes
• •
Syste`mestemporise´s
Propri´et´es
e agee Syst`emedme´moirepart´
Request1
Access1
Free
V´erificationStatistique
Request2
Access2
Deux files de processus, une seule memoire ´ Unseulprocessuspeutacce´dera`lam´emoireenmeˆmetemps
Marie Duflot-Kremer
Syste`mesprobabilistes:modeles,v´erificationetsimulation `
10 / 31
