"ERROR:Probabilities sum to less than one,strengthen guard" while analysing a very simple model for Bell States.

[Anuroop Kuppam]

I wrote a very simple model for EPR pair measurement or Bell states. It is as follows:

dtmc

module EPRpair

EPRstate : [1..4];

[initi] true -> 1/4 : (EPRstate'=1) + 1/4 : (EPRstate'=2) + 1/4 : (EPRstate'=3) + 1/4 : (EPRstate'=4);

[firstmeas] true -> (EPRstate' = EPRstate);

[secondmeas] true -> (EPRstate' = EPRstate);

endmodule

module Observer

comp_state : [0..2] init 0;

outcome1 : [0..2];

outcome2 : [0..2]; //value of 2 represents an unknown state.

[initi] (comp_state=0) -> (comp_state'=1); 

[firstmeas] (comp_state=1) -> 1/2 : (outcome1'=0) & (comp_state'=2) + 1/2 : (outcome1'=1) & (comp_state'=2);

[secondmeas] (comp_state=2) & ((EPRstate=1) | (EPRstate=2)) -> (outcome2'=1-outcome1) & (comp_state'=2);

[secondmeas] (comp_state=2) & ((EPRstate=3) | (EPRstate=4)) -> (outcome2'=outcome1) & (comp_state'=2);

endmodule

However when I try to verify the model with property P=? [ ((comp_state=2)&(outcome1=1))=>((comp_state=2)&(outcome2=1)) ] ,

It gave me can error stating:

Probabilities in command 3 of module "Observer" sum to less than one (e.g. 0.0) for some states. Perhaps some of the updates give out-of-range values. One possible solution is to strengthen the guard (line 19, column 1).

How do I resolve this.

Thanks.

[Marcin Copik]

Hi Anuroop,

the update "outcome2' = 1 - outcome1" may give values out of range for the variable outcome2, when outcome1 is equal to 2 - new value of outcome2 will be -1. It's probably a mistake in the model, because the transition to a non-existing state doesn't make any sense.

Best regards,

Marcin

--
You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchecker+unsubscribe@googlegroups.com.
To post to this group, send email to prismmodelchecker@googlegroups.com.
Visit this group at http://groups.google.com/group/prismmodelchecker.
For more options, visit https://groups.google.com/d/optout.

[Anuroop Kuppam]

Thanks Marcin.

To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
To post to this group, send email to prismmod...@googlegroups.com.