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.

翻译：时间自动机是实时系统的形式化模型。文献中已考虑并成功应用了带有离散概率分支的扩展。概率时间自动机要求所有分支概率和时钟约束均为常数。本报告研究了放宽这一约束的概率时间自动机：分支概率和时钟约束均可参数化。我们正式定义了这种概率时间自动机变体，并通过不可数参数马尔可夫决策过程定义了其语义。研究表明，参数化L/U-PTA中的可达概率可简化为仅考虑参数化分支概率的PTA，从而能够利用文献中的现有技术。最后，我们将PTA的符号反向语义和数字时钟语义推广到具有参数化概率与约束的场景中。