On nested depth first search

References

[1]C.Courcoubetis,M.Vardi,P.Wolper,M,Yannakakis,Memory-efficientalgorithmsforthe

verificationoftemporalproperties,Formalmethodsinsystemdesign1(1992)275–288.[2]P.Godefroid,G.J.Holzmann,OntheVerificationofTemporalPropertiesInProc.PSTV93,,

ProtocolSpecificationTestingandVerification,Liege,Belgium,1993,North-Holland,109–124.[3]G.J.Holzmann,DesignandValidationofComputerProtocols,PrenticeHallSoftwareSe-ries,1992.[4]G.J.Holzmann,D.Peled,Animprovementinformalverification,7thInternationalConfer-enceonFormalDescriptionTechniques,Berne,Switzerland,1994,177–194.[5]D.Peled.Combiningpartialorderreductionswithon-the-flymodelchecking.FormalMeth-odsinSystemDesign8(1996),39–64.[6]M.Y.Vardi,P.Wolper,Anautomata-theoreticapproachtoautomaticprogramverification,

1stAnnualIEEESymposiumonLogicinComputerScience,1986,Cambridge,England,322–331.

9

never/*non-progress:do::skip

break::!progress

od;accept:do::!progressod

*/

Figure6:Non-ProgressB¨uchiAutomaton,expressedasNeverClaim

AlthoughwedonotknowhowtomodifythealgorithmfromFigure5forcompati-bilitywithpartialorderreduction,thereisasimplealternative.Thenon-progressprop-ertycantriviallybeexpressedasamodelcheckingproblem,forinstancebyexpressingit

,whereisabooleanfunctionthatyieldswiththeLTLproperty:

inprogressstates,andotherwise.ThisLTLpropertycanbetranslatedintotheB¨uchiautomatonshowninFigure6,whichcanbeusedtosolvetheproblemwiththealgorithmfromFigure4.

ThemethodfromFigures4andFigure6arepartofthelatestversionofthemodelcheckerSPIN(Version2.9).TheautomatonfromFigure6doesnothavetobespecifiedbytheuser,butisautomaticallygeneratedbySPINwhentheuserselectsasearchfornon-progresscycles.Theadditionofthetwo-statenon-progressautomatoninFigure6canintheworstcasedoublethememoryrequirementsofthesearchbasedonFigure4,comparedtoadirectapplicationofthealgorithmfromFigure5(avoidingtheneedfortheautomatonfromFigure6).ThealgorithmfromFigure4,however,canbeoptimizedsignificantlybycombiningitwithapartialorderreductionstrategy.Themeasurementsin[4]suggestthatareducedsearchbasedonFigure4shouldinalmostallcasesoutper-formanexhaustivesearchbasedonFigure5.

7Conclusion

Theoriginalalgorithmsforperformingnesteddepthfirstsearchestodetectthepresenceofacceptancecycles([1])orthepresenceofnon-progresscycles([3])arebothincom-patiblewithpartialorderreduction,suchasproposedin[5,4].Wehavediscussedamod-ificationofoneofthetwoalgorithmsthatsecurescompatibilitywithreductionmethods,andthatsufficestosolvebothsearchproblemsefficientlyanduniformly.

Acknowledgement:TheauthorsaremostgratefultoMichaelFerguson,whosekeen

8

procdfs(s)

iferror(s)thenreporterrorfiadds,0toStatespaceforeachsuccessortofsdo

ift,0notinStatespacethendfs(t)fiod

ndfs(s)/*different*/end

procndfs(s)/*thenestedsearch*/

ifsisProgressStatethenreturnfi/*new*/adds,1toStatespaceaddstoStack/*new*/foreachsuccessortofsdo

ift,1notinStatespacethenndfs(t)fi

elseiftisinStackthenreportcyclefi/*different*/od

deletesfromStack/*new*/end

Figure5:NestedDepthFirstSearchforNon-ProgressCycles

6AbsenceofStarvation

In[3]adifferentversionofanesteddepth-firstsearchisdescribedtosolveaslightlydifferenttypeofproblem.Theproblemhereisthedetectionofcyclesinthereachabilitygraphthatdonotcontainanyuser-definedprogressstates.Anyinfiniteexecutionthatcontainsonlyfinitelymanytraversalsofprogressstatescorrespondstostarvation.Thealgorithmfrom[3]isshowninFigure5(shownhereinthesameformatasFig-ures1and2).ThedifferenceswithFigure2areasfollows.Fromeveryreachablestatewestartthenestedsearch,butinthesecondsearchnotraversalsthroughprogressstatesareallowed.Wheneveracycleisclosedonthestackfromthisseconddepth-firstsearch,anerrorcanbereported.Inthisvariantofthesearch,therefore,alsothenon-reducedvariantreliesoninformationfromthesearchstack.(Notethatanexplicitsearchstackmustbemaintainedhereonlyforthesecondsearch,whileinFigure4theexplicitstackmustbemaintainedonlyforthefirstsearch.)

