Model checking nondeterministic and randomly timed systems [Elektronische Ressource] / by Martin Richard Neuhäußer

ModelCheckingNondeterministicand
RandomlyTimedSystems
MartinR.Neuha¨ußerGraduationcommittee:
Prof.Dr.Ir.A.J.Mouthaan UniversityofTwente,
(chairman) eNetherlands
Prof.Dr.Ir.Joost-PieterKatoen RWTHAachen/UniversityofTwente,
(promotor) Germany/eNetherlands
Dr.Marie¨lleI.A.Stoelinga UniversityofTwente,eNetherlands
(referent)
Prof.Dr.JosC.M.Baeten EindhovenUniversityofTechnology,eNetherlands
Prof.Dr.Ir.BoudewijnR.Haverkort UniversityofTwente,eNetherlands
Prof.Dr.-Ing.HolgerHermanns SaarlandUniversity,Germany
Prof.Dr.JacoC.vandePol UniversityofTwente,eNetherlands
Prof.Dr.RobertoSegala UniversityofVerona,Italy
IPADissertationSeries????-??.
CTITPh.D.-esisSeriesNo.??-???,ISSN????-????.
ISBN:???-??-???-????-?.
eresearchreportedinthisdissertationhasbeencarriedoutundertheauspicesoftheInsti-
tuteforProgrammingResearchandAlgorithmics(IPA)andwithinthecontextoftheCenterfor
TelematicsandInformationTechnology(CTIT).eresearchfundingwasprovidedbytheNWO
Grantthroughtheproject:VerifyingQuantitativePropertiesofEmbeddedSo?ware(QUPES).
Translationoftheabstract:VietYenNguyen(MSc).
ATypesetinLTX.E
Coverdesign:AnjaBalsfulland
Publisher:Wo¨hrmannPrintService-http://www.wps.nl.
Copyright©????byMartinR.Neuha¨ußer,Aachen,Germany.MODELCHECKING
NONDETERMINISTICAND
RANDOMLYTIMEDSYSTEMS
Dissertation
toobtainthedoctor’sdegree
attheUniversityofTwente,ontheauthorityof
therectormagni?cus,Prof.Dr.H.Brinksma,
onaccountofthedecisionofthegraduationcommittee
tobepubliclydefended
onFriday,January??,????at??:??
by
MartinRichardNeuha¨ußer
bornon??September????
inKulmbach,Germanyedissertationhasbeenapprovedbythepromotor:
Prof. Dr.Ir.Joost-PieterKatoenModelCheckingNondeterministicand
RandomlyTimedSystems
VonderFakulta¨tfu¨rMathematik,Informatikund
Naturwissenscha?enderRheinisch-Westfa¨lischenTechnischen
HochschuleAachenzurErlangungdesakademischenGrades
einesDoktorsderNaturwissenscha?engenehmigteDissertation
vorgelegtvon
Diplom-Informatiker
MartinRichardNeuha¨ußer
aus
Kulmbach
Berichter: Prof.Dr.Ir.Joost-PieterKatoen
Prof.Dr.FranckvanBreugel
¨ ¨TagdermundlichenPrufung:??.Januar????
DieseDissertationistaufdenInternetseitenderHochschulbibliothekonlineverfu¨gbar.Abstract
Formalmethodsinitiallyfocusedonthemathematicallyprecisespeci?cation,designand
analysisoffunctionalaspectsofso?wareandhardwaresystems.Inthiscontext,model
checkinghasprovedtobetremendouslysuccessfulinanalyzingqualitativeproperties
ofdistributedsystems. isobservationhasencouragedpeopleinthe?eldofperfor-
manceanddependabilityevaluationtoextendexistingmodelcheckingtechniquesto
alsoaccountforquantitativemeasures.Asaresult,nowadays,theautomaticanalysisof
Markovianmodelshasbecomeanindispensabletoolforthedesignandevaluationof
safetyandperformancecriticalsystems.
Markovianmodelsareclassi?edaccordingtotheirunderlyingnotionoftime,being
eitherdiscreteorcontinuous. Inthediscrete-timesetting,Markovdecisionprocesses
areanondeterministicmodelwhichiswidelyknowninmathematics,computerscience
andoperationsresearch. Moreover,e?cientalgorithmsareavailablefortheiranalysis.
isstandsinsharpcontrasttothecontinuous-timesetting,wherenotechniquesexist
toanalyzemodelsthatcombinestochastictimingandnondeterminism.Inthepresent
thesis,webridgethisgapandproposequanti?ablyprecisemodelcheckingalgorithms
foravarietyofnondeterministicandstochasticmodels.
We?rstconsidercontinuous-timeMarkovdecisionprocesses(CTMDPs).Touniquely
determinethequantitativepropertiesofaCTMDP,allitsnondeterministicchoicesmust
beresolvedaccordingtosomestrategy.erefore,weproposeahierarchyofscheduler
classesandinvestigatetheirimpactontheachievableperformanceanddependability
measures. Inthiscontext,weidentifylateschedulers,whichresolvethenondetermin-
ismasneatlyaspossible.Apartfromtheirinterestingtheoreticalproperties,theyfacili-
tatetheanalysisoflocallyuniformCTMDPsconsiderably.InalocallyuniformCTMDP,
thetiminginastateisindependentofthescheduler.isobservationculminatesinan
e?cientandquanti?ablypreciseapproximationalgorithmforlocallyuniformCTMDPs.
IncontrasttoCTMDPswhichcloselyentanglenondeterminismandstochastictime,
interactiveMarkovchains(IMCs)areahighlyversatilemodelthatstrictlyuncouplesthe
twoaspects.Duetothisseparationofconcerns,IMCsarelocallyuniformbyde?nition.
isallowsustoapplyanalysistechniqueswhicharesimilartothosethatwedeveloped
forlocallyuniformCTMDPs,alsotoIMCs.Inthisway,wesolvetheopenproblemof
modelcheckingarbitraryIMCs.
Inthenextstep,wereturntoCTMDPsandprovethattheycanbetransformedinto
alternatingIMCsinameasurepreservingway.Asourproofdoesnotrelyonlocaluni-
formity,itenablestheanalysisofquantitativemeasuresonarbitraryCTMDPsbymodel
checkingtheirinducedIMCs. However,theunderlyingschedulerclassslightlydi?ersviii
fromthelateschedulersthatweusedinitially.Infact,itcoincideswiththetime-andhis-
torydependentschedulersthatareproposedintheliterature.us,ourresultforIMCs
alsosolvesthelongstandingproblemofmodelcheckingarbitraryCTMDPs.
However,theapplicabilityofmodelcheckingislimitedbytheinfamousstatespaceex-
plosionproblem:Evensystemsofmoderatesizeo?enyieldmodelswithanexponentially
largerstatespacethatfoilstheiranalysis.Totacklethisproblem,manytechniqueshave
beendevelopedthatminimizethestatespacewhilepreservingimportantpropertiesof
themodel.Inprocessalgebras, bisimulation minimizationidenti?esprocesseswiththe
samequantitativebehaviorandreplacesequivalentonesbyasinglerepresentative.De-
pendingontheredundancyinthemodel,thiscanleadtoenormousreductionsinthe
sizeofthestatespace. AsIMCshaveaprocessalgebraicbackground,itisnotsurpris-
ingthatbisimulationminimizationisreadilyavailableforthem.However,thisisnotthe
caseforCTMDPs. atiswhyweintroducebisimulationminimizationforCTMDPs
andprovethatitpreservesallquantitativemeasures.
Finally,weapplytheachievedresultsandproposeanalternativesemanticsfor gener-
alizedstochasticPetrinets(GSPN),whichavoidstheshortcomingsofearlierde?nitions
thatwereneededtoruleoutnondeterministicchoices.Moreprecisely,wetransforma
GSPNmodelintoanequivalentIMCwhichcanbemodelchecked.
Toshowtheapplicabilityofourapproach,weanalyze the dependabilityof a worksta-
tion clusterwhichismodeledbyanondeterministicGSPN.ecomparisonofourre-
sultswiththosethatareavailableintheliteratureisilluminating:Whenthelatterwere
published,noanalysistechniquefornondeterministicandrandomlytimedsystemswas
available.erefore,thenondeterministicchoicesintheGSPNmodelwerereplacedby
staticprobabilitydistributions.
Formeasuresthataremostlyindependentoftheschedulingpolicy,ourresultscoin-
cidewiththoseintheliterature. However,forothermeasures,choosingantagonistic
schedulersmitigatestheinferreddependabilitycharacteristicofthesystemthatwestudy
byupto??%.esefalsepositivesintheearlieranalysesclearlyprovethenecessityof
nondeterministicmodelinginthe?eldofperformanceanddependabilityanalysis.Samenvatting
Formelemethodenwordenvanoudshertoegepastmeteenwiskundigrigoureuzebena-
deringvanspeci?catie,ontwerpenanalysevanfunctioneleaspecteninhard-enso?ware.
Metnamemodelcheckingbleekenormsuccesvoltezijnomkwalitatieveeigenschappen
vangedistribueerdesystementeanalyseren.Ditmoedigdeonderzoekersinperforman-
ceevaluatieenbetrouwbaarheidsanalyseaanomdiezelfdetechniekentebenuttenvoor
kwantitatieveanalyses.AlsgevolgdaarvanisdeautomatischeanalysevanMarkovmo-
delleneenonmisbaarmiddelgewordenvoorhetontwerpenevaluatievanbetrouwbare
systemen.
Markovmodellenwordendoorgaansgeclassi?ceerdaandehandvanhunonderliggen-
deinterpretatievantijd,hetzijdiscreetofcontinu.Betre?endeheteerstgenoemde,zijn
Markovdecisionprocesseswijdverspreidindewiskunde,informaticaenoperationele
research.Erzijne?cie¨ntealgoritmenbeschikbaaromdezemodellenteanalyseren.Dit
staatinscherpcontrastmethaarcontinue-tijdstegenhanger.Erwarentothedennoggeen
techniekenontwikkeldvoormodellenmetstochastischetimingennon-determinisme.
Inditproefschri?overbruggenwedezetekortkomingmetonzebehandelingvankwan-
titiefpreciezemodelcheckingalgoritmesvooreenscalavannon-deterministischeen
stochastischemodellen.
WebehandeleneerstContinuous-TimeMarkovDecisionProcesses(CTMDPs).Om
dekwantitatieveeigenschappenvaneennon-deterministischmodeltebepalenmoeten
allenon-deterministischekeuzesvastgelegdwordenvolgenseenstrategie.Omdiereden
presenterenwijeenhierarchievanschedulerklassesenonderzoekenwijhunimpactop
performanceenbetrouwbaarheidsmaten.Indezecontextidenti?cerenwedeklassevan
”lateschedulers”. Naasthuninteressantetheoretischeeigenschappen,faciliterenzijde
analysevanlokaaluniformCTMDPs.Voordezeschedulersenmodellenpresenterenwe
namelijkeenpreciesbenaderingsalgoritme.
IntegenstellingtotCTMDPs,waarbijnon-determinismeenstochastischetijdsterk
verstrengeldzijn,zijnInteractiveMarkovChains(IMCs)eenextreemveelzijdigforma-
lismewaarindezetweeaspectenzijnontkoppeld.DoordezeontkoppelingzijnIMCsper
de?nitielokaaluniform.Detechniekendiewehebbenontwikkeldvoorlokaaluniform
CTMDPszijnconceptueelvergelijkbaarmetdievoorIMCs.Opdezewijzehebbenwe
hetopenstaandemodelcheckingprobleemvanIMCsopgelost.
VervolgenslatenwezienhoeCTMDPsa2eeldbaarzijnopalternerendeIMCswaarbij
dematenbehoudenblijven. OnsbewijsvanditresultaatvereistnietdatdeCTMDP
lokaaluniformis. DitmaaktkwantitatieveanalysesmogelijkvooralgemeneCTMDPs
doorhungeinduceerdeIMCsteanalyseren.Deschedulerklassediehierbijnodig