zbMATH — the first resource for mathematics

A parallel relation-based algorithm for symbolic bisimulation minimization. (English) Zbl 07157062
Enea, Constantin (ed.) et al., Verification, model checking, and abstract interpretation. 20th international conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11388, 535-554 (2019).
Summary: 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.
For the entire collection see [Zbl 1409.68014].
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI