This is the homepage of Karoliina Lehtinen. Welcome.

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 graduated with a doctorate in 2017 from the Laboratory for Foundations of Computer Science, University of Edinburgh, supervised by Dr. Julian Bradfield and Dr. Sandra Quickert. I also hold an M.A. and M.Phil from the University of Cambridge, where I was supervised by Dr. Bjarki Holm and Prof. Anuj Dawar.

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.

The exact complexity of solving parity games has been an open question for over 25 years. A breakthrough occurred in 2017, when two independent quasi-polynomial algorithms were published. I propose a third independent approach, based on the tight connection between the modal \( \mu\) calculus and parity games, providing descriptive-complexity perspective on the issue. This work has been accepted for publication at LiCS 2018. Here's my take on how a logician might solve parity-games in quasi-polynomial time: pdf.

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

I spent two months this spring in Israel, working with Udi Boker at IDC Herzeliya on weak alternating automata. In the world of automata, there is a trade-off between how concisely an automaton can represent a property and the complexity of checking for membership and emptiness. Weak automata allow for simpler algorithms than more complex automata types, but are often larger.

Our ongoing research aims to close some of the gaps between known upper and lower bounds for turning various types of automata into weak ones.

The study of monitorability asks what type of properties can be verified at runtime. The classical notion of monitorability, due to Pnueli and Zacks, is defined independently of the specification logic and the monitor model. Recently, Francalanza et al. have proposed a more operational take on runtime monitoring, leading to a different concept of monitorability. I am part of a collaboration which aims to reconcile these different approaches.

I've recently been looking at how to find monitorable approximations of unmonitorable branching-time specifications expressed in Hennessy--Milner Logic with recursion (\( \mu\)HML).

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.

A modal \(\mu\) perspective on solving parity games in quasi-polynomial time. M.K.Lehtinen. LICS 2018 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

Monitoring beyond monitorability. M.K.Lehtinen pdf slides

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

I am a teaching a course called Research Skills.

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.