property specification question

[Mridu Nanda]

Hi,

Thanks so much for answering my previous questions on this forum! I have a new problem I was hoping to get some help with. 

Right now, I am trying to compute the probability of reaching a "WIN STATE" in my mdp model. There are some paths in my model that will reach the "WIN STATE", but some other paths that will never reach the "WIN STATE." Ideally, I would like to calculate P=? [F s=WIN_STATE]; however, this is not possible because I am using an mdp model with non-determinism (I am letting the attacker pick certain choices). Therefore my two options are checking Pmin=? [F s=WIN_STATE] or Pmax=? [F s=WIN_STATE]. Neither gives me the desired result: the former, is trivially 0 since I know there exists paths that never "win" and the latter is trivially 1 since I know there exists paths that will always "win."

What type of property should I check for in my mdp model, if I want a probability that means "out of all the possible paths, there are X paths that will result in a WIN STATE"?

Thanks,

Mridu

[Gethin Norman]

Hi Mridu,

if you have an MDP model with non-deterministic choices, then Pmin=?[F s=WIN_STATE] and Pmax=?[F s=WIN_STATE] find the minimum and maximum probabilities over all strategies (i.e. resolutions of the non-deterministic choices). If there is only non-deterministic choices in the model (i.e. no probabilistic choices), then you can change the model to a DTMC and then the non-deterministic choices will be replaced with uniform random choices and P=?[F s=WIN_STATE] will return the fraction of paths that reach the WIN_STATE.

thanks

Gethin

> --
> 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 prismmodelchec...@googlegroups.com.
> To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/80384156-a0bc-4223-8494-76ed33fc4ecan%40googlegroups.com.