How to check Senstivity of parameters

[Sai Aka]

Hey PRISM Forum,

I am a cryptographer, and I am new to PRISM. I am using it to verify a security protocol with a bunch of randomness associated with it. This randomness is fixed and estimated by reasoned statistical models. Now I have built a DTMC regarding this, and this DTMC has different states. My main focus here is the success state. I have PCTL, and I am getting the required results, but due to the large number of parameters present, I am having a hard time visualizing the results. I am thinking something along the lines of using machine learning on the generated PRISM results to extract feature importance, as this would give insights on how parameters influence different results. But I am a bit unwilling to run analysis on syntetic data. My queries are: Do we have any features for estimating how parameters affect the final results? Also, what is the typical way we show the results we get through PRISM? I would really appreciate your response; even short insights will help me a lot. 

 

Regards,

Sai Aka

[Dave Parker]

Hi Sai,

First, on "what is the typical way we show the results we get through
PRISM": it's very common that the output of a PRISM analysis is
numerical (e.g. the probability of "success") and also that it depends
on one or more parameters in the model. If the number of parameters is
relatively small, it is therefore common to compute/plot the result of
the query for a range of suitable values of these parameter(s) and see
what dependencies/trends exist and how sensitive the results are to
these varations. In PRISM teminology (notably when using the GUI), these
are called "experiments" [1], and are achieved by leaving the value of
one or more constants unspecified in the model and then defining a
single value or range of values at the time of verification.

A related alternative is to do parameteric model checking [2]. That will
give you a symbolic expression for the query in terms of the parameters.
This is more powerful, but also much more expensive to compute and so
will likely only be feasible for a relatively small number of
parameters, and a smaller state space for the DTMC.

If you have many parameters and just want to do a kind of sensitivity
analysis, you could try interval Markov chains [3,4]. That lets you
specify the transition probabilities in your model as intervals (which
could arise by considering a range of parameter values). You can then
ask for the minimum and maximum probability (e.g., of "success") over
all possible probabilities in those intervals.

I hope that gives you a few ideas. Please feel to ask further questions.

Best wishes,

Dave

[1] https://www.prismmodelchecker.org/manual/RunningPRISM/Experiments
[2]
https://www.prismmodelchecker.org/manual/RunningPRISM/ParametricModelChecking
[3]
https://www.prismmodelchecker.org/manual/ThePRISMLanguage/UncertainModels
[4]
https://www.prismmodelchecker.org/manual/PropertySpecification/UncertainModels

> --
> 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
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/e0ba21e9-8b6a-4b30-b2c0-1c250cd7e477n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/e0ba21e9-8b6a-4b30-b2c0-1c250cd7e477n%40googlegroups.com?utm_medium=email&utm_source=footer>.