Model Checking MC/MDP for Many Initial States

[Matthew Cleaveland]

Hi Everyone,

I am working with an MC/MDP model. I want to compute the maximum probability of the model reaching an unsafe state within T steps for a large number of initial states. Right now I just run a separate instance of model checking for each initial state. But I imagine that PRISM is doing a lot of redundant work under the hood (e.g. compute the probability of states reaching the unsafe state within T-1 steps).

So is there a way to have PRISM store/reuse/output these intermediate values? More generally, is there a faster way to do this than just running a separate model checking instance for each initial state?

Thanks,
Matthew

[Gethin Norman]

Hi Matthew,

you can use init … endinit to specify a set of initial states and you can then use filters to get the probabilities for multiple states.

See

https://www.prismmodelchecker.org/manual/ThePRISMLanguage/MultipleInitialStates
https://www.prismmodelchecker.org/manual/PropertySpecification/Filters

this should reduce work and speed things up (as long as the model does not become too large)

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/CAG6e_ZuFtWz6gWSL%2BSH6U0QB66YUZi5yzyJF2P2dKsPaKF0Vuw%40mail.gmail.com.

[Dave Parker]

Hi Matthew,

Just to add to that: If the states you are interested in are already
reachable, you do not need to use init … endinit (because that may limit
the solution methods available to you). The filters that Gethin
mentioned will by default display the results for all reachable states
(at least those where the value is non-zero). E.g.:

prism dice.pm -pf 'filter(print,P=?[F d=6])'

You can also use -exportvector to get a file containing the values for
all states (zero or non-zero). E.g.:

prism dice.pm -pf 'P=?[F d=6]' -exportvector vec.txt

Best wishes,

Dave