Difference between CTMC, DTMC, and MDP

Question

I've been reading the Handbook of Model Checking recently; I'm especially interested in probabilistic model checking, so have been led to the PRISM model checker. For background, I am very familiar with TLA+ and use of its model checker for safety & liveness properties. My goal is to specify & model-check a simple probabilistic consensus protocol like snowflake (pdf).

One thing which confuses me is the difference between Markov Decision Problems (MDPs), Discrete-Time Markov Chains (DTMCs), and Continuous-Time Markov Chains (CTMCs). I'd assumed probabilistic model-checking was just a way of assigning weights to nondeterministic steps; things like network messages being dropped, nodes crashing, random choice of nodes to send messages to, that sort of thing. Why are these different models necessary? What can you express in one but not the other?

I see on this page the documentation says:

In every state of the model, there is a set of commands (belonging to any of the modules) which are enabled, i.e. whose guards are satisfied in that state. The choice between which command is performed (i.e. the scheduling) depends on the model type.

But aren't we model-checking it in some way where it doesn't matter which action is "performed", since both possible transitions are checked via some breadth-first search mechanism?

Answer 1

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:

1. Are the transitions dependent on an action (e.g. user input, or some environment interaction)
2. 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.