University Teaching Qualification

Today I got the official notification of what I already knew unofficially. I am qualified to teach at the university. In other words, I received the certificate that is called “University Teaching Qualification” (or, in Dutch, BasisKwalificatie Onderwijs, BKO).

This certificate signifies that I have required pedagogical competencies to teach University students. Among others, I have shown that I can design new bachelor and master courses in a responsible way (and yes, I am using the design to teach my BSc course on automata & complexity theory).  Also, I gathered enough proof to show that I can give lectures in a way that gets students engaged!

Liveness Analysis for Parameterised Boolean Equation Systems – ATVA’14

Today I have talked about our paper “Liveness Analysis for Parameterised Boolean Equation Systems” at ATVA’14 (which is currently being held in Sydney). Let’s take a look at what this work is about.

To start with, a parameterised Boolean equation system (PBES) is a system of fixed point equations that can, e.g., be used in model checking modal mu-calculus properties, check behavioural equivalence between systems, or solve Datalog queries.

Let’s take a look at what such a system looks like:
$$\begin{array}{ll}
\nu X(i,j,k,l\colon N) & = (i = 1 \land j = 1 \land k = 1 \Rightarrow X(2,j,k,l+1)) \\
& \land (j = 1 \Rightarrow Y(i,1,1,k)) \\
& \land \forall m \colon N . (j = 2 \Rightarrow Y(i,j,m+k,k)); \\
\nu Y(i,j,k,l \colon N) & = (j \neq 2 \Rightarrow k < 10) \\
& \land (j = 2 \Rightarrow X(1,1,l+1,1)) \land X(2,2,1,l);\\
\mathbf{init}~X(1,1,1,1);
\end{array}$$

So, in short, we have a system of mutually recursive fixed point equations, where the variables are parameterised with variables ranging over abstract data types; the right hand sides range over formulas over these data types and first order variables. In general we are interested in the solution to a specific instance of a variable, like \(X(1,1,1,1)\) in the example above.

Typically, we solve PBESs using instantiation into Boolean equation systems (BESs) or parity games (both are equivalent). The main motivation for instantiating is that it is easy to automate. However, this can easily lead to an infinite BES. For instance, in the example above, \(X(2,2,1,1)\) depends on \(Y(2,2,v+1,1)\) for infinitely many values of \(v\).

In our paper, we present a static analysis technique for PBESs that can be used to overcome such problems. In the example, we can observe that parameter \(k\) to the equation for \(Y\) is only relevant when \(j \neq 2\), but in the infinity in the example, we only reach \(Y\) with \(j = 2\), hence if we look closely, we can see that it is sound to replace \(Y(i,j,m+k,k)\) by \(Y(i,j,1,k)\)! This is exactly what the approach in the paper establishes in three steps:

  1. We analyse the structure of the PBES to determine a set of control flow parameters. Using these control flow parameters we build a control flow graph.
  2. In the next step, we label the nodes in the control flow graph with those data parameters that are possibly relevant at that control flow location, and use backwards reachability to propagate relevance. All parameters that occur not in the labelling of a particular control flow location are not relevant (dead) at that location.
  3. Once we have established this labelling, we can use the information to reset dead variables in every recursion in the PBES.

The first analysis that we present treats all control flow parameters simultaneously. However, this approach suffers from an exponential blow-up. We therefore also present an approximate analysis that considers separate control flow graphs that does not suffer from this blow-up, yet closely approximates the global analysis.

The analysis has been implemented in the mCRL2 toolset, in the tool pbesstategraph. Our running example is reduced to: $$
\begin{array}{ll}
\nu X(i,j,k,l\colon N) & = (i = 1 \land j = 1 \land
k = 1 \Rightarrow X(2,1,1,1)) \\
& \land (j = 1 \Rightarrow Y(i,1,1,1)) \\
& \land
(j = 2 \Rightarrow Y(i,2,1,k)); \\
\nu Y(i,j,k,l \colon N) & = (j \neq 2 \Rightarrow k < 10) \\
& \land (j = 2 \Rightarrow X(1,1,l+1,1)) \land
X(2,2,1,1);\\
\textbf{init}~X(1,1,1,1);
\end{array}$$

