  We propose a new abstract formalism for probabilistic timed systems,
Parametric Interval Probabilistic Timed Automata, based on an extension of
Parametric Timed Automata and Interval Markov Chains. In this context, we
consider the consistency problem that amounts to deciding whether a given
specification admits at least one implementation. In the context of Interval
Probabilistic Timed Automata (with no timing parameters), we show that this
problem is decidable and propose a constructive algorithm for its resolution.
We show that the existence of timing parameter valuations ensuring consistency
is undecidable in the general context, but still exhibit a syntactic condition
on parameters to ensure decidability. We also propose procedures that resolve
both the consistency and the consistent reachability problems when the
parametric probabilistic zone graph is finite.
