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

Related Modules in the Bachelor TCS


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:

  • Symbolic automata determinization

    Supervisor: Tom van Dijk

    In order to deal with large verification tasks, we can represent automata using decision diagrams. This is also known as symbolic computation because instead of dealing with single states of the automaton, we deal with sets of states simultaneously.

    A typical task here is to go from a nondeterministic automaton to a deterministic automaton. This is useful for certain algorithms, where you actually need the deterministic automaton.

    In earlier work of a decade ago, a problem here is that determination is a bit tricky to do symbolically. In order to deal with large systems, instead of enumerating states, we want to be a bit smarter by starting with a minimization algorithm before computing the deterministic automaton. This research is about implementing a prototype of this idea and seeing if it works in practice.

  • From BDDs to Quantified SAT: Efficient Algorithms for Fault Trees

    Keywords: BDDs, Fault Trees, TQBF

    Topics: Efficient Algorithms

    Committee: Ernst Moritz Hahn (e.m.hahn@utwente.nl), Stefano Maria Nicoletti (s.m.nicoletti@utwente.nl)

    Project Description:

    Fault Trees (FTs) are a widespread formalism that can model system-level failures, largely employed in industry and academia. In our work, we studied a custom-made logic to reason about FTs. Currently, both FTs and formulae in the logic are translated to Binary Decision Diagrams (BDDs) to favour model checking procedures. The question remains open of whether it is possible to translate formulae of this logic in a suitable quantified logic instead of making use of BDDs.

    Tasks:

    The suggested tasks are the following:

    1. Find a translation for formulae into a suitable quantified logic (TQBF, 1st order...)
    2. Construct a case study to test the newfound translation
    3. Implement the translation via the use of an appropriate SAT solver
    4. Produce some statistics and compare this translation with the one based on BDDs

    Requirements:

    The student should have an interest in industrially-viable solutions, formal methods and tools.

    What will you gain?

    You will gain understanding of a widely popular formalism for risk-assessment in industrial systems, on applicable formal methods and efficient algorithms.

    Curious? Please, feel free to contact us for further discussion, even if you are still undecided.

  • Incremental parity game solving

    Supervisor: Tom van Dijk

    We can solve full parity games using Oink (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.

  • 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 or tangle learning and then see how far we can go.

  • 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. We have a few ideas, probably bisimulation and using a different technique to go from a BDD to AIG are the most viable ones to try first. Goal is to start with one and just see how far we get.

  • 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 easily explore other avenues for finding hard games for parity game algorithms.

  • Theory proving tangle learning properties

    Supervisors: Tom van Dijk, Peter Lammich

    I consider tangle learning to be the most promising family of algorithms to crack the open parity game problem (finding a polynomial-time algorithm). Eventually, I want to be able to prove properties of tangle learning algorithms using a theorem prover like Isabelle. This topic is about formalizing properties of tangle learning in Isabelle.

    This topic is relatively low-risk once you learn how to use Isabelle, you can just start proving lemmata. Peter is an expert on Isabelle and Tom is an expert on parity games.

  • Theory proving parity game algorithms

    Supervisors: Tom van Dijk, Peter Lammich

    There are various parity game algorithms and while we believe that the proofs of correctness are valid, it would be more interesting to prove this systematically using an interactive theory prover such as Isabelle. Goal of the study is to look at algorithms such as priority promotion, quasipolynomial Zielonka, and fixpoint algorithms in order to prove their correctness in Isabelle.

    A follow-up challenge would be to prove that the "two binary counters" parity game family is indeed exponentially hard for various solvers.

    Peter is an expert on Isabelle and Tom is an expert on parity games.

Contact