BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Stephan Kreutzer

Stephan Kreutzer appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Discrete Mathematicsmath.COLogic in Computer ScienceData Structures and AlgorithmsComputational ComplexityComputer Science and Game Theorymath.LO

Catalog footprint

What is connected

18works
7topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

18 published item(s)

preprint2022arXiv

Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

We present a fixed-parameter tractable algorithm for first-order model checking on interpretations of graph classes with bounded local cliquewidth. Notably, this includes interpretations of planar graphs, and more generally, of classes of bounded genus. To obtain this result we develop a new tool which works in a very general setting of dependent classes and which we believe can be an important ingredient in achieving similar results in the future.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

The Directed Grid Theorem

The grid theorem, originally proved by Robertson and Seymour in Graph Minors V in 1986, 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 (see [Reed 97, Johnson, Robertson, Seymour, Thomas 01]), 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 Reed, Johnson, Robertson, Seymour and Thomas conjecture. Only very recently, this result has been extended to all classes of digraphs excluding a fixed undirected graph as a minor (see [Kawarabayashi, Kreutzer 14]). 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 and to prove the directed grid theorem. As consequence of our results we are able to improve results in Reed et al. in 1996 [Reed, Robertson, Seymour, Thomas 96] (see also [Open Problem Garden]) on disjoint cycles of length at least l and in [Kawarabayashi, Kobayashi, Kreutzer 14] on quarter-integral disjoint paths. We expect many more algorithmic results to follow from the grid theorem.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

DAG-width is PSPACE-complete

Berwanger et al. show 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)}$. This gives a polynomial time algorithm for determining the DAG-width of a graph for any fixed $k$. However, if the DAG-width of the graphs from a class 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 all generalisations of tree width similar to DAG-width. 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 which would approximate an optimal decomposition up to an additive constant. 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 constant is PSPACE-complete.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Differential games, locality and model checking for FO logic of graphs

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 restricted. We prove that, in a certain sense, 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 on interpretations of nowhere dense graph classes.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Neighborhood complexity and kernelization for nowhere dense classes of graphs

