Reachability and liveness in parametric timed automata

We study timed systems in which some timing features are unknown parameters.Parametric timed automata (PTAs) are a classical formalism for such systems butfor which most interesting problems are undecidable. Notably, the parametricreachability emptiness problem, i.e., the emptiness of the parameter valuationsset allowing to reach some given discrete state, is undecidable.Lower-bound/upper-bound parametric timed automata (L/U-PTAs) achievedecidability for reachability properties by enforcing a separation ofparameters used as upper bounds in the automaton constraints, and those used aslower bounds. In this paper, we first study reachability. We exhibit a subclass of PTAs(namely integer-points PTAs) with bounded rational-valued parameters for whichthe parametric reachability emptiness problem is decidable. Using this class,we present further results improving the boundary between decidability andundecidability for PTAs and their subclasses such as L/U-PTAs. We then study liveness. We prove that: (1) deciding the existence of at least one parameter valuation for whichthere exists an infinite run in an L/U-PTA is PSpace-complete; (2) the existence of a parameter valuation such that the system has adeadlock is however undecidable; (3) the problem of the existence of a valuation for which a run remains in agiven set of locations exhibits a very thin border between decidability andundecidability.Comment: This manuscript is an extended version of two conference papers published in the proceedings of ICFEM 2016 and ACSD 201