Negative reward

76 views
Skip to first unread message

Mark

unread,
Nov 19, 2017, 10:43:59 AM11/19/17
to PRISM model checker
Hi

It is known that PRISM does not support negative reward. Is there any othrt probabilistic model checker that accepts prism language as input and also accepts negative rewards in states?

Dave Parker

unread,
Nov 19, 2017, 1:43:28 PM11/19/17
to prismmod...@googlegroups.com, dine...@gmail.com
What kind of reward property do you want to check? If you want an
instantaneous property, e.g. R=?[I=k] "the expected state reward at time
step k", it should be doable. Similarly, for cumulative properties where
the rewards are all negative, it is possible. But the case where a
mixture of positive and negative rewards are accumulated cannot be done
right now.

Best wishes,

Dave

Mark

unread,
Nov 19, 2017, 1:47:53 PM11/19/17
to PRISM model checker
Unfortunately, I am trying to model heating and cooling (properties are in cumulative reward format), so both positive and negative reward will be required. Seems like the mixture is not doable, any future support coming for this ?

Dave Parker

unread,
Nov 19, 2017, 2:11:37 PM11/19/17
to prismmod...@googlegroups.com, dine...@gmail.com
Thinking about it, we could potentially add support for Markov chains,
but I don't know a good general algorithm to tackle this class of
problem for Markov decision processes. What model do you have?

Failing that, an alternative, if your state space is not too big, is to
add another variable to your model that counts the reward explicitly.
This will require putting a bound on the max (and min) values that the
counter can take.

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 https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

Mark

unread,
Nov 19, 2017, 2:26:31 PM11/19/17
to PRISM model checker
Hi Dave

I have a DTMC model, it will be great if PRISM allow the reward mixture in DTMC atleast. 

Dave Parker

unread,
Nov 19, 2017, 2:36:22 PM11/19/17
to prismmod...@googlegroups.com, dine...@gmail.com
Let's assume you have a property R{"r"}=? [ F "target" ], which computes
the expected cumulated amount of reward "r" until "target" is reached.
Split your reward structure "r" into two separate reward structures,
"pos" and "neg", containing the positive and negative rewards,
respectively. For the latter, negate them so that rewards in "neg" are
also positive. Then use the property:

R{"pos"}=? [ F "target" ] - R{"neg"}=? [ F "target" ]

and this will give you what you want. It will only work if poth parts
are finite, i.e. if "target" is eventually reached with probability 1.

Dave

On 19/11/2017 19:26, dine...@gmail.com wrote:
> Hi Dave
>
> I have a DTMC model, it will be great if PRISM allow the reward mixture
> in DTMC atleast.
>
> On Sunday, November 19, 2017 at 7:11:37 PM UTC, d.a.parker wrote:
>
> Thinking about it, we could potentially add support for Markov chains,
> but I don't know a good general algorithm to tackle this class of
> problem for Markov decision processes. What model do you have?
>
> Failing that, an alternative, if your state space is not too big, is to
> add another variable to your model that counts the reward explicitly.
> This will require putting a bound on the max (and min) values that the
> counter can take.
>
> Dave
>
> > an email to prismmodelchec...@googlegroups.com <javascript:>
> > <mailto:prismmodelchec...@googlegroups.com
> <javascript:>>.
> > To post to this group, send email to prismmod...@googlegroups.com
> <javascript:>
> > <mailto:prismmod...@googlegroups.com <javascript:>>.
> <https://groups.google.com/group/prismmodelchecker>.
> > For more options, visit https://groups.google.com/d/optout
> <https://groups.google.com/d/optout>.
>
> --
> 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>.

Joachim Klein

unread,
Nov 20, 2017, 12:33:59 PM11/20/17
to prismmod...@googlegroups.com, Mark
Hi Mark,

I took your question as the motivation to start working on adding proper
PRISM support for mixed positive and negative rewards.

If you like and feel comfortable building from source, you can check out

https://github.com/kleinj/prism/tree/snapshot-ex-dtmc-weights-2017-11-20

which allows the such rewards for DTMCs in the explicit engine. This is
just a development snapshot, so things might be broken, but the basic
functionality seems to work.

This should also work with interval iteration in the explicit engine.

Total expected reward is currently not supported in the presence of
negative rewards.

Any feedback is appreciated.


Cheers,
Joachim Klein

K. Anuarul Hoque

unread,
Nov 20, 2017, 12:41:32 PM11/20/17
to Joachim Klein, prismmod...@googlegroups.com
Hi Joachim

Great, thanks for your effort. I will give it a try.
--
Regards
----------------------------------------------------
Khaza Anuarul Hoque, Ph.D. 
FQRNT Postdoctoral Research Fellow
Dept. of Computer Science, University of Oxford, UK.

Joachim Klein

unread,
Nov 23, 2017, 7:00:39 AM11/23/17
to prismmod...@googlegroups.com
Hi,

> If you like and feel comfortable building from source, you can check out
>
> https://github.com/kleinj/prism/tree/snapshot-ex-dtmc-weights-2017-11-20

A quick and dirty development version that now also includes support for
mixed positive and negative rewards for both the explicit and the
symbolic engines is available at

https://github.com/kleinj/prism/tree/snapshot-dtmc-weights-2017-11-23

Cheers,
Joachim

Mohammad Abdulaziz

unread,
Apr 25, 2022, 7:45:18 AMApr 25
to PRISM model checker
Hi Joachim,

Is there support for total expected rewards in the presence of mixed positive and negative rewards?

best,
Mohammad

Dave Parker

unread,
Apr 26, 2022, 11:53:25 AMApr 26
to prismmod...@googlegroups.com, Mohammad Abdulaziz
Hi Mohammad,

As far as I remember, that code was just for Markov chains. Mixtures of
positive/negative rewards in infinite-horizon properties for MDPs are
harder to handle.

Best wishes,

Dave
> https://github.com/kleinj/prism/tree/snapshot-dtmc-weights-2017-11-23 <https://github.com/kleinj/prism/tree/snapshot-dtmc-weights-2017-11-23>
>
>
> Cheers,
> Joachim
>
> --
> 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/8d76a680-04d5-4933-ba13-abdb9bd9b70dn%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/8d76a680-04d5-4933-ba13-abdb9bd9b70dn%40googlegroups.com?utm_medium=email&utm_source=footer>.
Reply all
Reply to author
Forward
0 new messages