Abstract: This paper solves a reachability problem in priced probabilistic timed automata, which is minimal cost ensuring a probabilistic lower bound. Proper paths that ensure a probability bound in the model are searched. The corresponding priced timed automatons based on these paths are then constructed, and minimal costs obtained. This way, the total minimal cost is naturally obtained. Next, a priced probabilistic timed automaton is extended
to a multi-priced probabilistic timed automaton with multiple price variables. A similar reachability problem in the extended model can also be solved, which is minimal cost on primary cost while ensuring probabilistic lower bound and with respect to secondary cost upper bounds.

Key words: timed automata, probability, minimal cost, multiple prices, reachability