37 citations · 102 across the 14 of their papers we have counts for
15 papers
A New Perspective on FO Model Checking of Dense Graph Classes
Jakub Gajarský, Petr Hliněný, Daniel Lokshtanov +2
We study the first-order (FO) model checking problem of dense graphs, namely those which have FO interpretations in (or are FO transductions of) some sparse graph classes. We give…
Shrub-depth: Capturing Height of Dense Graphs
Robert Ganian, Petr Hliněný, Jaroslav Nešetřil +2
The recent increase of interest in the graph invariant called tree-depth and in its applications in algorithms and logic on graphs led to a natural question: is there an analogousl…
FO Model Checking on Posets of Bounded Width
Jakub Gajarský, Petr Hliněný, Daniel Lokshtanov +4
Over the past two decades the main focus of research into first-order (FO) model checking algorithms have been sparse relational structures-culminating in the FPT-algorithm by Groh…
First order limits of sparse graphs: Plane trees and path-width
Jakub Gajarsky, Petr Hlineny, Tomas Kaiser +5
Nesetril and Ossona de Mendez introduced the notion of first order convergence as an attempt to unify the notions of convergence for sparse and dense graphs. It is known that there…
Faster Existential FO Model Checking on Posets
Jakub Gajarský, Petr Hliněný, Jan Obdržálek +1
We prove that the model checking problem for the existential fragment of first-order (FO) logic on partially ordered sets is fixed-parameter tractable (FPT) with respect to the for…
Tree-depth and Vertex-minors
Petr Hliněný, O-joung Kwon, Jan Obdržálek +1
In a recent paper, Kwon and Oum claim that every graph of bounded rank-width is a pivot-minor of a graph of bounded tree-width (while the converse has been known true already befor…
Expanding the expressive power of Monadic Second-Order logic on restricted graph classes
Robert Ganian, Jan Obdržálek
We combine integer linear programming and recent advances in Monadic Second-Order model checking to obtain two new algorithmic meta-theorems for graphs of bounded vertex-cover. The…
Kernelization Using Structural Parameters on Sparse Graph Classes
Jakub Gajarský, Petr Hliněný, Jan Obdržálek +5
Meta-theorems for polynomial (linear) kernels have been the subject of intensive research in parameterized complexity. Heretofore, meta-theorems for linear kernels exist on graphs…
FO Model Checking of Interval Graphs
Robert Ganian, Petr Hlineny, Daniel Kral +3
We study the computational complexity of the FO model checking problem on interval graphs, i.e., intersection graphs of intervals on the real line. The main positive result is that…
STANSE: Bug-finding Framework for C Programs
Jan Obdržálek, Jiří Slabý, Marek Trtík
STANSE is a free (available under the GPLv2 license) modular framework for finding bugs in C programs using static analysis. Its two main design goals are 1) ability to process lar…
Lower Bounds on the Complexity of MSO1 Model-Checking
Robert Ganian, Petr Hliněný, Alexander Langer +3
One of the most important algorithmic meta-theorems is a famous result by Courcelle, which states that any graph problem definable in monadic second-order logic with edge-set quant…
Efficient Loop Navigation for Symbolic Execution
Jan Obdrzalek, Marek Trtik
Symbolic execution is a successful and very popular technique used in software verification and testing. A key limitation of symbolic execution is in dealing with code containing l…
Better algorithms for satisfiability problems for formulas of bounded rank-width
Robert Ganian, Petr Hliněný, Jan Obdržálek
We provide a parameterized polynomial algorithm for the propositional model counting problem #SAT, the runtime of which is single-exponential in the rank-width of a formula. Previo…
Are there any good digraph width measures?
Robert Ganian, Petr Hliněný, Joachim Kneis +4
Several different measures for digraph width have appeared in the last few years. However, none of them shares all the "nice" properties of treewidth: First, being \emph{algorithmi…
Qualitative Reachability in Stochastic BPA Games
Tomáš Brázdil, Václav Brožek, Antonín Kučera +1
We consider a class of infinite-state stochastic games generated by stateless pushdown automata (or, equivalently, 1-exit recursive state machines), where the winning objective is…