underlyingbluestack

RevisitingUnderapproximateReachabilityforMultipushdownSystemsS.
Akshay1,PaulGastin2,SKrishna1,andSparsaRoychowdhury11IITBombay,Mumbai,India2ENSParis-Saclay,Paris,FranceAbstractBooleanprogramswithmultiplerecursivethreadscanbecap-turedaspushdownautomatawithmultiplestacks.
ThismodelisTuringcomplete,andhence,oneisofteninterestedinanalyzingarestrictedclassthatstillcapturesusefulbehaviors.
Inthispaper,weproposeanewclassofboundedunderapproximationsformulti-pushdownsystems,whichsubsumesmostexistingclasses.
Wedevelopanecientalgorithmforsolvingtheunder-approximatereachabilityproblem,whichisbasedonecientx-pointcomputations.
WeimplementitinourtoolBHIMandillustrateitsapplicabilitybygeneratingasetofrelevantbenchmarksandexaminingitsperformance.
AsanadditionaltakeawayBHIMsolvesthebinaryreachabilityprobleminpushdownautomata.
Toshowtheversatilityofourapproach,wethenextendouralgorithmtothetimedsettingandprovidetherstimplementationthatcanhandletimedmulti-pushdownautomatawithclosedguards.
Keywords:MultipushdownSystems·UnderapproximateReachability·Timedpushdownautomata.
1IntroductionThereachabilityproblemforpushdownsystemswithmultiplestacksisknowntobeundecidable.
However,multi-stackpushdownautomata(MPDAhereafter)representatheoreticallyconciseandanalyticallyusefulmodelofmulti-threadedrecursiveprogramswithsharedmemory.
Asaresult,severalpreviousworksintheliteraturehaveproposeddierentunder-approximateclassesofbehav-iorsofMPDAthatcanbeanalyzedeectively,suchasRoundBounded,ScopeBounded,ContextBoundedandPhaseBounded[18,19,27,14,20,28].
Fromaprac-ticalpointofview,theseunderapproximationshaveledtoecienttoolsinclud-ing,GetaFix[21],SPADE[23].
Ithasalsobeenargued(e.
g.
,see[24])thatsuchboundedunderapproximationssucetondseveralbugsinpractice.
Inmanysuchtoolsecientx-pointtechniquesareusedtospeed-upcomputations.
Weextendknownx-pointbasedapproachesbydevelopinganewalgo-rithmthatcanhandlealargerclassofboundedunderapproximationsthanthewell-knownboundedcontextandboundedscopeunderapproximationsforPartlysupportedbyUMIReLaX,DST/CEFIPRA/INRIAprojectEQuaVe&TCS.
cTheAuthor(s)2020A.
BiereandD.
Parker(Eds.
):TACAS2020,LNCS12078,pp.
387–404,2020.
https://doi.
org/10.
1007/978-3-030-45190-521TACASEvaluationArtifact2020Accepted388S.
Akshayetal.
multi-pushdownsystemswhileremainingecientlyimplementable.
Ouralgo-rithmworksforanewclassofunderapproximatebehaviorscalledholeboundedbehaviors,whichsubsumescontext/scopeboundedunderapproximations,andisorthogonaltophaseboundedunderapproximations.
A"hole"isamaximalsequenceofpushoperationsofaxedstack,interspersedwithwell-nestedse-quencesofanystack.
Thus,inasequenceα=βγwhereβ=[push1(push2push3pop3pop2)push1(push3pop3)]10andγ=push2push1pop2pop1(pop1)20,βisaholewithrespecttostack1.
Thesuxγhas2holes(thepush2andthepush1).
Thuswesaythatαis3-holebounded.
Ontheotherhand,thenumberofcon-textswitches(andscopebound)inαis>50.
A(k-)holeboundedsequenceisonesuch,where,atanypointofthecomputation,thenumberof"open"holesareboundedatthispoint(byk).
Weshowthattheclassofholeboundedsequencessubsumesmostofthepreviouslydenedclassesofunderapproximationsandis,infact,containedintheverygenericclassoftree-widthboundedsequences.
Thisimmediatelyshowsdecidabilityofthereachabilityproblemforourclass.
Analyzingthemoregenericclassoftree-widthboundedsequencesisoftenmuchmoredicult;forinstance,buildingbottom-uptreeautomataforthispurposedoesnotscaleverywellasitexploresalarge(andoftenuseless)statespace.
Ourtechniqueisradicallydierentfromusingtreeautomata.
Undertheholeboundedassumption,wepre-computeinformationregardingwell-nestedsequencesandholesusingx-pointcomputationsandusetheminouralgorithm.
Usingecientdatastructurestoimplementthisapproach,wedevelopatool(BHIM)forBoundedHolereachabilityinMulti-stackpushdownsystems.
HighlightsofBHIM.
Twosignicantaspectsofthex-pointapproachinBHIMare:(i)weecientlysolvethebinaryreachabilityproblemforpushdownautomata.
i.
e.
,BHIMcom-putesallpairsofstates(s,t)suchthattisreachablefromswithemptystacks.
Thisallowsustogobeyondreachabilityandhandlesomelivenessquestions;(ii)wepre-computethesetofpairsofstatesthatareendpointsofholes.
Thisallowsustogreatlylimitthesearchforanacceptingrun.
Whilethex-pointapproachsolves(binary)reachabilityeciently,itdoesnotaprioriproduceawitnessofreachability.
Weremedythissituationbyproposingabacktrackingalgorithm,whichcleverlyusesthecomputationsdoneinthex-pointalgorithm,togenerateawitnesseciently.
BHIMisparametrizedwithrespecttotheholebound:ifnon-emptinesscanbecheckedorwitnessedbyawell-nestedsequence(thisisaneasywitnessandBHIMlooksforeasywitnessesrst,thengraduallyincreasescomplexity,ifnoeasywitnessisfound),thenitissucienttohavetheholebound0.
Increasingthiscomplexitymeasureasrequiredtocertifynon-emptinessgivesanecientimplementation,inthesensethatwesearchforharderwitnessesonlywhennoeasierwitnesses(w.
r.
tthiscomplexitymeasure)exist.
Inexamplesdescribedintheexperimentalsection,asmall(lessthan4)boundsucesandweexpectthistobethecaseformostpracticalexamples.
Finally,weextendourapproachtohandletimedmulti-stackpushdownsys-tems.
ThisshowstheversatilityofourapproachandalsorequiresustosolveRevisitingUnderapproximateReachabilityforMultipushdownSystems389severaltechnicalchallengeswhicharespecictothetimedsetting.
ImplementingthisapproachinBHIMmakesit,tothebestofourknowledge,thersttoolthatcananalyzetimedmulti-stackpushdownautomatawithclosedguards.
WeanalyzetheperformanceofBHIMinpractice,byconsideringbenchmarksfromtheliterature,andgeneratingtimedvariantsofsomeofthem.
OneofourbenchmarksisavariantoftheBluetoothexample[11,23],whereBHIMwasabletocatchaknownracedetectionerror.
Anotherinterestingbenchmarkisamodelofaparameterizedmultipleproducerconsumerexample,havingpa-rametersM,NonthequantitiesoftwoitemsA,Bproduced.
Here,BHIMcoulddetectbugsbyndingwitnesseshavingjust2holes,while,itisunlikelythatex-istingtoolsworkingonscope/contextboundedunderapproximationscanhandlethemasthenumberofscope/contextswitchesisdependentonM,N(infact,itistwicetheleastcommonmultipleofMandN).
Inthetimedsetting,oneofthemainchallengeshasbeentheunavailabilityoftimedbenchmarks;evenintheuntimedsetting,manybenchmarkswereunavailableduetotheirproprietarynature.
Duetolackofspace,proofs,technicaldetailsandparametricplotsofexperimentsarein[4].
RelatedWork.
Amongotherunder-approximations,scopebounded[27]sub-sumescontextandroundboundedunderapproximations,anditalsopavespathforGetaFix[21],atooltoanalyzerecursive(andmulti-threaded)booleanpro-grams.
Asmentionedearlierholeboundednessstrictlysubsumesscopebounded-ness.
Ontheotherhand,GetaFixusessymbolicapproachesviaBDDs,whichisorthogonaltotheimprovementsmadeinthispaper.
Indeed,ournextstepwouldbetobuildasymbolicversionofBHIMwhichextendsthehole-boundedapproachtoworkwithsymbolicmethods.
GiventhatBHIMcanalreadyhandlesyntheticexampleswith12-13holes(see[4]),weexpectthistoleadtoevenmoredrasticimprovementsandapplicability.
Forsequentialprograms,asummary-basedal-gorithmisusedin[21];summariesarelikeourwell-nestedsequences,exceptthatwell-nestedsequencesadmitcontextsfromdierentstacksunlikesummaries.
Asaresult,ourclassofboundedholebehaviorsgeneralizessummaries.
Manyotherdierenttheoreticalresultslikephasebounded[18],orderbounded[8]whichgivesinterestingunderapproximationsofMPDA,aresubsumedintree-widthboundedbehaviors,buttheydonotseemtohavepracticalimplementations.
Addingreal-timeinformationtopushdownautomatabyusingclocksortimedstackshasbeenconsidered,bothinthediscreteanddense-timedsettings.
Re-cently,therehasbeenaurryoftheoreticalresultsinthetopic[10,1,2,5,6].
How-ever,tothebestofourknowledgenoneofthesealgorithmshavebeensuccessfullyimplemented(except[6]whichimplementsatree-automatabasedtechniqueforsingle-stacktimedsystems)formulti-stacksystems.
Onereasonisthattheseal-gorithmsdonotemployscalablex-pointbasedtechniques,butinsteaddependonregionautomaton-basedsearchortreeautomata-basedsearchtechniques.
2UnderapproximationsinMPDAAmulti-stackpushdownautomaton(MPDA)isatupleM=(S,,s0,Sf,n,Σ,Γ)where,Sisanitenon-emptysetoflocations,isanitesetof390S.
Akshayetal.
transitions,s0∈Sistheinitiallocation,SfSisasetofnallocations,n∈Nisthenumberofstacks,Σisaniteinputalphabet,andΓisanitestackalphabetwhichcontains⊥.
Atransitiont∈canberepresentedasatuple(s,op,a,s),where,s,s∈Sarerespectively,thesourceanddestinationlocationsofthetransitiont,a∈Σisthelabelofthetransition,andopisoneofthefollowingoperations(1)nop,ornostackoperation,(2)(↓iα)whichpushesα∈Γontostacki∈{1,2,n},(3)(↑iα)whichpopsstackiifthetopofstackiisα∈Γ.
Foratransitiont=(s,op,a,s)wewritesrc(t)=s,tgt(t)=sandop(t)=op.
Atthemomentweignoretheactionlabelabutthiswillbeusefullaterwhenwegobeyondreachabilitytomodelchecking.
AcongurationoftheMPDAisatuple(s,λ1,λ2,λn)suchthat,s∈Sisthecurrentlocationandλi∈Γrepresentsthecurrentcontentofithstack.
ThesemanticsoftheMPDAisdenedasfollows:arunisacceptingifitstartsfromtheinitialstateandreachesanalstatewithallstacksempty.
ThelanguageacceptedbyaMPDAisdenedasthesetofwordsgeneratedbytheacceptingrunsoftheMPDA.
SincethereachabilityproblemforMPDAisTuringcomplete,weconsiderunder-approximatereachability.
Asequenceoftransitionsiscalledcompleteifeachpushinthatsequencehasamatchingpopandviceversa.
Awell-nestedsequencedenotedwsisdenedinductivelyasfollows:apossiblyemptysequenceofnop-transitionsisws,andsoisthesequencetwstwhereop(t)=(↓iα)andop(t)=(↑iα)areamatchingpairofpushandpopoperationsofstacki,i∈{1.
.
.
n}.
Finallytheconcatenationoftwowell-nestedsequencesisawell-nestedsequence,i.
e.
,theyareclosedunderconcatenation.
Thesetofallwell-nestedsequencesdenedbyanMPDAisdenotedWS.
Ifwevisualizethisbydrawingedgesbetweenpushesandtheircorrespondingpops,well-nestedsequenceshavenocrossingedges,asinand,wherewehavetwostacks,depictedwithredandvioletedges.
Weemphasizethatawell-nestedsequencecanhavewell-nestededgesfromanystack.
Inasequenceσ,apush(pop)iscalledapendingpush(pop)ifitsmatchingpop(push)isnotinthesamesequenceσ.
BoundedUnderapproximations.
Asmentionedintheintroduction,dier-entboundedunder-approximationshavebeenconsideredintheliteraturetogetaroundtheTuringcompletenessofMPDA.
Duringacomputation,acontextisasequenceoftransitionswhereonlyonestackornostackisused.
Incontextboundedcomputationsthenumberofcontextsarebounded[25].
Aroundisase-quenceof(possiblyempty)contextsforstacks1,2,n.
Roundboundedcompu-tationsrestrictthetotalnumberofroundsallowed[19,5,6].
Scopeboundedcom-putationsgeneralizeboundedcontextcomputations.
Here,thecontextchangeswithinanypushanditscorrespondingpopisbounded[19,20,28].
Aphaseisacontiguoussequenceoftransitionsinacomputation,wherewerestrictpoptoonlyonestack,buttherearenorestrictionsonthepushes[18].
Aphaseboundedcomputationisonewherethenumberofphasechangesisbounded.
Tree-width.
Agenericwayoflookingatthemistoconsiderclasseswhichhaveaboundonthetree-width[22].
Infact,thenotionsofsplit-width/clique-RevisitingUnderapproximateReachabilityforMultipushdownSystems391width/tree-widthofcommunicatingnitestatemachines/timedpushdownsys-temshasbeenexploredin[3],[13].
Thebehaviorsoftheunderlyingsystemarethenrepresentedasgraphs.
Ithasbeenshowninthesereferencesthatifthefam-ilyofgraphsarisingfromthebehavioursoftheunderlyingsystem(sayS)haveaboundedtree-width,thenthereachabilityproblemisdecidableforSvia,tree-automata.
However,thisdoesnotimmediatelygiverisetoanecientimplemen-tation.
Thetree-automataapproachusuallygivesnon-deterministicorbottom-uptreeautomata,whichwhenimplementedinpractice(see[6])tendtoblowupinsizeandexplorealargeanduselessspace.
Hencethereisaneedforecientalgorithms,whichexistformorespecicunderapproximationssuchascontext-bounded(leadingtox-pointalgorithmsandtheirimplementations[21]).
2.
1Anewclassofunder-approximationsOurgoalistobridgethegapbetweenhavingpracticallyecientalgorithmsandhandlingmoreexpressiveclassesofunder-approximationsforreachabilityofmulti-stackpushdownsystems.
Todoso,wedeneaboundedapproximationwhichisexpressiveenoughtocoverpreviouslydenedpracticallyinterestingclasses(suchascontextboundedetc),whileatthesametimeallowingecientdecidablereachabilitytests,aswewillseeinthenextsection.
Denition1.
(Holes).
Letσbecompletesequenceoftransitions,oflengthninaMPDA,andletwsbeawell-nestedsequence.
–Aholeofstackiisamaximalfactorofσoftheform(↓iws)+,wherews∈WS.
Themaximalityoftheholeofstackifollowsfromthefactthatanypossibleextensionceasestobeaholeofstacki;thatis,theonlypossibleeventsfollowingamaximalholeofstackiareapush↓jofsomestackj=i,orapopofsomestackj=i.
Ingeneral,wheneverwespeakaboutahole,theunderlyingstackisclear.
–Apush↓iinahole(ofstacki)iscalledapendingpushat(i.
e.
,justbefore)apositionx≤n,ifitsmatchingpopoccursinσatapositionz>x.
–Ahole(ofstacki)issaidtobeopenatapositionx≤n,ifthereisapendingpush↓ioftheholeatx.
Let#x(hole)denotethenumberofopenholesatpositionx.
Theholeboundofσisdenedasmax1≤x≤|σ|#x(hole).
–Aholesegmentofstackiisaprexofaholeofstacki,endinginaws,whileanatomicholesegmentofstackiisjustthesegmentoftheform↓iws.
Asanexample,considerthesequenceσinFigure1oftransitionsofaMPDAhavingstacks1,2(denotedrespectivelyredandblue).
Weusesuperscriptsfors0ws1↓11↓21↓31ws2ws3ws4↓12↓22↑31↑21ws5↓41↓51↑22↑51↑12↑41↑11sfFigure1.
Arunσwith2holes(2redpatches)oftheredstackand1hole(onebluepatch)ofthebluestack.
392S.
Akshayetal.
eachpush,popofeachstacktodistinguishtheithpush,jthpopandsoonofeachstack.
Therearetwoholesofstack1(redstack)denotedbytheredpatches,andoneholeofstack2(bluestack)denotedbythebluepatch.
Thesubsequence↓11↓21ws2oftherstholeisnotamaximalfactor,sinceitcanbeextendedby↓31ws3intherunσ,extendingthehole.
Considerthepositioninσmarkedwith↓12.
Atthisposition,thereisanopenholeoftheredstack(therstredpatch),andthereisanopenholeofthebluestack(thebluepatch).
Likewise,attheposition↑51,thereare2openholesoftheredstack(2redpatches)andoneopenholeofthebluestack2(thebluepatch).
Theholeboundofσis3.
Thegreenpatchconsistingof↑31,↑21andws5isapop-holeofstack1.
Likewise,thepops↑22,↑51,↑12areallpop-holes(oflength1)ofstacks2,1,2respectively.
Denition2.
(HoleBoundedReachabilityProblem)GivenaMPDAandK∈N,theK-holeboundedreachabilityproblemisthefollowing:DoesthereexistaK-holeboundedacceptingrunoftheMPDAProposition1.
Thetree-widthofK-holeboundedMPDAbehaviorsisatmost(2K+3).
Withthis,from[22][5][6],decidabilityandcomplexityfollow.
Thus,Corollary1.
TheK-holeboundedreachabilityproblemforMPDAisdecidableinO(|M|2K+3)where,MisthesizeoftheunderlyingMPDA.
Next,weturntotheexpressivenessofthisclasswithrespecttotheclassicalunderapproximationsofMPDA:rst,theholeboundedclassstrictlysubsumesscopeboundedwhichalreadysubsumescontextboundedandroundboundedclasses.
AlsoholeboundedMPDAandphaseboundedMPDAareorthogonal.
Proposition2.
ConsideraMPDAM.
ForanyK,letLKdenoteasetofse-quencesacceptedbyMwhichhavenumberofroundsornumberofcontextsorscopeboundedbyK.
ThenthereexistsK≤KsuchthatLKisKholebounded.
Moreover,thereexistlanguageswhichareKholeboundedforsomeconstantK,whicharenotKroundorcontextorscopeboundedforanyK.
Finally,thereexistsalanguagewhichisacceptedbyphaseboundedMPDAbutnotacceptedbyholeboundedMPDAandviceversa.
Proof.
WerstrecallthatifalanguageLisK-round,orK-contextbounded,thenitisalsoK-scopeboundedforsomeK≤K[20,19].
Hence,weonlyshowthatscopeboundedsystemsaresubsumedbyholeboundedsystems.
LetLbeaK-scopeboundedlanguage,andletMbeaMPDAacceptingL.
Considerarunρofw∈LinM.
Assumethatatanypointiintherunρ,#i(holes)=k,andtowardsacontradiction,let,k>K.
Considertheleftmostopenholeinρwhichhasapendingpush↓pwhosepop↑pistotherightofi.
Sincek>Kisthenumberofopenholesati,thereareatleastk>Kcontextchangesinbetween↓pand↑p.
ThiscontradictstheK-scopeboundedassumption,andhencek≤K.
Toshowthestrictcontainment,considerthevisiblypushdownlanguage[7]givenbyLbh={anbn(ap1cp1+1bp1dp1+1···apncpn+1bpndpn+1)|n,p1,p1,pn,pn∈RevisitingUnderapproximateReachabilityforMultipushdownSystems393N}.
Apossiblewordw∈Lbhisa3b3a2c3b2d3a2c3bd2ac2bd2witha,brepre-sentingpushinstack1,2respectivelyandc,drepresentingthecorrespondingmatchingpopfromstack1,2.
Arunρacceptingthewordw∈Lbhwillstartwithasequenceofpushesofstack1followedbyanothersequenceofpushesofstack2.
Notethat,thenumberofthepushesnissameinbothstacks.
ThenthereisagroupGconsistingofawell-nestedsequenceofstack1(equalaandc)followedbyapopofthestack1(anextrac),anotherwell-nestedsequenceofstack2(equalbandd)andapopofthestack2(anextrad),repeatedntimes.
Fromthedenitionofthehole,thetotalnumberofholesrequiredinGis0.
But,weneed1holeforthesequenceofa'sandanotherforthesequenceofb'satthebeginningoftherun,whichcreatesatmost2holesduringtherun.
Thus,theholeboundforanyacceptingrunρis2,andthelanguageLbhis2-holebounded.
However,Lbhisnotk-scopeboundedforanyk.
Indeed,foreachm≥1,considerthewordwm=ambm(ac2bd2)m∈Lbh.
Itiseasytoseethatwmis2m-scopebounded(thematchingc,dofeacha,bhappens2mcontextswitcheslater)butnotk-scopeboundedfork0then21foralli∈[n]do\\Addpopforstacki22SetOfListsp:=AddPopi(,M,AHSi,HSi,WR)\SetOfLists;23SetOfListsnew:=SetOfListsnew∪SetOfListsp;24forall3∈SetOfListspdo25if3.
last∈Sfand3.
NumberOfHoles=0then26returnFalse;\\Ifreacheddestinationstate27whileSetOfListsnew=;28returnTrue;2.
Push-PopClosure:Forstackoperations,considerapushtransitiononsomestack(saystacki)ofsymbolγ,enabledfromastates1,reachingstates2.
Ifthereisamatchingpoptransitionfromastates3tos4,whichpopsthesamestacksymbolγfromthestackiandifwehave(s2,s3)∈Rc,thenwecanaddthetuple(s1,s4)toRc.
ThefunctionWellNestedReachrepeatsthisprocessandthetransitiveclosuredescribedaboveuntilax-pointisreached.
LetusdenotetheresultingsetoftuplesbyWR.
Thus,Lemma1.
(s1,s2)∈WRiawell-nestedrunintheMPDAfroms1tos2.
Beyondwell-nestedreachability.
AnaivealgorithmforK-holeboundedreachabilityforK>0istostartfromtheinitialstates0,anddoaBreadthFirstSearch(BFS),nondeterministicallychoosingbetweenextendingwithawell-nestedsegment,creatingholesegments(withapendingpush)andclosingholesegments(usingpops).
Weacceptwhentherearenoopenholesegmentsandreachanalstate;thisgivesanexponentialtimealgorithm.
Giventheexpo-nentialdependenceonthehole-boundK(Corollary1),thisexponentialblowupisunavoidableintheworstcase,butwecandomuchbetterinpractice.
Inpar-ticular,thenaivealgorithmmakesarbitrarynon-deterministicchoicesresultinginablindexplorationoftheBFStree.
RevisitingUnderapproximateReachabilityforMultipushdownSystems395Inthissection,weusethebinarywell-nestedreachabilityalgorithmasanecientsubroutinetolimitthesearchinBFStoitsreachablepart(notethatthisisquitedierentfromDFSaswellsincewedonotjustgodownonepath).
Thecruxisthatatanypoint,wecreateanewholeforstacki,onlywhen(i)weknowthatwecannotreachthenalstatewithoutcreatingthisholeand(ii)weknowthatwecancloseallsuchholeswhichhavebeencreated.
Checking(i)iseasy,sincewejustusetheWRrelationforthis.
Checking(ii)blindlywouldcorrespondtodoingaDFS;however,weprecomputethisinformationandsimplylookitup,resultinginaconstanttimeoperationaftertheprecomputation.
Precomputingholeinformation.
Recallthataholeofstackiisamaximalsequenceoftheform(↓iws)+,wherewsisawell-nestedsequenceand↓irep-resentsapushofstacki.
Aholesegmentofstackiisaprexofaholeofstacki,endinginaws,whileanatomicholesegmentofstackiisjustthesegmentoftheform↓iws.
Ahole-segmentofstackiwhichstartsfromstatesintheMPDAandendsinstates,canberepresentedbythetriple(i,s,s),thatwecallaholetriple.
WecomputethesetHSiofallholetriples(i,s,s)suchthatstartingats,thereisaholesegmentofstackiwhichendsatstates,asdetailedinlines(5-9)ofAlgorithm1.
Indoingso,wealsocomputethesetAHSiofallatomicholesegmentsofstackiandstorethemastuplesoftheform(i,sp,α,sq)suchthatspandsqaretheMPDAstatesrespectivelyattheleftandrightendpointsofanatomicholesegmentofstacki,andαisthesymbolpushedonstacki(sp↓i(α)ws→sq).
AguidedBFSexploration.
Westartwithalist0=[s0]consistingoftheinitialstateandconstructaBFSexplorationtreewhosenodesarelistsofboundedlength.
AlistisasequenceofstatesandholetriplesrepresentingaK-holeboundedruninaconciseform.
IfHirepresentsaholetripleforstacki,thenalistisasequenceoftheform[s,Hi,Hj,Hk,Hi,H,s].
Thesimplestkindoflistisasinglestates.
Forexample,alistwith3holesofstacksi,j,kis=[s0,(i,s,s),(j,r,r),(k,t,t),t].
Theholetriples(inred)denoteopenholesinthelist.
Themaximumnumberofopenholesinalistisbounded,makingthelengthofthelistalsobounded.
Letlast()representthelastelementofthelist.
Thisisalwaysastate.
ForanodevstoringlistintheBFStree,ifv1,.
.
.
vkareitschildren,thenthecorrespondinglists1,kareobtainedbyextendingthelistbyoneofthefollowingoperations:1.
Extendwithahole.
Assumethereisaholeofsomestacki,whichstartsatlast()=s,andendsats.
Ifthelistattheparentnodeviss],thenforall(i,s,s)∈HSi,weobtainthelisttrunc()·append[(i,s,s),s]atthechildnode(i.
e.
,weremovethelastelementsof,thenappendtothislisttheholetriple(i,s,s),followedbys).
2.
Extendwithapop.
Supposethereisatransitiont=(sk,↑i(α),a,sk)fromlast()=sk,whereisoftheform[s0,h,u,v),(i,s,s),(j,t,tsk],suchthatthereisnoholetripleofstackiafter(i,s,s),weextendtherunbymatchingthispop(withitspush).
However,toobtainthelastpend-ingpushofstackicorrespondingtothishole,justHSiinformationisnot396S.
Akshayetal.
enoughsincewealsoneedtomatchthestackcontent.
Instead,wecheckifwecansplitthehole(i,s,s)into(1)aholetriple(i,s,sa)∈HSi,and(2)atuple(i,sa,α,s)∈AHSi.
Ifboth(1)and(2)arepossible,thenthepoptransitiontcorrespondstothelastpendingpushofthehole(i,s,s).
tindeedmatchesthependingpushrecordedintheatomichole(i,sa,α,s)in,enablingtheringoftransitiontfromthestatesk,reach-ingsk.
Inthiscase,weaddthechildnodewiththelistobtainedfromasfollows.
Wereplace(i)skwithsk,and(ii)(i,s,s)with(i,s,sa),re-spectivelysignifyingringofthetransitiontandthe"shrinking"ofthehole,byshiftingtheendpointoftheholesegmenttotheleft.
Whenweobtaintheholetriple(i,s,s)(thestartandendpointsoftheholeseg-mentcoincide),wemayhaveuncoveredthelastpendingpushandthereby"closed"theholesegmentcompletely.
Atthispoint,wemaychoosetoremove(i,s,s)fromthelist,obtaining[s0,h,u,v),(j,t,tsk].
Foreverysuch=[s0,h,u,v),(i,s,sa),(j,t,tsk]andall(sk,sm)∈WSwealsoextendto=[s0,h,u,v),(i,s,sa),(j,t,tsm].
Noticethatthesizeofthelistinthechildnodeobtainedonapop,iseitherthesameasthelistintheparent,orissmaller.
Thenumberoflistsisboundedsincethenumberofstatesandthelengthofthelistsarebounded.
TheBFSexplorationtreewillthusterminate.
CombiningtheabovestepsgivesusAlgorithm1,whosecorrectnessgivesus:Theorem1.
GivenaMPDAandapositiveintegerK,Algorithm1terminatesandanswers"false"ithereexistsaK-holeboundedacceptingrunoftheMPDA.
ComplexityoftheAlgorithm.
Themaximumnumberofstatesofthesys-temis|S|.
ThetimecomplexityoftransitiveclosureisO(|S|3),usingaFloyd-Warshallimplementation.
ThetimecomplexityofcomputingWellNestedReachwhichusesthetransitiveclosure,isO(|S|5)+O(|S|2S|)).
TocomputeAHSfornstacksthetimecomplexityisO(nS|2)andtocomputeHSfornstacksthecomplexityisO(n*|S|2).
Formultistacksystems,eachlistkeepstrackof(i)thenumberofholesegments(≤K),and(ii)informationpertainingtoholes(start,endpointsofholes,andwhichstacktheholecorrespondsto).
Intheworstcase,thiswillbe(2K+2)possiblestatesinalist,aswearekeepingthestatesatthestartandendpointsofalltheholesegmentsandastackperhole.
So,thereare≤|S|2K+3*nK+1lists.
Intheworstcase,whenthereisnoK-holeboundedrun,wemayendupgeneratingallpossiblelistsforagivenboundKontheholesegments.
ThetimecomplexityisthusboundedabovebyO(|S|2K+3*nK+1+|S|5+|S|3*||).
BeyondReachability.
Wecansolvetheusualsafetyquestionsinthe(bounded-hole)underapproximatesetting,bycheckingforunderapproximatereachabilityontheproductofthegivensystemwiththecomplementofthesafeset.
GiventhewayAlgorithm1isdesigned,thex-pointalgorithmallowsustogobeyondreachability.
Inparticular,wecansolveseveral(increasinglydicult)variantsoftherepeatedreachabilityproblem,withoutmuchmodication.
Considerthequestion:ForagivenstatesandMPDA,doesthereexistarunρstartingfroms0whichvisitssinnitelyoftenThisisdecidableifwecanRevisitingUnderapproximateReachabilityforMultipushdownSystems397decomposeρintoaniteprexρ1andaninnitesuxρ2s.
t.
(1)bothρ1,ρ2arewell-nested,or(2)ρ1isK-holeboundedcomplete(allstacksempty),andρ2iswell-nested,or(3)ρ1isK-holebounded,andρ2=(ρ3)ω,whereρ3isK-holebounded.
Itiseasytoseethat(1)issolvedbytwocallstoWellNestedReachandchoosingnon-emptyruns.
(2)issolvedbyacalltoAlgorithm1,modiedsothatwereachs,andthencallingWellNestedReach.
Lastly,tosolve(3),rstmodifyAlgorithm1tocheckreachabilitytoswithpossiblynon-emptystacks.
Thenrunthemodiedalgorithmtwice:rststartfroms0andreachs;secondstartfromsandreachsagain.
4GeneratingaWitnessWenextfocusonthequestionofgeneratingawitnessforanacceptingrunwhenouralgorithmguaranteesnon-emptiness.
Thisquestionisimportanttoaddressfromthepointofviewofapplicability:ifourgoalistoseeifbadstatesarereachable,i.
e.
,non-emptinesscorrespondstopresenceofabug,thewitnessrungivesthetraceofhowthebugcameaboutandhencepointstowhatcanbedonetoxit(e.
g.
,designingacontroller).
Weremarkthatthisquestionisdicultingeneral.
Whiletherearenaivealgorithmswhichcanexploreforthewitness(thusalsosolvingreachability),thesedonotusex-pointtechniquesandhencearenotecient.
Ontheotherhand,sinceweusex-pointcomputationstospeedupourreachabilityalgorithm,ndingawitness,i.
e.
,anexplicitrunwitnessingreachability,becomesnon-trivial.
Generationofawitnessinthecaseofwell-nestedrunsissimplerthanthecasewhentherunhasholes,andrequiresusto"unroll"pairs(s0,sf)∈WRrecursivelyandgeneratethesequenceoftransitionsresponsiblefor(s0,sf).
GettingWitnessesfromHoles.
Nowwemoveontothemorecomplicatedcaseofbehaviourshavingholes.
RecallthatinBFSexplorationwestartfromthestatesreachablefroms0bywell-nestedsequences,andexploresubsequentstatesobtainedeitherfrom(i)aholecreation,or(ii)apopoperationonastack.
Proceedinginthismanner,ifwereachanalconguration(saysf),withallholesclosed(whichimpliesemptystacks),thenwedeclarenon-emptiness.
Togenerateawitness,westartfromthenalstatesfreachableintherun(aleafnodeintheBFSexplorationtree)andbacktrackontheBFSexplorationtreetillwereachtheinitialstates0.
Thisresultsingeneratingawitnessruninthereverse,fromtherighttotheleft.
AssumethatthecurrentnodeoftheBFStreewasobtainedusingapopoperation.
Therearetwopossibilitiestoconsiderhere(seebelow)dependingonwhetherthispopoperationclosedorshrunksomehole.
Recallthateachholehasaleftendpointandarightendpointandisofaspecicstacki,dependingonthependingpushes↓iithas.
So,iftheMPDAhaskstacks,thenalistintheexplorationtreecanhavekkindsofholes.
Thewitnessalgorithmuseskstackscalledwitnessstackstocorrectlyimplementthebacktrackingprocedure,todealwithkkindsofholes.
WitnessstacksshouldnotbeconfusedwiththestacksoftheMPDA.
398S.
Akshayetal.
AssumethatthecurrentpopoperationisclosingaholeofkindiasinFigure2.
Thisholeconsistsoftheatomicholes,and.
Theatomicholeconsistsofthepushandthewell-nestedsequence(samefortheothertwoatomicholes).
Searchingamongpossiblepushtransitions,weidentifythematchingpushassociatedwiththecurrentpop,resultinginclosingthehole.
Onbacktracking,thisleadstoaparentnodewiththeatomicholehavingasleftendpoint,thepush,andtherightendpointasthetargetofthews.
Wepushontothewitnessstacki,abarrier(adelimitersymbol#)followedbythematchingpushtransitionandthenthews,.
Thebarriersegregatesthecontentsofthewitnessstackwhenwehavetwopoptransitionsofthesamestackinthereverserun,closing/shrinkingtwodierentholes.
Figure2.
Backtrackingtospitouttheholeinreverse.
Thetransitionsoftheatomicholearerstwritteninthereverseorder,followedbythoseofinreverse,andthenofinreverse.
Assumethatthecurrentpopoperationisshrinkingaholeofkindi.
Thelistatthepresentnodehasthishole,anditsparentwillhavealargerhole(seeFigure2,wherethepar-entnodeofhas).
Asinthecaseabove,werstidentifythematchingpushtransition,andcheckifitagreeswiththepushinthelastatomicholesegmentintheparent.
Ifso,wepopulatethewitnessstackiwiththerightmostatomicholesegmentoftheparentnode(seeFigure2,ispopulatedinthestack).
Eachtimewendapoponbacktrack-ingtheexplorationtree,wendtherightmostatomicholesegmentoftheparentnode,andkeeppushingitonthestack,untilwereachthenodewhichisobtainedasaresultofaholecre-ation.
Nowwehavecompletelyrecoveredtheentireholeinformationbybacktracking,andllthewitnessstackwiththereversedatomicholesegmentswhichconstitutedthishole.
Noticethatwhenwenishprocessingaholeofkindi,thenthewitnessstackihastheholereversedinsideit,followedbyabarrier.
Thenextholeofthesamekindiwillbetreatedinthesamemanner.
IfthecurrentnodeoftheBFStreeisobtainedbycreatingaholeofkindiinthex-pointalgorithm,thenwepopthecontentsofwitnessstackitillwereachabarrier.
Thisspitsouttheatomicholesegmentsoftheholefromtherighttotheleft,givingusasequenceofpushtransitions,andtherespectivewsinbetween.
Thetransitionsconstitutingthewsareretrievedandadded.
Noticethatpoppingthewitnessstackitillabarrierspitsoutthesequenceoftransitionsinthecorrectreverseorderwhilebacktracking.
5AddingTimetoMulti-pushdownsystemsInthissection,webrieydescribehowthealgorithmsdescribedinsection3canbeextendedtoworkinthetimedsetting.
Duetolackofspace,wefocusonRevisitingUnderapproximateReachabilityforMultipushdownSystems399someofthesignicantchallengesandadvances,leavingtheformaldetailsandalgorithmstothesupplement[4].
ATMPDAextendsaMPDASwithasetXofclockvariables.
Transitionscheckconstraintswhichareconjunctions/disjunc-tionsofconstraints(calledclosedguardsintheliterature)oftheformx≤corx≥cforc∈NandxanyclockfromX.
Symbolspushedonstacks"age"withtimeelapse;thatos,theystorethetimeelapsedsincetheywerepushedontothestack.
Apopissuccessfulonlywhentheageofthesymbollieswithinacertaininterval.
TheacceptanceconditionisasinthecaseofMPDA.
Therstmainchallengeinadaptingthealgorithmsinsection3tothetimedsettingwastotakecareofallpossibletimeelapsesalongwiththeoperationsdenedinAlgorithm1.
TheusageofclosedguardsinTMPDAmeansthatitsuf-cestoexploreallrunswithintegraltimeelapses(foraproofseee.
g.
,Lemma4.
1in[5]).
Thuscongurationsarepairsofstateswithvaluationsthatarevectorsofnon-negativeintegers,eachofwhichisboundedbythemaximalconstantinthesystem.
Now,tocheckreachabilityweneedtoextendalltheprecomputations(transitiveclosure,well-nestedreachability,aswellasatomicandnon-atomicholesegments)withthetimeelapseinformation.
Todothis,weuseaweightedversionoftheFloyd-Warshallalgorithmbystoringtimeelapsesduringprecom-putations.
Thisallowsustousethisprecomputedtimedwell-nestedreachabilityinformationwhileperformingtheBFStreeexploration,thusensuringthatanyexploredstateisindeedreachablebyatimedrun.
Indoingso,themostchalleng-ingpartisextendingtheBFStreewrtapop.
Here,wenotonlyhavetondasplitofaholeintoanatomichole-segmentandahole-segmentasinAlgorithm1,butalsoneedtokeeptrackofpossiblepartitionsoftime,makingthealgorithmquitechallenging.
TimedWitness:Asintheuntimedcase,wegenerateawitnesscertifyingnon-emptinessofTMPDA.
But,producingawitnessforthex-pointcomputationasdiscussedearlierrequiresunrolling.
Thex-pointcomputationgeneratesapre-computedsetWRToftuples((s,ν),t,(s,ν)),wheres,sarestatestistimeelapsedinthewell-nestedsequenceandν,ν∈N|X|areintegralvaluations,i.
e.
,integervaluestakenbyclocks.
Thissetoftuplesdoesnothaveinformationabouttheintermediatetransitionsandtime-elapses.
Tohandlethis,usingthepre-computedinformation,wedenealexicographicprogressmeasurewhichensuresterminationofthissearch.
Themainideaisasfollows:therstprogressmeasureistocheckifthereatime-elapsettransitionpossiblebetween(s,ν)and(s,ν)andifso,weprintthisout.
Ifnot,ν=ν+t,andsomesetofclockshavebeenresetinthetransition(s)from(s,ν)to(s,ν).
Thesecondprogressmeasurelooksatthesequenceoftransitionsfrom(s,ν)to(s,ν),consistingofresettransitions(atmostthenumberofclocks)thatresultinνfromν.
Ifneithertherstnorthesecondprogressmeasureapply,thenν=ν,andwearelefttoexplorethelastprogressmeasure,byexploringatmost|S|numberoftransitionsfrom(s,ν)to(s,ν).
Usingthisprogressmeasure,wecanseamlesslyextendthewitnessgenerationtothetimedsetting.
Thechallengesinvolvedtherein,canbeseeninthefullversion[4].
400S.
Akshayetal.
6ImplementationandExperimentsWeimplementedatoolBHIM(BoundedHolesInMPDA)inC++basedonAlgorithm1,whichtakesanMPDAandaconstantKasinputandreturnsTrueithereexistsaK-holeboundedrunfromthestartstatetoanacceptingstateoftheMPDA.
Incasethereissuchanacceptingrun,BHIMgeneratesonesuch,withminimalnumberofholes.
ForagivenholeboundK,BHIMrsttriestoproduceawitnesswith0holes,anditerativelytriestoobtainawitnessbyincreasingtheboundonholestillK.
Inmostcases,BHIMfoundthewitnessbeforereachingtheboundK.
WheneverBHIM'switnesshadKholes,itisguaranteedthattherearenowitnesseswithasmallernumberofholes.
ToevaluatetheperformanceofBHIM,welookedatsomeavailablebench-marksandmodeledthemasMPDA.
WealsoaddedtimingconstraintstosomeexamplessuchthattheycanbemodeledasTMPDA.
OurtestswererunonaGNU/LinuxsystemwithIntelRCoreTMi7–4770KCPU@3.
50GHz,and16GBofRAM.
Detailsofallexampleshere,aswellasanadditionalexampleofalinuxkernelbugcanbefound[4].
BluetoothDriver[25].
TheBluetoothdevicedriverexample[25],hasanarbitrarynumberofthreads,workingwithasharedmemory.
Wemodelthisusinga2-stackpushdownsystem,whereasystemstaterepresentsthecurrentvaluationoftheglobalvariables,andthestacksareusedtomaintainthecall-returnbetweendierentfunctions,aswellastokeeptrackofcontextswitchesbetweenthreads.
Aknownerroraspointedoutin[25]isaraceconditionbetweentwothreadswhereonethreadtriestowritetoaglobalvariableandtheotherthreadtriestoreadfromit.
BHIMfoundthiserror,withawell-nestedwitness.
Atimedextensionofthisexamplewasalsoconsidered,where,awitnesswasobtainedagainwithholebound0.
BluetoothDriverv2[11,23].
AmodiedversionofBluetoothdriveriscon-sidered[11,23],whereacounterismaintainedtocountthenumberofthreadsactivelyusingthedriver.
WemodelthiswithaAtwostackMPDA.
Withawell-nestedwitness,BHIMfoundtheerrorofinterruptedI/O,wherethestoppingthreadkillsthedriverwhiletheotherthreadisbusywithI/O.
AMulti-threadedProducerConsumerProblem.
Theproducercon-sumerproblem(seee.
g.
,[26])isaclassicexampleofconcurrencyandsynchro-nization.
Aninterestingscenarioiswhentherearemultipleproducersandcon-sumers.
Assumethattwoingredientscalled'A'and'B'areproducedinapro-ductionlineinbatches(ofMandNrespectively).
TheseparametersMandNarexedforeachdaybutmayvaryacrossdays.
Thereisanotherconsumermachinethat(1)consumesoneunitof'A'andoneunitof'B'inthatorder;(2)repeatsthisprocessuntilallingredientsareconsumed.
Inbetweenifoneoftheingredientsrunsout,thenwenon-deterministicallyproducemorebatchesoftheingredientandthencontinue.
Toavoidwastagethefactoryaimstoconsumeallingredientsproducedinaday,hencetheproblemofinterestistocheckifallA'sandB'sproducedinadayareconsumed.
Wecanmodelthisfactoryusingatwo-stackpushdownsystem,onestackperproduct,A,B,wherethesizesofthebatches,M>0andN>0respectively,areparameters.
TheproductionRevisitingUnderapproximateReachabilityforMultipushdownSystems401NameLocationsTransitionsStacksHolesTimeEmpty(milisec)TimeWitness(milisec)Memory(KB)Bluetooth458920149.
30.
2416934Bluetoothv2471342092.
20.
1765632MultiProdCons(3,2)71122126.
5290.
2815632MultiProdCons(24,7)3234221879.
3310.
6321836BinarySearchTree29782260.
85.
15143untimed-Lcrit6102214.
90.
74692untimed-Maze912208.
250.
075558Lbh(fromSec.
2.
1)7132222.
20.
64404Table1.
Experimentalresults:TimeEmptyandTimeWitnesscolumnrepresentsno.
ofmillisecondsneededforemptinesscheckingandtogeneratewitnessrespectively.
andconsumptionofthe'A'sand'B'saremodeledusingpushandpopintherespectivestack.
ForagivenMandN,thelanguageacceptedbythesystemisnon-emptyithereisarunwherealltheproduced'A'sand'B'sarecon-sumed.
Thelanguageacceptedbythetwo-stackpushdownsystemisgivenbyLM,N=((aM+bN)+(ab)+)+,wherea,brepresentrespectively,thepushonstack1,2anda,brepresentthepoponstack1,2andhencemusthappenequalnumberoftimes.
ForanyM,N>0,anyacceptingrunofthetwostackpushdownsystemcannotbewell-nested.
Further,inanacceptingrun,theminimumnumberofitemsproduced(andhenceitslength)mustbeamultipleofLCM(M,N).
Astheconsumptionof'A'sand'B'shappeninanorderonebyonei.
e.
,inasequencewhereconsumptionof'A'and'B'alternate,theminimumnumberofcontextchanges(andthescopebound)requiredinanacceptingrundependsonMandN(infactitisO(2*LCM(M,N)).
Ontheotherhand,theshortestacceptingrunis2-holebounded:atanypositionoftheword,theopenholescomefromtheunmatchedsequencesofaandbseensofar.
ThusforanyM,N>0,BHIMwasabletocheckfornon-emptinessofLM,Nwithawitnessofholebound2.
Criticaltimeconstraints[9].
Thisisoneofthetimedexamples,whereweconsiderthelanguageLcrit={aybzcydz|y,z≥1}withtimeconstraintsbetweenoccurrencesofsymbols.
Therstcmustappearafter1time-unitofthelasta,therstdmustappearwithin3time-unitsofthelastb,andthelastbmustappearwithin2timeunitsfromthestart,andthelastdmustappearat4timeunits.
LcritisacceptedbyaTMPDAwithtwotimedstacks.
Lcrithasnowell-nestedword,is4-contextbounded,butonly2hole-bounded.
ConcurrentInsertionsinBinarySearchTrees.
Concurrentinsertionsinbinarysearchtreesisaveryimportantproblemindatabasemanagementsystems.
[17,11]proposesanalgorithmtosolvethisproblemforconcurrentimplementations.
However,incorrectimplementationoflocksallowsathreadtooverwriteothers.
Wemodiedthealgorithm[17]tocapturethisbug,andmodeleditasMPDA.
BHIMfoundthebugwithawitnessofhole-bound2.
MazeExample.
Finallyweconsiderarobotnavigatingamaze,pickingitems;anextended(fromsingletomultiplestack)versionoftheexamplefrom[6].
Intheuntimedsetting,awitnessfornon-emptinesswasobtainedwithhole-bound0,whileintheextensionwithtime,thewitnesshadahole-bound2.
402S.
Akshayetal.
NameLocationsTransitionsStacksClockscmaxAged(Y/N)HolesTimeEmpty(milisec)TimeWitness(milisec)Memory(KB)Bluetooth4589202Y0152.
80.
1195568Lcrit610228Y29965.
23.
7203396Maze912225Y2349.
30.
3111604Table2.
Experimentalresultsoftimedexamples.
Thecolumncmaxisdenedasthemaximumconstantintheautomaton,andAgeddenotesifthestackistimedornotResultsandDiscussion.
TheperformanceofBHIMispresentedinTable1foruntimedexamplesandinTable2fortimedexamples.
Apartfromtheresultsinthetables,tochecktherobustnessofBHIMwrtparameterslikethenumberoflocations,transitions,stacks,holesandclocks(forTMPDA),welookedatexampleswithanemptylanguage,bymakingacceptingstatesnon-acceptingintheexamplesconsideredsofar.
ThisforcesBHIMtoexploreallpossiblepathsintheBFStree,generatingthelistsatallnodes.
ThescalabilityofBHIMwrtalltheseparametersarein[4].
BHIMVs.
Stateoftheart.
WhatmakesBHIMstandapartwrttheexistingstateofthearttoolsisthat(i)noneoftheexistingtoolshandleunderapprox-imationscapturedbyboundedholes,(ii)noneoftheexistingtoolsworkwithmultiplestacksinthetimedsetting(evenclosedguards!
).
ThestateoftheartresearchinunderapproximationswrtuntimedmultistackpushdownsystemshasproducedsomerobusttoolslikeGetaFixwhichhandlesmulti-threadedprogramswithboundedcontextswitches.
WhilewehaveadaptedsomeoftheexamplesfromGetaFix,thelatestavailableversionofGetaFixhassomeissuesinhandlingthoseexamples3.
Likewise,SPADE,MAGICandthecounterimplementation[16]arecurrentlynotmaintained,resultinginanon-comparisonofBHIMandthesetools.
MostexampleshandledbyBHIMcorrespondtonon-contextbounded,ornon-scopebounded,ortimedlanguageswhicharebeyondGetaFix:the2-holeboundedwitnessfoundbyBHIMforthelanguageL9,5forthemultiproducerconsumercasecannotbefoundbyGetaFix/MAGIC/SPADEwithlessthan90contextswitches.
Inthetimedsetting,theMazeexamplewhichhasa2hole-boundedwitnesswheretherobotvisitscertainlocationsequalnumberoftimesisbeyond[6],whichcanhandleonlysinglestack.
7FutureWorkAsimmediatefuturework,weareworkingonBHIMv2tobesymbolic,in-spiredfromGetaFix.
ThecurrentavatarofBHIMshowcasestheeciencyofx-pointtechniquesextendedtolargerboundedunderapproximations;indeedgoingsymbolicwillmakeBHIMmuchmorerobustandscalable.
Thisversionwillalsoincludeaparsertohandlebooleanprograms,allowingustoevaluatelargerrepositoriesofavailablebenchmarks.
Acknowledgements.
WewouldliketothankGennaroParlatoforthediscussionsonGetaFixandforprovidingusbenchmarksandanonymousreviewersformorepointers.
3wedidgetintouchwithoneoftheauthors,whoconrmedthis.
RevisitingUnderapproximateReachabilityforMultipushdownSystems403References1.
Abdulla,P.
A.
,Atig,M.
F.
,Stenman,J.
:Dense-timedpushdownautomata.
In:Proceedingsofthe27thAnnualIEEESymposiumonLogicinComputerSci-ence,LICS2012,Dubrovnik,Croatia,June25-28,2012.
p.
35–44(2012),https://doi.
org/10.
1109/LICS.
2012.
152.
Abdulla,P.
A.
,Atig,M.
F.
,Stenman,J.
:Theminimalcostreachabilityprobleminpricedtimedpushdownsystems.
In:LanguageandAutomataTheoryandAppli-cations-6thInternationalConference,LATA2012,ACoruna,Spain,March5-9,2012.
Proceedings.
pp.
58–69(2012),https://doi.
org/10.
1007/978-3-642-28332-163.
Akshay,S.
,Gastin,P.
,Juge,V.
,Krishna,S.
N.
:Timedsystemsthroughthelensoflogic.
In:34thAnnualACM/IEEESymposiumonLogicinComputerScience,LICS2019,Vancouver,BC,Canada,June24-27,2019.
pp.
1–13(2019)4.
Akshay,S.
,Gastin,P.
,Krishna,S.
,Roychowdhury,S.
:Revisitingunderapproxi-matereachabilityformultipushdownsystems(2020),https://arxiv.
org/abs/2002.
059505.
Akshay,S.
,Gastin,P.
,Krishna,S.
N.
:AnalyzingTimedSystemsUsingTreeAu-tomata.
LogicalMethodsinComputerScienceVolume14,Issue2(May2018),https://lmcs.
episciences.
org/44896.
Akshay,S.
,Gastin,P.
,Krishna,S.
N.
,Sarkar,I.
:Towardsanecienttreeau-tomatabasedtechniquefortimedsystems.
In:28thInternationalConferenceonConcurrencyTheory,CONCUR2017,September5-8,2017,Berlin,Germany.
pp.
39:1–39:15(2017),https://doi.
org/10.
4230/LIPIcs.
CONCUR.
2017.
397.
Alur,R.
,Madhusudan,P.
:Visiblypushdownlanguages.
In:Proceedingsofthethirty-sixthannualACMsymposiumonTheoryofcomputing.
pp.
202–211.
ACM(2004)8.
Atig,M.
F.
:Model-CheckingofOrderedMulti-PushdownAutomata.
Log-icalMethodsinComputerScienceVolume8,Issue3(Sep2012).
https://doi.
org/10.
2168/LMCS-8(3:20)20129.
Bhave,D.
,Dave,V.
,Krishna,S.
N.
,Phawade,R.
,Trivedi,A.
:Aperfectclassofcontext-sensitivetimedlanguages.
In:InternationalConferenceonDevelopmentsinLanguageTheory.
pp.
38–50.
Springer,Berlin,Heidelberg(2016)10.
Bouajjani,A.
,Echahed,R.
,Robbana,R.
:Ontheautomaticvericationofsystemswithcontinuousvariablesandunboundeddiscretedatastructures.
In:InternationalHybridSystemsWorkshop.
pp.
64–85.
Springer(1994)11.
Chaki,S.
,Clarke,E.
,Kidd,N.
,Reps,T.
,Touili,T.
:Verifyingconcurrentmessage-passingCprogramswithrecursivecalls.
In:InternationalConferenceonToolsandAlgorithmsfortheConstructionandAnalysisofSystems.
p.
334–349.
Springer(2006)12.
Cormen,T.
H.
,Leiserson,C.
E.
,Rivest,R.
L.
,Stein,C.
:Introductiontoalgorithms.
MITpress(2009)13.
Cyriac,A.
:Vericationofcommunicatingrecursiveprogramsviasplit-width.
(Vericationdeprogrammesrecursifsetcommunicantsviasplit-width).
Ph.
D.
thesis,EcolenormalesuperieuredeCachan,France(2014),https://tel.
archives-ouvertes.
fr/tel-0101556114.
Cyriac,A.
,Gastin,P.
,Kumar,K.
N.
:MSOdecidabilityofmulti-pushdownsystemsviasplit-width.
In:InternationalConferenceonConcurrencyTheory.
pp.
547–561.
Springer,Berlin,Heidelberg(2012)15.
Dang,Z.
,Ibarra,O.
H.
,Bultan,T.
,Kemmerer,R.
A.
,Su,J.
:Binaryreachabilityanalysisofdiscretepushdowntimedautomata.
In:InternationalConferenceonComputerAidedVerication.
p.
69–84.
Springer(2000)404S.
Akshayetal.
16.
Hague,M.
,Lin,A.
W.
:Synchronisation-andreversal-boundedanalysisofmulti-threadedprogramswithcounters.
In:ComputerAidedVerication-24thInterna-tionalConference,CAV2012,Berkeley,CA,USA,July7-13,2012Proceedings.
p.
260–276(2012),https://doi.
org/10.
1007/978-3-642-31424-72217.
Kung,H.
,Lehman,P.
L.
:Concurrentmanipulationofbinarysearchtrees.
ACMTransactionsonDatabaseSystems(TODS)5(3),354–382(1980)18.
LaTorre,S.
,Madhusudan,P.
,Parlato,G.
:Arobustclassofcontext-sensitivelanguages.
In:LogicinComputerScience,2007.
LICS2007.
22ndAnnualIEEESymposiumon.
pp.
161–170.
IEEE(2007)19.
LaTorre,S.
,Madhusudan,P.
,Parlato,G.
:Thelanguagetheoryofboundedcontext-switching.
In:LatinAmericanSymposiumonTheoreticalInformatics.
pp.
96–107.
Springer(2010)20.
LaTorre,S.
,Napoli,M.
:Reachabilityofmultistackpushdownsystemswithscope-boundedmatchingrelations.
In:InternationalConferenceonConcurrencyTheory.
p.
203–218.
Springer(2011)21.
LaTorre,S.
,Parthasarathy,M.
,Parlato,G.
:Analyzingrecursiveprogramsusingaxed-pointcalculus.
ACMSigplanNotices44(6),211–222(2009)22.
Madhusudan,P.
,Parlato,G.
:Thetreewidthofauxiliarystorage.
In:ACMSIG-PLANNotices.
vol.
46,pp.
283–294.
ACM(2011)23.
Patin,G.
,Sighireanu,M.
,Touili,T.
:Spade:Vericationofmultithreadeddynamicandrecursiveprograms.
In:InternationalConferenceonComputerAidedVeri-cation.
pp.
254–257.
Springer(2007)24.
Qadeer,S.
:Thecaseforcontext-boundedvericationofconcurrentprograms.
In:ModelCheckingSoftware,15thInternationalSPINWorkshop,LosAngeles,CA,USA,August10-12,2008,Proceedings.
pp.
3–6(2008),https://doi.
org/10.
1007/978-3-540-85114-1225.
Qadeer,S.
,Wu,D.
:Kiss:keepitsimpleandsequential.
ACMsigplannotices39(6),14–24(2004)26.
Silberschatz,A.
,Gagne,G.
,Galvin,P.
B.
:Operatingsystemconcepts.
Wiley(2018)27.
Torre,S.
L.
,Napoli,M.
,Parlato,G.
:Scope-boundedpushdownlanguages.
Interna-tionalJournalofFoundationsofComputerScience27(02),215–233(2016)28.
Torre,S.
L.
,Parlato,G.
:Scope-boundedMultistackPushdownSys-tems:Fixed-Point,Sequentialization,andTree-Width18,173–184(2012).
https://doi.
org/10.
4230/LIPIcs.
FSTTCS.
2012.
173OpenAccessThischapterislicensedunderthetermsoftheCreativeCommonsAttribution4.
0InternationalLicense(http://creativecommons.
org/licenses/by/4.
0/),whichpermitsuse,sharing,adaptation,distributionandreproductioninanymediumorformat,aslongasyougiveappropriatecredittotheoriginalauthor(s)andthesource,providealinktotheCreativeCommonslicenseandindicateifchangesweremade.
Theimagesorotherthirdpartymaterialinthischapterareincludedinthechapter'sCreativeCommonslicense,unlessindicatedotherwiseinacreditlinetothematerial.
Ifmaterialisnotincludedinthechapter'sCreativeCommonslicenseandyourintendeduseisnotpermittedbystatutoryregulationorexceedsthepermitteduse,youwillneedtoobtainpermissiondirectlyfromthecopyrightholder.