Advances in Algorithmic Meta Theorems

TL;DR

This paper reviews recent advances in algorithmic meta theorems for logic-based model checking, highlighting progress on various graph classes and new logical frameworks that improve computational tractability.

Contribution

It provides an overview of recent developments in algorithmic meta theorems, including new results for FO and CMSO model checking on specific graph classes and logical frameworks.

Findings

Progress in FO model checking on hereditary graph classes

Development of the twinwidth width measure

New meta theorems for logics between FO and CMSO

Abstract

Tractability results for the model checking problem of logics yield powerful algorithmic meta theorems of the form: Every computational problem expressible in a logic $L$ can be solved efficiently on every class $\mathscr{C}$ of structures satisfying certain conditions. The most prominent logics studied in the field are (counting) monadic second-order logic (C)MSO, and first-order logic FO and its extensions. The complexity of CMSO model checking in general and of FO model checking on monotone graph classes is very well understood. In recent years there has been a rapid and exciting development of new algorithmic meta theorems. On the one hand there has been major progress for FO model checking on hereditary graph classes. This progress was driven by the development of a combinatorial structure theory for the logically defined monadically stable and monadically dependent graph classes, as well as by the advent of the new width measure twinwidth. On the other hand, new algorithmic meta theorems for new logics with expressive power between FO and CMSO offer a new unifying view on methods like the irrelevant vertex technique and recursive understanding. In this paper we overview the recent advances in algorithmic meta theorems and provide rough sketches for the methods to prove them.