<p>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?"</p>

<p>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:</p>

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

<p>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.</p>

<p>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).</p>

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

<p>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.</p>

CC BY-SA 4.0
2019-10-07T14:31:41.143Z
So to model communicating sequential processes (like what is often modeled with TLA+) you'd probably use a CTMC? Where each process executes at an independent rate and their action is determined by what communication they receive from one another.
ahelwer
CC BY-SA 4.0
2019-10-08T11:31:55.243Z
If you have several processes, each modeled with some finite state system, you usually model their interaction as a product system. Then, the transition probabilities are determined by however the systems work (there is no canonical definition for the product of probabilistic systems).
If, however, you want each state to represent a process, and only model the communication, then CTMCs might be in order, but keep in mind that usually CTMCs assume an exponential distribution on their signals, which might not be what you want.
Shaull
CC BY-SA 4.0
2019-10-06T06:00:03.293Z
2019-10-06T06:00:03.293Z
Shaull
<p>I've been reading the <a href="https://www.springer.com/gp/book/9783319105741" rel="nofollow noreferrer">Handbook of Model Checking</a> recently; I'm especially interested in probabilistic model checking, so have been led to the <a href="https://www.prismmodelchecker.org/" rel="nofollow noreferrer">PRISM</a> model checker. For background, I am very familiar with TLA+ and use of its model checker for safety &amp; liveness properties. My goal is to specify &amp; model-check a simple probabilistic consensus protocol like snowflake (<a href="https://ipfs.io/ipfs/QmUy4jh5mGNZvLkjies1RWM4YuvJh5o2FYopNPVYwrRVGV" rel="nofollow noreferrer">pdf</a>).</p>

<p>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?</p>

<p>I see on <a href="http://prismmodelchecker.org/manual/ThePRISMLanguage/ParallelComposition" rel="nofollow noreferrer">this page</a> the documentation says:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>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?</p>

CC BY-SA 4.0
2019-10-08T14:32:45.597Z
Similar question on the CS StackExchange: https://cs.stackexchange.com/q/40689/110483
ahelwer
<model-checking><markov-chains><formal-methods><temporal-logic><linear-temporal-logic>
Difference between CTMC, DTMC, and MDP
ahelwer
# Difference between CTMC, DTMC, and MDP

(Asked by: username_0 on 2019-10-06)

I've been reading the [Handbook of Model Checking](https://www.springer.com/gp/book/9783319105741) recently; I'm especially interested in probabilistic model checking, so have been led to the [PRISM](https://www.prismmodelchecker.org/) 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](https://ipfs.io/ipfs/QmUy4jh5mGNZvLkjies1RWM4YuvJh5o2FYopNPVYwrRVGV)).

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](http://prismmodelchecker.org/manual/ThePRISMLanguage/ParallelComposition) 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?

**Tags:** model-checking, markov-chains, formal-methods, temporal-logic, linear-temporal-logic
> **Comments:**
> **username_0**: Similar question on the CS StackExchange: https://cs.stackexchange.com/q/40689/110483  

---

## 1 answers

### Answer by username_1 on 2019-10-06. Score: 3 | Accepted answer

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.

> **Comments:**
> **username_0**: So to model communicating sequential processes (like what is often modeled with TLA+) you'd probably use a CTMC? Where each process executes at an independent rate and their action is determined by what communication they receive from one another.  
> **username_1**: If you have several processes, each modeled with some finite state system, you usually model their interaction as a product system. Then, the transition probabilities are determined by however the systems work (there is no canonical definition for the product of probabilistic systems). If, however, you want each state to represent a process, and only model the communication, then CTMCs might be in order, but keep in mind that usually CTMCs assume an exponential distribution on their signals, which might not be what you want.  

---

