Decidable Model Checking of Probabilistic Hybrid Automata