Nicolas Markey

Résumé

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model checking WMTL (LTL with cost-constrained modalities) is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).

@article{lmcs4(2)-BLM,
  author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
                         Markey, Nicolas},
  title =               {Model Checking One-clock Priced Timed Automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {4},
  number =              {2},
  year =                {2008},
  month =               may,
  doi =                 {10.2168/LMCS-4(2:9)2008},
  abstract =            {We consider the model of priced (a.k.a.~weighted)
                         timed automata, an extension of timed automata with
                         cost information on both locations and transitions,
                         and we study various model-checking problems for
                         that model based on extensions of classical temporal
                         logics with cost constraints on modalities. We prove
                         that, under the assumption that the model has only
                         one clock, model-checking this class of models
                         against the logic~WCTL, CTL with cost-constrained
                         modalities, is PSPACE-complete (while it has been
                         shown undecidable as soon as the model has three
                         clocks). We~also prove that model checking WMTL (LTL
                         with cost-constrained modalities) is decidable only
                         if there is a single clock in the model and a single
                         stopwatch cost variable (\textit{i.e.}, whose slopes
                         lie in~\(\{0,1\}\)).},
}