Wrong rate combination in CTMCs?

[c-kloukinas]

Hi, I'm trying to model M/M/s/K queues with Prism and I've stumbled upon a behaviour I do not understand. I'm uploading two models that I expected to behave exactly the same but they don't. Their difference is in the server guard. Right asks that there are at least N requests waiting (waiting>=N) for server N to fire, while wrong asks just that there's some request waiting (waiting>0). I don't understand why with the wrong model prism considers that the total service rate from the state where waiting=1 is the server rate times the number of servers - only one of them will manage to fire and serve the request. The only difference that I'd expect between the two models is that the choice of server is more non-deterministic in the wrong model than the right one.

The dot diagrams of the transitions show the difference - no need for experiments really.

Nevertheless, I've also tested them with "S=? [ (waiting=n) ]", to compute the probability that there are n requests waiting (for n=0:1:Capacity), and the right model produced the answers I expected, based on the formulae I got from: http://profs.degroote.mcmaster.ca/ads/parlar/courses/o711/documents/Formulas-HL-9e-2011-10-31.pdf

Best, Christos

MMcK-right.prism.pp.gz MMcK-wrong.prism.pp.gz

[kleinj]

To get a sense what's going on in these kinds of situations, the simulator in xprism is quite helpful, as it let's you play around with the behavior and you can see the different actions.

From having a quick look at the models, it seems that looking at it as follows might make sense: As soon as a req comes in (that won't get lost), a server starts working on in. So, there are always exactly waiting servers processing. Thus, there is a race between those servers which finishes first srvX (or if another request comes in in the mean time). This is modelled in your "right" variant.

In your "wrong" variant, all the servers are always processing, i.e., there are more servers processing than there are requests and all are racing which finishes first. I.e., a request may be processed by more than one server and, in particular, it might finish faster on one than on the others.

[c-kloukinas]

Hi, I actually don't get much info by simulating the wrong model - just a long trace of req,srv pairs.

I don't understand the explanation you provide either. If a request may be processed by more than one server in the wrong model, then to me this says that: 1) transitions are not atomic, so multiple transitions can fire at the same time (indeed, multiple transitions of the same module!!!) ; and 2) when waiting>=s (s is the number of servers), then the rate of servicing shouldn't be ms, because some of the servers may be serving the same request simultaneously, so ms should be just a max rate.

Neither of these two make sense to me, which makes me strongly suspect that Prism is actually translating the "wrong" model incorrectly. It should translate it just like it does for the "right" model. In short, I claim that: a) you cannot service a request that is not there; and b) only one server can service a request - transitions are atomic. Given these two, I expect Prism to treat the two models the same - it doesn't.

[kleinj]

Okay, to clarify, let's say that there are 3 levels:

1. what you intend to model ("a request is only processed by one server"),
2. your model, but interpreted with the semantics of your scenario ("the state variable waiting corresponds to the requests that are currently processed"),
3. the actual PRISM model / CTMC ("there is some state s, which has rate r to go to some other state", "there are multiple actions enabled in some state, with rates r1, r2, r3").

I was trying to give you an explanation on level 2 of what your model actually does at level 3. I see no indication that PRISM (which only operates at level 3, similar to a compiler/iterpreter for a program) behaves in a wrong way, i.e., it translates the model to a CTMC as described in http://www.prismmodelchecker.org/manual/ThePRISMLanguage/CTMCs.

So, let's say you instantiate your models with c=3 and srvRate=reqRate=2. Then, in the simulator (see 'manual exploration'), in the first step action req1 is available with rate 2. In the next step, in the right model you have two actions that are available, req1 (~another request arrives) and srv1 (~the first request is finished). Both have rate 2 and there is a race which of them happens first. Let's say there is another req1. Now, there are 3 actions enabled, req1, srv1, srv2, all racing.

In your wrong model, as soon as the first req1 happened, now there are 3 additional actions enabled srv1, srv2, srv3. All 4 actions race which happens first. This is at level 3, and PRISM simply translates that into the combined rate for going from waiting=1 to waiting=0. Note that none of the 4 enabled actions can happen at the same time, but the expected time until one of them happens will be shorter than if you have fewer enabled actions.

Now, the question is how to interpret that at level 2? If you keep the interpretation from the right model (action srvX happening means that a request is finished processing), then you have now modelled a situation where, if you have one request (waiting=1), each of the 3 servers can finish processing the request (leading to waiting=0).

[c-kloukinas]

Thank you, this makes more sense! It seems that I was thinking in terms of a non-deterministic choice, instead of a race-condition - find it difficult to think in terms of the latter, as I have mainly used non-probabilistic model-checkers so far... :-( Tricky... looks like I'll essentially have to resolve non-deterministic choices manually to get correct models. Any reason for choosing this particular semantics?

[kleinj]

Well, if you have multiple possible outcomes (successor states, action taken) with individual rates, then the racing semantics is quite natural, I think. If you allow non-deterministic choice you leave the CTMC world and would have to switch to CTMDPs or Markov automata for the underlying model.