Adirectcombinationofthisalgorithmwiththereductionstrategyfrom[5]failsforthesamereasonsasbefore,butthistimethecorrectionalsofails.Notethatwhenthesecondsearchintersectsthesearchstackfromthefirstdepth-firstsearch,theredoesnotnecessarilyexistavalidpathbacktotherootoftheseconddepth-firstsearch(theseedstate).(Thepaththatexistsisinvalidifitcontainsprogressstates.)

7

procdfs(s)

iferror(s)thenreporterrorfiadds,0toStatespaceaddstoStack

foreach(selected)successortofsdoift,0notinStatespacethendfs(t)fiod

ifaccepting(s)thenndfs(s)fideletesfromStackend

procndfs(s)/*thenestedsearch*/adds,1toStatespace

foreach(selected)successortofsdoift,1notinStatespacethenndfs(t)fielseiftinStackthenreportcyclefiodend

Figure4:OptimizedNestedDepthFirstSearch,CompatiblewithReductionAddanintegerthatholdsa“selectionnumber.”Thepartialorderreductional-gorithmcanmakeseveralattemptstoselectasafe(reduced)subsetofsuccessorstates.InSPIN,theseselectionscorrespondtoprocessnumbers[4].Whenallattemptstochoseasafeselectionfail,acompleteexpansionofallsuccessorsisdone.Thefirstdepth-firstsearchwouldkeeptheselectionnumberfortheuseoftheseconddepth-firstsearch.Theseconddepth-firstsearchwouldgeneratethesetsofsuccessors(amplesets,intheterminologyof[5])accordingtothesameorder,andusetheselectionnumberthatwasheldbythefirstdepth-firstsearch,ignoringitsowncycleclosing.Aselectionnumberofzerowouldmeanselectingallsuccessorsfromthecurrentstate.

Amoremodestsolutionusesonlyonebitasaselectionnumber.Inthiscase,ifaselectioncausedclosingacycleinthefirstdepth-firstsearch,noalternativesubsetissought,andtheentiresetofsuccessorsisgeneratedfromthecurrentnode.Theselectionbitcommunicatestotheseconddepth-firstsearchwhethertouseitsfirstsubsetortodoafullsuccessorexpansion.

Theadditionoftheselectionbitisasmallmodificationofthereductionalgorithmdiscussedin[4]thatwewillnotelaboratefurtherhere.

6

5TheCorrection

Tocorrectthealgorithmitwillsufficeifwecanguaranteethattheseconddepth-firstsearchalwaysexploresthesamestatesthatarefoundinthefirstdepth-firstsearch.Wewillpresenttwochangestoaccomplishthis.

5.1IntersectionwithSearchStackfromFirstSearch

TheprobleminFigure3occurswhentheseconddepth-firstsearchreachesastatethatexistsalsoonthefirstsearchstack(state).Continuingthesecondsearchfromthisstate,thesearchcannowreachstateswithadifferent(longer)searchstackinthesec-onddepth-firstsearchthaninthefirst.Thismeansthatthethirdconditionfromthepar-tialorderreductionalgorithmisappliedtodifferentstates,andthesecondsearchmightnotfollowthefirstsearch.Wherethesetsofsuccessorstatesthatisselectedinthetwophasesofthesearchcandiffer.

Thesolutiontothisproblemisremarkablysimple:whentheseconddepth-firstsearchreachesastatethatexistsalsoonthestackfromthefirstsearch,thesearchcanbetermi-nated.Thereasonisthatreachingsuchastatefromtheseedstateimpliesimmediatelythatapathexiststhatleadsbacktotheseedstate:itisthepathofstatesonthefirstdepth-firstsearchstackthatstartsatthepointofintersection.Thispropertyisindependentoftheuseofthepartialorderreduction.Stoppingthesearchwhenreachingastateonthefirstsearchstackshortensthesearch,itimprovestheperformanceofthealgorithm,anditallowsforshortercounter-examplestoaninvalidcorrectnessclaimtobegenerated.ThechangeinthealgorithmofFigure2from[1]isshowninFigure4.Inthenewversionofthisalgorithm,thereisnolongeraneedtostoretheseedstate,butwedoneedinformationaboutthepresenceofstatesonthesearchstack.

5.2PreservingInformationBetweenSearches

Thefirstcorrectionofthenesteddepth-firstsearchalgorithmimprovesitsperformanceanditeliminatestheerrorthatoccurredinFigure3.But,itdoesnotcompletelysolvetheproblem.

