ABSTRACT. The model checking problem MC(L,C) for a logic L over a class C of structures is the problem to decide, given a formula phi in L and a structure A in C as input, whether phi is true in A.
It is well known that model checking is computationally intractable for common logics such as first-order logic (FO) and variants of monadic second-order logic (MSO1 and MSO2). In particular, the problems are PSPACE-complete even over two-element structures.

We therefore study model checking in the framework of parameterized complexity. The goal is to find model checking algorithms which on input phi and A decide whether phi is true in A in time f(| phi |) | A |, for a computable function f and a constant c. Model checking problems which can be solved by algorithms with this type of runtime are called fixed-parameter tractable (fpt).

The parameterized setting is more appropriate in the study of model checking problems as it separates the complexity in terms of the formula from the complexity in terms of the structure.

Nevertheless, it is not hard to see that on the class of all finite structures, model checking for FO and MSO is not fixed-parameter tractable (under standard complexity theoretical assumptions).
However, Courcelle proved that MC(MSO2, C) is fixed-parameter tractable if C has bounded tree width. And Seese proved that MC(FO, C) is fixed-parameter tractable if C is a class of graphs of bounded maximum degree.

This immediately raises the following natural question:

       For which classes of structures is first-order model checking fixed-paramter tractable.

Or phrased differently:

Can we identify a structural property P such that MC(L, C) is fixed-parameter tractable for a class C if, and only if, C has property P?

This programme has received significant attention in the community especially for first-order logic. Motivated by applications in parameterized graph algorithmics, for almost two decades  the problem has been studied primarily in the context of sparse classes of graphs. Following a series of results the sparse case has been settled completely by Grohe, Kreutzer and Siebertz in 2014 where they identified "nowhere density" as the appropriate parameter P characterising the tractable instances of first-order model checking precisely.

Since then, the efforts in the community has shifted towards dense classes of graphs and recently several interesting and promising results have appeared.

In this talk I will briefly review the general problem and research programme and the results obtained in the sparse setting. The focus of the talk, however, is on the new approaches towards the dense setting. There are several independent research directions that have been pursued and have made significant progress. I will present these current and future research directions and discuss the current state of the art.

Some results obtained in the pursuit of this research programme have found applications beyond model checking. In particular, the study of stable classes of graphs has resulted in very significant progress in algorithms on nowhere dense classes. I will briefly discuss this application of model theory in algorithm theory.

ABSTRACT. For every $q\in \mathbb N$ let $\textup{FO}_q$ denote the class of sentences of first-order logic FO of quantifier rank at most $q$. If a graph property can be defined in $\textup{FO}_q$, then it can be decided in time $O(n^q)$. Thus, minimizing $q$ has favorable algorithmic consequences. Many graph properties amount to the existence of a certain set of vertices of size $k$. Usually this can only be expressed by a sentence of quantifier rank at least $k$. We use the color coding method to demonstrate that some (hyper)graph problems can be defined in $\textup{FO}_q$ where $q$ is independent of $k$. This property of a graph problem is equivalent to the question of whether the corresponding parameterized problem is in the class $\textup{para-AC}^0$.

It is crucial for our results that the FO-sentences have access to built-in addition and multiplication. It is known that then FO corresponds to the circuit complexity class uniform $\textup{AC}^0$. We explore the connection between the quantifier rank of FO-sentences and the depth of $\textup{AC}^0$-circuits, and prove that $\textup{FO}_q \subsetneq \textup{FO}_{q+1}$ for structures with built-in addition and multiplication.

ABSTRACT. The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity.We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

ABSTRACT. We present a model-theoretic property of finite structures, that can be seen to be a finitary analogue of the well-studied downward L\"owenheim-Skolem property from classical model theory. We call this property the *L-equivalent bounded substructure property*, denoted L-EBSP, where L is either FO or MSO. Intuitively, L-EBSP states that a large finite structure contains a small ``logically similar'' substructure, where logical similarity means indistinguishability with respect to sentences of L having a given quantifier nesting depth. It turns out that this simply stated property is enjoyed by a variety of classes of interest in computer science: examples include regular languages of words, trees (unordered, ordered or ranked) and nested words, and various classes of graphs, such as cographs, graph classes of bounded tree-depth, those of bounded shrub-depth and n-partite cographs. Further, L-EBSP remains preserved in the classes generated from the above by operations that are implementable using quantifier-free translation schemes. All of the aforementioned classes admit natural tree representations for their structures. We use this fact to show that the small and logically similar substructure of a large structure in any of these classes, can be computed in time linear in the size of the tree representation of the structure, giving linear time fixed parameter tractable (f.p.t.) algorithms for checking L-definable properties of the large structure. We conclude by presenting a strengthening of L-EBSP, that asserts ``logical self-similarity at all scales'' for a suitable notion of scale. We call this the *logical fractal* property and show that most of the classes mentioned above are indeed, logical fractals.

