2
$\begingroup$

I'm looking into discrete-time Markov chains (DTMCs) for use in analyzing a probabilistic consensus protocol. One basic thing I haven't been able to figure out is how to model a set of independent processes: consider $N$ processes. These processes will concurrently execute a series of identical instructions labeled $0, 1, 2, 3,$ etc. and all are starting in instruction $0$. When probability is not involved, modeling this is simple: it's a state machine which branches nondeterministically off the start state to $N$ different states, where in each of those $N$ states a different process was the first to execute instruction $0$. What do we do when probability is involved? Do we do the same thing with $N$ states branching from the start state, where the probability of transitioning to each state is $\frac{1}{N}$? As in, it's uniformly random which process was the first one to execute instruction $0$?

Is this like taking the product of the state machines of each process?

I'm using a DTMC here, would I gain anything by moving to a CTMC if I don't care about anything beyond the global order of execution?

Bonus question: assigning probabilities to whichever action is taken first seems like a generalization of the non-probabilistic notion of fairness; if it is, what is the formal definition of this generalized notion of probabilistic fairness?

$\endgroup$
  • $\begingroup$ I don't find your model clear. What do you mean by "probability is involved"? $\endgroup$ – D.W. Oct 20 '19 at 7:00
  • $\begingroup$ Some of the instructions in each process involve choosing a subset of other processes at random to which to send a message. Thus I need to model the probabilistic aspect of the protocol, as in does it terminate with probability greater than some value. With non-probabilistic model checking I can only ask whether a terminating state is reachable, not its probability of being reached. $\endgroup$ – ahelwer Oct 20 '19 at 15:55
1
$\begingroup$

I will again refer to a lecture by Prof. Katoen.

What you need here is a way of combining the DTMCs. The problem is, that a combination of DTMCs does not give you a new DTMC. This is because you want to model the choice which of the $N$ processes proceeds nondeterministically. That is, you don't know anything about which process executes the next instruction.

For this, you have a new kind of probabilistic system - Markov Decision Processes (MDPs). In an MDP, you first choose which action in a state you will take. This action enables a probabilistic distribution (similar to DTMCs) which determines the probability of the next state. Notice that an MDP reduces essentially to a DTMC when only one action is always possible.

So to model your $N$ processes, you would combine their DTMCs, let's say $D_i$ into an MDP where states are of the form $\langle p_1, p_2, \ldots, p_n \rangle $ and in each state there are $N$ actions, denoted $\alpha_i$. If you take action $\alpha_i$, then you go to a state where only $p_i$ changes to $p_i^\prime$ according to the distribution of the process $i$. This way you compose your $N$ processes into one single system very similarly to making a product of state machines.

To analyze the resulting MDP, you can resolve the nondeterminism by all sorts of schedulers. But that this I think out of scope. Nevertheless, you could use a uniformly randomized scheduler as you hinted in you question - then every action is selected with a uniform probability.

$\endgroup$
  • 1
    $\begingroup$ Ah, so were MDPs developed to capture a distinction between probabilistic state transitions due to random choice and probabilistic state transitions due to nondeterminism? $\endgroup$ – ahelwer Oct 21 '19 at 20:34
  • 1
    $\begingroup$ Yes, that is indeed the purpose of MDPs. You need the distinction because processes can interleave in any way. The link to PRISM does not work (refers me to this question again), can you provide a new one? $\endgroup$ – J.Svejda Oct 22 '19 at 10:13
  • $\begingroup$ Oops, here's the link. I discovered something very interesting: if you have multiple actions enabled in a DTMC it branches to them with uniform probability as suggested in my original post, and you can ask what is the exact probability of reaching a given state. With a MDP, you can't ask for exact probability with nondeterministic state machines! Only max & min probability. So the MDP uses nondeterminism to generate a set of behaviors then asks for highest/lowest probability of reaching a state over all behaviors. $\endgroup$ – ahelwer Oct 22 '19 at 13:13
  • 1
    $\begingroup$ Well, yes. It's also what I meant with the "uniformly randomized scheduler". An MDP, given a scheduler that resolves nondeterminism, yields a DTMC. If you assume, that having a uniform probability over actions fits your model, then you don't need to study the nondeterministic behaviour. However, note that in an MDP of your processes, letting run only a single process and none other is fully possible. With a uniformly random scheduler, such behaviour has probability zero. If you want to consider nondeterministic behaviour, then min&max probabilities are actually really helpful. $\endgroup$ – J.Svejda Oct 22 '19 at 14:36
  • 1
    $\begingroup$ In my opinion, min&max, because you want to model any possible behaviour. Imagine, if a livelock between your processes happens with probability zero when the actions are uniformly distributed. This does not mean, that it cannot occur in a distributed system - interleaving of processes is arbitrary, you have no real information about it and cannot assume almost anything. If however you know that the maximal probability of a deadlock is zero, then you have a guarantee that a livelock in your system "almost surely" (this is a technical term) never happens. $\endgroup$ – J.Svejda Oct 22 '19 at 15:01
1
$\begingroup$

One approach is to model it as a composition of $N+1$ processes: a scheduler process, plus your $N$ basic processes. At each time step, the scheduler process selects which basic process will execute next. Your scheduler could be randomized: for instance, at each time step, it could choose which basic process to execute next uniformly at random, if you wanted.

Now the transitions of the entire system, and their probabilities, should be easy to derive. A state of the system is of the form $\langle s_0,s_1,\dots,s_N \rangle$ where $s_0$ is the state of the scheduler and $s_i$ is the state of the $i$th basic process. Each transition might have the form $\langle s_0,\dots,s_N \rangle \to \langle s'_0,s_1,\dots,s_{i-1},s'_i,s_{i+1},\dots,s_N \rangle$ (where $i$ is a deterministic function of $s_0$, and with probability given by the probability of $s_0 \to s'_0$ in the scheduler multiplied by the probability of $s_i \to s'_i$ in the $i$th basic process).

There are probably other ways to model it as well, maybe better ones for all I know. This is just one possibility that occurs to me.

$\endgroup$
  • $\begingroup$ Why do we need a scheduler? $\endgroup$ – ahelwer Oct 20 '19 at 19:29
  • $\begingroup$ @ahelwer, I don't claim that you need it, I am just giving one way that might be helpful. I bet you could model this without a scheduler too. $\endgroup$ – D.W. Oct 20 '19 at 19:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.