Nicolas Markey

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 with the same set of traces? We show that these problems are undecidable both for general PTA and for the restricted class of L/U-PTA, even for integer-valued parameters, or over bounded time. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA. We also consider robust versions of these problems, where we additionally require that the language be preserved for all valuations between the reference valuation and the new valuation.

@article{lmcs16(1)-ALM,
  author =              {Andr{\'e}, {\'E}tienne and Lime, Didier and Markey,
                         Nicolas},
  title =               {Language-preservation problems in parametric timed
                         automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {16},
  number =              {1},
  year =                {2020},
  month =               jan,
  doi =                 {10.23638/LMCS-16(1:5)2020},
  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 with the same set of traces? We~show that these
                         problems are undecidable both for general PTA and
                         for the restricted class of L{\slash}U-PTA, even for
                         integer-valued parameters, or over bounded time.
                         On~the other~hand, we~exhibit decidable subclasses:
                         1-clock PTA, and 1-parameter deterministic L-PTA and
                         U-PTA. We~also consider robust versions of these
                         problems, where we additionally require that the
                         language be preserved for all valuations between the
                         reference valuation and the new valuation.},
}