Difference between CTMC, DTMC, and MDP
The "probabilistic" element in probabilistic model checking is that the system being checked is probabilistic, not that we add probabilities to an existing deterministic or non-deterministic system.
Thus, what you are checking is whether a probabilistic system satisfies some property. For example "is it true that with probability at least 0.5, the system will reach an error state?"

Now, a probabilistic system is given by a set of states, and transitions between the states. However, this does not give a concrete definition of such systems. Specifically, there are two aspects to be considered:


Are the transitions dependent on an action (e.g. user input, or some environment interaction)
Is time discrete or continuous?


For property 1, if there is no user input, then the system just progresses with time, and is called a Markov Chain (assuming it's behaviour is independent of time). Otherwise, it is called a Markov Decision Process (MDP), where in each step an action is "played", and that determines the probabilities of moving to the next steps.

Now for property 2 - if time is discrete, then at every time point the system progresses. This gives rise to Discrete time Markov chains (DTMC, or often called just MC). If time is continuous, then (after modelling specifically what is meant by that), you get Continuous time Markov chains (CTMC).

You could also speak of continuous time MDPS, although this model is slightly less common. I'm not sure if PRISM supports it.

Different models are used for different settings. For example, CTMCs are common in modelling asynchronous protocols, or chemical reactions, whereas DTMCs are useful for synchronous probabilistic systems.