  Timed automata are the formal model for real-time systems. Extensions with
discrete probabilistic branching have been considered in the literature and
successfully applied. Probabilistic timed automata (PTA) do require all
branching probabilities and clock constraints to be constants. This report
investigates PTA in which this constraint is relaxed: both branching
probabilities and clock constraints can be parametric. We formally define this
PTA variant and define its semantics by an uncountable parametric Markov
Decision Process (pMDP). We show that reachability probabilities in parametric
L/U-PTA can be reduced to considering PTA with only parametric branching
probabilities. This enables the usage of existing techniques from the
literature. Finally, we generalize the symbolic backward and digital clock
semantics of PTA to the setting with parametric probabilities and constraints.
