Parametric Timed Bisimulation.

Timed automata (TA) constitute a mature formalism for discrete-state/continuous-time behavior of time-critical cyber-physical systems. Concerning the fundamental analysis problem of comparing a candidate implementation against a specification both given as TA, it has been shown that timed trace equivalence is undecidable, whereas timed bisimulation is decidable. However, the limited expressiveness of TA is a serious obstacle in practice such that many TA extensions have been proposed. For instance, parametric timed automata (PTA) incorporate parametric clock constraints with freely-adjustable time intervals thus generalizing the constant time bounds of TA. In this way, PTA constitute a promising theoretical foundation for re-engineering static real-time specifications, originally given as TA, in a generic and customizable way. In this paper, we provide, to the best of our knowledge, the first proposal for lifting the notion of timed bisimulation from TA to PTA. Unfortunately, as PTA are Turing-complete, most interesting semantic properties being decidable for TA (including timed bisimulation), become undecidable for PTA. To tackle this issue, we propose an over-approximation of PTA semantics in terms of plain TA semantics and investigate decidability properties of a promising sub-class of PTA, called L/U-PTA.