ABSTRACT. Let $\cmso$ denote the counting monadic second order logic of graphs. We give a constructive proof that for some computable function $f$, there is an algorithm $\algorithm$ that takes as input a $\cmso$ sentence $\varphi$, a positive integer $t$, and a connected graph $\agraph$ of maximum degree at most $\Delta$, and determines, in time $f(|\varphi|,\treewidthinput)\cdot 2^{O(\maximumdegree\cdot \treewidthinput)}\cdot |\agraph|^{O(\treewidthinput)}$, whether $\agraph$ has a supergraph $\agraph'$ of treewidth at most $t$ such that $\agraph'\models \varphi$.

The algorithmic metatheorem described above sheds new light on several unresolved questions within the framework of graph completion algorithms. In particular, using this metatheorem, we provide an explicit algorithm that determines, in time $f(d)\cdot 2^{O(\maximumdegree \cdot d)}\cdot |\agraph|^{O(d)}$, whether a connected graph of maximum degree $\Delta$ has a planar supergraph of diameter at most $d$. Additionally, we show that for each fixed $k$, the problem of determining whether $\agraph$ has an $k$-outerplanar supergraph of diameter at most $d$ is strongly uniformly fixed parameter tractable with respect to the parameter $d$.

This result can be generalized in two directions. First, the diameter parameter can be replaced by any contraction-closed effectively CMSO-definable parameter $\graphparameter$. Examples of such parameters are vertex-cover number, dominating number, and many other contraction-bidimensional parameters. In the second direction, the planarity requirement can be relaxed to bounded genus, and more generally, to bounded local treewidth.

ABSTRACT. We introduce the logic ITLe, an intuitionistic temporal logic based on structures (W,R,S) where R is a partial order used to interpret intuitionistic implication and S is an R-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for ITLe are decidable. We prove this by showing that the logic enjoys the strong finite model property; in contrast, we also consider a `persistent' version of the logic, ITLp, whose models are similar to product frames. We prove that, unlike ITLe, ITLp does not have the finite model property.

ABSTRACT. Clausal forms of logics are of great relevance in artificial intelligence, because they couple a high expressivity with a low complexity of reasoning problems. They have been studied for a wide range of classical, modal and temporal logics to obtain tractable fragments of intractable formalisms. In this paper we show that such restrictions can be exploited to lower the complexity of interval temporal logics as well. In particular, we show that for the Horn fragment of the interval logic A,Abar without diamonds the complexity lowers from NEXPTIME-complete to P-complete. We prove also that the tractability of the Horn fragments of interval temporal logics is lost as soon as other modal operators from the HS machinery are added to A,Abar, in most of the cases.

ABSTRACT. Modal Team Logic (MTL) extends Väänänen's Modal Dependence Logic (MDL) by Boolean negation. Its satisfiability problem is decidable, but the exact complexity is not yet understood very well. We investigate a model-theoretical approach and generalize the successful filtration technique to work in team semantics. We identify an "existential" fragment of MTL that enjoys the exponential model property and is therefore, like Propositional Team Logic (PTL), complete for the class AEXP(poly). Moreover, superexponential filtration lower bounds for different fragments of MTL are proven, up to the full logic having no filtration for any elementary size bound. As a corollary, superexponential gaps of succinctness between MTL fragments of equal expressive power are shown.

ABSTRACT. The computational properties of modal and propositional dependence logics have been extensively studied over the past few years, starting from a result by Sevenster showing NEXPTIME-completeness of the satisfiability problem for modal dependence logic. Thus far, however, the validity and entailment properties of these logics have remained uncharacterised to a great extent. This paper establishes a complete classification of the complexity of validity and entailment in modal and propositional dependence logics. In particular, we address the question of the complexity of validity in modal dependence logic. By showing that it is NEXPTIME-complete we refute an earlier conjecture proposing a higher complexity for the problem.

ABSTRACT. We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about open and abstract circuits, with a new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and form, in the presence of feedback, so-called dataflow categories, which have expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.

ABSTRACT. We prove that the B\"uchi topology, the automatic topology, the alphabetic topology and the strong alphabetic topology are Polish, and provide consequences of this.

ABSTRACT. In the presence of suitable power spaces, compactness of X can be characterized as the singleton {X} being open in the space O(X) of open subsets of X. Equivalently, this means that universal quantification over a compact space preserves open predicates.

Using the language of represented spaces, one can make sense of notions such as a $\Sigma^0_2$-subset of the space of $\Sigma^0_2$-subsets of a given space. This suggests higher-order analogues to compactness: We can, e.g., investigate the spaces X where {X} is a $\Delta^0_2$-subset of the space of $\Delta^0_2$-subsets of X. Call this notion $\nabla$-compactness. As $\Delta^0_2$ is self-dual, we find that both universal and existential quantifier over $\nabla$-compact spaces preserve $\Delta^0_2$ predicates.

Recall that a space is called Noetherian iff every subset is compact. Within the setting of Quasi-Polish spaces, we can fully characterize the $\nabla$-compact spaces: A Quasi-Polish space is Noetherian iff it is $\nabla$-compact. Note that the restriction to Quasi-Polish spaces is sufficiently general to include plenty of examples.