# Algorithms and Datastructures for Efficient Analysis of Systems

## Background

One branch of theoretical computer science is the analysis of algorithms, protocols, hardware circuits and software. We want to analyse a system such as a piece of software or a hardware circuit for desirable properties, or to automatically generate systems with desirable properties. Examples of properties are functional correctness, the absence of forbidden states or deadlocks, or reactivity properties such as that a system is responsive.

Many of these questions just boil down to running algorithms on graphs. For example, to check whether some system fulfills a reactivity property specified in LTL, we would simply construct an automaton such that if it has an accepting run, this accepting run proves that the system is not correct. That is, if the language of the automaton is empty, then the system is correct.

Of course, this is only the beginning because if this was all there is to it, then there would not be much research to do. The core challenge in this area is called state space explosion: in order to analyse a system, we usually need to consider exponentially or even double exponentially many different situations. This motivates a lot of research into new algorithms to reduce the number of different situations, often by inventing tricks to analyse similar states simultaneously, or by limiting a system to only "relevant" runs, and abstracting away from runs that don't seem relevant. We are constantly trying to find new tricks to push the limits of what we can compute efficiently.

In the formal methods and tools group at the UT, we work with many techniques including binary decision diagrams and parity games. However, we are also interested in studying abstraction techniques such as IC3, guided refinement, partial order reduction, and so forth. Our other goal is to ensure high performance of algorithms, by smart engineering/coding. There are competitions between scientists and it would be nice if we can win them by using smart algorithms that are fast!

• Labeled transition 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.

• Parity games

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.

• Symbolic model checking with binary decision diagrams

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.

### Other topics

Also open ideas for high performance algorithms / data structures are welcome. We have a focus on efficient implementations and empirical evaluation of algorithms.

#### Prerequisites

• Programming experience recommended
• An affinity with algorithms and logical reasoning

#### Related Modules in the Bachelor TCS

• Discrete Structures and Algorithms (automata and graph algorithms)
• Software Systems (implementing software)

## Available Project Proposals

If you are interested in the general topic of Systems Analysis, or if have your own project idea related to the topic, please contact us directly. Alternatively, you can also work on one of the following concrete project proposals:

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.

• 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.
• Applying dynamic variable ordering to fault tree analysis

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.

• Incremental parity game solving

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.

• Small parity game strategies

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.

• Symbolic parity game algorithms

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

• Reducing AIGER circuit size

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.

• Quasi-polynomial tangle learning

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.