相关论文: Fixed-parameter tractability, definability, and mo…

Fagin's seminal result characterizing $\mathsf{NP}$ in terms of existential second-order logic started the fruitful field of descriptive complexity theory. In recent years, there has been much interest in the investigation of quantitative…

Formal verification using the model checking paradigm has to deal with two aspects: The system models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of…

Over the past two decades the main focus of research into first-order (FO) model checking algorithms has been on sparse relational structures - culminating in the FPT algorithm by Grohe, Kreutzer and Siebertz for FO model checking of…

We investigate parameterizations of both database instances and queries that make query evaluation fixed-parameter tractable in combined complexity. We introduce a new Datalog fragment with stratified negation, intensional-clique-guarded…

In this paper we investigate to which extent a very simple and natural "reachability as deducibility" approach, originated in the research in formal methods in security, is applicable to the automated verification of large classes of…

We study a variant of Set Cover where each element of the universe has some demand that determines how many times the element needs to be covered. Moreover, we examine two generalizations of this problem when a set can be included multiple…

We investigate the isomorphism problem in the setting of definable sets (equivalent to sets with atoms): given two definable relational structures, are they related by a definable isomorphism? Under mild assumptions on the underlying…

We consider the problems of deciding whether an input graph can be modified by removing/adding at most k vertices/edges such that the result of the modification satisfies some property definable in first-order logic. We establish a number…

We study an extensive class of movement minimization problems which arise from many practical scenarios but so far have little theoretical study. In general, these problems involve planning the coordinated motion of a collection of agents…

We study probabilistic complexity classes and questions of derandomisation from a logical point of view. For each logic L we introduce a new logic BPL, bounded error probabilistic L, which is defined from L in a similar way as the…

This paper studies the problem of model-checking of probabilistic automaton and probabilistic one-counter automata against probabilistic branching-time temporal logics (PCTL and PCTL$^*$). We show that it is undecidable for these problems.…

We classify the complexity of the LTL satisfiability and model checking problems for several standard parameterisations. The investigated parameters are temporal depth, number of propositional variables and formula treewidth, resp.,…

The elimination distance to some target graph property P is a general graph modification parameter introduced by Bulian and Dawar. We initiate the study of elimination distances to graph properties expressible in first-order logic. We…

The embedding problem is to decide, given an ordered pair of structures, whether or not there is an injective homomorphism from the first structure to the second. We study this problem using an established perspective in parameterized…

Over the past two decades several fragments of first-order logic have been identified and shown to have good computational and algorithmic properties, to a great extent as a result of appropriately describing the image of the standard…

We carry out a systematic study of a natural covering problem, used for identification across several areas, in the realm of parameterized complexity. In the {\sc Test Cover} problem we are given a set $[n]=\{1,...,n\}$ of items together…

The NP-complete Permutation Pattern Matching problem asks whether a permutation P (the pattern) can be matched into a permutation T (the text). A matching is an order-preserving embedding of P into T. In the Generalized Permutation Pattern…

For a first-order theory $T$, the Constraint Satisfaction Problem of $T$ is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of $T$. In this article we develop sufficient…

In this note, we provide complexity characterizations of model checking multi-pushdown systems. Multi-pushdown systems model recursive concurrent programs in which any sequential process has a finite control. We consider three standard…

We introduce an extension of decision problems called resiliency problems. In resiliency problems, the goal is to decide whether an instance remains positive after any (appropriately defined) perturbation has been applied to it. To tackle…