Probabilistic distributions in PRISM

[Sara Himmiche]

Hi, 

I was wondering if with PRISM it is possible to model different probabilistic distributions or is it made for discrete probabilities only, and also how to model the fact that a variable is related to a special distribution. I use PTAs in PRISM.

I hope to find answers here.

Thanks in advance.

Sara.

[Gethin Norman]

Sara,

only discrete distributions are possible for PTAs (and also for DTMCs and MDPs). CTMCs allow for exponential delays and more general distributed delays can be modelled using phase type distributions (however this is often complex and will cause a rapid increase in the state space). For example how to model deterministic delays with exponential distributions is explained at the end of the frequently asked questions page:

http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMModelling

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 post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.