Automatic verification of real-time systems with discrete probability distributions