Using Backwards Reachability Algorithm

[prana...@gmail.com]

Hello,

I was reading the 'Model Checking for Probabilistic Timed Automata' paper (NPS13) and it talks about PRISM supporting verification via backward reachability methods.

But I couldn't figure out a way to use it. I tried searching the sourcecode, but couldn't find any leads. Is there a version of PRISM which allows one to use this method? Or is there any open-source implementation of the backwards reachability algorithm?

Thanks,
Pranav

[Dave Parker]

Hi Pranav,

I just checked - this is actually still in a separate branch and has not
been pushed into the main release. If you are interested in getting
access to the source, I can send you some details separately.

Best wishes,

Dave.

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