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?