We prove that whenever $G$ is a graph from a nowhere dense graph class $\mathcal{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,ε)\cdot |A|^{1+ε}$, where $r$ is any positive integer, $ε$ is any positive real, and $f$ is a function that depends only on the class $\mathcal{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. As an algorithmic application of the above result, we show that for every fixed $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., 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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Routing with Congestion in Acyclic Digraphs

We study the version of the $k$-disjoint paths problem where $k$ demand pairs $(s_1,t_1)$, $\dots$, $(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$.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

The Erdos-Posa Property for Directed Graphs

A classical result by Erdos and Posa states that there is a function $f: {\mathbb N} \rightarrow {\mathbb N}$ such that for every $k$, every graph $G$ contains $k$ pairwise vertex disjoint cycles or a set $T$ of at most $f(k)$ vertices such that $G-T$ is acyclic. The generalisation of this result to directed graphs is known as Younger's conjecture and was proved by Reed, Robertson, Seymour and Thomas in 1996. This so-called Erdos-Posa-property can naturally be generalised to arbitrary graphs and digraphs. Robertson and Seymour proved that a graph $H$ has the Erdos-Posa-property if, and only if, $H$ is planar. In this paper we study the corresponding problem for digraphs. We obtain a complete characterisation of the class of strongly connected digraphs which have the Erdos-Posa-property (both for topological and butterfly minors). We also generalise this result to classes of digraphs which are not strongly connected. In particular, we study the class of vertex-cyclic digraphs (digraphs without trivial strong components). For this natural class of digraphs we obtain a nearly complete characterisation of the digraphs within this class with the Erdos-Posa-property. In particular we give positive and algorithmic examples of digraphs with the Erdos-Posa-property by using directed tree decompositions in a novel way.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

The Generalised Colouring Numbers on Classes of Bounded Expansion

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Kernelization and Sparseness: the case of Dominating Set

We prove that for every positive integer $r$ and for every graph class $\mathcal G$ of bounded expansion, the $r$-Dominating Set problem admits a linear kernel on graphs from $\mathcal G$. Moreover, when $\mathcal G$ is only assumed to be nowhere dense, then we give an almost linear kernel on $\mathcal G$ for the classic Dominating Set problem, i.e., for the case $r=1$. These results generalize a line of previous research on finding linear kernels for Dominating Set and $r$-Dominating Set. However, the approach taken in this work, which is based on the theory of sparse graphs, is radically different and conceptually much simpler than the previous approaches. We complement our findings by showing that for the closely related Connected Dominating Set problem, the existence of such kernelization algorithms is unlikely, even though the problem is known to admit a linear kernel on $H$-topological-minor-free graphs. Also, we prove that for any somewhere dense class $\mathcal G$, there is some $r$ for which $r$-Dominating Set is W[$2$]-hard on $\mathcal G$. Thus, our results fall short of proving a sharp dichotomy for the parameterized complexity of $r$-Dominating Set on subgraph-monotone graph classes: we conjecture that the border of tractability lies exactly between nowhere dense and somewhere dense graph classes.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Deciding first-order properties of nowhere dense graphs

Nowhere dense graph classes, introduced by Nesetril and Ossona de Mendez, 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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Decomposition Theorems and Model-Checking for the Modal $μ$-Calculus

We prove a general decomposition theorem for the modal $μ$-calculus $L_μ$ in the spirit of Feferman and Vaught's theorem for disjoint unions. In particular, we show that if a structure (i.e., transition system) is composed of two substructures $M_1$ and $M_2$ plus edges from $M_1$ to $M_2$, then the formulas true at a node in $M$ only depend on the formulas true in the respective substructures in a sense made precise below. As a consequence we show that the model-checking problem for $L_μ$ is fixed-parameter tractable (fpt) on classes of structures of bounded Kelly-width or bounded DAG-width. As far as we are aware, these are the first fpt results for $L_μ$ which do not follow from embedding into monadic second-order logic.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Directed Width Measures and Monotonicity of Directed Graph Searching

We consider generalisations of tree width to directed graphs, that attracted much attention in the last fifteen years. About their relative strength with respect to "bounded width in one measure implies bounded width in the other" many problems remain unsolved. Only some results separating directed width measures are known. We give an almost complete picture of this relation. For this, we consider the cops and robber games characterising DAG-width and directed tree width (up to a constant factor). For DAG-width games, it is an open question whether the robber-monotonicity cost (the difference between the minimal numbers of cops capturing the robber in the general and in the monotone case) can be bounded by any function. Examples show that this function (if it exists) is at least $f(k) > 4k/3$ (Kreutzer, Ordyniak 2008). We approach a solution by defining weak monotonicity and showing that if $k$ cops win weakly monotonically, then $O(k^2)$ cops win monotonically. It follows that bounded Kelly-width implies bounded DAG-width, which has been open since the definition of Kelly-width by Hunter and Kreutzer in 2008. For directed tree width games we show that, unexpectedly, the cop-monotonicity cost (no cop revisits any vertex) is not bounded by any function. This separates directed tree width from D-width defined by Safari in 2005, refuting his conjecture.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Vertex Disjoint Path in Upward Planar Graphs

The $k$-vertex disjoint paths problem is one of the most studied problems in algorithmic graph theory. In 1994, Schrijver proved that the problem can be solved in polynomial time for every fixed $k$ when restricted to the class of planar digraphs and it was a long standing open question whether it is fixed-parameter tractable (with respect to parameter $k$) on this restricted class. Only recently, \cite{CMPP}.\ achieved a major breakthrough and answered the question positively. Despite the importance of this result (and the brilliance of their proof), it is of rather theoretical importance. Their proof technique is both technically extremely involved and also has at least double exponential parameter dependence. Thus, it seems unrealistic that the algorithm could actually be implemented. In this paper, therefore, we study a smaller class of planar digraphs, the class of upward planar digraphs, a well studied class of planar graphs which can be drawn in a plane such that all edges are drawn upwards. We show that on the class of upward planar digraphs the problem (i) remains NP-complete and (ii) the problem is fixed-parameter tractable. While membership in FPT follows immediately from \cite{CMPP}'s general result, our algorithm has only single exponential parameter dependency compared to the double exponential parameter dependence for general planar digraphs. Furthermore, our algorithm can easily be implemented, in contrast to the algorithm in \cite{CMPP}.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Graph Operations on Parity Games and Polynomial-Time Algorithms

Parity games are games that are played on directed graphs whose vertices are labeled by natural numbers, called priorities. The players push a token along the edges of the digraph. The winner is determined by the parity of the greatest priority occurring infinitely often in this infinite play. A motivation for studying parity games comes from the area of formal verification of systems by model checking. Deciding the winner in a parity game is polynomial time equivalent to the model checking problem of the modal mu-calculus. Another strong motivation lies in the fact that the exact complexity of solving parity games is a long-standing open problem, the currently best known algorithm being subexponential. It is known that the problem is in the complexity classes UP and coUP. In this paper we identify restricted classes of digraphs where the problem is solvable in polynomial time, following an approach from structural graph theory. We consider three standard graph operations: the join of two graphs, repeated pasting along vertices, and the addition of a vertex. Given a class C of digraphs on which we can solve parity games in polynomial time, we show that the same holds for the class obtained from C by applying once any of these three operations to its elements. These results provide, in particular, polynomial time algorithms for parity games whose underlying graph is an orientation of a complete graph, 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. Previous results concerning restricted classes of parity games which are solvable in polynomial time include classes of bounded tree-width, bounded DAG-width, and bounded clique-width. We also prove that recognising the winning regions of a parity game is not easier than computing them from scratch.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

On the Parameterized Intractability of Monadic Second-Order Logic

One of Courcelle's celebrated results states that if 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 C by linear time parameterized algorithms, where the parameter is the tree-width plus the size of the formula. 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 cannot be extended much further. More specifically, we show that if C is a class of graphs which is closed under colourings and satisfies certain constructibility conditions and is such that the tree-width of C is not bounded by \log^{84} n then MSO_2-model checking is not fpt unless SAT can be solved in sub-exponential time. If the tree-width of C is not poly-logarithmically bounded, then MSO_2-model checking is not fpt unless all problems in the polynomial-time hierarchy can be solved in sub-exponential time.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Directed Nowhere Dense Classes of Graphs

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 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 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. This rather surprising result is inspired by Nesetril and Ossana de Mendez (2008) and yet a different and more delicate proof is needed, which is a significant part of our contribution.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Lower Bounds for the Complexity of Monadic Second-Order Logic

Courcelle's famous theorem from 1990 states that any property of graphs definable in monadic second-order logic (MSO) can be decided in linear time on any class of graphs of bounded treewidth, or in other words, MSO is 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 MSO-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 subgraphs and whose treewidth is not bounded by a polylogarithmic function (in fact, $\log^c n$ for some small c suffices) then MSO-model checking is intractable on C (under a suitable assumption from complexity theory).

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Extended Computation Tree Logic

We introduce a generic extension of the popular branching-time logic CTL which refines the temporal until and release operators with formal languages. For instance, a language may determine the moments along a path that an until property may be fulfilled. We consider several classes of languages leading to logics with different expressive power and complexity, whose importance is motivated by their use in model checking, synthesis, abstract interpretation, etc. We show that even with context-free languages on the until operator the logic still allows for polynomial time model-checking despite the significant increase in expressive power. This makes the logic a promising candidate for applications in verification. In addition, we analyse the complexity of satisfiability and compare the expressive power of these logics to CTL* and extensions of PDL.

0 citations0 reviewsNo code linkedOpen access