A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
Symbolic computation using BDDs and bisimulation minimization are alternative ways to cope with the state space explosion in model checking. The combination of both techniques opens up many parameters that can be tweaked for further optimization. Most importantly, the bisimulation can either be represented as equivalence classes or as a relation. While recent work argues that storing partitions is more efficient, we show that the relation-based approach is preferable. We do so by deriving a relation-based minimization algorithm based on new coarse-grained BDD operations. The implementation demonstrates that the relational approach uses fewer memory and performs better.
|A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization (VMCAI 2019 slides.pptx)||1.61MiB|