代价和概率时间自动机上概率有界的成本优化可达性

着重解决代价和概率时间自动机模型的可达性问题，即满足一定概率要求的最小代价问题. 在该模型中搜索满足概率要求的路径，据此路径构造相应的代价时间自动机，求解此路径的最小代价，从而求得满足概率要求的总的最小代价. 另外，通过扩展代价和概率时间自动机模型，得到多代价和概率时间自动机. 相应的可达性问题，即满足一定概率要求的符合辅助成本约束的主成本最小代价问题，也可类似地得到解决.

Cost Optimized Reachability with Probability Bound in Priced Probabilistic Timed Automata

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 extendedto 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.