Accurate behavioral models of software systems can be incredibly useful thanks to the vast array of model based techniques that exist, e.g. automated testing through model based testing, verification of requirements using modal formulas, or providing visual insight using state space visualization techniques. However, acquiring such models can be quite difficult. We propose a set …continue reading

The quantitative modal mu-calculus is equal to the modal mu-calculus except that formulas yield real values including (-)infinity instead of true or false. Quantitative modal formulas can be translated to parameterised real equation systems (PRESs), and subsequently to real equation systems (RESs), which is quite similar as translating to PBESs and BESs in case of …continue reading

In this talk, I will focus on a work-in-progress behavioral abstraction enabling the comparison of two modelling methods. The first method is an adaption of the current modelling methodology at Rijkswaterstaat for tunnel control systems based on SysML Activity Diagrams, as introduced in my previous talk. The second method relies on the Dezyne specification language …continue reading

After five years of PhD research I am finishing my thesis on algorithms for fast term rewriting. In this talk I will look back on the project, summarize the results, and list the open problems

In this talk, I will give the intuition and outline of how to prove our new data-autonomous programming language AuDaLa Turing Complete. While doing that, I shall also discuss relevant aspects of the semantics, including the basics, null-elements and commands.

When formally verifying the correctness of mutual exclusion algorithms it is often assumed that interaction with the shared registers (i.e., reads and writes) are atomic. For instance, it is well-known that the correctness of Peterson’s algorithm relies on the atomicity assumption. Already in 1986, however, Lamport argued that implementing atomic interaction with shared registers basically …continue reading

A classical theorem states that the set of languages given by a pushdown automaton coincides with the set of languages given by a context-free grammar. In a recent article, Bas Luttik and I proved the pendant of this theorem in a setting with interaction: the set of processes given by a pushdown automaton coincides with …continue reading

Unconditional lowerbounds on run-time complexity are challenging. For instance, the best known lowerbound for CNF-SAT remains only linear, despite considerable research effort. Nevertheless, we consider NP-hardness a reliable indication that we should not search for a polynomial time algorithms. Having a similar framework indicating the intrinsic difficulty of problems within PTIME, such as linear, quadratic, …continue reading

This is joint work with Anton Golov (RU) Labelled transitions systems can be studied both in terms of modal logic and in terms of bisimulation. These two notions are connected by so-called Hennessy-Milner theorems, that show that states are bisimilar precisely when they satisfy the same formulas in some modal logic, in other words, when …continue reading

Complex abstract data types are often used to facilitate creating concise models of the behavior of realistic systems. However, static analysis techniques that aim to optimize such models often consider variables of complex types as a single indivisible unit. The use of complex data types thus negatively affects the optimizations that can be performed. To …continue reading