Stephan Kreutzer

FOCS Conference 2024 Conference Paper

Cycles of Well-Linked Sets and an Elementary Bound for the Directed Grid Theorem

• Meike Hatzel
• Stephan Kreutzer
• Marcelo Garlet Milani
• Irene Muzi

In 2015, Kawarabayashi and Kreutzer proved the directed grid theorem - the generalisation of the well-known excluded grid theorem to directed graphs - confirming a conjecture by Reed, Johnson, Robertson, Seymour, and Thomas from the mid-nineties. The theorem states the existence of a function $f$ such that every digraph of directed tree-width $f(k)$ contains a cylindrical grid of order $k$ as a butterfly minor, but the given function grows non-elementarily with the size of the grid minor. More precisely, it contains a tower whose height depends on the size of the grid. In this paper, we present an alternative proof of the directed grid theorem which is conceptually much simpler, more modular in its composition and also improves the upper bound for the function $f$ to a power tower of height 22. Our proof is inspired by the breakthrough result of Chekuri and Chuzhoy, who proved a polynomial bound for the excluded grid theorem for undirected graphs. We translate a key concept of their proof to directed graphs by introducing cycles of well-linked sets (CWS), and show that any digraph of high directed tree-width contains a large CWS, which in turn contains a large cylindrical grid, improving the result due to Kawarabayashi and Kreutzer from a non-elementary to an elementary function. An immediate application of our result is that we can improve the bound for Younger's conjecture-the directed Erdős-Pósa property-proved by Reed, Robertson, Seymour and Thomas [2] from a non-elementary to an elementary function. The same improvement applies to other types of Erdős-Pósa style problems on directed graphs. To the best of our knowledge, this is the first significant improvement on the bound for Younger's conjecture since it was proved in 1996. Since its publication in STOC 2015, the Directed Grid Theorem has found numerous applications (see for example [3]–[7]), all of which directly benefit from our main result. Finally, we believe that the theoretical tools developed in this work may find applications beyond the directed grid theorem, in a similar way as the path-of-sets-system framework due to Chekuri and Chuzhoy [8] did for undirected graphs (see for example [9]–[11]).

STOC Conference 2024 Conference Paper

Edge-Disjoint Paths in Eulerian Digraphs

• Dario Giuliano Cavallaro
• Ken-ichi Kawarabayashi
• Stephan Kreutzer

Disjoint paths problems are among the most prominent problems in combinatorial optimisation. The edge- as well as the Vertex-Disjoint Paths problem are NP-complete, both on directed and undirected graphs. But on undirected graphs, Robertson and Seymour developed an algorithm for both problems that runs in cubic time for every fixed number ‍ p of terminal pairs, i.e. they proved that the problem is fixed-parameter tractable on undirected graphs. This is in sharp contrast to the situation on directed graphs, where Fortune, Hopcroft, and Wyllie proved that both problems are NP-complete already for ‍ p =2 terminal pairs. In this paper, we study the Edge-Disjoint Paths problem (EDPP) on Eulerian digraphs, a problem that has received significant attention in the literature. Marx proved that the Eulerian EDPP is NP-complete even on structurally very simple Eulerian digraphs. On the positive side, polynomial time algorithms are known only for very restricted cases, such as ‍ p ≤ 3 or where the demand graph is a union of two stars. The question for which values of ‍ p the Edge-Disjoint Paths problem can be solved in polynomial time on Eulerian digraphs has already been raised by Frank, Ibaraki, and Nagamochi almost 30 years ago. But despite considerable effort, the complexity of the problem is still wide open and is considered to be the main open problem in this area. In this paper, we solve this long-open problem by showing that the Edge-Disjoint Paths problem is fixed-parameter tractable on Eulerian digraphs in general (parameterized by the number of terminal pairs). The algorithm itself is reasonably simple but the proof of its correctness requires a deep structural analysis of Eulerian digraphs.

STOC Conference 2024 Conference Paper

Packing Even Directed Circuits Quarter-Integrally

• Maximilian Gorsky
• Ken-ichi Kawarabayashi
• Stephan Kreutzer
• Sebastian Wiederrecht

We prove the existence of a computable function f ∶ℕ→ℕ such that for every integer k and every digraph D , either D contains a collection C of k directed cycles of even length such that no vertex of D belongs to more than four cycles in C , or there exists a set S ⊆ V ( D ) of size at most f ( k ) such that D − S has no directed cycle of even length. Moreover, we provide an algorithm that finds one of the two outcomes of this statement in time g ( k ) n O (1) for some computable function g ∶ ℕ→ℕ.

SODA Conference 2023 Conference Paper

A half-integral Erdős-Pósa theorem for directed odd cycles

• Ken-ichi Kawarabayashi
• Stephan Kreutzer
• O-joung Kwon
• Qiqin Xie

We prove that there exists a function f: ℕ → ℝ such that every directed graph G contains either k directed odd cycles where every vertex of G is contained in at most two of them, or a set of at most f ( k ) vertices meeting all directed odd cycles. We also give a polynomial-time algorithm for fixed k which outputs one of the two outcomes. Using this algorithmic result, we give a polynomial-time algorithm for fixed k to decide whether such k directed odd cycles exist, or there are no k vertex-disjoint directed odd cycles. This extends the half-integral Erdős-Pósa theorem for undirected odd cycles by Reed [Combinatorica 1999] to directed graphs.

CSL Conference 2022 Conference Paper

Differential Games, Locality, and Model Checking for FO Logic of Graphs

• Jakub Gajarský
• Maximilian Gorsky
• Stephan Kreutzer

We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fraïssé games in which the game is played on only one graph and the moves of both players are restricted. We prove that these games are strong enough to capture essential information about graphs from graph classes which are interpretable in nowhere dense graph classes. This, together with the newly introduced notion of differential locality and the fact that the restriction of possible moves by the players makes it easy to decide the winner of the game in some cases, leads to a new approach to the FO model checking problem which can be used on various graph classes interpretable in classes of sparse graphs.

SODA Conference 2022 Conference Paper

Directed Tangle Tree-Decompositions and Applications

• Archontia C. Giannopoulou
• Ken-ichi Kawarabayashi
• Stephan Kreutzer
• O-joung Kwon

The tangle tree-decomposition theorem, proved by Robertson and Seymour in their seminal graph minors series, turns out to be an extremely valuable tool in structural and algorithmic graph theory. In this paper, we prove the analogous result for digraphs, the directed tangle tree-decomposition theorem. More precisely, we introduce directed tangles and provide a directed tree-decomposition of digraphs G that distinguishes all maximal directed tangles in G. Furthermore, for any integer k, we construct a directed tree-decomposition that distinguishes all directed tangles of order k. By relaxing the bound slightly, we can make the previous result algorithmic: for fixed k, we design a polynomial-time algorithm that finds a directed tree-decomposition distinguishing all directed tangles of order 6 k –1 separated by some separation of order less than k. As a direct application of the tangle tree-decomposition theorem, we prove that for every fixed k there is a polynomial-time algorithm which, on input G, and source and sink vertices ( s 1, t 1 ), …, ( s k, t k ), either finds a family of paths P 1, …, P k such that each P i links s i to t i and every vertex of G is contained in at most two paths, or determines that there is no set of pairwise vertex-disjoint paths each connecting s i to t i. This result improves previous results (with “two” replaced by “three”), and given known hardness results, our result cannot be extended to fixed parameter tractability nor fully vertex-disjoint directed paths.

SODA Conference 2020 Conference Paper

The Directed Flat Wall Theorem

• Archontia C. Giannopoulou
• Ken-ichi Kawarabayashi
• Stephan Kreutzer
• O-joung Kwon

At the core of the Robertson-Seymour Theory of Graph Minors lies a powerful structure theorem which captures, for any fixed graph H, the common structural features of all the graphs not containing H as a minor [15]. An important step towards this structure theorem is the Flat Wall Theorem [14], which has a lot of algorithmic applications (for example, the minor-testing and the disjoint paths problem with fixed number terminals). In this paper, we prove the directed analogue of this Flat Wall Theorem. Our result builds on the recent Directed Grid Theorem by two of the authors (Kawarabayashi and Kreutzer), and we hope that this is an important and significant step toward the directed structure theorem, as with the case for the undirected graph for the graph minor project.

SODA Conference 2019 Conference Paper

Polynomial Planar Directed Grid Theorem

• Meike Hatzel
• Ken-ichi Kawarabayashi
• Stephan Kreutzer

