Nicolas Markey

Résumé

Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language (or trace)? We show that these problems are undecidable both for general PTA, and even for the restricted class of L/U-PTA. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA.

@inproceedings{formats2015-AM,
  author =              {Andr{\'e}, {\'E}tienne and Markey, Nicolas},
  title =               {Language Preservation Problems in Parametric Timed
                         Automata},
  editor =              {Sankaranarayanan, Sriram and Vicario, Enrico},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'15)},
  acronym =             {{FORMATS}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9268},
  pages =               {27-43},
  year =                {2015},
  month =               sep,
  doi =                 {10.1007/978-3-319-22975-1_3},
  abstract =            {Parametric timed automata (PTA) are a powerful
                         formalism to model and reason about concurrent
                         systems with some unknown timing delays. In this
                         paper, we address the (untimed) language- and
                         trace-preservation problems: given a reference
                         parameter valuation, does there exist another
                         parameter valuation with the same untimed language
                         (or trace)? We show that these problems are
                         undecidable both for general PTA, and even for the
                         restricted class of L/U-PTA. On the other hand, we
                         exhibit decidable subclasses: 1-clock PTA, and
                         1-parameter deterministic L-PTA and U-PTA.},
}