资源描述：
《model-checking one-clock priced timed automata》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、Model-CheckingOne-ClockPricedTimedAutomataPatriciaBouyer1⋆,KimG.Larsen2⋆⋆,andNicolasMarkey1⋆1LSV,CNRS&ENSdeCachan,France{bouyer,markey}@lsv.ens-cachan.fr2AalborgUniversity,Denmarkkgl@cs.aau.dkAbstract.Weconsiderthemodelofpriced(a.k.a.weighted)timedau-tomata,anextensionoftimedautomatawithcostinfo
2、rmationonbothlocationsandtransitions.Weprovethatmodel-checkingthisclassofmodelsagainstthelogicWCTL,CTLwithcost-constrainedmodalities,isPSPACE-completeunderthe“single-clock”assumption.Incontrast,ithasbeenrecentlyprovedthatthemodel-checkingproblemisundecid-ableforthismodelassoonasthesystemhasthree
3、clocks.Wealsoprove∗thatthemodel-checkingofWCTLbecomesundecidable,evenunderthis“single-clock”assumption.1IntroductionAninterestingdirectionofreal-timemodel-checkingthathasrecentlyreceivedsubstantialattentionistheextensionandre-targetingoftimedautomatatech-nologytowardsoptimalschedulingandcontroll
4、ersynthesis[1,18,7].Inparticu-lar,aspartofthiseffort,thenotionofpriced(orweighted)timedautomata[4,3]hasbeenpromotedasausefulextensionoftheclassicalmodeloftimedautomataallowingcontinuousconsumptionofresources(e.g.energy)tobemodelledandanalyzed.Anumberofoptimizationproblemshavebeenshowndecidablefor
5、pricedtimedautomataincludingminimum-costreachability[4,3],optimal(minimumandmaximumcost)reachabilityinmulti-pricedsettings[17]andcost-optimalinfiniteschedules[6,7].Unfortunately,theadditionofcostcomeswithaprice:certainproblemsbecomeundecidableforpricedtimedautomata.Infact,in[11]ithasrecentlybeens
6、hownthattheproblemofdeterminingcost-optimalwinningstrategiesforpricedtimedgamesisnotcomputable.Also,bythesameauthors,ithasbeenshownthatthemodel-checkingproblemforpricedtimedautomataw.r.t.WCTL—CTLwithcost-constrainedmodalities—isundecidable[10].In[5]ithasbeenshownthatthesenegativeresultsholdevenf
7、orpricedtimed(game)automatawithnomorethanthreeclocks.⋆PartlysupportedbyACI“S´ecurit´e&Informatique”CORTOS.⋆⋆PartlysupportedbyaninvitedprofessorshipfromENSCachan.However,whenrestrictingtothesettingofpricedtimedgameautomatawit