The grid theorem, originally proved by Robertson and Seymour in 1986 [RS10, Graph Minors V], is one of the most central results in the study of graph minors and has found many algorithmic applications, especially in the analysis of routing problems. The relation between treewidth and grid minors is particularly tight for planar graphs, as every planar graph of treewidth at least 6 k contains a grid of order k as a minor [RST94]. This polynomial, in fact linear, bound on the size of grid minors has enabled many important consequences, such as sublinear separators and subexponential algorithms for many NP-hard problems on planar graphs. In the mid-90s, Reed and Johnson, Robertson, Seymour and Thomas proposed a notion of directed treewidth and conjectured an excluded grid theorem for directed graphs. This theorem was proved in 2015 [KK15] by the latter two authors but the function relating directed treewidth and grid minors is very big, even in the planar case. Directed grids have found several algorithmic applications such as low-congestion routing. See e. g. [CE15, CEP16, KKK14, EMW16, AKKW16]. However, in the undirected case the polynomial, in fact linear, bound on the size of grid minors in planar graphs have made this tool so extremely successful. Consequently, the lack of polynomial bounds for directed grid minors in planar digraphs has so far prevented further applications of this technique in the directed setting. The main result of this paper is to close this gap and to establish a polynomial bound for the directed grid theorem on planar digraphs. We are optimistic that this will enable further applications of directed treewidth and its dual notion of directed grids in the context of planar digraphs. Towards the end, we also give “treewidth sparsifier” for directed graphs, which has been already considered in undirected graphs. This result allows us to obtain an Eulerian subgraph of bounded degree in D that still has high directed treewidth. We believe this result is of independent interest for structural graph theory.

CSL Conference 2017 Conference Paper

Current Trends and New Perspectives for First-Order Model Checking (Invited Talk)

• Stephan Kreutzer

The model-checking problem for a logic LLL is the problem of decidig for a given formula phi in LLL and structure AA whether the formula is true in the structure, i. e. whether AA models phi. Model-checking for logics such as First-Order Logic (FO) or Monadic Second-Order Logic (MSO) has been studied intensively in the literature, especially in the context of algorithmic meta-theorems within the framework of parameterized complexity. However, in the past the focus of this line of research was model-checking on classes of sparse graphs, e. g. planar graphs, graph classes excluding a minor or classes which are nowhere dense. By now, the complexity of first-order model-checking on sparse classes of graphs is completely understood. Hence, current research now focusses mainly on classes of dense graphs. In this talk we will briefly review the known results on sparse classes of graphs and explain the complete classification of classes of sparse graphs on which first-order model-checking is tractable. In the second part we will then focus on recent and ongoing research analysing the complexity of first-order model-checking on classes of dense graphs.

SODA Conference 2017 Conference Paper

Polynomial Kernels and Wideness Properties of Nowhere Dense Graph Classes

• Stephan Kreutzer
• Roman Rabinovich 0001
• Sebastian Siebertz

Nowhere dense classes of graphs [21, 22] are very general classes of uniformly sparse graphs with several seemingly unrelated characterisations. From an algorithmic perspective, a characterisation of these classes in terms of uniform quasi-wideness, a concept originating in finite model theory, has proved to be particularly useful. Uniform quasi-wideness is used in many fpt-algorithms on nowhere dense classes. However, the existing constructions showing the equivalence of nowhere denseness and uniform quasi-wideness imply a non-elementary blow up in the parameter dependence of the fpt-algorithms, making them infeasible in practice. As a first main result of this paper, we use tools from logic, in particular from a sub-field of model theory known as stability theory, to establish polynomial bounds for the equivalence of nowhere denseness and uniform quasi-wideness. As an algorithmic application of our new methods, we obtain for every fixed value of r ∊ ℕ a polynomial kernel for the distance- r dominating set problem on nowhere dense classes of graphs. This is particularly interesting, as it implies that for every subgraph-closed class C, the distance- r dominating set problem admits a kernel on C for every value of r if, and only if, it admits a polynomial kernel for every value of r (under the standard assumption of parameterized complexity theory that FPT ≠ W[2]). Finally, we demonstrate how to use the new methods to improve the parameter dependence of many fixed- parameter algorithms. As an example we provide a single exponential parameterized algorithm for the C onnected D ominating S et problem on nowhere dense graph classes.

TCS Journal 2016 Journal Article

Complexity and monotonicity results for domination games

• Stephan Kreutzer
• Sebastian Ordyniak

