PTA_algorithm_applications

《PTA_algorithm_applications》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、PricedTimedAutomata:AlgorithmsandApplicationsGerdBehrmann,KimG.Larsen,andJacobI.Rasmussen⋆⋆⋆AalborgUniversityAbstract.Thiscontributionreportsontheconsiderableeffortmadere-centlytowardsextendingandapplyingwell-establishedtimedautomatatechnologytooptimalschedulingandplanningproblems.Theeffort

2、oftheauthorsinthisdirectionhastoalargeextentbeencarriedoutaspartoftheEuropeanprojectsVhs[22]andAmetist[17]andareavailableintherecentlyreleasedUppaalCora[12],avariantofthereal-timeverificationtoolUppaal[20,5]specializedforcost-optimalreachabilityfortheextendedmodelofpricedtimedautomata.1Int

3、roductionandMotivationSinceitsintroductionbyAlurandDill[2]themodeloftimedautomatahasestablisheditselfasastandardmodelingformalismfordescribingreal-timesys-tembehavior.Anumberofmaturemodelcheckingtools(e.g.Kronos,Uppaal,IF[11,20,16])arebynowavailableandhavebeenappliedtothequantitativeanaly

4、sisofnumerousindustrialcase-studies[25].Aninterestingapplicationofreal-timemodelcheckingthathasrecentlybeenreceivingsubstantialattentionistoextendandre-targetthetimedautomatatechnologytowardsoptimalschedulingandplanning.Theextensionsincludemostimportantlyanaugmentationofthebasictimedautom

5、ataformalismal-lowingforthespecificationoftheaccumulationofcostduringbehavior[7,3].Thestate-exploringalgorithmshavebeenmodifiedtoallowfor“guiding”the(symbolic)state-spaceexplorationinorderthat“promising”and“cheap”statesarevisitedfirst,andtoapplybranch-and-boundtechniques[6]toprunepartsofthes

6、earchtreethatareguaranteednottoimproveonsolutionsfoundsofar.Alsonewsymbolicdatastructuresallowingforefficientsymbolicstate-spacerepresentationwithadditionalcost-informationhavebeenintroducedandim-plementedinordertoefficientlyobtainoptimalornear-optimalsolutions[19].WithintheVhsandAmetistproje

7、ctssuccessfulapplicationsofthistechnologyhavebeenmadetoanumberofbenchmarkexamplesandindustrialcasestud-ies.Withthisnewdirection,weareenteringtheareaofOperationsResearchandArtificialIntelligencewithawell-establishedandextensivelistofexistingtechniques(MILP,constraintp