Fully-Implicit Relational Coarsest Partitioning for Faster Bisimulation (As Preparation for Fully-Implicit Lumping)

The present work applies interleaved MDD partition representation to the bisimulation problem. In the course of considering fully-implicit lumping (see section 2.6) for Markov systems, we have implemented fully-implicit partitioning, using interleaved MDDs for bisimulation partitioning, in the context of the SmArTverification tool. We compare the execution time and memory consumption of our fully-implicit methods (using interleaved MDDs) with the execution time and memory consumption of partially-implicit methods (using non-interleaved MDDs), as applied to the same bisimulation problems. We found that the fully implicit method had prohibitively large run-times for models with few variables with many values. The performance of the fully implicit method was reasonable for models with many variables having few values, although generally slower than the hybrid method which used non-interleaved MDDs to represent the state-space partition.