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.
KeywordsBisimulation minimization Symbolic model checking BDDs Decision diagrams Parallel computing
- 4.Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: 27th ACM/IEEE Design Automation Conference, pp. 40–45 (1990)Google Scholar
- 10.van Dijk, T.: Sylvan: multi-core decision diagrams. Ph.D. thesis, University of Twente (2016). https://doi.org/10.3990/1.9789036541602