Invalid adversary for co-safe LTL reward property

[gamoreno]

Hi, I've run into an issue with an invalid adversary being generated when I use a co-safe LTL reward property. I've reduced the model as much as I could while still producing the invalid adversary.

If I use the property Rmin=? [ F done ] on the model in genmodel.prism.zip, I get an adversary with the expected behavior. However, if I use the property Rmin=? [ true U done ] I get an adversary with invalid transitions. I run PRISM as follows:

prism genmodel.prism -pctl 'Rmin=? [ true U done ]' -exportadv exp-u.adv -exportstates exp-u.sta

The invalid transitions are the following:

5 7 1 SafeRightMove
6 8 1 SafeUpMove
7 8 1 SafeDownMove

where the states are:

5:(2,3)
6:(3,1)
7:(3,2)
8:(3,3)

For example, the transition from state 5:(2,3) with action SafeRightMove should go to state 8:(3,3), because that action increases the value of x (the first component in the tuple). It can't go to state 7:(3,2) because action SafeRightMove does not change y, the second component.

As I mentioned above, if I used the equivalent formula using F (probably not equivalent in terms of how PRISM solves it), I get the expected result. I've tried this in 4.6 and 4.7 with the same result. Have I missed something about the use of co-safe LTL properties?

[davexparker]

Hi @gamoreno. When solving for cosafe properties (anything more complex than an F), PRISM builds and solves a product model (which combines the MDP and a finite automaton representing the property), so the adversary you are seeing is over the states of that. Use the switches -exportprodtrans and -exportprodstates to get the transitions/states of the product model. The resulting memoryless strategy over that product model can be seen as a finite-memory strategy over the MDP. Ask if you need help interpreting that.

[gamoreno]

@davexparker, thanks for the explanation! I didn't know those options existed.