Is Prism able to check CTL property with providing counter examples?

[Terry Zhou]

Hi 

Can anyone tell me if I can use PRISM to model check CTL property against the DTMC model, with getting counter examples?

Or if PRISM does NOT do this, can you recommend a CTL model checking tool that can provide counter examples? 

Many thanks,

Terry

[Dave Parker]

Hi Terry,

PRISM has partial support for CTL model checking with counterexamples.
See here:

http://www.prismmodelchecker.org/manual/PropertySpecification/Non-probabilisticProperties

If that doesn't suffice, NuSMV and SPIN are well known model checkers
that support this (for non-probabilistic models), and I'm sure there are
others.

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.

[Terry Zhou]

Hi Dave,

Thank you for the information.
BTW, does PRISM have a plan to enhance the counterexample generation for
support more types of properties?

cheers,
Terry

[Dave Parker]

Hi Terry,

We have generation of some types of probabilistic counterexample implemented, and hope to get that into the main release soon.

If you meant other types of CTL counterexamples, I'm not sure what else we would add, but feel free to tell us what would be useful to you.

Best wishes,

Dave.