Workers in forests: developments in parallel decision diagrams

RiSE will host a talk by Tom van Dijk on April 28, 2016

ABSTRACT

A well-known technique in formal methods to deal with large state spaces is symbolic model checking using decision diagrams. Decision diagrams conveniently and concisely store functions, especially Boolean functions that represent state spaces and transition relations, but also other functions, for example rational functions to encode transition rates. In the last decade, increases in processing power of computers no longer comes from increased processor speed, but mainly from increased parallelism. This has inspired research into scalable parallel techniques, for example using multi-core machines, but also using networks of computers or many-core GPGPUs. Efficient parallelism is not quite trivial. The application of parallelization to symbolic model checking has been problematic and prone to significant overheads in the past, but recent advances in efficient fine-grained task-based parallelism and scalable lock-free datastructures enable effective scalable parallel (multi-core) implementations of algorithms on decision diagrams. This talk discusses the implementation of Sylvan, a parallel decision diagram library implemented in C, and its application to symbolic state space exploration and symbolic bisimulation minimisation.