Counterexample generation in PRISM

[David Sanan]

Hi,

May i ask whether PRISM can generate a counterexample, please?

Thank you very much, I look forward to your response.

Best regards

[Dave Parker]

Hi David,

We don't current support counterexamples for probabilistic properties
I'm afraid. We just provide non-probabilistic counterexamples (traces)
for violations of (non-probabilistic) CTL formulae:

https://prismmodelchecker.org/manual/PropertySpecification/Non-probabilisticProperties

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 view this discussion, visit https://groups.google.com/d/msgid/
> prismmodelchecker/a71db0bb-7ea0-4535-8454-
> ca9e91ebdfb6n%40googlegroups.com <https://groups.google.com/d/msgid/
> prismmodelchecker/a71db0bb-7ea0-4535-8454-
> ca9e91ebdfb6n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Dave Parker]

Hi David,

If you're working with MDPs, then the optimal (or worst-case)
policy/strategy provides quite useful information. You can explore this
in the simulator in the graphical user interface or export it to a file.
See here for some details:

https://prismmodelchecker.org/manual/RunningPRISM/Strategies

and feel free to ask here if there are questions.

Best wishes,

Dave

> Dear Prof. Dve,
> Thank you very much for your response.
> If an MDP does not satisfy the probabilistic properties, what
> information can be provided by PRISM for analysis, please?
> Thanks again.
> Best regards
>
> Dave Parker <david....@cs.ox.ac.uk <mailto:david....@cs.ox.ac.uk>>
> 于2024年11月27日周三 17:12写道：

>
> Hi David,
>
> We don't current support counterexamples for probabilistic properties
> I'm afraid. We just provide non-probabilistic counterexamples (traces)
> for violations of (non-probabilistic) CTL formulae:
>
> https://prismmodelchecker.org/manual/PropertySpecification/Non-

> probabilisticProperties <https://prismmodelchecker.org/manual/
> PropertySpecification/Non-probabilisticProperties>

>
> Best wishes,
>
> Dave
>
> > Hi,
> > May i ask whether PRISM can generate a counterexample, please?
> > Thank you very much, I look forward to your response.
> > Best regards
> >
> > --
> > 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:prismmodelchecker%2Bunsu...@googlegroups.com>
> > <mailto:prismmodelchec...@googlegroups.com
> <mailto:prismmodelchecker%2Bunsu...@googlegroups.com>>.

> > To view this discussion, visit https://groups.google.com/d/msgid/

> <https://groups.google.com/d/msgid/>
> > prismmodelchecker/a71db0bb-7ea0-4535-8454-
> > ca9e91ebdfb6n%40googlegroups.com <http://40googlegroups.com>
> <https://groups.google.com/d/msgid/ <https://groups.google.com/d/
> msgid/>
> > prismmodelchecker/a71db0bb-7ea0-4535-8454-
> > ca9e91ebdfb6n%40googlegroups.com?
> utm_medium=email&utm_source=footer <http://40googlegroups.com?
> utm_medium=email&utm_source=footer>>.
>