Laudatio for Doctor Malvin Gattinger
Here is my laudatio for Malvin Gattinger, who successfully defended his PhD Thesis on New Directions in Model Checking Dynamic Epistemic Logic yesterday, in the Aula of the University of Amsterdam.
Very learned doctor Gattinger, dear Malvin,
The very first time we met was in the Fall of 2013, when I was pioneering with a new course at ILLC, developing connections between logic and functional programming. The course was called ‘Functional Specification of Algorithms’. You were one of my students then. I remember that I was greatly impressed with you and with some of your fellow students: Yfke Dulek, Jouke Witteveen, Nadine Theiler (such talent, all of them now pursuing PhD’s in Amsterdam).
One of the selected topics of the course was knowledge representation and the computational difficulty of representing ignorance about large numbers. I floated some ideas about this in one of the course lectures, and you picked this up and made it the topic of your course paper. Later on you developed this further, and it became a beautiful master thesis. Then we had a stroke of luck. You managed to get selected as PhD student in the Joint Research Centre for Logic, a collaboration between ILLC at the University of Amsterdam and the prestigious Tsinghua University in Beijing, an initiative of Johan van Benthem and Fenrong Liu. Your topic: model checking for dynamic epistemic logic. And a stroke of luck for me too, for you continued to be my teaching assistant for the FSA course, and I became your PhD thesis supervisor.
The China connection proved fruitful. You met professor Kaile Su and went to visit him in Brisbane in Australia, and you got acquainted with state-of-the-art theorem proving and model checking techniques in modal logic. Kaile Su became your co-supervisor. Later we also recruited Alexandru Baltag as co-supervisor. In the Summer of 2015, we had Yanjing Wang over from Beijing, and the two of you hit it off marvellously together.
In the Autumn of 2015 we went on a trip together to Beijing. This was a huge success, and a great experience. We stayed as guests of professor Fenrong Liu, at Tsinghua University, and we presented new work on dynamic gossip networks during the 3rd Tsinghua Logic Colloquium in Beijing. Also, during our time in Beijing, there was ample opportunity for further collaboration with Yanjing Wang. This joint work with Yanjing made it into Chapter 5 of your thesis.
During the Beijing trip we went back and forth to Taipei in Taiwan (the other China), where we attended LORI-V, and where you presented the first paper on Symbolic Model Checking for Dynamic Epistemic Logic of which Johan van Benthem, Kaile Su and me were co-authors, but of which you were undoubtedly the main author.
Your presentation was received very well in Taipei, on 28 October, 2015. Since then, you have extended the work considerably, we published a journal version of it, and it developed into the solid core of your PhD dissertation. In my preparation for today I have looked again at your Taipei slides. It is remarkable that the key elements of your contribution were already there: your sense of the limits of explicit model checking for Dynamic Epistemic Logic, and your plan to overcome those by representing models in a more compact and efficient way, using the tool set of binary decision diagrams. This essentially translates modal logic to propositional logic, with a clever encoding of the accessibility relations. This was done before, surely, for temporal logic, but never for Dynamic Epistemic Logic.
At the time of the talk, you already had an efficient implementation SMCDEL, and you could demonstrate that your tool was vastly superior to my own more simple-minded DEMO-S5 model checker. You blew me out of the sky then. Next, you also indicated how the action models of DEL could be translated into knowledge transformers. In your talk you demonstrated this for S5 action models such as public announcements, and in later work you extended this to arbitrary action models, and you also extended the framework to include factual change.
This is beautiful work. What your thesis demonstrates, is that logic can be enriched with insights from computer science, and that computer science can find a new area of application in logic. To make this connection between logic and computer science bear fruit is difficult, because the mind-set that it requires is rare. Logic demands that one has a taste for the pure and abstract, and a bit of contempt for what is practical helps. Computer science demands a practical frame of mind, and a bit of disgust for what can be perceived as useless theory is not uncommon here. So in order to bridge the gap one has to develop a paradoxical mix of tastes, somewhat in the spirit of German idealism. To a deep philosophical mind like yours, the theoretical and the practical appear as categories of the understanding, and they can be reconciled by means of Anschauung und Vorstellung. But of course, one has to be German to be able to do that.
Although logic and computer science can be far apart, many of my students were delighted with learning about functional programming, and with getting acquainted with a new tool set that could help them to put logic in action. You have helped me a great deal in shaping that course and making it into a success. You really went out of your way to give feedback and useful advice to anyone struggling with the functional way of thinking. Later on I found out that this extended far beyond this one course. You have a habit of going out of your way to help others, and I admire you for that.
Malvin, you are my last student, and I owe you thanks for making my exit from the academic community a bit easier. I know now that nothing is lost by my decision to drop logic and turn to meditation and poetry writing instead. I think of you as in many ways an improved version of myself. I know a bit about functional programming, but with lightning speed you surpassed me and became a true expert. To get informed about the state-of-the-art Haskell tricks I would now have to turn to you for advice. I have been helpful to a few students, but I have also set my boundaries. You are offering your help to anyone who is requesting it. I have done some work on epistemic model checking. You have introduced a new and superior method for that. I can safely bow out and leave now.
It is pleasant for me to know about your next step ahead. Quite recently you accepted an offer from the University of Groningen to join them as a Postdoc. Professor Rineke Verbrugge wrote to me: “Malvin gave a truly spectacularly good presentation during his job interview, totally accessible, also for the non-logicians.” So your talents are being recognized, and that gives me great pleasure. And Rineke and her colleagues have good taste, but I knew that already.
Congratulations, dear Malvin, with this splendid success. It is my pleasure to extend my congratulations to your girlfriend Emma, to your paranymphs Jana en Esteban (also among my students in the FSA course), to your parents, to your sister, and to your many friends here. I am sure they are all very proud of you. How can I know this? By sensing the pride that I feel myself in my heart when I think of you. It has been a great pleasure and an honour to be your supervisor. I wish you every success with your life and with your career, and I hope and expect that we will stay in touch.