@InProceedings{SwaminathanFraenzleFORMATS09,
  author =       {Martin Fr{\"a}nzle and Mani Swaminathan},
  title =        {Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata},
  booktitle =    {The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2009)},
  editor =       {J. Ouaknine and F. Vaandrager},
  year =         {2009},
  month =        {September},
  publisher =    {Sringer Verlag},
  subproject =   {R1},
  access =       {open},
  bibtex =       {fraenzle.formats09.bib},
  pdf =          {fraenzle.formats09.pdf},
  abstract =     {We investigate the optimum reachability problem 
                  for Multi-Priced Timed Automata (MPTA) that admit both 
                  positive and negative costs on edges and locations, 
                  thus bridging the gap between the results of Bouyer 
                  et al. (2007) and of Larsen and Rasmussen (2008). 
                  Our contributions are the following: (1) We show that 
                  even the location reachability problem is undecidable 
                  for MPTA equipped with both positive and negative costs, 
                  provided the costs are subject to a bounded budget, in 
                  the sense that paths of the underlying Multi-Priced 
                  Transition System (MPTS) that operationally exceed the 
                  budget are considered as not being viable. This undecidability 
                  result follows from an encoding of Stop- Watch Automata using 
                  such MPTA, and applies to MPTA with as few as two cost variables, 
                  and even when no costs are incurred upon taking edges. 
                  (2) We then restrict the MPTA such that each viable 
                  quasi-cyclic path of the underlying MPTS incurs a minimum 
                  absolute cost. Under such a condition, the location reachability 
                  problem is shown to be decidable and the optimum cost is shown to 
                  be computable for MPTA with positive and negative costs and a 
                  bounded budget. These results follow from a reduction of the optimum 
                  reachability problem to the solution of a linear constraint system 
                  representing the path conditions over a finite number of viable paths 
                  of bounded length.},
}