Model checking is by now a well-established method to verify the correctness of a computer system model against its specification. It is particularly helpful in the case of large or distributed systems where humans easily get lost in the host of details. It is, for example, being used in hardware design and in design of safety-critical systems. Still, research into model checking is going on at full power. In particular, researchers look into extensions of model checking, making the modelling or specification language more powerful, so that a larger class of systems can be modelled, and more accessible, so that more modellers can have their models checked.
I am particularly interested in probabilistic model checking, i.e. looking into models that contain a random element. These models may be used to describe randomised algorithms, fault-tolerant systems, and quality-of-service requirements. Some model checking algorithms do exist for probabilistic systems, e.g. if they are modelled as Markov chains or Markov decision processes. Still, one may want to include more quantitative features, such as time and cost variables, to describe a system that has to satisfy multi-dimensional constraints (such a constraint may have the form “With high probability, the system will finish its task in time and in budget.”). The main problem here is that with each additional feature or dimension, model checking becomes more difficult, perhaps even unsolvable. I am interested in finding out how difficult several combinations of features are. As a consequence, I have published and expect to publish on the (un)decidability and complexity of several extensions of quantitative model checking.
On a more hobby-like basis, I sometimes like to make remarks on philosophy of science, life, and everything. There is life before and beyond science, as can easily be seen from the many decisions we make based on (almost) no scientific evidence. See my private pages for more information.
My research on probabilistic model checking is closely related to the research of Frits Vaandrager on model checking of timed systems. We are collaborating closely in the context of the EU project Quasimodo, the ESI project Octopus and the NWO/DFG project ROCKS. There are many opportunities for continued collaboration, in particular related to the application of model checking to industrial problems (such as analysis of communication protocols and performance analysis of embedded systems). There are also interesting possibilities for collaboration with the group of Peter Lucas, for instance on the use of Bayesian statistics in statistical model checking. Probabilistic models show up naturally in the area of model-based testing, the research area of Jan Tretmans. Probabilistic model checking is also most relevant for analysis of security protocols, see e.g. the work of Miguel Andres and Peter van Rossum from the Digital Security group, and I am very interested to explore possibilities for collaboration here.
During the last years, I have collaborated with the following people, in addition to the projects already mentioned above:
June 2010, David N. Jansen