Improving bisimulation engine.

[ivan.zapreev]

Implement David Jansen's suggestions for lumping:

Based on the thesis of Tim, I can see the following some
optimizations of the lumping implementation and perhaps
some changes in MRMC that won't affect its efficiency in
other parts, but still improve the lumping:

• Figure 3.1 on page 31: Memory savings are possible by
  • Replacing the list of blocks by a dynamically-growing array of blocks [e. g. a list of arrays of, say, 512 blocks each]. (saves almost 8B per block, if the number of blocks is large.)
  • Saving the flags of blocks more efficient. (saves 3.75B per block.)
  • Replacing the double-linked list of states by a single-linked list. (saves 4B per state.) Needs a simple, fast trick for deletion of a state from a list.
  • Replacing the array of pointers to states plus the pointers from each state to its block by an array that contains, for each state, a pointer to its block. (saves 4B per state.)

  In total, I estimate that this will reduce MRMC memory usage
  during lumping by about 20%. These optimizations will not
  affect timing behavior much (except via reduced swapping).

• By organizing the (sparse) transition matrix in columns instead of in rows, we can implement the lumping algorithm more efficiently (page 33,but-last paragraph: looking up $Q(s_i,s_j)$ will then take constant time, not $O(\log n)$), while matrix-vector multiplications can be executed with the same efficiency as now (but in a different order).

[ivan.zapreev]

Here are my answers in the point-wise manner:

• The bisimulation engine:
  • This is a good suggestion but the problem is we have to change a considerable amount of code in order to implement this. Also list like L are dependent on the original data structure. This is not a substantial improvement in saving in terms of space. Although this can be implemented if we are improving the entire code and making it more modular.
  • The suggested method has to use a bitset in the partition data structure which keeps track of the flags used (SPLITTER, PARTITION, ABSORBING). The problem is we don't know the size of the bitset and over allocating space for it (MAX no of blocks = No of States) is a bad strategy because whenever there is a reduction factor of 30 or more in the number of states then this would in fact harm us more. As in Tim Kemna's; thesis we in high majority of cases have state-space reduction of way over 30. The other approach is to use a list of bitsets but this costs us penalty of time, because of unnecessary list traversals as we have to reach the end of the bitset is to allocate new flags for new blocks.
  • Saves space but has time penalty. The trick suggested by David is good but requires 6 assignment compared to 2 assignments with doubly linked case. (For removing blocks etc.) This is so because of the pointer we have from array of states to the state elements that constitute the list.
  • Huge time penalty, as we cannot get away with the list of states because we need to constantly traverse the list of states in a block. This is possible only when we have pointers from block to state not from states to block.
• The sparse matrix: This is not applicable because storing matrix row-wise is essential for good performance of iterative methods and other operations related to matrix-vector multiplications. If we store matrix elements column-wise then we most likely significantly reduce the tool's performance