In this paper we study Domination Games, a class of games introduced by Fomin, Kratsch, and Müller in [8]. Domination games are a variant of the well-known graph searching games (also called cops and robber games), where a number of cops tries to capture a robber hiding on the vertices of a graph. Variants of these games are often used to provide a game-theoretic characterization of important graph parameters such as pathwidth, treewidth, and hypertreewidth. We are primarily interested in questions concerning the complexity and monotonicity of these games. We show that dominating games are computationally much harder than standard cops and robber games and establish strong non-monotonicity results for various notions of monotonicity that arise naturally in the context of domination games. Answering a question of [8], we show that there are graphs where the shortest winning strategy for a minimal number of cops must necessarily be of exponential length.

TCS Journal 2016 Journal Article

DAG-width is PSPACE-complete

• Saeed Akhoondian Amiri
• Stephan Kreutzer
• Roman Rabinovich

Berwanger et al. show in [2] that for every graph G of size n and DAG-width k there is a DAG decomposition of width k and size n O ( k ). They also establish a polynomial time algorithm for deciding whether the DAG-width of a graph is at most a fixed number k. However, if the DAG-width of the graphs is not bounded, such algorithms become exponential. This raises the question whether we can always find a DAG decomposition of size polynomial in n as it is the case for tree width and most other generalisations of tree width similar to DAG-width. In this paper we show that there is an infinite class of graphs such that every DAG decomposition of optimal width has size super-polynomial in n and, moreover, there is no polynomial size DAG decomposition of width at most k + k 1 − ε for every ε ∈ ( 0, 1 ). In the second part we use our construction to prove that deciding whether the DAG-width of a given graph is at most a given value is PSpace-complete.

TCS Journal 2016 Journal Article

Graph operations on parity games and polynomial-time algorithms

• Christoph Dittmann
• Stephan Kreutzer
• Alexandru I. Tomescu

In this paper we establish polynomial-time algorithms for special classes of parity games. In particular we study various constructions for combining graphs that often arise in structural graph theory and show that polynomial-time solvability of parity games is preserved under these operations. This includes the join of two graphs, repeated pasting along vertices, and the addition of a vertex. As a consequence we obtain polynomial time algorithms for parity games whose underlying graph is an orientation of a complete graph (such as tournaments), a complete bipartite graph, a block graph, or a block-cactus graph. These are classes where the problem was not known to be efficiently solvable before.

MFCS Conference 2016 Conference Paper

Routing with Congestion in Acyclic Digraphs

• Saeed Akhoondian Amiri
• Stephan Kreutzer
• Dániel Marx
• Roman Rabinovich 0001

We study the version of the k-disjoint paths problem where k demand pairs (s_1, t_1), .. ., (s_k, t_k) are specified in the input and the paths in the solution are allowed to intersect, but such that no vertex is on more than c paths. We show that on directed acyclic graphs the problem is solvable in time n^{O(d)} if we allow congestion k-d for k paths. Furthermore, we show that, under a suitable complexity theoretic assumption, the problem cannot be solved in time f(k)n^{o(d*log(d))} for any computable function f.

MFCS Conference 2016 Conference Paper

The Generalised Colouring Numbers on Classes of Bounded Expansion

• Stephan Kreutzer
• Michal Pilipczuk
• Roman Rabinovich 0001
• Sebastian Siebertz

The generalised colouring numbers adm_r(G), col_r(G), and wcol_r(G) were introduced by Kierstead and Yang as generalisations of the usual colouring number, also known as the degeneracy of a graph, and have since then found important applications in the theory of bounded expansion and nowhere dense classes of graphs, introduced by Nesetril and Ossona de Mendez. In this paper, we study the relation of the colouring numbers with two other measures that characterise nowhere dense classes of graphs, namely with uniform quasi-wideness, studied first by Dawar et al. in the context of preservation theorems for first-order logic, and with the splitter game, introduced by Grohe et al. We show that every graph excluding a fixed topological minor admits a universal order, that is, one order witnessing that the colouring numbers are small for every value of r. Finally, we use our construction of such orders to give a new proof of a result of Eickmeyer and Kawarabayashi, showing that the model-checking problem for successor-invariant first-order formulas is fixed parameter tractable on classes of graphs with excluded topological minors.

STOC Conference 2015 Conference Paper

The Directed Grid Theorem

• Ken-ichi Kawarabayashi
• Stephan Kreutzer

