资源描述：
《weighted timed automata model-checking and gamesnew》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、WeightedTimedAutomata:Model-CheckingandGamesPatriciaBouyer1,2LSV–CNRS&ENSdeCachan–FranceAbstractInthispaper,wepresentweighted/pricedtimedautomata,anextensionoftimedautomatonwithcosts,andsolveseveralinterestingproblemsonthatmodel.Keywords:Weighted/priced
2、timedautomata,model-checking,games.1IntroductionModel-checkingofreal-timesystems.Timedautomata[3,4]areawell-establishedmodelforreal-timesystems.Oneofthemostimportantpropertiestheyenjoyisprobablythatreachabilitypropertiescanbedecidedforthatclassofsys-tem
3、s.Thishasgivenrisetomultipleworks,bothontheoreticalaspectsandonmorepracticalandalgorithmicaspects.Indeed,evenseveraltoolshavebeendevelopformodel-checkingthismodel,forinstanceHyTech[24],Kronos[21]orUppaal[29],andtherearealreadyseveralsuccessstories,forin
4、stance,ifwewanttoonlyciteoneoftheseexamples,thecorrectionandverificationoftheBang&Olufsenaudio/videoprotocol[22].Weighted/pricedtimedautomata.Weightedtimedautomata3extendclassi-caltimedautomatawithcostinformationbothonlocationsandedgesoftheautomaton.Thec
5、ostlabellingalocationrepresentsthepricepertimeunitforstayinginthatlocation,whereasthecostlabellinganedgerepresentsthepricefortakingthetransition.Thatway,everyrunintheautomatonhasaglobalcost,whichistheaccumulatedpricealongtherunofeverydelayanddiscretetra
6、nsition.Thismodelisparticularlyrelevantformodellingre-sourceconsumptioninreal-timesystems.Thisisfundamentalinthecontext1WorksupportedbyACISICortos,aprogramoftheFrenchministryofresearch.2Email:bouyer@lsv.ens-cachan.fr3Inthispaper,wefollowtheterminologyof
7、[5],butthismodeliscalledpricedtimedautomatonin[9].c2006PublishedbyElsevierScienceB.V.Bouyerofembeddedsystems,whicharefacedwithseveralresourceconstraints(forinstancebandwidth,memory,powerconsumption,etc...).Model-checkingandgameswithanoptimizationcriteri
8、um.Costcanbeusedasameasureofthe“performance”oftherunsinatimedautomaton,anditcanbeusedforoptimizingtheperformanceofthemodel.Forinstance,thismodelcanbeusedforsolvingschedulingproblems,andforcomputingtheoptimalcostforschedulingallta
