Negative reward

[Mark]

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]

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]

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]

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]

Hi Dave

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

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

[Dave Parker]

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:>>.

> > Visit this group at
> https://groups.google.com/group/prismmodelchecker

> <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]

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]

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.

Web: http://www.kahoque.com

[Joachim Klein]

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]

Hi Joachim,

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

best,

Mohammad

[Dave Parker]

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>.