The grid theorem, originally proved in 1986 by Robertson and Seymour in Graph Minors V, is one of the most central results in the study of graph minors. It has found numerous applications in algorithmic graph structure theory, for instance in bidimensionality theory, and it is the basis for several other structure theorems developed in the graph minors project. In the mid-90s, Reed and Johnson, Robertson, Seymour and Thomas, independently, conjectured an analogous theorem for directed graphs, i.e. the existence of a function f : N-> N such that every digraph of directed tree width at least f(k) contains a directed grid of order k. In an unpublished manuscript from 2001, Johnson, Robertson, Seymour and Thomas give a proof of this conjecture for planar digraphs. But for over a decade, this was the most general case proved for the conjecture. Only very recently, this result has been extended by Kawarabayashi and Kreutzer to all classes of digraphs excluding a fixed undirected graph as a minor. In this paper, nearly two decades after the conjecture was made, we are finally able to confirm the Reed, Johnson, Robertson, Seymour and Thomas conjecture in full generality. As consequence of our results we are able to improve results by Reed 1996 on disjoint cycles of length at least l and by Kawarabayashi, Kobayashi, Kreutzer on quarter-integral disjoint paths. We expect many more algorithmic results to follow from the grid theorem.

SODA Conference 2014 Conference Paper

An Excluded Grid Theorem for Digraphs with Forbidden Minors

• Ken-ichi Kawarabayashi
• Stephan Kreutzer

STOC Conference 2014 Conference Paper

An excluded half-integral grid theorem for digraphs and the directed disjoint paths problem

• Ken-ichi Kawarabayashi
• Yusuke Kobayashi 0001
• Stephan Kreutzer

The excluded grid theorem, originally proved by Robertson and Seymour in Graph Minors V, is one of the most central results in the study of graph minors. It has found numerous applications in algorithmic graph structure theory, for instance as the basis for bidimensionality theory on graph classes excluding a fixed minor. In 1997, Reed [25] and later Johnson, Robertson, Seymour and Thomas [17] conjectured an analogous theorem for directed graphs, i.e. the existence of a function f : N → N such that every digraph of directed tree-width at least f ( k ) contains a directed grid of order k . In this paper, we make significant progress toward this conjecture. Namely, we prove that every digraph of directed tree-width at least f ( k ) contains a "half-integral" directed grid of order k . This structural result allows us to contribute to the disjoint paths problem. We show that the following can be done in polynomial time: Suppose that we are given a digraph G and k terminal pairs ( s 1 , t 1 ), ( s 2 , t 2 ),..., ( s k , t k ), where k is a fixed constant. In polynomial time, either • we can find k paths P 1 ,..., P k such that P i is from s i to t i for i = 1,..., k and every vertex in G is in at most four of the paths, or • we can conclude that G does not contain disjoint paths P 1 ,..., P k such that P i is from s i to t i for i = 1,..., k . To the best of our knowledge, this is the first positive result for the general directed disjoint paths problem. Note that the directed disjoint paths problem is NP-hard even for k = 2. Therefore, polynomial-time algorithms for semiintegral disjoint paths is the best one can hope for.

STOC Conference 2014 Conference Paper

Deciding first-order properties of nowhere dense graphs

• Martin Grohe
• Stephan Kreutzer
• Sebastian Siebertz

Nowhere dense graph classes, introduced by Nešetřil and Ossona de Mendez [30], form a large variety of classes of "sparse graphs" including the class of planar graphs, actually all classes with excluded minors, and also bounded degree graphs and graph classes of bounded expansion. We show that deciding properties of graphs definable in first-order logic is fixed-parameter tractable on nowhere dense graph classes. At least for graph classes closed under taking subgraphs, this result is optimal: it was known before that for all classes C of graphs closed under taking subgraphs, if deciding first-order properties of graphs in C is fixed-parameter tractable, then C must be nowhere dense (under a reasonable complexity theoretic assumption). As a by-product, we give an algorithmic construction of sparse neighbourhood covers for nowhere dense graphs. This extends and improves previous constructions of neighbourhood covers for graph classes with excluded minors. At the same time, our construction is considerably simpler than those. Our proofs are based on a new game-theoretic characterisation of nowhere dense graphs that allows for a recursive version of locality-based algorithms on these classes. On the logical side, we prove a "rank-preserving" version of Gaifman's locality theorem.

SODA Conference 2013 Conference Paper

Packing directed cycles through a specified vertex set

• Ken-ichi Kawarabayashi
• Daniel Král'
• Marek Krcál
• Stephan Kreutzer

