Multi-Objective Adversary Generation Mismatch

amyx...@gmail.com

unread,

Jul 13, 2020, 4:40:51 AM7/13/20

to PRISM model checker

Hello,

I'm having trouble with multi-objective adversary generation.

My model is an MDP and a reward module (MDPmodel.txt). The property I am verifying is "multi(Pmax=? [G (m0=1 & m15=1 & m2387=1 & m2403=1)], R{"numAgents"}min=? [ C ])", so PRISM outputs a series of points (probability, expected reward) along the Pareto front. I'm also exporting the adversaries. For each adversary file, I determine the path and multiply all the probabilities along that path together. That way, I can match the adversary to the correct point on the Pareto front.

The adversary probabilities and Pareto front probabilities match most of the time. However, sometimes the probabilities do not match.

I've attached the PRISM model and adversaries that were generated. Verifying the previously mentioned property, PRISM outputs:

[(0.30428716339152756, 4.121694167440077), (0.0, -0.0), (0.34596138249839214, 4.885753279050772), (0.6339338540543447, 11.745370721857357), (0.6249499133125954, 10.6356054030579), (0.4822001886503896, 7.4159540890835105), (0.5099010505515822, 7.973779480650391), (0.5345909961572378, 8.531604872217269)]

=============

Given each of the nine adversary files, I've calculated the path and total probability (simply multiplying the probability at each timestep together):

adv1.tra

Path: [0, 1, 32, 11]

Probability: 0.34596179391436654

adv2.tra

Path: [0, 3, 26, 11]

Probability: 0.4241146927428122

adv3.tra

Path: [0, 29, 32, 24]

Probability: 0.6249495900596912

adv4.tra

Path: [0, 1, 26, 11]

Probability: 0.3042874017931711

adv5.tra

Path: [0, 1, 32, 11]

Probability: 0.34596179391436654

adv6.tra

Path: [0, 3, 32, 22]

Probability: 0.5099007970900321

adv7.tra

Path: [0, 29, 32, 24]

Probability: 0.6249495900596912

adv8.tra

Path: [0, 3, 32, 11]

Probability: 0.48220031148866505

adv9.tra

Path: [0, 3, 32, 24]

Probability: 0.534590699889220

=======

Highlighted are the Pareto front points that have no corresponding adversary files, and vice-versa. This does not make sense to me - why there would be any Pareto points/adversaries that do not match? am I calculating the probabilities incorrectly? There are no unmatched points when I set the total time (constant finalTime in the PRISM model file) to be 2. Currently, the total number of timesteps is 3.

Attached is the MDP model (MDPmodel.txt) and a zip file of the nine adversary files. For ease of understanding the model, I've also attached a much simpler MDP (MDPmodel_simple.txt) that has the same overall structure. The simple model does not have this mismatch issue.

(Note: not sure if this is related, but adv3 and adv7 generate the same path, which I also do not know why PRISM would output).

Any help or insight would be appreciated, thank you.

adversaries.zip

MDPmodel_simple.txt

MDPmodel.txt

Dave Parker

unread,

Jul 16, 2020, 6:25:06 AM7/16/20

to prismmod...@googlegroups.com, amyx...@gmail.com

Hi Amy,

Thanks for reporting this. I've looked into it. The values for the
Pareto curve seem to be correct - it's just a problem with the adversary
generation (this is quite tricky to get right when there is a mixture of
min/max objectives, as here).

For info, regarding adv3 and adv7 being the same: PRISM generates the
Pareto curve by doing a search over different weighted sums of the
objectives, which finds corner points on the curve. Different weights
can end up generating the same corner point (indeed, otherwise, it might
not converge), so that is why you see the same points more than once.

Any, I pushed a fix to the main repo:

https://github.com/prismmodelchecker/prism

For me, that changed adv2 to one that I think is now correct, but it
would be good to know if this fixes things for you.

Best wishes,

Dave

