Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 16:30 - 17:00 at Sala III - Model Checking Chair(s): Xiaokang Qiu

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.60MiB