A seminal result of Reed et al. [15] in 1996 states that the Erdős-Pósa property holds for directed cycles, i. e. for every integer n there is an integer t such that every directed graph G has n pairwise vertex disjoint directed cycles or contains a set T ⊆ V ( G ) of at most t vertices such that G − T contains no directed cycle. In this paper, we consider the Erdő-Pósa property for directed cycles through a vertex in a given vertex set S, i. e. the question if for every integer n there is an integer t such that if G is a directed graph G and S is a set of vertices then G has n pairwise vertex disjoint directed cycles each containing a vertex of S or contains a set T of at most t vertices such that G − T contains no such directed cycle. For undirected graphs, this property holds for cycles through a vertex in a vertex set S (see Kakimura, Kawarabayashi and Marx [9], and Pontecorvi and Wollan [12]). In this paper, we show the following: The Erdős-Pósa does hold for half-integral packings of directed cycles each containing a vertex from S, i. e. where every vertex of the graph is contained in at most 2 cycles. On the other hand, an example shows that the Erdős-Pósa property does not hold without this relaxation.

SODA Conference 2012 Conference Paper

Directed nowhere dense classes of graphs

• Stephan Kreutzer
• Siamak Tazari

Many natural computational problems on graphs such as finding dominating or independent sets of a certain size are well known to be intractable, both in the classical sense as well as in the framework of parameterized complexity. Much work therefore has focussed on exhibiting restricted classes of graphs on which these problems become tractable. While in the case of undirected graphs, there is a rich structure theory which can be used to develop tractable algorithms for these problems on large classes of undirected graphs, such a theory is much less developed for directed graphs. Many attempts to identify structure properties of directed graphs tailored towards algorithmic applications have focussed on a directed analogue of undirected tree-width. These attempts have proved to be successful in the development of algorithms for linkage problems but none of the existing width-measures allow for tractable solutions to important problems such as dominating sets and many other related problems. In this paper we take a radically different approach to identifying classes of directed graphs where domination and other problems become tractable. In particular, whereas most existing approaches treat the class of acyclic graphs as simple in their respective width measure, we will specifically study classes of digraphs which do not contain all acyclic digraphs. It is this new approach that make the algorithmic results reported herein possible. More specifically, we introduce the concept of shallow directed minors and based on this a new classification of classes of directed graphs which is diametric to existing directed graph decompositions and directed width measures proposed in the literature. We then study in depth one type of classes of directed graphs which we call nowhere crownful. The classes are very general as they include, on the one hand, all classes of directed graphs whose underlying undirected class is nowhere dense, such as planar, bounded-genus, and H -minor-free graphs; and on the other hand, also contain classes of high edge density whose underlying class is not nowhere dense. Yet we are able to show that problems such as directed dominating set and many others become fixed-parameter tractable on nowhere crownful classes of directed graphs. This is of particular interest as these problems are not tractable on any existing digraph measure for sparse classes. The algorithmic results are established via proving a structural equivalence of nowhere crownful classes and classes of graphs which are directed uniformly quasi-wide. While this result is inspired by [Nešetřil and Ossona de Mendez 2008], their proof method does not extend to the directed case and a different and much more involved proof is needed, turning it into a particularly significant part of our contribution.

TCS Journal 2012 Journal Article

Foreword: Special Issue on Theory and Applications of Graph Searching Problems

• Fedor V. Fomin
• Pierre Fraigniaud
• Stephan Kreutzer
• Dimitrios M. Thilikos

TCS Journal 2011 Journal Article

Digraph decompositions and monotonicity in digraph searching

• Stephan Kreutzer
• Sebastian Ordyniak

Graph decompositions such as tree-decompositions and associated width measures have been the focus of much attention in structural and algorithmic graph theory. In particular, it has been found that many otherwise intractable problems become tractable on graph classes of bounded tree-width. More recently, proposals have been made to define a similar notion to tree-width for directed graphs. Several proposals have appeared so far, supported by algorithmic applications. In this paper we explore the limits of algorithmic applicability of digraph decompositions and show that various natural candidates for problems, which potentially could benefit from digraphs having small “directed width”, remain NP-complete even on almost acyclic graphs. Closely related to graph and digraph decompositions are graph searching games. An important property of graph searching games is monotonicity and a large number of papers addresses the question whether particular variants of these games are monotone. However, so far for two natural types of graph searching games–underlying DAG- and Kelly-decompositions–the question whether they are monotone was still open. We settle this issue by showing that both variants, the visible and the inert invisible graph searching games on directed graphs, are non-monotone.

SODA Conference 2010 Conference Paper

On Brambles, Grid-Like Minors, and Parameterized Intractability of Monadic Second-Order Logic

• Stephan Kreutzer
• Siamak Tazari

