Probabilistic Model Checking of Disease Spread and Prevention

《Probabilistic Model Checking of Disease Spread and Prevention》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、ProbabilisticModelCheckingofDiseaseSpreadandPreventionSamuelHuangScholarlyPaperfortheDegreeofMastersinScienceAbstractThisworkinvestigatesthebenefitsofmodelcheckinguponcontactnetworks,amodelofdiseasetransmissionthroughapopulation.Manysuchmodelsareprob-abilistic

2、indesign,andthusamodelcheckerframeworkthatsupportsrandomnessisimportant.Wedemonstratehowtocharacterizeadiseaseasitisspreadintermsoftheportionsofthepopulationthatitaffects,aswellashowtoevaluateandexplorepreventativeandcontrolledmeasurestolimitthedisease’seffects

3、.Forthepurposesofthiswork,wefocusuponseveraldifferentvaccinationstrategies.Wealsoexplorethesensitivityofourframeworkthatinvolvesusingaprobabilisticmodelcheckerhastochangesintheunderlyingdiseasetransmissionmodel;weshowthatmanydesirablepropertiesandtraitsthatone

4、mightwanttoincludeareeasilyrepresentableusingourapproaches.1IntroductionAdvancesinepidemiology,thestudyoffactorsaffectinghealthandillnessofpopulations,canbedirectlybeneficialtohumansociety.Alargesubfieldofepidemiologicalresearchfocusesuponthepreventionandcontrol

5、ofdiseasepropagationthroughapopulation.Inparticular,theyareconcernedwith:•Outbreakinvestigation•Modeling•DatacollectionandanalysisDevelopinganaccurateandappropriatemodelforthepurposeofinvestigatingandpre-dictingdiseaseoutbreaksisactivelybeingpursued.Ifadiseas

6、ewerepredictedtobecomerampantinthenearfuture,onewouldliketodeterminethepropercauseofactiontoavoidorotherwisereducetheimpactthediseasewouldhaveuponthepopulationunder1study.Ifoneisstudyingrecordsofanalreadypasseddisease’sprogressionthroughapopulation,anaturalco

7、ncernmaybeastohow/wherethediseaseoriginated.Inthisworkweconsidertheusefulnessofapplyingexistingmodelcheckingbasedapproachestoproblemsposedbyepidemiology,specificallythosefocusingondiseasepreventionandcontrol.Traditionalmodelcheckingalgorithmsworkoverdeterminis

8、-ticstructures,whereasso-calledprobabilisticmodelcheckingrelaxesthedeterminismassumptiontoallowformodelswithuncertainty,orprobabilisticbehavior[5].Bothtraditionalandprobabilisticmodelchec