Afailurecanstillhappen.Firstnotethatthefirstdepth-firstsearchcanbacktrackfromagraphcomponentwithoutperformingasecondsearch.(Thesecondsearchisonlyinitiatedfromacceptingstates.)Whilesearchinganothercomponentofthegraph,thatdoescontainacceptingstates,therecanbeatransitionthatleadsbacktotheearlierstates,thatdonotasyetappearinthesecondstatespace.Thisreturntransitionwouldnotbefollowedinthefirstsearch,sinceitleadsonlytopreviouslyvisitedstates.Duringasecondsearch,however,thetransitionmustbefollowed,Asimilarscenarionowexists,inwhichthestatesarevisitedwithadifferentsearchstackineachofthetwosearches,andthereachabilitypropertiesarenotpreserved.

Toeliminatealsothisproblem,onemustpreserveinformationabouttheselectionofsuccessorsbetweenthetwosearches.Thereareseveralpossibilities:

5

Figure3:FailureoftheReducedNestedDepth-FirstSearch

thatisbasedonthisconditioncandependontheprecisesearchorderandthecontentsofthesearchstackateachpointduringthesearch.

Adirectcombinationofthepartialorderreductiontechniquefrom[5,4]withthenesteddepth-firstsearchmethodfrom[1]thereforeresultsinanincorrectalgorithm.Sincethecontentsofthedepth-firstsearchstacksinthefirstandinthesecondsearchinthenesteddepth-firstsearchalgorithmfromFigure2differ,thestatespacethatiscon-structedduringthefirstandthesecondpartofthesearchneednolongerbeequalduringareducedsearch.Thismeansthatthesecondsearchmaybeincapableofprovingthatanacceptingstateisreachablefromitself,evenifitispartofastronglyconnectedcom-ponentinthereachabilitygraphthatisconstructedduringthefirstsearch.

TheexampleinFigure3illustratestheproblem.Considerthecasewherethefirst

and.Inthefullstatespace,thereissearchreachesstate.Itssuccessorsare

anothersuccessor,butitisnotselected.Firstedgeistaken,leadingtoacceptingstate.Now,thefirstsearchcontinuestosearchallthenodesaccessiblefrom.Whenbacktrackingto,thesecondsearchstarts,withasitsseedstate,lookingforacycle.Suchacycleexistsbytakingtheedges,andthenagain.However,oncereachingduringthesecondsearch,acycleconsistingofandisfound.Noticethatthiscyclewasnotfoundinthefirstsearch,aswasnotonthesearchstackofthefirstsearchwhilesearchingforsuccessorsof.Closingthiscyclewiththeedgeinthesecondsearchmakesthesecondsearchselectanalternativesubsetofsuccessors,e.g.,,viatheedge.Butnow,itispossiblethatthecyclethroughseedstateremainsundetected.

4

procdfs(s)

iferror(s)thenreporterrorfiadds,0toStatespaceforeachsuccessortofsdo

ift,0notinStatespacethendfs(t)fiod

ifaccepting(s)thenseed:=s;ndfs(s)fiend

procndfs(s)/*thenestedsearch*/adds,1toStatespaceforeachsuccessortofsdo

ift,1notinStatespacethenndfs(t)fielseift==seedthenreportcyclefiodend

Figure2:NestedDepth-FirstSearch

constructedbythealgorithmfromFigure1sufficestoseparatethetwosearches.Thatis:thesizeofStatespaceneednotdoubleasinitiallysuggestedin[1],butcanremainvirtuallyunchanged.Thesearchtime,however,candoublewhenallstatesarereachableinboththefirstandthesecondsearch,andnocyclesthroughacceptingstatesexist.Noticethatalsointhemodifiedalgorithm,thereisstillnoneedtostoretheedgesofthegraph,nortoaccessthedepth-firstsearchstack.

4ReducedSearch

Thestatespacethatisconstructedwiththedepth-firstsearchprocedurecanbereducedsubstantiallyifwelimitthenumberofsuccessorstatesthatisexploredfromeachreach-ablestate.

In[5]areductionofthistypeisdiscussedthatpreservestheB¨uchiacceptanceprop-ertiesfromthefullstatespacealsointhereducedstatespace,providedthatthreecondi-tionsaresatisfied.Twoofthethreeconditionsdealwithdependencybetweenexecutionsteps,andthevisibilityofindividualexecutionsteps.Theydonotalterthepropertiesofeitherthebasicorthenestedthedepth-firstsearch.

Athirdcondition,however,introducesadependencyontheinformationthatisstoredinthedepth-firstsearchstack.Theconditionstatesthatareductionofthesetofsucces-sorstatesfromstatesisinvalidifatleastoneofthosesuccessorstatesappearsonthedepth-firstsearchstack.Thismeansthatreachabilitypropertiesduringareducedsearch

