Automatic verification and synthesis of stochastic processes