Maurice Laveaux: Modern (Thread-Safe) Decision Diagram Library

Event Details

Some time ago we have introduced a thread-safe term library in the mCRL2 toolset and have transformed some of the algorithms to parallelised variants. Similarly, we rely on a thread-safe decision diagram with parallelised algorithms for computing symbolic reachability and bisimulation. These (highly efficient) implementations often sacrifice readability of source code for the purpose of achieving performance, which makes it hard to extend them and do experiments. Furthermore, both libraries make different design choices in their implementation. In this talk I will be evaluating the design decisions that have been made and give insights into possible alternatives based on a prototype implementation.