3

procdfs(s)

iferror(s)thenreporterrorfiaddstoStatespace

foreachsuccessortofsdo

iftnotinStatespacethendfs(t)fiodend

Figure1:BasicDepth-FirstSearchAlgorithm,UsedForReachabilityAnalysis

2BasicDepth-FirstSearch

Abasicdepth-firstsearchalgorithmgeneratesandexamineseveryglobalstatethatisreachablefromagiveninitialstate,asillustratedinFigure1.

Afterafirstcheckforthevalidityofthestateanditsproperties,thestatedescriptorisenteredintoaglobalStatespace,usuallywiththehelpofstandardhash-tablelookupprocedures.Arecursivecalltothesearchprocedureisthenmadeforeachstatethatisreachablefromthisstateinoneatomicexecutionstep,i.e.,foreachpossiblesuccessorinthereachabilitygraphthatisnotalreadyrepresentedinStatespace.

NotethatStatespaceneedstorepresentonlythenodesofthereachabilitygraph;therepresentationoftheedgesbetweenthenodesisnotneeded.Notealsothatnoin-formationisneededaboutthepresenceofanystateonthedepth-firstsearchstack.

3NestedDepth-FirstSearch

TheprocedurefromFigure1cannotbeuseddirectlytosolveamodelcheckingproblem,butitcanreadilybeadapted.Inmodelchecking,thereachabilitygraph,partiallyrepre-sentedintheStatespacestructure,isusedtodefineaB¨uchiautomaton.Theacceptanceconditionsinthisautomatonareusuallyderivedfromaspecialpropertyautomatonthatisaddedtotheglobalsystem,asdescribedin[6,3].

Themodelcheckingprobleminthiscontextreducestotheproblemofdetectingtheexistenceinthegraphofacceptingstatesthatarepartofastronglyconnectedcomponentandthereforereachablefromthemselves.

Theprocedurein[1]appliesanesteddepth-firstproceduretosolvethisproblem,asillustratedinFigure2.Whenthenormalsearchretractstoanacceptingstate,asecondsearchisstarted,tosearchforacyclethroughthisstate.Ifthesecondsearchfailstofindacycle,thefirstsearchresumesfromthepointwhereitwasinterrupted.Itisshownin[2]thataddingtwobitstoeveryglobalstatethatisstoredintheStatespacethatis

2

OnNestedDepthFirstSearch

GerardHolzmann,DoronPeled,MihalisYannakakis

BellLaboratories700MountainAvenueMurrayHill,NJ07974

gerard,doron,mihalis@research.bell-labs.com

ExtendedAbstract

Abstract

Weshowinthispaperthatthealgorithmforsolvingthemodelcheckingproblemwithanesteddepth-firstsearchproposedin[1]caninterferewithalgorithmsthatsupportpartialorderreduction.Weintroducearevisedversionofthealgorithmthatguaranteescompatibility.Thechangealsoimprovestheperformanceofthenesteddepth-firstsearchalgorithmwhenpartialorderreductionisnotused.

1Introduction

Themodelcheckingproblemforconcurrentsystemscanbesolvedelegantlybymodel-ingthesystemanditscorrectnessrequirementsasautomataoninfinitewords(i.e.,B¨uchiAutomata),andbyverifyingthatthelanguageoftheproductofsystemandrequirementautomataisempty.Theemptinessproblemitselfwouldnormallyrequirethecompu-tationofthestronglyconnectedcomponentsoftheproductsystem.Thiscomputationcanbeavoidedwithanesteddepth-firstsearchprocedure,asdiscussedin[1,2,3].Thememoryrequirementsofareachabilityanalysis,basedoneitherdepth-firstorbreadth-firstsearchorder,canbereducedfurtherwiththehelpofpropertypreservingreductionstrategies.Onesuchmethodwasdescribedin[5,4].Werecentlydiscoveredthatthetwomethodsarenotcompletelycompatible,whichmeansthatadirectcombinationwillresultinanincompletemodelcheckingprocedure.

Section2firstgivesasynopsisofthebasicandnesteddepth-firstsearchmethods.Section3discussesreduction,andillustratestheundesirableside-effectsofadirectcom-binationofthealgorithms.Section4describesamodificationofthenesteddepth-firstsearchalgorithmthatavoidstheproblem.InSection5,finally,wediscussavariationofthealgorithmfrom[3]thatcanbeusedforprovingabsenceofstarvation,butthatdoesnotappeartobecompatiblewiththereductionstrategy.Analternativetechnique,thatiscompatible,isalsodiscussed.

1