On 13/07/2020 02:58, amyx...@gmail.com wrote:
> Hello,
>
> I'm having trouble with multi-objective adversary generation.
>
> My model is an MDP and a reward module (MDPmodel.txt). The property I am
> verifying is "multi(Pmax=? [G (m0=1 & m15=1 & m2387=1 & m2403=1)],
> R{"numAgents"}min=? [ C ])", so PRISM outputs a series of points
> (probability, expected reward) along the Pareto front. I'm also
> exporting the adversaries. For each adversary file, I determine the path
> and multiply all the probabilities along that path together. That way, I
> can match the adversary to the correct point on the Pareto front.
>
> The adversary probabilities and Pareto front probabilities match most of
> the time. However, sometimes the probabilities do not match.
>
> I've attached the PRISM model and adversaries that were generated.
> Verifying the previously mentioned property, PRISM outputs:
>

> [(0.30428716339152756, 4.121694167440077),**(0.0, -0.0),
> (0.34596138249839214, 4.885753279050772), (*0.6339338540543447*,
> 11.745370721857357)*,* (0.6249499133125954,
> 10.6356054030579),**(0.4822001886503896, 7.4159540890835105),

> (0.5099010505515822, 7.973779480650391), (0.5345909961572378,
> 8.531604872217269)]
>
> =============
> Given each of the nine adversary files, I've calculated the path and
> total probability (simply multiplying the probability at each timestep
> together):
>
> adv1.tra
> Path: [0, 1, 32, 11]
> Probability: 0.34596179391436654
>
> adv2.tra
> Path: [0, 3, 26, 11]

> Probability: *0.4241146927428122*

> --
> 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/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com?utm_medium=email&utm_source=footer>.

Amy Fang

unread,

Jul 16, 2020, 3:04:56 PM7/16/20

to PRISM model checker

Hi Dave,

Thanks for the fix and the quick response.

The issue with adv2 has been resolved on my end as well, but the Pareto point (0.6339338540543447, 11.745370721857357) still does not correspond to any of the adversaries.

I've tested it on a couple other models (similar structure, different number of states and probabilities) - I've noticed that the pattern now seems to be that only the highest probability point on the Pareto curve does not have a corresponding adversary.

Let me know if that's also an issue you're having, or if something is wrong on my end.

Thanks,
Amy

> an email to prismmod...@googlegroups.com
> <mailto:prismmodelchecker+unsub...@googlegroups.com>.

Dave Parker

unread,

Jul 17, 2020, 5:58:09 AM7/17/20

to prismmod...@googlegroups.com, Amy Fang

Hi Amy,

If you look at the output carefully, you'll see that there are also some
preliminary computations, one per objective, to get the end points of
the Pareto curve. We were not doing strategy export for those. I've just
added it (again, pushed to master on github). See if that works for you.
Note that this will shift the numbering of the adv files, since that
preliminary computation will now create adv1.tra and adv2.tra.

Best wishes,

Dave

> > an email to prismmod...@googlegroups.com <javascript:>
> > <mailto:prismmodelchec...@googlegroups.com
> <javascript:>>.

> > To view this discussion on the web, visit
> >
> https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com>
>
> >

> <https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
>
> --
> 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/7a574fd3-59e2-410b-94a6-9d486ff8b685o%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/7a574fd3-59e2-410b-94a6-9d486ff8b685o%40googlegroups.com?utm_medium=email&utm_source=footer>.

Amy Fang

unread,

Jul 17, 2020, 12:58:49 PM7/17/20

to PRISM model checker

Yes, this seems to work for me now. Thank you so much for all your help!

Best,

Amy

> > <mailto:prismmodelchecker+unsub...@googlegroups.com

> <javascript:>>.
> > To view this discussion on the web, visit
> >
> https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com>
>
> >
> <https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/prismmodelchecker/fb293745-a8ca-482c-a363-93a71a032c92o%40googlegroups.com?utm_medium=email&utm_source=footer>>.
>
>
> --
> 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 prismmod...@googlegroups.com
> <mailto:prismmodelchecker+unsub...@googlegroups.com>.

Reply all

Reply to author

Forward