POPL 2019 (series) / VMCAI 2019 (series) / VMCAI 2019 - 20th International Conference on Verification, Model Checking, and Abstract Interpretation /
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 |
Mon 14 JanDisplayed time zone: Belfast change
Mon 14 Jan
Displayed time zone: Belfast change
16:00 - 17:30 | |||
16:00 30mTalk | Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking VMCAI Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Laurent Fribourg , Romain Soulat , Jean-Marc Mota | ||
16:30 30mTalk | A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization VMCAI File Attached | ||
17:00 30mTalk | Flat Model Checking for Counting LTL using Quantifier-free Presburger Arithmetic VMCAI |