Algorithms and Datastructures for Efficient Analysis of Systems

Systems are often modeled as a transition system with labels: a transition system has system states and transitions between the states. Basically a graph where we call the vertices states and the edges transitions. Furthermore, states and transitions can have labels, indicating for example communication, or actions, or information about the states. In graph theory, these are also called colors.

We use the LTSmin toolset that we develop to analyse systems via the PINS interface, which is a way to connect any input specification language with the analysis backends. We can then perform analysis tasks such as computing the number of reachable system states, whether a CTL or LTL formula holds, et cetera.

A parity game is a two-player game played on a directed graph. Vertices on the graph have numbers called priorities; a play is a path on the graph that ends in a cycle, and the goal for player 0 is that the highest number on this cycle is even, and for player 1 that the highest number on this cycle is odd. We study algorithms that solve parity games: compute who wins the parity game (or parts of the parity game) and compute a winning strategy (choices that lead to a winning cycle).

Parity games are a very simple concept, but there is an unsolved open problem lurking in the shadows. Parity games are suspected to have a polynomial-time solution, but none have been found yet! We study a variety of parity game algorithms to learn fundamental properties of what makes parity games difficult.

A core problem in the analysis and construction of systems is the state space explosion problem. In order to analyse a system, we need to consider all possible states, evaluate all different interleavings of communicating processes, all combinations of subsystem states, and so forth. This results in what is called an exponential blowup, where adding one component doubles the number of states of the system. The state space explosion problem motivates a lot of research in model checking and synthesis.

One approach that deals with state space explosion is to not consider/evaluate every single state of the system (called "explicit" state evaluation) but to reason about (abstract) sets of states. Then if these sets are concisely represented, we save perhaps exponential space and time, and thus avoid the state space explosion problem. Essentially this is a kind of abstraction technique (and one can consider many techniques as merely abstraction techniques). In particular at the UT we use binary decision diagrams (BDDs) to represents a set of states as a Boolean formula that is encoded as a decision graph. Clever use of BDDs lets us analyse systems that sometimes have many billions of system states within seconds when they can be encoded by relatively small BDDs.

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:

• Port Lace to Rust. Rust already has the "rayon" crate. Perhaps using Lace we can obtain better performance?
• 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, 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.

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. 

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".

Supervisor: Tom van Dijk

Hardware circuits are modeled using and-inverter-graphs (AIG), a graph structure with AND-gates, latches, and negations. It is very important to reduce the size of the AIG. We want to explore various analysis techniques, including bisimulation minimisation, substitutions, logic rewriting, etc.

In practice this means modifying Knor (github.com/trolando/knor) to generate smaller outputs. Currently we have explored bisimulation minimisation, different way to encode a BDD, and using the ABC postprocessing tool. Open ideas are: a) more ways of encoding the BDD; b) deeper study of ABC; c) using Mockturtle instead of ABC.

C++ programming experience highly useful but not strictly necessary.

Supervisor: Tom van Dijk

One of the most robust algorithms (most resistant to hard parity games) is tangle learning. But this algorithm does have exponential hard games. Recently, an algorithm by Pawel Parys is strictly below exponential ("quasi-polynomial"). It is straight-forward to apply tangle learning to this algorithm, I just haven't had time to get to this yet. The topic is about implementing this algorithm, and then finding and understanding lower bound examples for QTL (the challenging part).

It is quite possible that we already have a parity game construction that is already challenging for QTL. In that case, we can explore other avenues for finding hard games for parity game algorithms.

This topic is currently unavailable.