@InProceedings{ swaminathanfraenzleformats09,
title = {Revisiting Decidability and Optimum Reachability for
Multi-Priced Timed Automata},
author = {Martin Fr{\"a}nzle and Mani Swaminathan},
booktitle = {The 7th International Conference on Formal Modelling and
Analysis of Timed Systems (FORMATS 2009)},
year = {2009},
editor = {J. Ouaknine and F. Vaandrager},
month = {September},
pages = {149-163},
publisher = {Springer},
series = {Lecture Notes in Computer Science (LNCS)},
volume = {5813},
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.},
access = {open},
bibtex = {fraenzle.formats09.bib},
category = {Real-Time Systems},
conference-long={International Conference on Formal Modeling and Analysis
of Timed Systems},
conference-short={FORMATS},
cross-site = { },
pdf = {fraenzle.formats09.pdf},
subproject = {R1}
}