Nicolas Markey

Abstract

Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.

@inproceedings{cav2016-BCM,
  author =              {Bouyer, Patricia and Colange, Maximilien and Markey,
                         Nicolas},
  title =               {Symbolic Optimal Reachability in Weighted Timed
                         Automata},
  editor =              {Chaudhuri, Swarat and Farzan, Azadeh},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'16)},
  acronym =             {{CAV}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9779},
  pages =               {513-530},
  year =                {2016},
  month =               jul,
  doi =                 {10.1007/978-3-319-41528-4_28},
  url =                 {http://arxiv.org/abs/1602.00481},
  abstract =            {Weighted timed automata have been defined in the
                         early 2000's for modelling resource-consumption or
                         -allocation problems in real-time systems. Optimal
                         reachability is decidable in weighted timed
                         automata, and a symbolic forward algorithm has been
                         developed to solve that problem. This algorithm uses
                         so-called priced zones, an extension of standard
                         zones with cost functions. In order to ensure
                         termination, the algorithm requires clocks to be
                         bounded. For unpriced timed automata, much work has
                         been done to develop sound abstractions adapted to
                         the forward exploration of timed automata, ensuring
                         termination of the model-checking algorithm without
                         bounding the clocks. In this paper, we take
                         advantage of recent developments on abstractions for
                         timed automata, and propose an algorithm allowing
                         for symbolic analysis of all weighted timed
                         automata, without requiring bounded clocks.},
}