  This paper proposes an algorithm to maximize reachability probabilities for
rectangular automata with random clocks via a history-dependent prophetic
scheduler. This model class incorporates time-induced nondeterminism on
discrete behavior and nondeterminism in the dynamic behavior. After computing
reachable state sets via a forward flowpipe construction, we use backward
refinement to compute maximum reachability probabilities. The feasibility of
the presented approach is illustrated on a scalable model.
