# What's decidable about parametric timed automata?

## TL;DR

This paper surveys the decidability landscape of parametric timed automata, highlighting which restrictions lead to decidability and discussing open problems and related formalisms.

## Contribution

It provides a comprehensive overview of decision problems for PTAs, emphasizing the impact of various restrictions and identifying open research challenges.

## Key findings

- Decidability is generally lost when bounding time, parameters, or their domains.
- Restrictions like limiting clocks or their use can restore decidability.
- The survey discusses tools and related formalisms for PTAs.

## Abstract

Parametric timed automata (PTAs) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After 25 years of research on PTAs, it is now well-understood that any non-trivial problem studied is undecidable for general PTAs. We provide here a survey of decision and computation problems for PTAs. On the one hand, bounding time, bounding the number of parameters or the domain of the parameters does not (in general) lead to any decidability. On the other hand, restricting the number of clocks, the use of clocks (compared or not with the parameters), and the use of parameters (e.g. used only as upper or lower bounds) leads to decidability of some problems. We also put emphasis on open problems. We also discuss formalisms close to parametric timed automata (such as parametric hybrid automata or parametric interrupt timed automata), and we study tools dedicated to PTAs and their extensions.