Algorithms and Datastructures for Efficient Analysis of Systems

Supervisor: Tom van Dijk, Milan Lopuhaä - Zwakenberg, Mariëlle Stoelinga

One approach for fault tree analysis uses binary decision diagrams to represent the fault trees. Recently we implemented dynamic variable ordering in the Sylvan binary decision diagram library, which is highly parallel (using multiple cores on the computer). We want to see how well this performs on BDDs obtained from fault tree analysis. 

We are interested to do execute parallel loads with many small tasks, this is called fine-grained parallelism. The task-based approach is also called fork-join parallelism: each task spawns a number of other tasks and waits for their result in order to continue.

Lace has very good performance in C. Notably, the "fibonacci" benchmark, where each task is just summing the results of two subtasks, is very sensitive to overhead from for example memory accesses related to the load balancing. Lace has almost no overhead, especially compared to many other approaches.

Potential research tasks:

• We have a version of Lace ported to Rust. We are now interested in further testing the performance using new benchmarks, and potentially refining the implementation in Rust.
• Port Lace to C++. Modern C++ has a number of interesting language features. Perhaps it is possible to integrate the high performance queue datastructure in Lace to a C++ framework?
• Adapt the TP-PARSEC task parallelism benchmarks to work with Lace (in C), so that we can a) compare Lace systematically to other approaches supported by TP-PARSEC, b) compare Lace systematically to other versions of Lace, to see how proposed changes affect realistic workloads.

Supervisor: Tom van Dijk

We can solve full parity games using Oink (https://github.com/trolando/oink) but typically it takes way more time to generate the full game than it takes to come up with the solution. We want to see if we can solve parity games partially, during generation. Ideally, intermediate outcomes can be reused in later attempts. This study is about figuring out how to do this with a variety of algorithms and determine which approach is most useful in practice.

In practice, this probably means integrating Strix with Oink somehow. I have contact information of a Strix developer.

When solving parity games for reactive synthesis, we are interested in winning strategies that are small. Different algorithms sometimes give different results, leading to the idea that perhaps there is a way to design an algorithm that is more likely to yield a small winning strategy. That is what this topic is about. We have a few open ideas: a) only consider vertices of a certain priority; b) when finding a winning region or a tangle, try to recursively find a smaller winning region or tangle; c) study a specific parity game for which we know there are different possibilities, in order to learn more about why some algorithms result in nonefficient strategies.

Supervisor: Tom van Dijk

We can solve parity game using algorithms that use BDDs, in earlier years we did this with fixpoint algorithms already. However these algorithms are quite vulnerable to particular parity games. Goal of the project is to study different symbolic versions of parity game algorithms, that are more robust, such as tangle learning, tangle attractors, fixpoints with justification, and possibly quasi-polynomial algorithms.

It is relatively straight forward to start with justification fixpoints and see how far we can go. We have "fixpoints with freezing", and I think the next targets would be "fixpoints with justification" and "priority promotion".