CSL Conference 2009 Conference Paper

On the Parameterised Intractability of Monadic Second-Order Logic

• Stephan Kreutzer

Abstract One of Courcelle’s celebrated results states that if \({\mathcal C}\) is a class of graphs of bounded tree-width, then model-checking for monadic second order logic ( MSO 2 ) is fixed-parameter tractable (fpt) on \({\mathcal C}\) by linear time parameterised algorithms. An immediate question is whether this is best possible or whether the result can be extended to classes of unbounded tree-width. In this paper we show that in terms of tree-width, the theorem can not be extended much further. More specifically, we show that if \({\mathcal C}\) is a class of graphs which is closed under colourings and satisfies certain constructibility conditions such that the tree-width of \({\mathcal C}\) is not bounded by log 16 n then MSO 2 -model checking is not fpt unless Sat can be solved in sub-exponential time. If the tree-width of \({\mathcal C}\) is not poly-log. bounded, then MSO 2 -model checking is not fpt unless all problems in the polynomial-time hierarchy can be solved in sub-exponential time.

SODA Conference 2008 Conference Paper

Computing excluded minors

• Isolde Adler
• Martin Grohe
• Stephan Kreutzer

TCS Journal 2008 Journal Article

Digraph measures: Kelly decompositions, games, and orderings

• Paul Hunter
• Stephan Kreutzer

We consider various well-known, equivalent complexity measures for graphs such as elimination orderings, k -trees and cops and robber games and study their natural translations to digraphs. We show that on digraphs the translations of these measures are also equivalent and induce a natural connectivity measure. We introduce a decomposition for digraphs and an associated width, Kelly-width, which is equivalent to the aforementioned measure. We demonstrate its usefulness by exhibiting potential applications including polynomial-time algorithms for NP-complete problems on graphs of bounded Kelly-width, and complexity analysis of asymmetric matrix factorization. Finally, we compare the new width to other known decompositions of digraphs.

SODA Conference 2007 Conference Paper

Digraph measures: Kelly decompositions, games, and orderings

• Paul Hunter 0001
• Stephan Kreutzer

TCS Journal 2007 Journal Article

Generalising automaticity to modal properties of finite structures

• Anuj Dawar
• Stephan Kreutzer

We introduce a complexity measure of modal properties of finite structures which generalises the automaticity of languages. It is based on graph-automata-like devices called labelling systems. We define a measure of the size of a structure that we call rank, and show that any modal property of structures can be approximated up to any fixed rank n by a labelling system. The function that takes n to the size of the smallest labelling system doing this is called the labelling index of the property. We demonstrate that this is a useful and fine-grained measure of complexity and show that it is especially well suited to characterise the expressive power of modal fixed-point logics. From this we derive several separation results of modal and non-modal fixed-point logics, some of which are already known whereas others are new.

TCS Journal 2006 Journal Article

Backtracking games and inflationary fixed points

• Anuj Dawar
• Erich Grädel
• Stephan Kreutzer

We define a new class of games, called backtracking games. Backtracking games are essentially parity games with an additional rule allowing players, under certain conditions, to return to an earlier position in the play and revise a choice or to force a countback of the number of moves. This new feature makes backtracking games more powerful than parity games. As a consequence, winning strategies become more complex objects and computationally harder. The corresponding increase in expressiveness allows us to use backtracking games as model-checking games for inflationary fixed-point logics such as IFP or MIC. We identify a natural subclass of backtracking games, the simple games, and show that these are the “right” model-checking games for IFP by (a) giving a translation of formulae φ and structures A into simple games such that A ⊨ φ if, and only if, Player 0 wins the corresponding game and (b) showing that the winner of simple backtracking games can again be defined in IFP.

CSL Conference 2005 Conference Paper

The Complexity of Independence-Friendly Fixpoint Logic

• Julian C. Bradfield
• Stephan Kreutzer

Abstract We study the complexity of model-checking for the fixpoint extension of Hintikka and Sandu’s independence-friendly logic. We show that this logic captures ExpTime; and by embedding PFP, we show that its combined complexity is ExpSpace -hard, and moreover the logic includes second order logic (on finite structures).

MFCS Conference 2005 Conference Paper

The Expressive Power of Two-Variable Least Fixed-Point Logics

• Martin Grohe
• Stephan Kreutzer
• Nicole Schweikardt

