Stephan Kreutzer

dblp:k/StephanKreutzer · DBLP profile ↗
← Back
81ranked-venue papers
20as first author
9since 2021 · last 2026
0009-0002-9409-5356ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 77 · 18 first-author · 9 since 2021Databases, data management, data science and information retrieval · 3 · 2 first-authorArtificial intelligence and machine learning · 2 · 1 first-authorGraphics, computer vision, multimedia, augmented reality and games · 1Applied, interdisciplinary, general and emerging computing · 1
YearPublicationVenuePosition
2026 Well-Quasi-Ordering Eulerian Digraphs: Bounded Carving Width
abstract
We prove that every class of Eulerian directed graphs of bounded carving width (equivalently, of bounded degree and treewidth) is well-quasi-ordered by strong immersion. In fact, we prove a stronger result, namely that every class of Eulerian directed graphs of bounded carving width, where every vertex is additionally labelled from a well-quasi-order, fixes a linear order on its incident edges, and may impose further restrictions on how the immersion is allowed to route paths through it, is well-quasi-ordered by an adequate notion of strong immersion. To this extent, we develop a framework seemingly suited to prove well-quasi-ordering for classes of Eulerian directed graphs by (strong) immersion and present a first meta theorem in that direction. We complement our results by observing that the class of Eulerian directed graphs of unbounded degree is not well-quasi-ordered by strong immersion, even if we assume the treewidth of the class to be at most two. We conclude with a dichotomy result, proving for a very restricted class of Eulerian directed graphs of unbounded degree that it is not well-quasi-ordered by strong immersion, but it is well-quasi-ordered by weak immersion.
Dario Cavallaro, Ken-ichi Kawarabayashi, Stephan Kreutzer
ICALP3
2026 The Directed Disjoint Paths Problem with Congestion
abstract
The classic result by Fortune, Hopcroft, and Wyllie [TCS ’80] states that the directed disjoint paths problem is NP-complete even for two pairs of terminals. Extending this well-known result, we show that the directed disjoint paths problem is NP-complete for any constant congestion \(c \ge 1\) and \(k \ge 3c - 1\) pairs of terminals. This refutes a conjecture by Giannopoulou et al. [SODA ’22], which says that the directed disjoint paths problem with congestion two is polynomial-time solvable for any constant number \(k\) of terminal pairs. We then consider the cases that are not covered by this hardness result. The first nontrivial case is \(c = 2\) and \(k = 3\). Our second main result is to show that this case is polynomial-time solvable.
Matthias Bentert, Dario Cavallaro, Amelie Heindl, Ken-ichi Kawarabayashi, Stephan Kreutzer, Johannes Schröder
SODA5
2024 Cycles of Well-Linked Sets and an Elementary Bound for the Directed Grid Theorem
abstract
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]).
Meike Hatzel, Stephan Kreutzer, Marcelo Garlet Milani, Irene Muzi
FOCS2
2024 Edge-Disjoint Paths in Eulerian Digraphs
abstract
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.
Dario Cavallaro, Ken-ichi Kawarabayashi, Stephan Kreutzer
STOC3
2024 Packing Even Directed Circuits Quarter-Integrally
abstract
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)nO(1) for some computable function g∶ ℕ→ℕ.
Maximilian Gorsky, Ken-ichi Kawarabayashi, Stephan Kreutzer, Sebastian Wiederrecht
STOC3
2023 A half-integral Erdős-Pósa theorem for directed odd cycles
abstract
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.
Ken-ichi Kawarabayashi, Stephan Kreutzer, O-joung Kwon, Qiqin Xie
SODA2
2022 Differential Games, Locality, and Model Checking for FO Logic of Graphs
Jakub Gajarský, Maximilian Gorsky, Stephan Kreutzer
CSL3
2022 Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
abstract
An interpretation is an operation that maps an input graph to an output graph by redefining its edge relation using a first-order formula. This rich framework includes operations such as taking the complement or a fixed power of a graph as (very) special cases.
Édouard Bonnet, Jan Dreier, Jakub Gajarský, Stephan Kreutzer, Nikolas Mählmann, Pierre Simon, Szymon Torunczyk
LICS4
2022 Directed Tangle Tree-Decompositions and Applications
abstract
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 6k–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 (s1, t1),…, (sk, tk), either finds a family of paths P1,…, Pk such that each Pi links si to ti 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 si to ti. 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.
Archontia C. Giannopoulou, Ken-ichi Kawarabayashi, Stephan Kreutzer, O-joung Kwon
SODA3
2020 The Directed Flat Wall Theorem
abstract
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.
Archontia C. Giannopoulou, Ken-ichi Kawarabayashi, Stephan Kreutzer, O-joung Kwon
SODA3
2020 Computing Shrub-Depth Decompositions
abstract
Shrub-depth is a width measure of graphs which, roughly speaking, corresponds to the smallest depth of a tree into which a graph can be encoded. It can be thought of as a low-depth variant of clique-width (or rank-width), similarly as treedepth is a low-depth variant of treewidth. We present an fpt algorithm for computing decompositions of graphs of bounded shrub-depth. To the best of our knowledge, this is the first algorithm which computes the decomposition directly, without use of rank-width decompositions and FO or MSO logic.
Jakub Gajarský, Stephan Kreutzer
STACS2
2020 Model-Checking on Ordered Structures
abstract
We study the model-checking problem for first- and monadic second-order logic on finite relational structures. The problem of verifying whether a formula of these logics is true on a given structure is considered intractable in general, but it does become tractable on interesting classes of structures, such as on classes whose Gaifman graphs have bounded treewidth. In this article, we continue this line of research and study model-checking for first- and monadic second-order logic in the presence of an ordering on the input structure. We do so in two settings: the general ordered case, where the input structures are equipped with a fixed order or successor relation, and the order-invariant case, where the formulas may resort to an ordering, but their truth must be independent of the particular choice of order. In the first setting we show very strong intractability results for most interesting classes of structures. In contrast, in the order-invariant case we obtain tractability results for order-invariant monadic second-order formulas on the same classes of graphs as in the unordered case. For first-order logic, we obtain tractability of successor-invariant formulas on classes whose Gaifman graphs have bounded expansion. Furthermore, we show that model-checking for order-invariant first-order formulas is tractable on coloured posets of bounded width.
Kord Eickmeyer, Jan van den Heuvel, Ken-ichi Kawarabayashi, Stephan Kreutzer, Patrice Ossona de Mendez, Michal Pilipczuk, Daniel Quiroz 0001, Roman Rabinovich 0001, Sebastian Siebertz
ACM Trans. Comput. Log.4
2020 First-Order Interpretations of Bounded Expansion Classes
abstract
The notion of bounded expansion captures uniform sparsity of graph classes and renders various algorithmic problems that are hard in general tractable. In particular, the model-checking problem for first-order logic is fixed-parameter tractable over such graph classes. With the aim of generalizing such results to dense graphs, we introduce classes of graphs with structurally bounded expansion , defined as first-order transductions of classes of bounded expansion. As a first step towards their algorithmic treatment, we provide their characterization analogous to the characterization of classes of bounded expansion via low treedepth covers (or colorings), replacing treedepth by its dense analogue called shrubdepth.
Jakub Gajarský, Stephan Kreutzer, Jaroslav Nesetril, Patrice Ossona de Mendez, Michal Pilipczuk, Sebastian Siebertz, Szymon Torunczyk
ACM Trans. Comput. Log.2
2019 Polynomial Planar Directed Grid Theorem
abstract
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 6k 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.
Meike Hatzel, Ken-ichi Kawarabayashi, Stephan Kreutzer
SODA3
2019 Algorithmic Properties of Sparse Digraphs
abstract
The notions of bounded expansion [Nešetřil and Ossona de Mendez, 2008] and nowhere denseness [Nešetřil and Ossona de Mendez, 2011], introduced by Nešetřil and Ossona de Mendez as structural measures for undirected graphs, have been applied very successfully in algorithmic graph theory. We study the corresponding notions of directed bounded expansion and nowhere crownfulness on directed graphs, introduced by Kreutzer and Tazari [Kreutzer and Tazari, 2012]. The classes of directed graphs having those properties are very general classes of sparse directed graphs, as they include, on one hand, all classes of directed graphs whose underlying undirected class has bounded expansion, such as planar, bounded-genus, and H-minor-free graphs, and on the other hand, they also contain classes whose underlying undirected class is not even nowhere dense. We show that many of the algorithmic tools that were developed for undirected bounded expansion classes can, with some care, also be applied in their directed counterparts, and thereby we highlight a rich algorithmic structure theory of directed bounded expansion and nowhere crownful classes.
Stephan Kreutzer, Irene Muzi, Patrice Ossona de Mendez, Roman Rabinovich 0001, Sebastian Siebertz
STACS1
2019 Routing with congestion in acyclic digraphs
abstract
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 .
Saeed Akhoondian Amiri, Stephan Kreutzer, Dániel Marx, Roman Rabinovich 0001
Inf. Process. Lett.2
2019 Polynomial Kernels and Wideness Properties of Nowhere Dense Graph Classes
abstract
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 article, 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. A powerful method in parameterized complexity theory is to compute a problem kernel in a pre-computation step, that is, to reduce the input instance in polynomial time to a sub-instance of size bounded in the parameter only (independently of the input graph size). Our new tools allow us to obtain for every fixed radius r ∈ N a polynomial kernel for the distance- r dominating set problem on nowhere dense classes of graphs. This result is particularly interesting, as it implies that for every class C of graphs that is closed under taking subgraphs, the distance- r dominating set problem admits a kernel on C for every value of r if, and only if, it already admits a polynomial kernel for every value of r (under the standard assumption of parameterized complexity theory that FPT ≠ W[2]).
Stephan Kreutzer, Roman Rabinovich 0001, Sebastian Siebertz
ACM Trans. Algorithms1
2018 On Zero-One and Convergence Laws for Graphs Embeddable on a Fixed Surface
abstract
We show that for no surface except for the plane does monadic second-order logic (MSO) have a zero-one-law - and not even a convergence law - on the class of (connected) graphs embeddable on the surface. In addition we show that every rational in [0,1] is the limiting probability of some MSO formula. This strongly refutes a conjecture by Heinig et al. (2014) who proved a convergence law for planar graphs, and a zero-one law for connected planar graphs, and also identified the so-called gaps of [0,1]: the subintervals that are not limiting probabilities of any MSO formula. The proof relies on a combination of methods from structural graph theory, especially large face-width embeddings of graphs on surfaces, analytic combinatorics, and finite model theory, and several parts of the proof may be of independent interest. In particular, we identify precisely the properties that make the zero-one law work on planar graphs but fail for every other surface.
Albert Atserias, Stephan Kreutzer, Marc Noy
ICALP2
2018 First-Order Interpretations of Bounded Expansion Classes
Jakub Gajarský, Stephan Kreutzer, Jaroslav Nesetril, Patrice Ossona de Mendez, Michal Pilipczuk, Sebastian Siebertz, Szymon Torunczyk
ICALP2
2018 Coloring and Covering Nowhere Dense Graphs
abstract
In [M. Grohe, S. Kreutzer, and S. Siebertz, J. ACM, 64 (2017), 17] it was shown that nowhere dense classes of graphs admit sparse neighborhood covers of small degree. We show that a monotone graph class admits sparse neighborhood covers if and only if it is nowhere dense. The existence of such covers for nowhere dense classes is established through bounds on so-called weak coloring numbers. The core results of this paper are various lower and upper bounds on the weak coloring numbers and other, closely related, generalized coloring numbers. We prove tight bounds for these numbers on graphs of bounded treewidth. We clarify and tighten the relation between the density of shallow minors and the various generalized coloring numbers. These upper bounds are complemented by new, stronger exponential lower bounds on the weak and strong coloring numbers, and by superpolynomial lower bounds on the weak coloring numbers on classes of polynomial expansion. Finally, we show that computing weak $r$-coloring numbers is NP-complete for all $r\geq 3$.
Martin Grohe, Stephan Kreutzer, Roman Rabinovich 0001, Sebastian Siebertz, Konstantinos S. Stavropoulos
SIAM J. Discret. Math.2
2017 Current Trends and New Perspectives for First-Order Model Checking (Invited Talk)
abstract
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.
Stephan Kreutzer
CSL1
2017 Neighborhood Complexity and Kernelization for Nowhere Dense Classes of Graphs
abstract
We prove that whenever G is a graph from a nowhere dense graph class C, and A is a subset of vertices of G, then the number of subsets of A that are realized as intersections of A with r-neighborhoods of vertices of G is at most f(r,eps)|A|^(1+eps), where r is any positive integer, eps is any positive real, and f is a function that depends only on the class C. This yields a characterization of nowhere dense classes of graphs in terms of neighborhood complexity, which answers a question posed by [Reidl et al., CoRR, 2016]. As an algorithmic application of the above result, we show that for every fixed integer r, the parameterized Distance-r Dominating Set problem admits an almost linear kernel on any nowhere dense graph class. This proves a conjecture posed by [Drange et al., STACS 2016], and shows that the limit of parameterized tractability of Distance-r Dominating Set on subgraph-closed graph classes lies exactly on the boundary between nowhere denseness and somewhere denseness.
Kord Eickmeyer, Archontia C. Giannopoulou, Stephan Kreutzer, O-joung Kwon, Michal Pilipczuk, Roman Rabinovich 0001, Sebastian Siebertz
ICALP3
2017 Model-checking for successor-invariant first-order formulas on graph classes of bounded expansion
abstract
A successor-invariant first-order formula is a formula that has access to an auxiliary successor relation on a structure's universe, but the model relation is independent of the particular interpretation of this relation. It is well known that successor-invariant formulas are more expressive on finite structures than plain first-order formulas without a successor relation. This naturally raises the question whether this increase in expressive power comes at an extra cost to solve the model-checking problem, that is, the problem to decide whether a given structure together with some (and hence every) successor relation is a model of a given formula. It was shown earlier that adding successor-invariance to first-order logic essentially comes at no extra cost for the model-checking problem on classes of finite structures whose underlying Gaifman graph is planar [1], excludes a fixed minor [2] or a fixed topological minor [3], [4]. In this work we show that the model-checking problem for successor-invariant formulas is fixed-parameter tractable on any class of finite structures whose underlying Gaifman graphs form a class of bounded expansion. Our result generalises all earlier results and comes close to the best tractability results on nowhere dense classes of graphs currently known for plain first-order logic.
Jan van den Heuvel, Stephan Kreutzer, Michal Pilipczuk, Daniel Quiroz 0001, Roman Rabinovich 0001, Sebastian Siebertz
LICS2
2017 Polynomial Kernels and Wideness Properties of Nowhere Dense Graph Classes
abstract
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 Connected Dominating Set problem on nowhere dense graph classes.
Stephan Kreutzer, Roman Rabinovich 0001, Sebastian Siebertz
SODA1
2017 Structural Properties and Constant Factor-Approximation of Strong Distance-r Dominating Sets in Sparse Directed Graphs
abstract
Bounded expansion and nowhere dense graph classes, introduced by Nesetril and Ossona de Mendez, form a large variety of classes of uniformly sparse graphs which includes the class of planar graphs, actually all classes with excluded minors, and also bounded degree graphs. Since their initial definition it was shown that these graph classes can be defined in many equivalent ways: by generalised colouring numbers, neighbourhood complexity, sparse neighbourhood covers, a game known as the splitter game, and many more. We study the corresponding concepts for directed graphs. We show that the densities of bounded depth directed minors and bounded depth topological minors relate in a similar way as in the undirected case. We provide a characterisation of bounded expansion classes by a directed version of the generalised colouring numbers. As an application we show how to construct sparse directed neighbourhood covers and how to approximate directed distance-r dominating sets on classes of bounded expansion. On the other hand, we show that linear neighbourhood complexity does not characterise directed classes of bounded expansion.
Stephan Kreutzer, Roman Rabinovich 0001, Sebastian Siebertz, Grischa Weberstädt
STACS1
2017 Deciding First-Order Properties of Nowhere Dense Graphs
abstract
Nowhere dense graph classes, introduced by Nešetřil and Ossona de Mendez [2010, 2011], 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 (parameterized by the length of the input formula). 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 neighborhood covers for nowhere dense graphs. This extends and improves previous constructions of neighborhood 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 characterization 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.
Martin Grohe, Stephan Kreutzer, Sebastian Siebertz
J. ACM2
2016 Routing with Congestion in Acyclic Digraphs
Saeed Akhoondian Amiri, Stephan Kreutzer, Dániel Marx, Roman Rabinovich 0001
MFCS2
2016 The Generalised Colouring Numbers on Classes of Bounded Expansion
abstract
The generalised colouring numbers $\mathrm{adm}_r(G)$, $\mathrm{col}_r(G)$, and $\mathrm{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 Nešetřil 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.
Stephan Kreutzer, Michal Pilipczuk, Roman Rabinovich 0001, Sebastian Siebertz
MFCS1
2016 Kernelization and Sparseness: the Case of Dominating Set
Pål Grønås Drange, Markus S. Dregi, Fedor V. Fomin, Stephan Kreutzer, Daniel Lokshtanov, Marcin Pilipczuk, Michal Pilipczuk, Felix Reidl, Fernando Sánchez Villaamil, Saket Saurabh 0001, Sebastian Siebertz, Somnath Sikdar
STACS4
2016 Directed elimination games
Viktor Engelmann, Sebastian Ordyniak, Stephan Kreutzer
Discret. Appl. Math.3
2016 Preface
Andrei A. Bulatov, Stephan Kreutzer
Theory Comput. Syst.2
2016 DAG-width is PSPACE-complete
Saeed Akhoondian Amiri, Stephan Kreutzer, Roman Rabinovich 0001
Theor. Comput. Sci.2
2016 Graph operations on parity games and polynomial-time algorithms
Christoph Dittmann, Stephan Kreutzer, Alexandru I. Tomescu
Theor. Comput. Sci.2
2016 Complexity and monotonicity results for domination games
Stephan Kreutzer, Sebastian Ordyniak
Theor. Comput. Sci.1
2015 Towards the Graph Minor Theorems for Directed Graphs
Ken-ichi Kawarabayashi, Stephan Kreutzer
ICALP (2)2
2015 Graph Searching Games and Width Measures for Directed Graphs
abstract
In cops and robber games a number of cops tries to capture a robber in a graph. A variant of these games on undirected graphs characterises tree width by the least number of cops needed to win. We consider cops and robber games on digraphs and width measures (such as DAG-width, directed tree width or D-width) corresponding to them. All of them generalise tree width and the game characterising it. For the DAG-width game we prove that the problem to decide the minimal number of cops required to capture the robber (which is the same as deciding DAG-width), is PSPACE-complete, in contrast to most other similar games. We also show that the cop-monotonicity cost for directed tree width games cannot be bounded by any function. As a consequence, D-width is not bounded in directed tree width, refuting a conjecture by Safari. A large number of directed width measures generalising tree width has been proposed in the literature. However, only very little was known about the relation between them, in particular about whether classes of digraphs of bounded width in one measure have bounded width in another. In this paper we establish an almost complete order among the most prominent width measures with respect to mutual boundedness.
Saeed Akhoondian Amiri, Lukasz Kaiser, Stephan Kreutzer, Roman Rabinovich 0001, Sebastian Siebertz
STACS3
2015 The Directed Grid Theorem
abstract
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.
Ken-ichi Kawarabayashi, Stephan Kreutzer
STOC2
2015 Colouring and Covering Nowhere Dense Graphs
Martin Grohe, Stephan Kreutzer, Roman Rabinovich 0001, Sebastian Siebertz, Konstantinos S. Stavropoulos
WG2
2014 An Excluded Grid Theorem for Digraphs with Forbidden Minors
abstract
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 [22] and later Johnson, Robertson, Seymour and Thomas [16] conjectured an analogous theorem for directed graphs, i.e. the existence of a function f : ℕ → ℕ 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 gave a proof of this conjecture for planar digraphs but no result beyond planar graphs is known to date. In this paper we prove the conjecture for the case of digraphs excluding a fixed undirected graph as a minor. For algorithmic applications our theorem is particularly interesting as it covers those classes of digraphs to which, on undirected graphs, theories based on the excluded grid theorem such as bidimensionality theory apply. We expect similar applications for directed graphs in particular to algorithmic versions of Erdős-Pósa type results and the directed disjoint paths problem.
Ken-ichi Kawarabayashi, Stephan Kreutzer
SODA2
2014 Deciding first-order properties of nowhere dense graphs
abstract
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.
Martin Grohe, Stephan Kreutzer, Sebastian Siebertz
STOC2
2014 An excluded half-integral grid theorem for digraphs and the directed disjoint paths problem
abstract
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.
Ken-ichi Kawarabayashi, Yusuke Kobayashi 0001, Stephan Kreutzer
STOC3
2013 Characterisations of Nowhere Dense Graphs (Invited Talk)
abstract
Nowhere dense classes of graphs were introduced by Nesetril and Ossona de Mendez as a model for "sparsity" in graphs. It turns out that nowhere dense classes of graphs can be characterised in many different ways and have been shown to be equivalent to other concepts studied in areas such as (finite) model theory. Therefore, the concept of nowhere density seems to capture a natural property of graph classes generalising for example classes of graphs which exclude a fixed minor, have bounded degree or bounded local tree-width. In this paper we give a self-contained introduction to the concept of nowhere dense classes of graphs focussing on the various ways in which they can be characterised. We also briefly sketch algorithmic applications these characterisations have found in the literature.
Martin Grohe, Stephan Kreutzer, Sebastian Siebertz
FSTTCS2
2013 Model Checking for Successor-Invariant First-Order Logic on Minor-Closed Graph Classes
abstract
Model checking problems for first- and monadic second-order logic on graphs have received considerable attention in the past, not the least due to their connections to problems in algorithmic graph structure theory. While the model checking problem for these logics on general graphs is computationally intractable, it becomes tractable on important classes of graphs such as those of bounded tree-width, planar graphs or more generally, classes of graphs excluding a fixed minor. It is well known that allowing an order relation or successor function can greatly increase the expressive power of the respective logics. This remains true even in cases where we require the formulas to be order- or successor-invariant, that is, while they can use an order relation, their truth in a given graph must not depend on the particular ordering or successor function chosen. Naturally, the question arises whether this increase in expressive power comes at a cost in terms of tractability on specific classes of graphs. In LICS 2012, Engelmann et al. studied this problem and showed that order-invariant monadic second-order logic (MSO) remains tractable on the same classes of graphs than MSO without an ordering. That is, adding order-invariance to MSO essentially comes at no extra cost in terms of model checking complexity. For successor-invariant first-order logic something similar should be true. However, they only managed to show that successor-invariant first-order logic is tractable on the class of planar graphs which is very far from the best tractability results currently known for first-order logic. In this paper we significantly improve the latter result and show that successor-invariant first-order logic is tractable on any class of graphs excluding a fixed minor. This is much closer to the best results known for FO without an ordering. The proof relies on the construction of k-walks in suitable supergraphs of the input graphs, i.e., walks which visit every vertex at least once and at most k times, for some k depending on the excluded minor H. The supergraphs may in general contain H minors, but they still exclude some possible larger minor H', so by results of Flum and Grohe [20] model checking on these graphs is still fixed-parameter tractable.
Kord Eickmeyer, Ken-ichi Kawarabayashi, Stephan Kreutzer
LICS3
2013 Quantitative Monadic Second-Order Logic
abstract
While monadic second-order logic is a prominent logic for specifying languages of finite words, it lacks the power to compute quantitative properties, e.g. to count. An automata model capable of computing such properties are weighted automata, but logics equivalent to these automata have only recently emerged. We propose a new framework for adding quantitative properties to logics specifying Boolean properties of words. We use this to define Quantitative Monadic Second-Order Logic (QMSO). In this way we obtain a simple logic which is equally expressive to weighted automata. We analyse its evaluation complexity, both data and combined complexity, and show completeness results for combined complexity. We further refine the analysis of this logic and obtain fragments that characterise exactly subclasses of weighted automata defined by the level of ambiguity allowed in the automata. In this way, we define a quantitative logic which has good decidability properties while being resonably expressive and enjoying a simple syntactical definition.
Stephan Kreutzer, Cristian Riveros
LICS1
2013 Packing directed cycles through a specified vertex set
abstract
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ős-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.
Ken-ichi Kawarabayashi, Daniel Král, Marek Krcál, Stephan Kreutzer
SODA4
2012 First-Order and Monadic Second-Order Model-Checking on Ordered Structures
abstract
Model-checking for first- and monadic second-order logic in the context of graphs has received considerable attention in the literature. It is well-known that the problem of verifying whether a formula of these logics is true in a graph is computationally intractable but it does become tractable on interesting classes of graphs such as classes of bounded tree-width. In this paper we continue this line of research but study model checking for first- and monadic second-order logic in the presence of an ordering on the input structure. We do so in two settings: the general ordered case, where the input structures are equipped with a fixed order or successor relation, and the order invariant case, where the formulas may resort to an ordering but their truth must be independent of the particular choice of order. In the first setting we show very strong intractability results for most interesting classes of graphs. In contrast, in order invariant case we obtain tractability results for order invariant monadic second-order logic on the same classes of graphs as in the unordered case. For first-order logic, we obtain tractability of successor-invariant FO on planar graphs.
Viktor Engelmann, Stephan Kreutzer, Sebastian Siebertz
LICS2
2012 Directed nowhere dense classes of graphs
abstract
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.
Stephan Kreutzer, Siamak Tazari
SODA1
2012 Linkless and Flat Embeddings in 3-Space
Ken-ichi Kawarabayashi, Stephan Kreutzer, Bojan Mohar
Discret. Comput. Geom.2
2012 Foreword: Special Issue on Theory and Applications of Graph Searching Problems
Fedor V. Fomin, Pierre Fraigniaud, Stephan Kreutzer, Dimitrios M. Thilikos
Theor. Comput. Sci.3
2011 Special Issue on "Theory and Applications of Graph Searching Problems"
Fedor V. Fomin, Pierre Fraigniaud, Stephan Kreutzer, Dimitrios M. Thilikos
Theor. Comput. Sci.3
2011 Digraph decompositions and monotonicity in digraph searching
Stephan Kreutzer, Sebastian Ordyniak
Theor. Comput. Sci.1
2010 Linkless and flat embeddings in 3-space and the unknot problem
abstract
We consider piecewise linear embeddings of graphs in 3-space ℜ3. Such an embbeding is linkless if every pair of disjoint cycles forms a trivial link (in the sense of knot theory). Robertson, Seymour and Thomas [47] showed that a graph has a linkless embedding in ℜ3 if, and only if, it does not contain as a minor any of seven graphs in Petersen's family (graphs obtained from K6 by a series of YΔ and ΔY operations). They also showed that a graph is linklessly embeddable in ℜ3 if, and only if, it admits a flat embedding into ℜ3, i.e. an embedding such that for every cycle C of G there exists a closed 2-disk D ⊆ ℜ3 with D ∩ G = ∂D = C. Clearly, every flat embeddings is linkless, but the converse is not true. We first consider the following algorithmic problem associated with embeddings in ℜ3:
Ken-ichi Kawarabayashi, Stephan Kreutzer, Bojan Mohar
SCG2
2010 Lower Bounds for the Complexity of Monadic Second-Order Logic
abstract
Courcelle's famous theorem from 1990 states that any property of graphs definable in monadic second-order logic (MSO2) can be decided in linear time on any class of graphs of bounded tree-width, or in other words, MSO2is fixed-parameter tractable in linear time on any such class of graphs. From a logical perspective, Courcelle's theorem establishes a sufficient condition, or an upper bound, for tractability of MSO2-model checking. Whereas such upper bounds on the complexity of logics have received significant attention in the literature, almost nothing is known about corresponding lower bounds. In this paper we establish a strong lower bound for the complexity of monadic second-order logic. In particular, we show that if C is any class of graphs which is closed under taking sub-graphs and whose tree-width is not bounded by a poly-logarithmic function (in fact, logcn for some small c suffices) then MSO2-model checking is intractable on C (under a suitable assumption from complexity theory).
Stephan Kreutzer, Siamak Tazari
LICS1
2010 On Brambles, Grid-Like Minors, and Parameterized Intractability of Monadic Second-Order Logic
abstract
Brambles were introduced as the dual notion to treewidth, one of the most central concepts of the graph minor theory of Robertson and Seymour. Recently, Grohe and Marx showed that there are graphs G, in which every bramble of order larger than the square root of the treewidth is of exponential size in |G|. On the positive side, they show the existence of polynomial-sized brambles of the order of the square root of the treewidth, up to log factors. We provide the first polynomial time algorithm to construct a bramble in general graphs and achieve this bound, up to log-factors. We use this algorithm to construct grid-like minors, a replacement structure for grid-minors recently introduced by Reed and Wood, in polynomial time. Using the gridlike minors, we introduce the notion of a perfect bramble and an algorithm to find one in polynomial time. Perfect brambles are brambles with a particularly simple structure and they also provide us with a subgraph that has bounded degree and still large treewidth; we use them to obtain a meta-theorem on deciding certain parameterized subgraph-closed problems on general graphs in time singly exponential in the parameter; the only other result with a similar flavor that is known to us is due to Demaine and Hajiaghayi and obtains a doubly-exponential bound on the parameter (albeit, for a more general class of parameterized problems). The second part of our work deals with providing a lower bound to Courcelle's famous theorem from almost two decades ago, stating that every graph property that can be expressed by a sentence in monadic second-order logic (MSO), can be decided by a linear time algorithm on classes of graphs of bounded treewidth. Whereas much work has been done on designing, improving, and applying algorithms on graphs of bounded treewidth, not much is known on the side of lower bounds: what bound on the treewidth of a class of graphs “forbids” polynomial-time parameterized algorithms to decide MSO-sentences? This question has only recently received attention with the first systematic study appearing in [Kreutzer 2009]. Using our results from the first part of our work we can improve on it significantly and establish a strong lower bound for Courcelle's theorem on classes of colored graphs.
Stephan Kreutzer, Siamak Tazari
SODA1
2009 Reachability in Succinct and Parametric One-Counter Automata
Christoph Haase, Stephan Kreutzer, Joël Ouaknine, James Worrell 0001
CONCUR2
2009 Domination Problems in Nowhere-Dense Classes
abstract
We investigate the parameterized complexity of generalisations and variations of the dominating set problem on classes of graphs that are nowhere dense. In particular, we show that the distance-$d$ dominating-set problem, also known as the $(k,d)$-centres problem, is fixed-parameter tractable on any class that is nowhere dense and closed under induced subgraphs. This generalises known results about the dominating set problem on $H$-minor free classes, classes with locally excluded minors and classes of graphs of bounded expansion. A key feature of our proof is that it is based simply on the fact that these graph classes are uniformly quasi-wide, and does not rely on a structural decomposition. Our result also establishes that the distance-$d$ dominating-set problem is FPT on classes of bounded expansion, answering a question of Ne{\v s}et{\v r}il and Ossona de Mendez.
Anuj Dawar, Stephan Kreutzer
FSTTCS2
2009 Distance d-Domination Games
Stephan Kreutzer, Sebastian Ordyniak
WG1
2008 On Datalog vs. LFP
Anuj Dawar, Stephan Kreutzer
ICALP (2)2
2008 Computing excluded minors
Isolde Adler, Martin Grohe, Stephan Kreutzer
SODA3
2008 Digraph Decompositions and Monotonicity in Digraph Searching
Stephan Kreutzer, Sebastian Ordyniak
WG1
2008 Digraph measures: Kelly decompositions, games, and orderings
Paul Hunter 0001, Stephan Kreutzer
Theor. Comput. Sci.2
2007 Model Theory Makes Formulas Large
Anuj Dawar, Martin Grohe, Stephan Kreutzer, Nicole Schweikardt
ICALP3
2007 Boundedness of Monadic FO over Acyclic Structures
Stephan Kreutzer, Martin Otto 0001, Nicole Schweikardt
ICALP1
2007 Locally Excluding a Minor
abstract
We introduce the concept of locally excluded minors. Graph classes locally excluding a minor are a common generalisation of the concept of excluded minor classes and of graph classes with bounded local tree-width. We show that first-order model-checking is fixed-parameter tractable on any class of graphs locally excluding a minor. This strictly generalises analogous results by Flum and Grohe on excluded minor classes and Frick and Grohe on classes with bounded local tree-width. As an important consequence of the proof we obtain fixed-parameter algorithms for problems such as dominating or independent set on graph classes excluding a minor, where now the parameter is the size of the dominating set and the excluded minor. We also study graph classes with excluded minors, where the minor may grow slowly with the size of the graphs and show that again, first-order model-checking is fixed-parameter tractable on any such class of graphs.
Anuj Dawar, Martin Grohe, Stephan Kreutzer
LICS3
2007 Digraph measures: Kelly decompositions, games, and orderings
Paul Hunter 0001, Stephan Kreutzer
SODA2
2007 Generalising automaticity to modal properties of finite structures
Anuj Dawar, Stephan Kreutzer
Theor. Comput. Sci.2
2006 Approximation Schemes for First-Order Definable Optimisation Problems
abstract
Let phi(X) be a first-order formula in the language of graphs that has a free set variable X, and assume that X only occurs positively in phi(X). Then a natural minimisation problem associated with phi(X) is to find, in a given graph G, a vertex set S of minimum size such that G satisfies phi(S). Similarly, if X only occurs negatively in phi(X), then phi(X) defines a maximisation problem. Many well-known optimisation problems are first-order definable in this sense, for example, minimum dominating set or maximum independent set. We prove that for each class Gscr of graphs with excluded minors, in particular for each class of planar graphs, the restriction of a first-order definable optimisation problem to the class Gscr has a polynomial time approximation scheme. A crucial building block of the proof of this approximability result is a version of Gaifman's locality theorem for formulas positive in a set variable. This result may be of independent interest
Anuj Dawar, Martin Grohe, Stephan Kreutzer, Nicole Schweikardt
LICS3
2006 DAG-Width and Parity Games
Dietmar Berwanger, Anuj Dawar, Paul Hunter 0001, Stephan Kreutzer
STACS4
2006 Backtracking games and inflationary fixed points
Anuj Dawar, Erich Grädel, Stephan Kreutzer
Theor. Comput. Sci.3
2005 The Expressive Power of Two-Variable Least Fixed-Point Logics
Martin Grohe, Stephan Kreutzer, Nicole Schweikardt
MFCS2
2005 An Extension of Muchnik's Theorem
abstract
One of the strongest decidability results in logic is the theorem of Muchnik which allows one to transfer the decidability of the monadic second-order theory of a structure to the decidability of the MSO-theory of its iteration, a tree built of disjoint copies of the original structure. We present a generalization of Muchnik's result to stronger logics, namely guarded second-order logic and its extensions by counting quantifiers. We also establish a strong equivalence result between monadic least fixed-point logic (M-LFP) and MSO on trees by showing that whenever M-LFP and MSO coincide on a structure they also coincide on its iteration.
Achim Blumensath, Stephan Kreutzer
J. Log. Comput.2
2004 Backtracking Games and Inflationary Fixed Points
Anuj Dawar, Erich Grädel, Stephan Kreutzer
ICALP3
2004 Expressive equivalence of least and inflationary fixed-point logic
Stephan Kreutzer
Ann. Pure Appl. Log.1
2004 Inflationary fixed points in modal logic
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.
Anuj Dawar, Erich Grädel, Stephan Kreutzer
ACM Trans. Comput. Log.3
2003 Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions
abstract
We survey logical formalisms based on inflationary and deflationary fixed points, and compare them to the (more familiar) logics based on least and greatest fixed points.
Erich Grädel, Stephan Kreutzer
LICS2
2003 Once upon a Time in a West - Determinacy, Definability, and Complexity of Path Games
Dietmar Berwanger, Erich Grädel, Stephan Kreutzer
LPAR3
2002 Generalising Automaticity to Modal Properties of Finite Structures
Anuj Dawar, Stephan Kreutzer
FSTTCS2
2002 Expressive Equivalence of Least and Inflationary Fixed-Point Logic
abstract
We study the relationship between least and inflationary fixed-point logic. By results of Gurevich and Shelah (1986), it has been known that on finite structures both logics have the same expressive power. On infinite structures however the question whether there is a formula in IFP not equivalent to any LFP-formula was still open. In this paper, we settle the question by showing that both logics are equally expressive on arbitrary structures. The proof will also establish the strictness of the nesting-depth hierarchy for IFP on some infinite structures. Finally, we show that the alternation hierarchy for IFP collapses to the first level on all structures, i.e. the complement of an inflationary fixed-point is an inflationary fixed-point itself.
Stephan Kreutzer
LICS1
2001 Query Languages for Constraint Databases: First-Order Logic, Fixed-Points, and Convex Hulls
Stephan Kreutzer
ICDT1
2001 Operational Semantics for Fixed-Point Logics on Constraint Databases
Stephan Kreutzer
LPAR1
2000 Fixed-Point Query Languages for Linear Constraint Databases
abstract
We introduce a family of query languages for linear constraint databases over the reals. The languages are defined over two-sorted structures, the first sort being the real numbers and the second sort consisting of a decomposition of the input relation into regions. The languages are defined as extensions of first-order logic by transitive closure or fixed-point operators, where the fixed-point operators are defined over the set of regions only. It is shown that the query languages capture precisely the queries definable in various standard complexity classes including PTIME.
Stephan Kreutzer
PODS1