Fair simulation relations, parity games, and state space reduction for Büchi automata

Abstract. We give efficient algorithms, improving optimal known bounds, for computing a variety of simulation relations on the state space of a Büchi automaton. Our algorithms are derived via a unified and simple parity-game framework. This framework inco

http://www.wendangwang.comPUT.

Vol.34,No.5,pp.1159–1175c2005SocietyforIndustrialandAppliedMathematics

FAIRSIMULATIONRELATIONS,PARITYGAMES,ANDSTATE¨SPACEREDUCTIONFORBUCHIAUTOMATA

KOUSHAETESSAMI ,THOMASWILKE ,ANDREBECCAA.SCHULLER§

Abstract.Wegivee cientalgorithms,improvingoptimalknownbounds,forcomputingavarietyofsimulationrelationsonthestatespaceofaB¨uchiautomaton.Ouralgorithmsarederivedviaauni edandsimpleparity-gameframework.Thisframeworkincorporatespreviouslystudiednotionslikefairanddirectsimulation,butalsoanewnaturalnotionofsimulationcalleddelayedsimulation,whichweintroduceforthepurposeofstatespacereduction.Weshowthatdelayedsimulation—unlikefairsimulation—preservestheautomatonlanguageuponquotientingandallowssubstantiallybetterstatespacereductionthandirectsimulation.

Usingourparity-gameapproach,whichreliesonanalgorithmbyJurdzi´nski,wegivee cientalgorithmsforcomputingalloftheabovesimulations.Inparticular,weobtainanO(mn3)-timeandO(mn)-spacealgorithmforcomputingboththedelayedandthefairsimulationrelations.ThebestprioralgorithmforfairsimulationrequirestimeandspaceO(n6).Ourframeworkalsoallowsonetocomputebisimulations:wecomputethefairbisimulationrelationinO(mn3)timeandO(mn)space,whereasthebestprioralgorithmforfairbisimulationrequirestimeandspaceO(n10).

Keywords.fairsimulationrelations,paritygames,statespacereduction,B¨uchiautomataAMSsubjectclassi cation.68Q45

DOI.10.1137/S0097539703420675

1.Introduction.Thereareatleasttwodistinctpurposesforwhichitisusefultocomputesimulationrelationshipsbetweenthestatesofautomata:(1)toe cientlyestablishlanguagecontainmentamongnondeterministicautomata;and(2)toreducethestatespaceofanautomatonbyobtainingitsquotientwithrespecttotheequiv-alencerelationunderlyingthesimulationpreorder.

Forstatemachineswithoutacceptanceconditions,thereisawell-understoodnotionofsimulationwithalonghistory(see,e.g.,[20,16]),mainlyaimedatcomparingthebranchingbehaviorofsuchmachines(ratherthanjusttheirsetsoftraces).Forω-automata,whereacceptance(fairness)conditionsarepresent,thereareavarietyofdi erentsimulationnotions(see,e.g.,[14,11]).Ataminimum,forsuchasimulationtobeofuseforpurpose(1),itmusthavethefollowingproperty:

(*)wheneverstateq “simulates”stateq,thelanguageoftheautomatonwith

startstateq containsthelanguageoftheautomatonwithstartstateq.

Aswewillseeinsection5,however,thispropertyaloneisnotsu cienttoassureusefulnessforpurpose(2),whichrequiresthefollowingstrongerproperty:

(**)the“simulationquotient”preservesthelanguageoftheautomaton.

Wewillstatepreciselywhatismeantbyasimulationquotientlater.

In[14],anumberofdi erentsimulationnotionsforω-automatawerestudiedusingagame-theoreticframework.Theauthorsalsointroducedanewnaturalnotionofsimulation,titledfairsimulation.TheyshowedhowtocomputefairsimulationsforbothB¨uchiand,moregenerally,Streettautomata.ForB¨uchiautomata,theiralgorithmrequiresO(n6)timetodetermine,foronepairofstates(q,q ),whetherq

bytheeditorsJanuary6,2003;acceptedforpublication(inrevisedform)August18,

2004;publishedelectronicallyJune3,2005.Thispaperisbasedontheconferencepaper[9].

http://www.wendangwang.com/journals/sicomp/34-5/42067.html UniversityofEdinburgh,Edinburgh,ScotlandEH89YL(kousha@inf.ed.ac.uk). Christian-Albrechts-Universit¨at,24098Kiel,Germany(wilke@http://www.wendangwang.comrmatik.uni-kiel.de).§CornellUniversity,Ithaca,NY14853(reba@math.cornell.edu).

1159 Received

Fair simulation relations, parity games, and state space reduction for Büchi automata相关文档

最新文档

返回顶部