About me

This is the homepage of Karoliina Lehtinen. Welcome.

Contact email: kleh at-sign informatik.uni-kiel.de

I am a postdoctoral researcher in Prof. Dr. Dirk Nowotka's Reliable Systems group at the Christian-Albrechts University of Kiel, Germany. I did my PhD in the Laboratory for Foundations of Computer Science, University of Edinburgh, supervised by Dr. Julian Bradfield and Dr. Sandra Quickert. I am originally from Finland, but ended up in Edinburgh and now Kiel after going to school in France and doing the Computer Science Tripos and M.Phil in Advanced Computer Science in Cambridge, where my dissertations were supervised by Dr. Bjarki Holm and Prof. Anuj Dawar.

My primary research interests are mathematical logics, infinite games, and automata theory, in particular in the contexts of verification and descriptive complexity. My PhD topic was complexity in the modal \( \mu\) calculus, which is currently my favourite logic.

Current Research

Parity Games

Parity games are infinite two-player path-forming games, played on finite graphs. Fun as that sounds, they are more than just a way to idle away long winter evenings: they turn out to be a way of modeling all sorts of verification problems.

Here's my take on how a logician might solve parity-games in quasi-polynomial time: pdf slides (to appear LiCS'18).

If you are in the business of implementing parity game algorithms, I would be interested in figuring out how this works out in practice.

Runtime Verification of Fixpoint Logic

Runtime monitoring is a light-weight verification technique, where the idea is to try to infer properties of a system by looking at its execution. I've recently been looking at what exactly this technique can achieve for the partial verification of branching-time specifications expressed in Hennessy--Milner Logic with recursion (\( \mu\)HML). I show that arbitrary specifications in this logic can have meaningful monitors, and that we can compute optimal ones. The main insight here is that the theory and practice of runtime monitoring, which has mostly been considered on linear time, can also extend to arbitrary branching-time properties.

Here's my take on how to compute optimal monitors for formulas of \( \mu\)HML: pdf slides

Check out the TheoFoMon project for related work.

Publications

A modal \(\mu\) perspective on solving parity games in quasi-polynomial time. M.K.Lehtinen. LiCS'18 (to appear) pdf slides.

\(\Sigma^{\mu}_2\) is decidable for \(\Pi^{\mu}_2\). M.K.Lehtinen & S.Quickert. Cie 2017 pdf

The descriptive complexity of modal \( \mu\) model-checking parity games. M.K.Lehtinen. GandALF 2017 pdf

Deciding the first levels of the modal \( \mu\) calculus by formula construction. M.K.Lehtinen & S.Quickert. CSL 2015. pdf

Disjunctive form and the modal \( \mu\) alternation hierarchy. M.K.Lehtinen. FICS 2015 pdf

Drafts

Runtime Verification of Fixpoint Logic: Synthesis of Optimal Monitors. M.K.Lehtinen pdf slides

Theses

Syntactic complexity in the modal \(\mu\) calculus. M.K.Lehtinen. Doctoral thesis from the University of Edinburgh, 2017. pdf

Parity games and the automaticity of modal \(\mu\). M.K.Lehtinen. M.Phil thesis from the University of Cambridge, 2012. pdf

Teaching

I will be teaching a course called Research Skills starting in April. More on this later.

I used to be the teaching assistant and tutor for Edinburgh's first year course on Functional Programming. Other courses I have been a TA or tutor for: the shiny new course Introduction to Theoretical Computer Science, the course Processing Formal and Natural Languages and the course Algorithms, Data Structures, Learning. I occasionally also find myself teaching folk dancing, which is a rather different experience.