This PBES has a finite instantiation, hence we can get an arbitrarily large reduction using this approach. Also in practice we have seen large reductions in size, and dramatic speedups for model checking, while the added overhead is limited.

Check out the ATVA slides and the paper. If you are interested in the details of the proofs, they are available in the arXiv version.

Migration of website complete

As you may have noticed I started working at the VU University in Amsterdam in October of this year, after spending nine nice years at TU Eindhoven for my B. Sc., M. Sc. and finally my Ph. D. Today I have finally finished migrating all the information that was available on my personal homepage at TU Eindhoven. The old homepage has been removed, and for the time being replaced by a link to this homepage.

You can soon expect improvements to my homepage, as well as blog posts on my recent research, and other things that occupy my mind.

PhD dissertation

After four years of hard work, I defended my PhD thesis, of which the summary is included below, on 17 September. I experienced the day of the defence as a great day. It was very nice to see so many of my family, friends and colleagues. Thank you!

Summary

Advanced Reduction Techniques for Model Checking

Cover_Front_smallModern-day software systems are highly complex, and typically consist of a number of in- teracting components running in parallel. Verification methods aim to prove correctness of such systems. Model checking is a commonly used verification technique, in which a model of the system under investigation is created. Subsequently, it is checked whether this model satisfies certain properties.

Model checking suffers from the infamous state space explosion problem: the number of states in a system grows exponentially in the number of parallel components. Part of the blow-up is also due to the presence of data in descriptions of model checking problems. Typically model checkers construct the full state space, causing the approach to break down already for a small number of parallel components. Properties are then checked on the state space, either directly, or by first combining the state space with a property, leading to, for example, a Boolean equation system or a parity game. The latter step leads to a further blow up.

In this thesis techniques are developed to counter this state space explosion problem in (parameterised) Boolean equation systems and parity games. The main contributions are as follows:

  • A structural operational semantics is presented that can equip Boolean equation systems with arbitrary right hand sides with a graph structure, called structure graph. Classical graph structures for analysing Boolean equation systems typically restrict right hand sides to purely conjunctive or disjunctive form, essentially redu- cing the equation system to a parity game. We use our graphs to study the effects of this restriction on right hand sides, and show that, in the context of bisimulation, this reduction never poses a disadvantage.
  • We investigate the reductions that can be achieved using strong bisimulation reduction of structure graphs, and we investigate idempotence identifying bisimulation. We show that, although it indeed identifies idempotence in a restricted subset of equation systems, it does not live up to its name for full-blown structure graphs.
  • The insights we gain by studying structure graphs motivate further investigation of weaker equivalences in the setting of parity games. Since the winner in parity games is determined by the infinitely often recurring priorities, intuitively, finite stretches of similar vertices can be compressed. We define the notions of stuttering equivalence and governed stuttering equivalence, and show that they preserve the winner in a parity game.
  • A new set of benchmarks for parity games is developed due to the unavailability of standard benchmarks. These benchmarks subsume the examples that are used for performance evaluation of solving algorithms in the literature. We provide a description of the benchmarks, and we analyse their characteristics.The efficacy of our equivalences for reducing parity games is evaluated using this set of benchmarks. It is shown that large reductions are possible, even reducing parity games to a single vertex with a self-loop. Average reductions of about 50% are achieved. Sometimes the technique allows solving parity games which cannot be solved directly; in general, however, the timing results do not show a clear advantage.
  • Finally, we move from a posteriori reduction of parity games, to static analysis tech- niques for parameterised Boolean equation systems, that allow the a priori reduc- tion of the induced parity games. Essentially, we present a heuristic that performs a live variable analysis. We show that this analysis is more effective at reducing the complexity than existing techniques, i.e. the reductions that we obtain are larger. Correctness of our analysis is shown using a generalisation of the equivalences that we introduced for parity games and Boolean equation systems.