Ticket #27 (closed defect: fixed)
CSRL, Time- and Reward- bounded until operator, Qureshi Sanders algorithm
| Reported by: | ivan.zapreev | Owned by: | ivan.zapreev |
|---|---|---|---|
| Priority: | major | Milestone: | MRMC v.1.4.1 |
| Component: | Core | Version: | 1.2.2 |
| Keywords: | Cc: | nguyen, christinajansen |
Description
We get different results if state space is reordered, in particular this affects the formula dependent (independent) lumping.
See
./test/functional_tests/ctmrm/csrl/lumping tests.
The possible problem is that Qureshi Sanders algorithm presumes state space ordering according to the state rewards, but Maneesh Khattri has the following opinion:
In my opinion, the ordering of the state space is not required, though it might be done for some ease. The reason for this is:
1. First see equation (6) & (7) in the paper "Model checking Markov reward models with impulse rewards" DSN-PDS-05: In the vector k, each element, for instance ki: i - (1 to K+1), corresponds to the number of residences in states with reward ri such that r1>r2>r3>…>rK+1>0. The r’s are the distinct state rewards in descending order.
2. Now look at equation (9) in the paper referenced in step 1: We consider each path in isolation, but for the computation of the distribution of uni. order statistics, each of the paths has to again be characterized by means of the k & j vectors. It is, of course, possible that a number of paths have the same mentioned vectors.
3. So, for the computation (9) we only need for each of the paths the correct k & j vectors. Each path is a sequence of states and it is possible to obtain the state rewards for each state in the sequence. Now, we only need to obtain the correct index in the k & j vectors for the reward being considered. For this we can now consider the implementation.
4. See get_dsr method in transient_ctmrm.c: This method gets reward array and obtains a list of all the distinct state rewards. In addition to this, the method also creates the index_ list. The list indicates for each state the position (index) in the r’s as in step 1. For example, if we have a residence in state 2 for which index_[2] = 1, then k1= k1+1, since there has been a new residence in state whose reward corresponds to k1.
5. When the dfpg method in transient_ctmrm.c is called it searches for paths, in a depth-first manner, which would satisfy until formula. It also creates the k vector, by looking at the index_ array for each visit to states.
6. In my opinion, given that we only need to make the vectors correctly, and since dsr and index_ are already ordered by descending value of ri’s it is not required to order the whole state space.
