On the use of weak automata for deciding linear ar

OntheUseofWeakAutomataforDeidingLinearArithmetiwithIntegerandRealVariablesBernardBoigelot,SebastienJodogne,andPierreWolperUniversitedeLiege,InstitutMonteore,B28,4000Liege,Belgiumfboigelot,jodogne,pwgmontefiore.ulg.a.be,~fboigelot,jodogne,pwg/Abstrat.Thispaperonsidersnite-automatabasedalgorithmsforhandlinglineararithmetiwithbothrealandintegervariables.Previousworkhasshownthatthistheoryanbedealtwithbyusingniteau-tomataoninnitewords,butthisinvolvessomediÆultanddeliatetoimplementalgorithms.Theontributionofthispaperistoshow,usingtopologialarguments,thatonlyarestritedlassofautomataoninnitewordsareneessaryforhandlingrealandintegerlineararithmeti.Thisallowstheuseofsubstantiallysimpleralgorithmsandopensthepathtotheimplementationofausablesystemforhandlingthisombinedtheory.1IntrodutionAmongthetehniquesusedtodevelopalgorithmsfordeidingorhekinglogi-alformulas,niteautomatahaveplayedanimportantroleinavarietyofases.Classialexamplesaretheuseofinnite-wordniteautomatabyBuhi[Bu62℄forobtainingdeisionproeduresfortherstandseondordermonaditheo-riesofonesuessoraswellastheuseoftreeautomatabyRabin[Rab69℄fordeidingtheseond-ordermonaditheoryofnsuessors.Morereentexamplesaretheuseofautomataforobtainingdeisionandmodelhekingproeduresfortemporalandmodallogis[VW86a,VW86b,VW94,KVW00℄.Inthislastset-ting,automata-basedproedureshavetheadvantageofmovingtheombina-torialaspetsoftheproedurestotheontextofautomata,whiharesimplegraph-likestrutureswelladaptedtoalgorithmidevelopment.Thisseparationofonernsbetweenthelogialandthealgorithmihasbeenquitefruitfulforinstaneintheimplementationofmodelhekersforlinear-timetemporallogi[CVWY90,Hol97℄.AsalreadynotiedbyBuhi[Bu60,Bu62℄,automata-basedapproahesarenotlimitedtosequentialandmodallogis,butanalsobeusedforPresburgerarithmeti.Toahievethis,oneadoptstheusualenodingofintegersinabaser2,thusrepresentinganintegerasawordoverthealphabetf0;:::;r1g.Byextension,n-omponentintegervetorsarerepresentedbywordsoverthealphabetf0;:::;r1gnandaniteautomatonoperatingoverthisalphabetrepresentsasetofintegervetors.Giventhatadditionandorderareeasilyrep-resentedbyniteautomataandthattheseautomataarelosedunderBooleanoperationsaswellasprojetion,oneeasilyobtainsadeisionproedureforPres-burgerarithmeti.Thisideawasrstexploredatthetheoretiallevel,yieldingforinstanetheverynieresultthatbase-independentnite-automatonrepre-sentablesetsareexatlythePresburgersets[Cob69,Sem77,BHMV94℄.Later,ithasbeenproposedasapratialmeansofdeidingandmanipulatingPresburgerformulas[BC96,Boi98,SKR98,WB00℄.TheintuitionbehindthisapplieduseofautomataforPresburgerarithmetiisthatniteautomataplaywithrespettoPresburgerarithmetiarolesimilartotheoneofBinaryDeisionDiagrams(BDDs)withrespettoBooleanlogi.TheseideashavebeenimplementedintheLASHtool[LASH℄,whihhasbeenusedsuessfullyintheontextofverifyingsystemswithunboundedintegervariables.Italmostimmediatelyomestomindthatifanitewordoverthealphabetf0;:::;r1ganrepresentaninteger,aninnitewordoverthesamealphabetextendedwithafrationalpartseparator(theusualdot)anrepresentarealnumber.Finiteautomataoninnitewordsanthusrepresentsetsofrealve-tors,andserveasameansofobtainingadeisionproedureforrealadditivearithmeti.Furthermore,sinenumberswithemptyfrationalpartsaneasilybereognizedbyautomata,thesametehniqueanbeusedtoobtainadeisionproedureforatheoryombiningtheintegersandthereals.Thisisnotpresentlyhandledbyanytool,butanbeofpratialuse,forinstaneintheveriationoftimedsystemsusingintegervariables[BBR97℄.However,turningthisintoaneetiveimplementedsystemisnotaseasyasitmightrstseem.Indeed,projetingandomplementingniteautomataoninnitewordsissigniantlymorediÆultthanforautomataonnitewords.Projetionyieldsnondetermin-istiautomataandomplementingordeterminizinginnite-wordautomataisanotoriouslydiÆultproblem.Anumberofalgorithmshavebeenproposedforthis[Bu62,SVW87,Saf88,KV97℄,buteventhoughtheirtheoretialomplexityremainssimplyexponentialasinthenitewordase,itmovesupfrom2O(n)to2O(nlogn)andnoneoftheproposedalgorithmsareaseasytoimplementandne-tuneasthesimpleRabin-Sottsubsetonstrutionusedinthenite-wordase.However,itisintuitivelysurprisingthathandlingrealsissomuhmorediÆultthanhandlingintegers,espeiallyinlightofthefatthattheusualpolyhedra-basedapproahtohandlingarithmetiisbothofloweromplexityandeasiertoimplementfortherealsthanfortheintegers[FR79℄.OnewouldexpetthathandlingrealswithautomatashouldbenomorediÆultthanhan-dlingintegers1.Theonlusionthatomesoutoftheseobservationsisthatinnite-wordautomataonstrutedfromlineararithmetiformulasmusthavea1Notethatoneannotexpetrealstobeeasiertohandlewithautomatathanintegerssine,bynature,thisrepresentationinludesexpliitinformationabouttheexisteneofintegervaluessatisfyingtherepresentedformula.speialstruturethatmakesthemeasiertomanipulatethangeneralautomataoninnitewords.Thatthisspeialstrutureexistsandthatitanexploitedtoobtainsimpleralgorithmsispreiselythesubjetofthispaper.Asastartingpoint,letuslookatthetopologialharaterizationofthesetsdenablebylineararithmetiformulas.Letusrstonsi