Abstract The present paper gives a classification of the expressive power of two-variable least fixed-point logics. The main results are: 1 The two-variable fragment of monadic least fixed-point logic with parameters is as expressive as full monadic least fixed-point logic (on binary structures). 2 The two-variable fragment of monadic least fixed-point logic without parameters is as expressive as the two-variable fragment of binary least fixed-point logic without parameters. 3 The two-variable fragment of binary least fixed-point logic with parameters is strictly more expressive than the two-variable fragment of monadic least fixed-point logic with parameters (even on finite strings).

LPAR Conference 2003 Conference Paper

Once upon a Time in a West - Determinacy, Definability, and Complexity of Path Games

• Dietmar Berwanger
• Erich Grädel
• Stephan Kreutzer

We study determinacy, definability and complexity issues of path games on finite and infinite graphs. Compared to the usual format of infinite games on graphs (such as Gale-Stewart games) we consider here a different variant where the players select in each move a path of arbitrary finite length, rather than just an edge. The outcome of a play is an infinite path, the winning condition hence is a set of infinite paths, possibly given by a formula from S1S, LTL, or first-order logic. Such games have a long tradition in descriptive set theory (in the form of Banach-Mazur games) and have recently been shown to have interesting application for planning in nondeterministic domains. It turns out that path games behave quite differently than classical graph games. For instance, path games with Muller conditions always admit positional winning strategies which are computable in polynomial time. With any logic on infinite paths (defining a winning condition) we can associate a logic on graphs, defining the winning regions of the associated path games. We explore the relationships between these logics. For instance, the winning regions of path games with an S1S-winning condition are definable in the modal mu-calculus. Further, if the winning condition is first-order (on paths), then the winning regions are definable in monadic path logic, or, for a large class of games, even in first-order logic. As a consequence, winning regions of LTL path games are definable in CTL.

CSL Conference 2002 Conference Paper

Partial Fixed-Point Logic on Infinite Structures

• Stephan Kreutzer

Abstract We consider an alternative semantics for partial fixed-point logic (PFP). To define the fixed point of a formula in this semantics, the sequence of stages induced by the formula is considered. As soon as this sequence becomes cyclic, the set of elements contained in every stage of the cycle is taken as the fixed point. It is shown that on finite structures, this fixed-point semantics and the standard semantics for PFP as considered in finite model theory are equivalent, although arguably the formalisation of properties might even become simpler and more intuitive. Contrary to the standard PFP semantics which is only defined on finite structures the new semantics generalises easily to infinite structures and transfinite inductions. In this generality we compare - in terms of expressive power - partial with other known fixed-point logics. The main result of the paper is that on arbitrary structures, PFP is strictly more expressive than inflationary fixed-point logic (IFP). A separation of these logics on finite structures would prove Ptime different from Pspace.

CSL Conference 2001 Conference Paper

Inflationary Fixed Points in Modal Logic

• Anuj Dawar
• Erich Grädel
• Stephan Kreutzer

Abstract We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal μ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed point operators to first order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC) we introduce has much greater expressive power than the μ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.

LPAR Conference 2001 Conference Paper

Operational Semantics for Fixed-Point Logics on Constraint Databases

• Stephan Kreutzer

Abstract In this paper we compare the expressive power of various fixed-point logics on linear or dense order constraint databases. This comparison is not done on absolute terms, i. e. by comparing their expressive power for arbitrary queries, rather for definability of partially recursive queries. The motivation for choosing this benchmark comes from fixed-point logics as query languages for constraint databases. Here, non-recursive queries are of no practical interest. It is shown that for linear constraint databases already transitive closure logic is expressive enough to define all partially recursive queries, i. e. , transitive-closure logic is expressively complete for this class of databases. It follows that transitive-closure, least, and stratified fixed-point logic are equivalent with respect to this benchmark.

CSL Conference 1999 Conference Paper

Descriptive Complexity Theory for Constraint Databases

• Erich Grädel
• Stephan Kreutzer

Abstract We consider the data complexity of various logics on two important classes of constraint databases: dense order and linear constraint databases. For dense order databases, we present a general result allowing us to lift results on logics capturing complexity classes from the class of finite ordered databases to dense order constraint databases. Considering linear constraints, we show that there is a significant gap between the data complexity of first-order queries on linear constraint databases over the real and the natural numbers. This is done by proving that for arbitrary high levels of the Presburger arithmetic there are complete first-order queries on databases over (ℕ, <, +). The proof of the theorem demonstrates a simple argument for the translating complexity results for prefix classes in logical theories to results on the complexity of query evaluation in contraint boundary databases.