Nicolas Markey

Abstract

We investigate a number of problems related to infinite runs of weighted timed automata, subject to lower-bound constraints on the accumulated weight. Closing an open problem from [Bouyer et al., "Infinite runs in weighted timed automata with energy constraints", FORMATS'08], 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 know initial credit. We show that the related problem of existence of an initial credit for which there ex- ist 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. Finally, 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.

@inproceedings{qest2012-BLM,
  author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
                         Markey, Nicolas},
  title =               {Lower-Bound Constrained Runs in Weighted Timed
                         Automata},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'12)},
  acronym =             {{QEST}'12},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {128-137},
  year =                {2012},
  month =               sep,
  doi =                 {10.1109/QEST.2012.28},
  abstract =            {We investigate a number of problems related to
                         infinite runs of weighted timed automata, subject to
                         lower-bound constraints on the accumulated weight.
                         Closing an open problem from [Bouyer
                         \textit{et~al.}, {"}Infinite runs in weighted timed
                         automata with energy constraints{"}, FORMATS'08], 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 know
                         initial credit. We show that the related problem of
                         existence of an initial credit for which there ex-
                         ist 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. Finally, 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.},
}