Nicolas Markey

Abstract

We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from an earlier paper, we show that the existence of an infinite lower-bound-constrained run is–for us somewhat unexpectedly–undecidable for weighted timed automata with four or more clocks.

This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.

Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in PSPACE).

@article{peva73()-BLM,
  author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
                         Markey, Nicolas},
  title =               {Lower-Bound Constrained Runs in Weighted Timed
                         Automata},
  publisher =           {Elsevier},
  journal =             {Performance Evaluation},
  volume =              {73},
  pages =               {91-109},
  year =                {2014},
  month =               mar,
  doi =                 {10.1016/j.peva.2013.11.002},
  abstract =            {We investigate a number of problems related to
                         infinite runs of weighted timed automata (with a
                         single weight variable), subject to lower-bound
                         constraints on the accumulated weight. Closing an
                         open problem from an earlier paper, we show that the
                         existence of an infinite lower-bound-constrained run
                         is--for us somewhat unexpectedly--undecidable for
                         weighted timed automata with four or more
                         clocks.\par This undecidability result assumes a
                         fixed and known initial credit. We show that the
                         related problem of existence of an initial credit
                         for which there exists a feasible run is decidable
                         in PSPACE. We also investigate the variant of these
                         problems where only bounded-duration runs are
                         considered, showing that this restriction makes our
                         original problem decidable in NEXPTIME. We prove
                         that the universal versions of all those problems
                         (i.e, checking that all the considered runs satisfy
                         the lower-bound constraint) are decidable in
                         PSPACE.\par Finally, we extend this study to
                         multi-weighted timed automata: the existence of a
                         feasible run becomes undecidable even for bounded
                         duration, but the existence of initial credits
                         remains decidable (in~PSPACE).},
}