Systèmes probabilistes : modèles, vérification et simulation
41 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Systèmes probabilistes : modèles, vérification et simulation

-

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
41 pages
Français

Description

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

Sujets

Informations

Publié par
Nombre de lectures 142
Langue Français

Exrait

Syst`emesprobabilistes
Marie Duflot-Kremer
Syst`emestemporis´es
Proprie´te´s
Syste`mesprobabilistes: mod`eles,v´ericationetsimulation
Marie
Duot-Kremer
p´tationbase´esuruntravailencollaborationavec resen Paolo Ballarini, Hilal Djafri, Serge Haddad et Nihal Pekergin Travailpartiellementnanc´eparleprojetANRCheckbound
18
octobre
Syst` probabilistes : emes
2010
mod`eles,ve´ricationetsimulation
Ve´ricationStatistique
1 / 31
temporise´s
Syste`mes
Propri´etes ´
2 / 31
Marie Duflot-Kremer
Syste`mestemporise´s
probabilistes
Syst`emes
V´ericationStatistique
Proprie´tes ´
Statistique
Verification ´
Syste`mesprobabilistes:
mod`ele´icationetsimulation s, ver
Syst`emesprobabilistes
Syste`mesprobabilistes
Syst`estemporise´s em
Propri´et´es
Pourquoiutiliserdesprobabilit´es?
Certainssyst`emessontprobabilistes. Environnement probabiliste.
lligsotreithme´persoubraubnia`tmebesaSsy
Approximationprobabilistedunsyst`eme. mentis´er´ecpaspne-tnnmeivorlneonnocetiannnO l’approxime par un comportement probabiliste.
V´ericationStatistique
et.sbAtsractionsprobabiletsiuopssedrtsysme`e´esdrmteisin [LLM+02]
Apporterunesolutionauxproble`mesnayantpasdesolution d´eterministe.40PN]0PFDKD,2[
Marie Duflot-Kremer
Syste`mesprobabilistes:
mod`eles,ve´ricationetsimulation
3 / 31
Syste`mesprobabilistes
Init
Syst`emestemporise´s
Proprie´te´s
Systemes probabilistes par nature `
Lancerdede´,depi`,tirageale´atoire. ece
V´ericationStatistique
Pourchaqueexpe´rience,onpeutd´eterminerlaprobabilit´e dun´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´ricationetsimulation
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´ricationStatistique
Etudedecommunicationssurunre´seau On veut savoir le temps moyen de transmission d’un message Onabesoinderepr´esenterleuxdemessagescirculantsurle ´ reseau Utilisationdunmod`eleprobabilistepourrepr´esenterlalongueuret lafr´equencedesmessages.
Marie Duflot-Kremer
Syst` es probabilistes : em
mod`eles,ve´ricationetsimulation
5 / 31
Syste`mesprobabilistes
Syste`mestemporises ´
Probabilit´es
pour
Propri´t´s e e
acc´l´erer e
V´ericationStatistique
Un exemple : le Quicksort iniste:eVoisre´dnmret Prendreldereinree´´lmene)tovip=(t lpsulssetiuo)sullusesppts(rpetiertteM`epr.aspret(anav grands) tnuadxueruisevembleauxxsous-tailppreuqAmethecr´allrigo formes. ´ En moyenne :O(n!log(n)) Pri:)eaulei´trasecab(tO(n2) Version probabiliste : otri´laeegarlenaM´glalreuqilppasipuauleabettlenemo ci-dessus ranceEpse´O(n!log(nr´ntee))leuquqelioseelt
Marie Duflot-Kremer
Syste`mesprobabilistes:
mode`les,ve´ricationetsimulation
6 / 31
Systemes probabilistes `
Syst`emestemporis´es
Propri´ete´s
Cas probabiliste plus simple
Ve´ricationStatistique
Automates communicants Onconsid`eredescanauxavecperte Nombreusesquestionsinde´cidables(accessibilite´re´pe´te´e...)
Avecprobabilite´s: tilie´essageauneprobabCahuqme!urdhaacequdteˆeper ` ´t e e ap t´e1bilirobapreselierv´Onpcevase´te´irpo Laedivitnoiac´vrebldaetdenci´e[BS03].
Marie Duflot-Kremer
Syst`emesprobabilistes:
modeles,ve´ricationetsimulation `
7 / 31
Syste`mesprobabilistes
Syste`mestemporise´s
Propri´et´es
Solutions probabilistes
Certainsproble`mesnontpasdesolutiond´eterministe
V´ericationStatistique
Silacongurationded´epartestsyme´trique,onnepeut romprelasyme´trie
Besoindunalgorithmeprobabilistepourromprelasyme´trie.
Exemple : Protocole CSMA/CD
[DFH+05]
mm n reseau  ´Co unicatio Collision de messages possible tentediialetadrisi´dnundoihoecesB!drerue´ivet´erentpo nouvelles collisions Choix probabiliste du temps d’attente.
Marie Duflot-Kremer
Syste`mesprobabilistes:mod`eles,ve´ricationetsimulation
8 / 31
Syst`emesprobabilistes
Syste`mestemporis´es
Sy t`mes probabilistes s e
en
Proprie´t´ es
temps
Ve´ricationStatistique
continu
Temps discret : limitation Besoindunemode´lisationplusne Exemple : distribution exponentielles Un taux"ahcruop´seeopirntemitioransquet satate`rp´ett´eloiavuirqabdPortnue´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´ericationStatistique
Request2
Access2
Deux files de processus, une seule memoire ´ Unseulprocessuspeutacce´dera`lam´emoireenmeˆmetemps
Marie Duflot-Kremer
Syste`mesprobabilistes:modeles,v´ericationetsimulation `
10 / 31