Mar 24, 2015: Tom van Dijk: Signature refinement using Sylvan

March 24, 2015Signature refinement using Sylvan
Room: HB 2ATom van Dijk

Bisimulation minimisation is a strategy that alleviates the exponential growth of transition systems in model checking by computing the smallest system that has the same behavior as the original system according to some notion of equivalence.

Examples of such notions are strong bisimulation, which preserves external and internal behavior of a system, but merges states with identical behavior, and branching bisimulation, which preserves external behavior but abstracts from internal behavior. Branching bisimulation preserves CTL* without next-state quantifier.

It has been shown in the literature that computing the minimal (or coarsest) bisimulation of a system can lead to spectaculair reductions and many happy PhD students.

One method to compute the minimal bisimulation is signature-based partition refinement - in short: signature refinement.

Work in the past decade extends signature-based partition refinement to symbolic methods using binary decision diagrams (applied to labeled transition systems) and multi-terminal decision diagrams (applied to interactive markov chains).


Currently, we study the application of Sylvan as the BDD library for symbolic signature refinement. In this research, our expectation was to find a reasonable parallel speedup, which we have found before in other BDD-based algorithms. However, we also discovered several other optimisations by implementing custom BDD operations for certain steps in the signature refinement algorithm. The result of which is an impressive speedup on certain models with branching bisimulation, for example from over 50,000 seconds in the original paper to 4 seconds in our work. In the presentation, we will present these preliminary results and explain the algorithms used.